O.x == "x opens the lock" N.x == "x is neutral" J.x == "x jams the lock"x and y represent combinations; a combination is a non-empty digit sequence. p and q represent (possibly empty) digit sequences. We also introduce the following notations for sequences:
p = q == "p and q contain the same digits in the same order" <p> = "the sequence that is the reverse of p"So for example <1233> = 3321.
The crucial notation that we introduce is:
[x] = "the combination to which x is related"In terms of the machines in Chapters 9 through 13 in [The Lady or the Tiger], [x] is the output of the machine for input x.
(A) [2x2] = x (B) [1x] = 2[x] (C) [5x] = <[x]> (D) [9x] = [x][x] (E1) N.x => J.[x] (E2) J.x => N.[x]We are also given that
(Z) exactly one of O.x, N.x, and J.x is trueOne consequence of this (see my discussion of [Trilemmas]) is:
(Z1) O.x == N.x == J.xAll these properties hold for all combinations x.
The problem is now to find the shortest x for which O.x.
O.x == "(Z1)" N.x == J.x == "logic, working towards (E1) and (E2)" (N.x => J.x) /\ (J.x => N.x) <= "(E1); (E2)" [x] = xSo any combination that is related to itself will open the lock.
Because expressions of the form [m2x2] occur often, we introduce a special notation:
m.x = [m2x2]We use a function-application notation here, with a reason. Let's compute 1.x:
1.x = "definition of ." [12x2] = "(B)" 2[2x2] = "(A)" 2xWhen we do this also for 5 and 9, we get
(B') 1.x = 2x (C') 5.x = <x> (D') 9.x = xxSo we see that these digits are operations: 1 prepends a 2, 5 reverses, and 9 duplicates a digit sequence.
We can also combine operations:
(*) n.(m.x) = nm.xWe prove this only for n=1; the other proofs are similar.
1.(m.x) = "(B')" 2(m.x) = "definition of ." 2[m2x2] = "(B) from right to left" [1m2x2] = "definition of ." 1m.xTo give a simple example, it is easy to compute that
51.78 = "(*) from right to left" 5.(1.78) = "(B')" 5.278 = "(C')" 872In the next step we will perform a similar situation, but then from bottom to top.
[x] = x <= "write x as m2y2" (Em,y| x = m2y2: [m2y2] = m2y2)Now we would like to write m2y2 as an operation on m and y. Since we know that we have a duplication operation, it seems that m2m2 is easier to rewrite. Therefore we calculate:
m2m2 = "(D') from right to left" 9.m2 = "definition of <...>, to put the 2 up front" 9.<2<m>> = "(C') from right to left" 9.(5.2<m>) = "(B') from right to left" 9.(5.(1.<m>)) = "(C') from right to left" 9.(5.(1.(5.m))) = "(*), three times" 9515.m = "definition of ." [95152m2]With this we can continue our earlier calculation:
(Em,y| x = m2y2: [m2y2] = m2y2) <= "take y:=m" (Em| x = m2m2: [m2m2] = m2m2) == "proof above" (Em| x = m2m2: [m2m2] = [95152m2]) <= "Leibniz' rule" (Em| x = m2m2: m2m2 = 95152m2) == "remove 2m2 at the end" (Em| x = m2m2: m = 9515) == "one-point rule" x = 9515295152Summarizing the complete calculation, we proved
(Ax| x = 9515295152: O.x)or equivalently O.9515295152. And this is a combination that opens the lock. I also believe this to be the shortest one, but have not been able to prove that.
Because of (Z) we know that a combination opens the lock iff it is not neutral and also doesn't jam it. In other words,
(Z2) O.x == !J.x /\ !N.x(This is another consequence of (Z): see [Trilemmas].) This allows us to prove a statement of the form O.x as follows:
O.x == "(Z2)" !J.x /\ !N.x <= "(E1) and (E2) from right to left" !N.[x] /\ !J.[x] == "(Z2) from right to left" O.[x]Applying this to the combination that we already found, and abbreviating m = 9515, we get
O.m2m2 --- already proved above == "(D') from right to left" O.(9.m2) == "definition of ." O.[92m22] => "the property we've just proven" O.92m22So 92951522 is also a working combination, and it is shorter that the one I (and Smullyan) found. Again, I cannot prove that it is the shortest.
Changes to calc/tlott-8-and-13.html: Sat Oct 30 12:38:39 MEST 2004 Marnix Klooster * Move from CVS to darcs: do not show the CVS date anymore. Thu Feb 7 19:43:35 MET 2002 marnix * Updated all files to use the m4 template Wed Sep 5 21:20:00 MEST 2001 marnix * Made explicit that last changed date is in GMT Wed Sep 5 21:08:51 MEST 2001 marnix * Now 'last changed' is on its own line Wed Sep 5 10:10:47 MEST 2001 marnix * Added date last changed Wed Sep 5 08:50:24 MEST 2001 marnix * Initial revision