The New Sudoku Players' Forum

[denis_berthier]

.
I made a stupid error in a Boolean manipulation in a previous post. My apologies to all for not finding it earlier and causing lots of useless debates.
Finding such a stupid error is never good for the ego, but I console myself by thinking that:
- only those who do nothing never make any error (except precisely doing nothing);
- I'm the one who found it;
- I got the new Dune DVD to watch.

Here is the correct version of the full post (changes appear only in part 4).



Let me propose a different proof of François's proposition that a track based on a subset E of an entity does not necessarily contain some candidate from this set.

It will not suppose the existence of several solutions.
It will require only trivial boolean logic.


1) I shall prove something much stronger:
Theorem: a track based on an arbitrary set E of candidates contains a candidate A0 iff for each candidate Ak≠A0 in E, A0 is a consequence of Ak in TR (TB).
(Note that:
- E doesn't have to be a subset of any entity;
- A0 doesn't have to be in E;
- the result is true even in the trivial cases where E contains only 1 or 2 elements
- no hypothesis is made on the number of solutions of the puzzle.)

If you think of it in pure logic terms, cleaned of all the useless definitions, you will realise that it is totally obvious.


"iff" means "if and only if".
Let A, B, C, D... be any candidates.
I'll write "A=>B" to mean that B can be derived from A within TR (i.e. within TB, in the only interpretation of TR that makes sense).
By the definition of a track P(A), B ∊ P(A) merely means A=>B.

Proof of the theorem:
By definition, P(A B C...) = P(A) ∩ P(B) ∩ P(C)...,
i.e. A0 ∊ P(A B C...) iff A0 ∊ P(A) and A0 ∊ P(B) and A0 ∊ P(C)...
i.e. A0 ∊ P(A B C...) iff A=>A0 and B=>A0 and C=>A0...
qed


2) In particular:
A ∊ P(A B C...) iff A=>A and B=>A and C=>A iff B=>A and C=>A ...
B ∊ P(A B C...) iff A=>B and B=>B and C=>B iff A=>B and C=>B ...
C ∊ P(A B C...) iff A=>C and B=>C and C=>C iff A=>C and B=>C ...
...
Therefore, one of the candidates A, B, C... is in P(A B C...) iff this candidate is a consequence in TR (TB) of each of the other ones separately.

This is obviously impossible (unless the puzzle is contradictory) when E is a subset of an undecided 2D-cell ("entity" in Robert's vocabulary).


3) Corollary: whether Robert's theorem 2.1 is true or not, its proof is false.
This doesn't say anything about theorem 2.1 being true or false.


4) But we can go further if we take TR = FOL (Thanks Defise for noticing this restriction):
Theorem 2.1: Let TR=FOL (not a resolution theory) and let E1, E2 form a partition of a 2D-cell ("entity"), with E1 and E2 non-empty. Then P'(E2) = P(E1)

Proof. Let E1 = A, B, C, ... and let E2 be its complement in some 2D-cell ("entity"), where none of E1 or E2 is empty.
By definition, P'(E2) is defined by X ∊ P'(E2) iff eliminating all the elements of E2 allows to prove X in TR (TB)
i.e. X ∊ P'(E2) iff the disjunction of all the elements in E1 implies X in TR (TB)
i.e. X ∊ P'(E2) iff (A or B or C...) => X
i.e. X ∊ P'(E2) iff A=>X and B=>X and C=>X... (The equivalence with the previous expression is valid only in FOL)
i.e. X ∊ P'(E2) iff X ∊ P(A) and X ∊ P(B) and X ∊ P(C) ...
i.e. X ∊ P'(E2) iff X ∊ P(E1)
qed

Remark:
Some may be surprised by this statement after my (erroneous) proof that it was false. But logic is logic.
I was the one who challenged the theorem. I'm the one who finally proves it in the context of FOL (totally useless for the "theory" of tracks).
.

[DEFISE]

Hi Denis,
What is certain is that it does not work with the only TB:

Puzzle 496 of assistant-sudoku :
9..54.6.....2...7..6...3..5.1.......4.8.7.1.9.9.....5.6..4...9..7...2.....1.89..3
We place 2 singles: 9r8c3, 4r9c2

