The eighth asylum: Trust and teachers

Chapter 3, Problem 8 from [The Lady or the Tiger]

Here is a [calculational solution] to this problem.

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 that

(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.
How did Craig prove that something was wrong with this asylum?

Representation

For all the problems from this chapter, we can use the following notations. x stands for an arbitrary person in an asylum, and p.x for an arbitrary statement involving (at least) x.

  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.x

For 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'.)

Solution

We have to prove that something is wrong, formally: (Ea: S.a =/= D.a).

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.x

Here 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