The New Sudoku Players' Forum

[Ajò Dimonios]

Hi Mith

Mith wrote:
P = (16)r4c56 = (1r4c56 AND 6r4c56)
¬P = NOT((16)r4c56) = NOT(1r4c56 AND 6r4c56) = (-1r4c56 OR -6r4c56) = (1r4c56 AND -6r4c56) OR (-1r4c56 AND 6r4c56) OR (-1r4c56 AND -6r4c56)

Q = (16)r4c789 = (1r4c789 AND 6r4c789)
¬Q = NOT((16)r4c789) = NOT(1r4c789 AND 6r4c789) = (-1r4c789 OR -6r4c789) = (1r4c789 AND -6r4c789) OR (-1r4c789 AND 6r4c789) OR (-1r4c789 AND -6r4c789)

P → ¬Q, and Q → ¬P, so they form a weak link. However, ¬P→ Q is false (as is ¬Q → P), so they do not form a strong link. At most one of (P, Q) is true. Since the AIC requires a strong link there, it is not a valid AIC.

I disagree with your reasoning in the point P → Q is false (as¬Q → P). The logical implications are not false, we are not judging whether the assumptions and conclusions are correct but only the logical mechanism which is true. For the rest I agree. My problem is that this proof is in contradiction with the fact that both ¬P and ¬Q are true and consequently P = ¬P and Q = ¬Q and ¬P = ¬Q (at least one hypothesis is true in all 3 inferences), so P = ¬P = ¬Q = Q => P = Q (there is a strong inference between P and Q even if both are false). Where is the error in this reasoning?

Paolo

[eleven]

