Who is the barber?
Here is a [calculational solution] to this problem.
I won't quote the
problem here, for two reasons: I only have access to a translated (Dutch)
version of the book; and I don't know about the copyright rules.
Representation
x, y, z stand for arbitrary men.
b is the barber, and Ber, Ben,
Rob, Ram, and Alf are the men mentioned in
the problem.
We model a man by a function from days to booleans, indicating whether
that man wears a wig on that day. A lot of the expressions that we
want to use are similar to 'on every day d, x
wears a wig whenever y wears one'. We could model this by
(Ad|: x.d <= y.d), where d stands for an
arbitrary day. But to simplify the notation, we will use [...]
to mean "on every day, ...", and leave out all
".d" arguments. So the statement above would be modeled by
writing it as [x <= y].
"x is a follower of y" is now modeled by [x <= y], "x is a follower of
both y and z" by [x <= y /\ z], and "always either x or y wears a wig,
but not both" by [x =/= y].
We are also given that every man has distinct wig-wearing behavior:
(A) x = y == [x == y]
Two properties of [...] that we will need is:
(B) [true] == true
(C) [P /\ Q] == [P] /\ [Q]
Finally, we note that [...] obeys Leibniz' rule: substituting equals
for equals within it, the resulting statement is equivalent to the
original one.
Solution
The five facts can now be represented as follows:
(1) [Ber =/= Ben]
(2) [Rob =/= Ram]
(3) [Ram == Alf /\ Ben]
(4) [Ber <= Alf /\ b]
(5) (Ax| [Ber <= Alf /\ x]: [b <= x])
[Note: I interpret Smullyans "the barber is a follower of X alone"
simply as "the barber is a follower of X". Smullyan probably added
the word "alone" to emphasize that the 1-person concept of
followership was intended, and not the 2-person concept. My initial
interpretation was a lot more complex: (Ay|: [b <= y] == y = x);
but that turned out to lead to a contradiction. rec.puzzles put
me correct.]
The obvious place to start is the common subexpression of (4) and (5).
For every x, for every day
Ber <= Alf /\ x
== "by (1) ---working towards (3)"
!Ben <= Alf /\ x
== "write out <= ---working towards (3)"
!Ben \/ !Alf \/ !x
== "rearrange ---working towards (3)"
!(Alf /\ Ben) \/ !x
== "by (3)"
!Ram \/ !x
== "by (2)"
Rob \/ !x
== "by the definition of <="
Rob <= x
With this we can rephrase (4) and (5) as
(4') [Rob <= b]
(5') (Ax| [Rob <= x]: [b <= x])
Now it is clear that we can choose x:=Rob and use the mutual implication
between b and Rob:
(5')
=> "choose x:=Rob"
[Rob <= Rob] => [b <= Rob]
== "logic; Leibniz"
[true] => [b <= Rob]
== "(B); simplify"
[b <= Rob]
Combining this result with (4') gives
[b <= Rob] /\ [Rob <= b]
== "(C)"
[(b <= Rob) /\ (Rob <=b)]
== "mutual implication is equivalence; Leibniz"
[b == Rob]
== "(A)"
b = Rob
Therefore Roberto is the barber.
Acknowledgements
Thanks to Nis Jorgensen for reassuring me that my memory of this problem
was correct, by looking it up in the book. Thanks to Mark Tilford and
Jonathan Dushoff for gently suggesting that my interpretation of this
problem was incorrect: I was reading it like a mathematician, not like
an ordinary human being :-)
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/tmam-3-7.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
Tue Sep 18 05:50:38 MEST 2001 marnix
* found a correct proof, after help on interpretation by rec.puzzles readers
Sat Sep 15 15:53:44 MEST 2001 marnix
* replaced 'proof' of barber-problem by proof of inconsistency
Fri Sep 14 19:27:01 MEST 2001 marnix
* added todo comment
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