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?
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
(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" q=jTherefore 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.
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)