(That said, eleven's wording is a bit ambiguous. Better: "there is a hidden pair 16 in r4c56, if neither digit can be in r4c789.")

Yes, probably this ambiguity in the common speech causes the problem, that simple boolean facts often are not understood intuitively.

"both cannot be there" can be understood as
- not (the one or the other), not the one and not the other, neither the one nor the other, none of them, -(A|B)
- not (the one and the other), not both at the same time, at most one of them, -(A&B), often shortly -(AB)

Same with "the one or the other must be there"
- at least one of them, the one or the other or both, A=B
- exactly one of them, either the one or the other, but not both, A XOR B, not really relevant in AIC's, (-A&B) | (A&-B)

[eleven]

If i understood Paolo's backdoor solution method right, it is, let's say, fancy:
Ask a solver for backdoors, then try to find an AIC, that at least one of 2 backdoors must be true. Thus if one would be false, the puzzle could be solved with singles from the other, i.e. it must be solvable with singles in any case (what a surprise).

[SpAce]

Yes, probably this ambiguity in the common speech causes the problem, that simple boolean facts often are not understood intuitively.

Thank you for the good summary of the issue. Both cases are indeed hard to (remember to) express accurately in normal speech. The latter is particularly annoying, because the disambiguation of "or" requires adding the redundant "or both" or "but not both" (but not both), unless one uses the "at least one" or "exactly one" forms (but not both).

[A totally unrelated Boolean peculiarity (with little practical significance) came to mind. We (should) all know that strong inferences ("at least one true") map to OR, and it works the same way with arbitrarily large strong inference sets (SIS). We've also been taught that weak inferences ("at most one true") map to NAND. That works in practice between two nodes, but it's not exactly accurate, because NAND really means "not all true" (i.e. "at least one false"). Because of that it doesn't work for larger weak inference sets (WIS). In fact, I don't think there's a simple way to implement "at most one" logic for more than two inputs.]

If i understood Paolo's backdoor solution method right, it is, let's say, fancy:
Ask a solver for backdoors, then try to find an AIC, that at least one of 2 backdoors must be true. Thus if one would be false, the puzzle could be solved with singles from the other, i.e. it must be solvable with singles in any case (what a surprise).

Exactly. My abstraction of the logic as a pseudo-DL:

Code: Select all

Backdoor1 = ... = Backdoor2 ->singles-> Backdoor1 => +Backdoor1; stte

My deeper analysis here, though I think this is the relevant part:

The logic is technically valid, but the value of such solutions is close to zero.

(The first part of that comment is obviously not related to this discussion in any way. There's no sound logic that could prove me wrong even in theory. It's ridiculous that we're even arguing about something that has only one answer by definition.)

[SpAce]

mith, thanks for joining the cause of defending the truth I will gladly retire from that ungrateful role.

[mith]

I disagree with your reasoning in the point P → Q is false (as¬Q → P). The logical implications are not false, we are not judging whether the assumptions and conclusions are correct but only the logical mechanism which is true.

This isn't how propositional logic works.

¬P → Q is a proposition. It means "If ¬P, then Q" or in a longer form "If proposition P is not true, then proposition Q must be true".

As a logical proposition, it is either true or false. We don't always have enough information to determine whether it is true or false, but in this case we do: we have an example of a case where proposition P is not true, where proposition Q is also not true. Since Q is not always true when P is false, the material conditional ¬P → Q is false.

That is just basic propositional calculus.

For the rest I agree. My problem is that this proof is in contradiction with the fact that both ¬P and ¬Q are true and consequently P = ¬P and Q = ¬Q and ¬P = ¬Q (at least one hypothesis is true in all 3 inferences), so P = ¬P = ¬Q = Q => P = Q (there is a strong inference between P and Q even if both are false). Where is the error in this reasoning?

There is one of two problems with your reasoning - I am not an expert on AICs by any means, this is just from the logic:

1. If "strong inference" means "at least one side is true", the error is that a chain of such strong inferences does not lead to a conclusion that the ends are strongly linked. You have just demonstrated this by contradiction. The point is that if both sides of a strong link can be true, you cannot guarantee anything about the ends of the chain. (In this case you could end up with TFTF, FTFT, or FTTF - and there is in fact a weak link between P and Q - but in general the first and third strong links could also both be true under this definition, and you could end up with things like TTFT or TTTT.) On the other hnd, with alternating strong and weak links, you can say that at least one end must be true, because it rules out that FTTF case. That's why AICs work.
2. If "strong inference" means "exactly one side is true", then ¬P = ¬Q is not valid. (But a chain of an odd number of such links would result in a strong link in the end; either TFTF or FTFT, for this length.) This is the definition I was using earlier when I stated that (1|6)r4c56 = (1|6)r4c789 is not a strong link (but I don't think this necessarily needs to be the definition).

In the language of AICs, it doesn't matter so much IMO which definition you use - what matters is that it is never the case that both sides of a strong link are false. The end goal is that either the first proposition in the chain is true (in which case T=F-T=F-... or T=T-F=T-... both do the job, all we care about is that first truth) or the last is true (which is established by the alternating: F=T-F=T-F=T, where the strong links always guarantee the right sides are T, and the weak links always guarantee the left sides of the strong links are false). The problem with the chain under discussion is that (16)r4c56 and (16)r4c789 are not strongly linked, they are weakly linked (they can both be false, at most one is true), so the chain is not alternating between strong and link and we cannot conclude anything about the ends.

[Ajò Dimonios]

Mith wrote:
I disagree with your reasoning in the point P → Q is false (as¬Q → P). The logical implications are not false, we are not judging whether the assumptions and conclusions are correct but only the logical mechanism which is true.


This isn't how propositional logic works.

¬P → Q is a proposition. It means "If ¬P, then Q" or in a longer form "If proposition P is not true, then proposition Q must be true".

As a logical proposition, it is either true or false. We don't always have enough information to determine whether it is true or false, but in this case we do: we have an example of a case where proposition P is not true, where proposition Q is also not true. Since Q is not always true when P is false, the material conditional ¬P → Q is false.

Certainly if you value the proposition I fully agree with you. I interpreted that you indicate as false in (P → Q is false (as¬Q → P) the "→" which is clearly correct that is true. If I start from a false hypothesis and use a true logic I can conclude with a thesis that can be true or false.

Mith wrote:
or the rest I agree. My problem is that this proof is in contradiction with the fact that both ¬P and ¬Q are true and consequently P = ¬P and Q = ¬Q and ¬P = ¬Q (at least one hypothesis is true in all 3 inferences), so P = ¬P = ¬Q = Q => P = Q (there is a strong inference between P and Q even if both are false). Where is the error in this reasoning?


There is one of two problems with your reasoning - I am not an expert on AICs by any means, this is just from the logic:

1. If "strong inference" means "at least one side is true", the error is that a chain of such strong inferences does not lead to a conclusion that the ends are strongly linked. You have just demonstrated this by contradiction. The point is that if both sides of a strong link can be true, you cannot guarantee anything about the ends of the chain. (In this case you could end up with TFTF, FTFT, or FTTF - and there is in fact a weak link between P and Q - but in general the first and third strong links could also both be true under this definition, and you could end up with things like TTFT or TTTT.) On the other hnd, with alternating strong and weak links, you can say that at least one end must be true, because it rules out that FTTF case. That's why AICs work.
2. If "strong inference" means "exactly one side is true", then ¬P = ¬Q is not valid. (But a chain of an odd number of such links would result in a strong link in the end; either TFTF or FTFT, for this length.) This is the definition I was using earlier when I stated that (1|6)r4c56 = (1|6)r4c789 is not a strong link (but I don't think this necessarily needs to be the definition).

In the language of AICs, it doesn't matter so much IMO which definition you use - what matters is that it is never the case that both sides of a strong link are false. The end goal is that either the first proposition in the chain is true (in which case T=F-T=F-... or T=T-F=T-... both do the job, all we care about is that first truth) or the last is true (which is established by the alternating: F=T-F=T-F=T, where the strong links always guarantee the right sides are T, and the weak links always guarantee the left sides of the strong links are false). The problem with the chain under discussion is that (16)r4c56 and (16)r4c789 are not strongly linked, they are weakly linked (they can both be false, at most one is true), so the chain is not alternating between strong and link and we cannot conclude anything about the ends.

Clearly as you indicate the weak point is the contradiction between the classical definition of strong inference and related theorems http://brunogreco.free.fr/bazar/sudoku/ ... hains1.htm and the result of the logical reasoning that I get when I start from two assumptions both true. The only possibility is that the case in which the two assumptions are both true does not fall within the definition but is another type of inference. The fact is that when we deal with Boolean variables, if there is a logic mechanism between true A and true B this is identical to that between ¬A and ¬B.

Paolo

[mith]

If I start from a false hypothesis and use a true logic

Yes, if you have a true material conditional P → Q, and you determine proposition P (hypothesis, if you prefer) is false, you cannot make a determination about whether Q is true or false.

The problem is that in this case ¬P → Q isn't true. It's not a "true logic" as you put it, because ¬P can be true but Q false (that is, 1 and 6 are not both in r4c56 but are also not both in r4c789). What that means in terms of propositional calculus is that the material conditional ¬P → Q itself is false. ¬P does not imply Q. (The situation is similar, in that you cannot make a determination about the truth value of Q, but the reason is different; here it is not the hypothesis that is false, but rather the conditional.)

Clearly as you indicate the weak point is the contradiction between the classical definition of strong inference and related theorems

There is no contradiction between definition and theorem as long as you are using the right definition and theorem. It's just not true in general to say ( A = B = C = D ) → ( A = D ) if the definition of a strong link is "at least one side is true" (because of FTTF). Whereas if the definition is "exactly one side is true", ( A = B = C = D ) → ( A = D ) is true (either FTFT or TFTF). The material conditional ( A = B = C = D ) → ( A = D ) is a theorem under the stricter definition of strong link, and not a theorem under the broad definition.

Regardless, you seem to agree that in the case of (16)r4c56 = (16)r4c789 both sides can be false, and therefore this cannot be a valid strong link as written (and as a result, an AIC using this link as a strong link cannot be valid). Yes? So I'm not sure what we're arguing about at this point.

[SpAce]

Just to make sure that at least one of the two people remaining in the discussion understands: the definition of a strong inference does not in any way, shape, or form prevent having both sides true. The definition is simply: "at least one side is true". There is no "stricter definition" either. If "exactly one"-logic is needed for some weird reason (I can't think of any), it's a different type of inference with a different symbol -- not a strong inference and not '='.

A strong inference is invalid only if both sides are or could be false. If both are or could be true, it doesn't change the logic or the outcome in any way. That happens often with derived strong links, like here. Both sides of that strong link are happily true. Obviously that wouldn't work if the definition were restricted to XOR instead of OR.

The confusion comes from the fact that natively strongly-linked candidates (bivalues, bilocations) are also weakly-linked. Such "conjugate" candidates have a natural XOR-relationship (exactly one). All it means is that the same two candidates can be used in a chain for either a strong or a weak inference, depending on the situation. The XOR-relationship in the grid is not visible or relevant in an AIC at all, because only one half of it (OR or NAND) is used in any inference. Thus strong inferences are always OR (at least one), and the symbol '=' should never be used or interpreted in any other way.

If one needs a XOR-inference for some exotic reason, the suggested symbol is '^' but no one needs it in normal AICs. The important part is that '=' is always OR and nothing else. Similarly '-' is always NAND (except with more than two inputs, but that's not relevant).

Inference Types
Alternating Inference Chains (AICs) just use weak and strong inferences to link a series of Boolean (true or false) arguments. As the name implies, within the chain these inferences must strictly alternate between weak and strong:
Weak inferences: Two Booleans cannot both be true (at least one must be false, but possibly both are). . . Linking symbol: -
Strong inferences: Two Booleans cannot both be false (at least one must be true, but possibly both are). . Linking symbol: =

Conjugate inferences: Two Booleans one of which must be true and the other false. . Linking symbol: Not Standardised ( ^ is one option)

A large number of inferences used in logic chains are 'conjugate' where the linked Booleans must contain one truth. Typical cases are a 'bivalue' cell holding two digits and a 'bilocal' digit that can only occupy two cells in a house. Conjugate inferences are therefore both weak and strong, but within AICs, they can only be used in one way or the other and must be notated accordingly using the standard '-' and '=" symbols.

Weak link: (5)r1c3 – (5)r1c9. At least one of these must be false, and possibly both may be false (when (5)r1c5 is true).
Strong link: (5)r123c5 = (5)r2c456. At least one of these must be true and possibly both are (when (5)r2c5 is true).
Conjugate link: (5)r1c9 ^ (5)r2c8. One must be true and the other false, can be used either as a weak '-' or strong "=" link in an AIC.

A common misconception is that all strong inferences can also be used as weak.

--
(AIC Primer)

[mith]

Yeah, I'm on the same page now.

I think it's important to emphasize again that the "chain of same type of link implies a that type of link between the ends" idea only actually works for XOR links (a chain of an odd number of XOR links does result in an XOR link between the ends). A chain of strong inferences as defined above does not prove any link between the ends. Whether such a theorem is actually useful, I don't know - in most cases you could probably just use the fact that it is also an AIC (since all the XOR links can be strong or weak as needed).

It would be easy for someone unfamiliar with the notation to get confused, since it looks like a bunch of equal signs.

[eleven]

Adding to the confusion is, that what historically was called a strong link, was a XOR link (called conjugate link by David), typically between exactly two possibilities for a candidate in a house.
Later, with alternating chains, where the endpoints have a OR relation, this was called a strong inference (called strong link by David), which you can also have in single links like between the extra candidates of a UR.
E.g. i remember the rule: a strong link can also be used as weak link, which is wrong with David's definition.
So the naming chaos in sudoku contributed a good part to many misconceptions.

[SpAce]

Yeah, I'm on the same page now.

Good, I figured it was probably a valid strong inference (Quite possibly a conjugate inference, too, I'm afraid.)

I think it's important to emphasize again that the "chain of same type of link implies a that type of link between the ends" idea only actually works for XOR links (a chain of an odd number of XOR links does result in an XOR link between the ends).

Indeed. Simple Coloring and 3D Medusa are examples of such patterns. Here's an example:

Code: Select all

.........1.....8...85.724.6.51..8.9...6.9.7...9.5..62.2.965.13...4.....7.........
.-----------------.-----------------.-------------.
|  69    4     27 | 18     18   56  | 29   57  3  |
|  1    a36    27 | 49-3  f34   56  | 8    57  29 |
| b39    8     5  | 39     7    2   | 4    1   6  |
:-----------------+-----------------+-------------:
|  7     5     1  | 2      6    8   | 3    9   4  |
| c34    2     6  | 134    9    13  | 7    8   5  |
|  48    9    d38 | 5     e34   7   | 6    2   1  |
:-----------------+-----------------+-------------:
|  2     7     9  | 6      5    4   | 1    3   8  |
|  58    13    4  | 138    128  139 | 259  6   7  |
|  568   136   38 | 7      128  139 | 259  4   29 |
'-----------------'-----------------'-------------'

Code: Select all

As a normal X-Chain:  3r2c2 = r3c1 - r5c1 = r6c3 - r6c5 = 3r2c5 => (3r2c2 == 3r2c5) ==> -3r2c4

As a conjugate chain: 3r2c2 ^ r3c1 ^ r5c1 ^ r6c3 ^ r6c5 ^ 3r2c5 => (3r2c2 ^^ 3r2c5) ==> -3r2c4

(The doubled link symbol is just a convention to mark derived inferences.)

When converting into Boolean logic it must be understood that each XORed pair needs to be ANDed, just like with normal chains. That and the related non-commutativity are what make the link symbols different from their corresponding Boolean operators. To emphasize the difference, I use 'x' below for XOR:

Code: Select all

(3r2c2 | 3r3c1) & -(3r3c1 & 3r5c1) & (3r5c1 | 3r6c3) & -(3r6c3 & 3r6c5) & (3r6c5 | 3r2c5)

(3r2c2 x 3r3c1) &  (3r3c1 x 3r5c1) & (3r5c1 x 3r6c3) &  (3r6c3 x 3r6c5) & (3r6c5 x 3r2c5)

That's still just two operators (compared to the normal three), which is nice. It's even simpler than the NOR+NOT form, though the latter could be used for any chain. (An example here. I just randomly used ':' for NOR lacking a better symbol).

A chain of strong inferences as defined above does not prove any link between the ends.

Exactly. As someone once said, there's nothing more useless than two adjacent strong links.

Whether such a theorem is actually useful, I don't know - in most cases you could probably just use the fact that it is also an AIC (since all the XOR links can be strong or weak as needed).

Indeed. Both forms work, and I don't really have a problem if someone wants to start using the ^ style for conjugate chains. Problem is, fewer people would understand them, and pure conjugate chains are pretty rare. It's also harder to verify that there's an odd number of links because they don't alternate. (It also means that, by definition, they're not AICs.)

Sadly the conjugate relationships don't really add much value except in spotting such chains. Nearly one half of the potential strong links are wasted in such chains, because they have to be used for weak inferences. That said, David had found some uses for them. You can find examples in the JExocet Compendium, at least in the SK-Loop Examples. I never digged deep enough to fully understand that part.

It would be easy for someone unfamiliar with the notation to get confused, since it looks like a bunch of equal signs.

Indeed. That's the most confusing part of Eureka. It also prevents using the '=' for its normal meaning in a Eureka context. Some time ago I experimented with my own Eureka fork in which I used ':' for strong links. I thought it worked pretty nicely. (I actually got the idea from that NOR experiment.)

[SpAce]

Btw, one possible use for a conjugate chain is a Remote Pair, which is pretty awkward to write as a chain otherwise:

Code: Select all

.---------------.------------------.------------.
|  126   8   16 |  9      12   7   | 3  5    4  |
|  3     7   4  |  6      8    5   | 1  2    9  |
|  9    b12  5  | a12     3    4   | 7  8    6  |
:---------------+------------------+------------:
| d12    6   37 |  34-12  5    123 | 9  147  8  |
|  5    c12  8  |  7      124  9   | 6  14   3  |
|  4     9   37 |  13     6    8   | 2  17   5  |
:---------------+------------------+------------:
|  16    4   2  |  8      9    16  | 5  3    7  |
|  8     3   16 |  5      7    126 | 4  9    12 |
|  7     5   9  |  1234   124  123 | 8  6    12 |
'---------------'------------------'------------'

Code: Select all

(1^2)r3c4 ^ (2^1)r3c2 ^ (1^2)r5c2 ^ (2^1)r4c1 => (12)r3c4,r4c1 ==> -12 r4c4

It works because it forms two conjugate parities, both of which have 12 in r3c4,r4c1:

Code: Select all

('1^2")r3c4 ^ ('2^1")r3c2 ^ ('1^2")r5c2 ^ ('2^1")r4c1 => ('1,'2 | 2",1")r3c4,r4c1 ==> -12 r4c4

I think this is something StrmCkr once tried to explain to me, but I rejected the idea because it wasn't expressible with our normal link symbols. With the conjugate symbol it actually works. Then again, it's hard to beat my favorite AIC form:

Code: Select all

(1,2,1,2 = 2,1,2,1)r3c42,b4p51 => -12 r4c4

(Of course the '=' could be replaced with '^' in that too, but it would add no value.)

[Ajò Dimonios]

I am fully convinced by the proof (A = B = C = D) → (A = D) that (A = D) is a strong inference. For this reason the strong inference definition: Definition 1: Let A, B be two assumptions. We say that A, B are thicklinked and note A == B when at least one of A, B is true. We say that A, B are thinlinked and note A - B when at most one of A, B is true should be generalized with: Definition 1: Let A, B be two assumptions. We say that A, B are thicklinked and note A == B when A is assumed false B turns out to be true and when B is assumed false A turns out to be True.
This uses the method of constructing a strong inference as a definition. This is certainly confirmed by experience, no one after writing an AIC that leads to certain eliminations checks after finding the solution that all the strong inferences of all the AICs written by the player are confirmed by the current definition of strong inference.

Paolo

[mith]

What proof? You demonstrated in your previous post that the implication is not valid for the definition “at least one is true”. For a chain A = B = C = D, you can have truth values of:

FTFT
FTTF
FTTT
TFTF
TFTT
TTFT
TTTF
TTTT

Since there is a case where A and D are both false, there is no strong link, by the definition you yourself are using for the chain.

You posted this previously and called it a contradiction. Why are you now saying you are “convinced by the proof”?