Chapter 3 of "The Lady or the Tiger" is about asylums that contain sane and crazy people: the sane always speak the truth, and the crazy always lie. Every one of them is either a doctor or a patient. Something is wrong with an asylum if it has either a crazy doctor or a sane patient.

Problem 8 from this chapter can be summarized as follows:

Inspector Craig arrived at the eighth asylum, and found out thatHow did Craig prove that something was wrong with this asylum?

- (1) two residents either trust each other, or they don't;
- (2) every resident has another resident as his teacher;
- (3) residents are only willing to teach those who trust themselves;
- (4) for every resident x there is a resident, who trusts precisely those residents who have a teacher trusted by x;
- (5) there is a resident who trusts all patients, and patients only.

D.x == "x is a doctor" S.x == "x is sane" x[p.x] == "x believes p.x"With these notations, we can put down the following axiom:

(A) x[p.x] == S.x == p.xFor this specific problem we will also use the following notations:

xVy == "x trusts y" xLy == "x is a teacher of y"(Since both 'trusts' and 'teacher' starts with a 't', I used the initials of the two Dutch words: 'vertrouwt' en 'leraar'.)

We can model the given facts as follows: for any residents x and y,

(2) (Ea: aLx) (3) xLy => x[yVy] (4) (Ea: (Ab: aVb == (Ec| cLb: xVc))) (5) QVx == !D.xHere we've given the 'queer' resident from property (5) the name Q.

When we look at our goal, (Ea: S.a =/= D.a), and compare this to our givens, we see that only fact (5) deals with D. Similarly only fact (3) deals with S:

xLy => x[yVy] --- (3) == "(A)" xLy => (S.x == yVy)In both of these cases, S and D are directly related to an expression of the form ...V... Looking now at fact (4), we see that it contains two V relations. The first one can be connected to S by substituting b:=a; the second one can be connected to D by substituting x:=Q. Therefore our strategy is to rewrite and simplify (4).

However, in our goal S.a and D.a are close together, but in fact (4) the two V relations are separated. This can be fixed by applying the following law of predicate logic:

(Ex| p.x: q.x) == r => "(Ex: p.x)" (Ex| p.x: q.x == r)In other words: equivalence distributes (in one direction) over an existential quantification with a non-empty domain.

We now have enough to start rewriting (4):

(Ax: (Ea: (Ab: aVb == (Ec| cLb: xVc)))) --- (4) => "the above-mentioned law: (Ec: cLb) is given as fact (2)" (Ax: (Ea: (Ab: (Ec| cLb: aVb == xVc)))) => "substitute b:=a, x:=Q, as was suggested above" (Ea,c| cLa: aVa == QVc) == "fact (5), with x:=c" (Ea,c| cLa: aVa == !D.c) == "rewrite aVa using (A), to prepare for the use of fact (3)" (Ea,c| cLa: c[aVa] == S.c == !D.c) == "fact (3), with x:=c and y:=a" (Ea,c| cLa: S.c == !D.c) == "separate (Ea...)" (Ec| (Ea: cLa): S.c == !D.c) => "weaken range of (E...)" (Ec: S.c == !D.c)And that is what we set out to prove.

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-3-8.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