P(7r6c7) = {7r6c7,7r9c4, 7r7c9, 6r9c8, 7r1c6}
P(8r6c7) = {8r6c7,7r9c4, 6r9c8, 7r1c6}
E1 = 234r6c7 E2 = 78r6c7
P ’(E1) is empty. (removing 234r6c7 allows no TB)
P(E2) = P(7r6c7) ∩ P(8r6c7) = {7r9c4, 6r9c8, 7r1c6}

[denis_berthier]

Hi Denis,
What is certain is that it does not work with the only TB:

Hi François,
Right, I was thinking in terms of FOL applied to Sudoku, but in a restricted resolution theory, we don't necessarily have (A or B or C...) => X equivalent to A=>X and B=>X and C=>X... (as I use it in section 4).

[DEFISE]

On the other hand, I think it’s difficult to prove a lot of things in TDP, since we do not know what P(A) is exactly when
“assume A true => contradiction”.
Indeed there is not only one way to reach a contradiction.

[denis_berthier]

On the other hand, I think it’s difficult to demonstrate a lot of things in TDP, since we do not know what P(A) is exactly when
“assume A true => contradiction”.
Indeed there is not only one way to reach a contradiction.

I'm not sure what you're talking about.
If A is a candidate, P(A) the set of all the values that can be asserted by TB.
If we apply the full power of FOL (as is necessary in section 4 of my preceding post) or if TB has the confluence property (a condition Robert never mentions), this is precisely defined.
I don't know what “assume A true => contradiction” means. In what context does this appear?

[Mauriès Robert]

.
I made a stupid error in a Boolean manipulation in a previous post. My apologies to all for not finding it earlier and causing lots of useless debates.
Finding such a stupid error is never good for the ego, but I console myself by thinking that:
- only those who do nothing never make any error (except precisely doing nothing);
- I'm the one who found it;
- I got the new Dune DVD to watch.

Hi Denis,
It is good to have recognised an error in your demonstration invalidating Theorem 2-1, but it is even better to recognise that without my instance of saying that there was an anomaly you would not have noticed and would have persisted in invalidating this theorem.
That said, while I am satisfied that you conclude that Theorem 2-1 is valid, I have difficulty understanding your demonstration. We can talk about it if you wish.
Robert

[DEFISE]

I don't know what “assume A true => contradiction” means. In what context does this appear?

You have proved the confluence property in the case where we start from a valid RS and apply the BT (singles, box/line, subsets).
(i.e. final RS is independent of the order in which the BT are applied.)

But I don't think confluence property is true when you start from an invalid RS, for example when we assume a false candidate to be true and then we apply the BT and later you obtain a contradiction.
To check…

[denis_berthier]

Hi Denis,
It is good to have recognised an error in your demonstration invalidating Theorem 2-1,

You mean recognised it as soon as I found it, contrary to you, who waited 2 or 3 years before admitting an error in yours?
And you still have to admit that your proof of theorem 2.1 is false.

but it is even better to recognise that without my instance of saying that there was an anomaly you would not have noticed and would have persisted in invalidating this theorem.

After seeing you cheating with the "iff" or claiming you don't know what 2D-cells (what you have re-baptised "entities") are, I stopped reading your stuff.

I am satisfied that you conclude that Theorem 2-1 is valid,

Let it be clear: the theorem is valid for the full power of FOL (my first interpretation of your TR), but not for any TB, as you must have noticed from the previous posts. This makes it true for FOL but totally useless for your "theory".

I'm not interested in wasting more time with tracks.

[denis_berthier]

I don't know what “assume A true => contradiction” means. In what context does this appear?

You have proved the confluence property in the case where we start from a valid RS and apply the BT (singles, box/line, subsets).
(i.e. final RS is independent of the order in which the BT are applied.)
But I don't think confluence property is true when you start from an invalid RS, for example when we assume a false candidate to be true and then we apply the BT and later you obtain a contradiction.

The confluence property applies to a set of resolution rules. There's no starting from this or that.
Adding a candidate (true or false) merely amounts to starting from a different puzzle.