Given antecedent P which is the following linked cell pattern:
- Code: Select all
ab - bc - cd
/ |
Xa |
\ |
af - ef - de
we wish to show directly that P implies Q, where consequent Q is the removal of 'a' as a possible candidate from the Xa-cell. Most proofs for this will show that P implies Q by proving the contrapositive; i.e. they assert "not Q" and show that it implies you can't satisfy P (in other words, ~Q implies ~P). Since assuming ~Q and proving ~P is the same as assuming that the Xa-cell equals 'a' and then finding a contradiction, some purists have avoided the forcing chain method because they have only seen it proven using a "T&E" tactic. This proof will avoid any assumptions about the content of the cells beyond what is given in P.
let A = set of solutions placing a in the ab-cell.
let B = set of solutions placing b in the ab-cell.
let B' = set of solutions placing b in the bc-cell.
let C = set of solutions placing c in the bc-cell.
let C' = set of solutions placing c in the cd-cell.
let D = set of solutions placing d in the cd-cell.
let D' = set of solutions placing d in the de-cell.
let E = set of solutions placing e in the de-cell.
let E' = set of solutions placing e in the ef-cell.
let F = set of solutions placing f in the ef-cell.
let F' = set of solutions placing f in the af-cell.
let A' = set of solutions placing a in the af-cell.
let A" = set of solutions placing a in the aX-cell.
Note that any of these sets could equal the empty set, thus no assumption is made here about the content of any of the various cells
From the content of the cells we do get the following equations:
A = not B; B = not A;
B' = not C; C = not B';
C' = not D; D = not C';
D' = not E; E = not D';
E' = not F; F = not E';
A' = not F'; F' = not A';
Note the subset relationship that if S is a subset of T,
then (not S) contains (not T).
It is used at the end of each of the following steps.
from the B-B' link we get B' is a subset of (not B);
therefore, from the equations above, B' is a subset of A;
hence C = (not B') contains (not A);
from the C-C' link we get C' is a subset of (not C);
therefore, from the equations above, C' is a subset of B' is a subset of A;
hence D contains (not A);
from the D-D' link we get D' is a subset of (not D);
therefore, from the equations above, D' is a subset of C' ... is a subset of A;
hence E contains (not A);
from the E-E' link we get E' is a subset of (not E);
therefore, from the equations above, E' is a subset of D' ... is a subset of A;
hence F contains (not A);
from the F-F' link we get F' is a subset of (not F);
therefore, from the equations above, F' is a subset of E' ... is a subset of A;
hence A' contains (not A);
due to links with A and A', A" is a subset of (not A), and A" is a subset of (not A').
taken together, this means A" is a subset of (not (union of A and A')).
but since A' contains (not A),
the union of A and A' >= union of A and (not A) = universal set of 'a' solutions.
and not (union of A and A') = empty or null set.
Thus A" is a subset of the empty set.
Since the only subset of the empty set is the empty set, we have
A" = empty set;
and from our definition of A", we know that if A" is the empty set, then 'a' can be removed as a candidate from the aX-cell.
Thus we have shown that P implies Q without any unwarranted assumptions about the contents of any of the cells.
This is valid no matter how many solutions the puzzle has. I think it should be reasonably easy to show via induction that the length of the chain can range from just an Xa and two ab-cells (essentially a naked pair situation) to as long a chain as the puzzle grid will allow.
It probably wouldn't take much tweaking to use this style of proof for all kinds of forcing net/chain hypotheses.
