I've never been very interested in rules based on the assumption of uniqueness, but the topic came out a few days ago in a conversation with Robert and it reminded me of an older conversation with Red Ed about UR1.1.
[2020/02/20: Added for clarity]:
1) The following discussion is not about rule UR1 but about UR1.1 (also named AR1 in Hodoku).
2) The following discussion is not about UR1.1 being true or not when one makes the assumption of uniqueness. It is about whether it can be proven without that assumption (or some other assumption yet to be explicited).
[2020/02/20: Added for clarity] As most discussions in any forum, this quickly spreads to unrelated topics. So, I'll keep this introductory post updated for the reader who wants a quick summary. At the end, I'll add relevant objections to my point of view and my answers.
UR1.1, definition
The UR1.1 rule I'll discuss is: if the following pattern of four cells spanning two rows, two columns and two blocks appears in a grid, then the value of the fourth cell is 3.
- Code: Select all
1 2
2 13
[2020/02/20: Added for clarity] The standard definition of rule UR1.1 has an additional condition: the 4 UR cells must be "unclued". But I'll show later in this post that this condition is logically irrelevant.
[2020/02/20: Added for clarity] For contrast, the UR1 rule always supposes the assumption of uniqueness and it relies on the following pattern, where there's no need to make any assumption about "unclued" cells:
- Code: Select all
12 12
12 123
RedEd's formulation of UR1.1 and his proof
see http://forum.enjoysudoku.com/post63659.html#p63659
[2020/02/20: Added for clarity] RedEd puts the usual additional conditions on the rule: none of the 4 cells may have any givens. He then claims to have a proof independent on the assumption of uniqueness
Red Ed wrote:Definition: an a/b/b/a pattern in a solution grid is anything isomorphic to that shown below:
- Code: Select all
. . . | .
a . . | b
b . . | a
---------+---
. . . | .
Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.
Theorem: if a puzzle-in-progress (that does not necessarily have a unique solution) has pencilmarks as shown below on four unclued cells then the bottom right value resolves to '3':
- Code: Select all
. . . | .
1 . . | 2
2 . . | 13
---------+---
. . . | .
Proof: suppose to the contrary the bottom right value resolves to '1'. Then (vacuously) the solution grid contains the 1/2/2/1 pattern on four unclued cells, C. So, by the Fact above, C=2/1/1/2 is also a solution. But wait! - the pencilmarks do not allow that other solution - contradiction.
My old answer to RedEd's proof
If you continue reading the above-mentioned thread, you'll see that I found the proof very smart, but I had two objections:
denis_berthier wrote:Using a kind of reasoning similar to RedEd's, let me show that any puzzle that can be solved with UR1.1 can be solved without it.
Suppose there is a puzzle P that can be solved thanks to the application of UR1.1 but that couldn't without it. Define P' as P plus one of the 3 entries in the UR1.1 pattern [supposing UR1.1 was used once; add similar entries if UR1.1 was used several times]. Then, by the very definition of P, P' can't be solved. As the entry added to P was proven from the axioms of P, it can't have introduced a contradiction in P'; nor can it have introduced a non-uniqueness problem. We thus get a contradiction.
Notice that this doesn't mean UR1.1 would be useless: it may still lead to simpler solutions.
[2020/02/20 added for keeping this post up-to-date]: there's indeed a stronger result, with almost the same proof: any elimination that can be made with UR1.1 can be made in FOL without it
denis_berthier wrote: RedEd's "basic fact"RedEd wrote:Fact: if a solution grid (not necessarily unique) contains an a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.
on which his whole proof rests, becomes obviously false if we accept only constructive solutions: how could r1c1 = 2 be constructively proved from the axioms of Sudoku and the entries when r1c1 = 1 has already been constructively proved at the time the UR1.1 pattern is detected? (or, to put it differently, how could two contradictory values be constructively proved if the puzzle is consistent?)
Conclusion: RedEd's proof has an implicit assumption: we must accept any kind of solution, including non constructive ones, e.g. those obtained by recursive backtracking with guessing.
Those objections remain valid. But I think I can now have simpler and stronger arguments. (I may have already written this or part of this somewhere, but I'm not sure.)
Some basic reminders of First Order Logic (FOL) and their consequences
Theorem 1: Let S be a theory in FOL (e.g. the theory consisting of the 4 basic Sudoku axioms plus the givens of a puzzle P). Let T be a theorem of S, i.e. any formula that can be deduced from the axioms of T according to the principles of FOL (e.g. the assertion of a candidate as a value for some cell: rc=n). Then any formula F derivable from S+T is derivable from S.
The proof is obvious: take any proof of F using T and replace any mention of T in it by the proof of T in S. This gives a proof of F that doesn't explicitly use T.
Corollary (formal version): any candidate asserted at any step of a resolution of a puzzle (based on the principles of FOL) can be used in further steps exactly as if it was a given.
Corollary (intuitive version 1): FOL cannot make any difference between a given and a value derived from the givens.
Corollary (intuitive version 2): any tentative rule trying to make any difference between a given and a value derived from the givens is extra-logical.
[2020/02/20: Added for clarity]
1) the assumption of uniqueness IS the typical example of something extra-logical
2) using a predicate "unclued" or "not-a-given" or anything similar is the mark of some extra-logical input
Consequence for RedEd's proof
Due to the presence of the word "unclued" in it, the "fact" on which RedEd's proof relies is meaningless in FOL. As a result, the apparent paradox in RedEd's theorem and the theorem itself merely vanish into nothingness.
As a second result, any tentative formulation of an UR1.1 rule can only be what I first stated, without any mention of unclued cells.
[2020/02/20: Added for clarity] As a third result, if rule UR1.1 was somehow valid, it could only be because of some dependence on the assumption of uniqueness (or on some other extra-logical assumption).
Validity of the tentative UR1.1 rule?
The tentative UR1.1 rule under consideration here is as I stated it at the start: if the following pattern of four cells spanning two rows, two columns and two blocks:
- Code: Select all
1 2
2 13
appears in a grid, then the value of the fourth cell is 3.
I can't see any logical reason why, if the first three cells are given, the fourth couldn't be 1.
This is not a proof that the rule is not valid, but I'm almost sure anyone can find a counter-example, e.g. a puzzle with the following template of givens:
- Code: Select all
1 2
2 1
[2020/02/20: Added for keeping this post up-to-date] If you scroll downwards in this page, you'll see I have finally found (quite easily) a single-solution puzzle with such a pattern:
- Code: Select all
12345678.
4......1.
5.9......
2176.4..5
3...1....
6..5231..
7.1..28..
8......2.
9.......3
[2020/02/24: Added for keeping this post up-to-date]
After some tweaking, I also found a puzzle directly contradicting the UR 1.1 rule as I stated it (scroll downwards):
- Code: Select all
12345678.
4......1.
5.9......
2.76.4..5
3...1....
69.5231..
7.1..28..
8......2.
9.......3
The content of cells r1r4 x c1c2 is:
- Code: Select all
1 2
2 18
UR1.1 would assign the value 8 to r4c2. But the unique solution has value 1 for that cell.
Final question
Is there any example of a real puzzle where a pure logic resolution leads to a situation with the
- Code: Select all
1 2
2 13
pattern, where none of the four cells were given?
If not, all the discussions of UR1.1 were pointless.
[2020/02/20: Added for keeping this post up-to-date] Leren has found 5 single-solution puzzles in Hodoku with such a pattern. Scroll downwards in this page. I've then tried to generate more using Sudoku Explainer and it's quite easy.
[2020/02/20: Added for keeping this post up-to-date] At this point, all the single-solution puzzles satisfying the conditions of the above "final question" have the 3 in their unique solution. After trying with Sudoku Explainer, it seems very difficult to build one where the 3 is not in the solution. Conversely, it is very easy to build multi-solution puzzles where the 1, the 2 and the 3 in the last cell are in different solutions. This corroborates the above proof that UR1.1, if somehow valid, must depend on the assumption of uniqueness.
[2020/02/20: added for completeness]Main objections to my point of view: forthcoming