# Which Dracula is the vampire?

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)