Chapter 5 of "The Lady or the Tiger" is about two groups of people: those who can only ask questions that should be answered with "Yes" (type A), and those who can only ask questions that should be answered with "No" (type B).
Problem 10 from this chapter is as follows (as found somewhere on the Internet):
"I met three sisters: Alice, Betty and Cynthia. Alice asked Betty: 'Are you the type, who could ask Cynthia, if she is the type to ask you, if you both belong to different groups?' You can derive the type of one of the sisters! Who is what?"
A.x == "x is of type A" B.x == "x is of type B" x[P.x] == "x (is of the type that) can/could ask P.x" x<P.x> == "x asks P.x"With these notations, we can put down the following axioms:
(A1) A.x =/= B.x (A2) x[P.x] == A.x == P.x (A3) x<P.x> => x[P.x]
a< b[c[A.b =/= A.c]] >Reasoning from this using our axioms, we get
a< b[c[A.b =/= A.c]] > => "(A3) with x:=a --the only thing we know about x<P.x>" a[ b[c[A.b =/= A.c]] ] == "(A2) with x:=a --the only thing we know about x[P.x]" A.a == b[c[A.b =/= A.c]] == "(A2) with x:=b --the only thing we know about x[P.x]" A.a == A.b == c[A.b =/= A.c] == "(A2) with x:=c --the only thing we know about x[P.x]" A.a == A.b == A.c == A.b =/= A.c == "logical manipulation on == and =/=; see subproof" A.b == A.c == A.b =/= A.c == "== and =/= are symmetric and associative" (A.b == A.b) == (A.c =/= A.c) == "logic: meaning of == and =/=" true == false == "logic" false A.a == false == "(A1) with x:=a" B.aSo the only thing that we can derive from the given fact is that Alice is of type B.
Changes to calc/tlott-5-10.html: Wed Nov 10 13:27:59 MET 2004 Marnix Klooster * Make clearer that this computation is the only thing we can do. 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