Who is the barber?

Chapter 3, Problem 7 from [To Mock a Mockingbird]

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