The case of John

Chapter 7, Problem 1 from [The Lady or the Tiger]

Here is a [calculational solution] to this problem.

John has committed a crime, and he and his identical twin are arrested and brought to court. It is common knowledge that one of the twins (either John or his brother) is a notorious liar: he never speaks the truth.

The judge asks one of the twins if he is John. "Yes, I am." Then he asks the other the same question. After hearing the answer (which is either "yes" or "no") the judge knows who is John. Do you?


We use the following abbreviations:
 j = "John"
 p = "the first twin that is questioned"
 q = "the second twin that is questioned"
 L.x == "x always lies"
 x<P.x> == "x says P.x"
where x is either p or q.

The knowledge about John and his twin brother can be formalized as follows:

  (A) p=j =/= q=j
  (B) L.p \/ L.q
  (C) x<P.x> /\ L.x => ~P.x


The two statements are
  (1) p< p=j >
  (2) q< q=j == z >
where z is q's answer (true for "yes" and false for "no").

We start reasoning from (B):

   L.p \/ L.q                                         --- (B)
=>   "weaken both disjuncts separately with (C):
      the LHS using (1) and the RHS using (2)"
   ~(p=j) \/ ~(q=j == z)
==   "use (A) to remove p"
   q=j \/ ~(q=j == z)
==   "logic: negation of LHS of \/ is true in RHS"
   q=j \/ ~(false == z)
==   "logic: simplify"
   q=j \/ z
If z were true (i.e., if the second twin would have said "yes"), then the result of this line of reasoning would be 'true': in that case the judge couldn't have derived anything. Therefore z is false, and we continue:
==   "z is false"
Therefore the second twin is John (and he denied that fact). We still don't know which of the twins is the notorious liar, though. We only know that both twins lied this time.
This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.
Changes to calc/tlott-7-1.html:

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Tue Feb  5 14:42:44 MET 2002  marnix
  * Added tlott-4-5 and tlott-7-1 (and made tlott.html and calc-sols.html m4-aware)