Which Dracula is the vampire?

Chapter 4, Problem 5 from [The Lady or the Tiger]

Here is a [calculational solution] to this problem.

Chapter 4 of "The Lady or the Tiger" brings us to Transsylvania. In this country we find both vampires (who always lie) and humans (who always speak the truth). However, part of the population is insane, so that they believe the truth to be false, and lies to be true. Therefore, e.g., a sane vampire and an insane human can never say opposite things.

In problem 5 Raymond Smullyan tells us about a Mr and Mrs Dracula, of which it is already known that one of them is sane and the other insane, and that one of them is a vampire and the other a human. Then Inspector Craig hears them say the following. He: "She is a vampire." She: "He is insane!"

Question: which one is the vampire?

Representation

We will use the following notations, where x is any person from Transsylvania:
  H.x == "x is a human (as opposed to vampire)"
  S.x == "x is sane (as opposed to insane)"
  x[P.x] == "x believes P.x"
  x<P.x> == "x says P.x"
The following axioms hold for every Transsylvanian x:
  (A1) x[P.x] == H.x == S.x == P.x
  (A2) x<P.x> => x[P.x]

Solution

We represent the two Transsylvanians as h (for "he") and s ("she"). Their two statements can be written formally as
  (1) h<~H.s>
  (2) s<~S.h>
and their known differences as
  (3) H.h =/= H.s
  (4) S.h =/= S.s
We can immediately apply (A2) and (A1) to her statement (2) to derive
   s<~S.h>                                   --- (2)
=>   "(A2) with x:=s"
   s[~S.h]
==   "(A1) with x:=s"
   H.s == S.s == ~S.h
==   "(4)"
   H.s
==   "(3)"
   ~H.h
Therefore he is the vampire, and she is human.

(Note that we didn't use his statement (1) at all. It doesn't say anything about their 'vampirity', but it does describe their sanity: a similar calculation

   h<~H.s>                                   --- (1)
=>   "(A2) with x:=h"
   h[~H.s]
==   "(A1) with x:=h"
   H.h == S.h == ~H.s
==   "(3)"
   S.h
==   "(4)"
   ~S.s
shows that he is sane, and she is insane.)
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-4-5.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)