You come at a road split, and you know that one of the two roads ahead leads to the city where you're heading, and the other leads to an area infested with robbers and the like. But you don't know which way goes where, and you really wish to avoid the crooks. There is a man standing there, and you recognize him: he is one of a twins. It is common knowledge that one of those twins always speaks the truth, and that the other always lies. But you never could tell them apart. Now, you can by asking one question know which way the city lies. What question?
~x = "x's twin brother" T.x == "x is the truth-speaking twin" x[p.x] == "x can/would say p.x" x<p.x> == "x says p.x"We can put down the following axioms:
(A) T.x != T.~x (B) x[p.x] == T.x == p.x (C) x<p.x> => x[p.x]
(1) b<Q == y> => (R == z)where
b = "the twin brother that is present at the road split" Q == "the question to be put to b" y == "the answer that you get back from b" R == "the right-hand road leads to the city" z == "the conclusion: whether R is true or not"Note that we chose one specific fact that we'd like to know the truth about ("the right-hand road leads to the city") from the many that we could choose. The solution that we present here can be used to find out the truth about any statement.
To solve the problem, we have to find a question (viz. Q) and a way to interpret the answer (viz. z) that makes (1) valid. We do that by calculation.
b<Q == y> => (R == z)
<= "(C), which is the only thing we know about x<p.x>"
b[Q == y] => (R == z)
<= "(B), which is the only thing we know about x[p.x]"
(T.b == Q == y) => (R == z)
<= "logic: strengthening, which is the simplest way to relate
all variables"
T.b == Q == y == R == z
Now by ordering the terms we can rewrite this in the form
Q == ... == z == ... <= "logic: strengthening" (Q == ...) /\ (z == ...)which give us a question, and the way to interpret the answer. But the rewriting can be done in a lot of ways. We show the two most interesting here. First the most straightforward one:
T.b == Q == y == R == z == "logic: reorder terms" Q == T.b == R == z == y == "(B)" Q == b[R] == z == y <= "logic: strengtening" (Q == b[R]) /\ (z == y)The question is: "Can you say that the right-hand road leads to the city?" If the answer is yes, then the right-hand road indeed does; if no, then it doesn't.
The notable thing about this solution is that it doesn't use fact (A): we only need to know that the twin we meet is always lying or always speaking the truth.
Now for a solution that does use (A):
T.b == Q == y == R == z == "logic: reorder terms" Q == T.b == R == z == y == "apply (A)" Q == !T.~b == R == z == y == "logic: move the negation" Q == T.~b == !R == z == !y == "(B)" Q == ~b[!R] == z == y <= "logic: strengtening" (Q == ~b[!R]) /\ (z == y)The question to pose is now: "Can your brother say that the left-hand road leads to the city?" If the answer is yes, we take the right-hand road, and we go left on a no.
This last solution is the one that is usually given. But for me the first one is the more surprising one. What was interesting is that I only found it after trying to construct a solution to the puzzle, instead of verifying one that came out of the blue.
Changes to calc/misc-twins.html: Mon Nov 1 14:43:42 MET 2004 Marnix Klooster * Fixed typo in equation (A). 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 Fri Sep 14 19:29:43 MEST 2001 marnix * added a opposite-twins puzzle