Mauriès Robert wrote:a subject that does not deserve so much

As long as we are concerned with Sudoku, I agree. UR1.1 is of zero use. Nobody has been able to provide an example in case of non-uniqueness.

But you have seen that the discussion was also about some general ways of reasoning and approaching Sudoku solving.

First Order Logic (FOL) clearly implies one cannot make a difference between a given and a value deduced from the givens, in terms of the further inferences they allow. Contrary to eleven's unfounded but repeated claims, this has absolutely nothing to do with my model of resolution.

On the other hand, there is RedEd's very smart proof. As a mathematician, I find this type of reasoning highly "perverse". It is obviously non-constructive, as I objected long ago, but on this point (and only on this point) I accept the counter-objection that this is only a restriction from my constructive approach (though I can easily code this type on rule in SudoRules).

But what's discussed here is, considering the logical background recalled in my first post, what's the (other) extra-logical assumption in RedEd's proof? My two cents is uniqueness, because in case of non-uniqueness, it seems that the a/b/b/ac pattern cannot be found in any resolution path if there is no given in the a/b/c part. All the examples examined until now support this conclusion.