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

(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 <= xWith 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 = RobTherefore Roberto is the barber.

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