The Barber Paradox

------------------

Suppose that, in a village, all men must be clean-shaven. By law, there must be a man in the village (the barber) who shaves those and only those men in the village who do not shave themselves. Does the barber shave himself?

If the barber shaves himself, then he would be shaving a man who DOES shave himself, and would therefore be in violation of the law. If he does not shave himself, then he would fail to shave a man in the village who does NOT shave himself. Either way, he would be in violation of the law! How can we resolve this seeming contradiction?

Logical Symbols

---------------

Man(x)      means x is a man in the village

Shaves(x,y) means x shaves y

ALL(x):     means "for all x, we have..."

EXIST(x):   means "there exists an x such that..."

=>          means "implies"

<=>         means "if and only if"

~           means "not"
 

Proof

-----

We begin by supposing the barber is a man in the village, and that for each man in the village, the barber shaves him if and only if that man does not shave himself.

      1     Man(barber)

          & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]

            Premise

    Splitting this premise...

      2     Man(barber)

                  Split, 1

      3     ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]

                  Split, 1

    Applying the above definition of the barber to the barber himself, we have...

      4     Man(barber) => [Shaves(barber,barber) <=> ~Shaves(barber,barber)]

            U Spec, 3

And since the barber is a man in the village, we obtain the contradiction that the barber shaves himself if and only if he does NOT shave himself!

       5     Shaves(barber,barber) <=> ~Shaves(barber,barber)

             Detach, 4, 2

Since we obtained a contradiction from our initial premise (line 1), that premise must be false. Negating the initial premise, and we have...

6     ~[Man(barber)

     & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]]

      Conclusion, 1

Generalizing...

7     ALL(barber):~[Man(barber)

     & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]]

      U Gen, 6

Switching the first universal quantifier...

8     ~EXIST(barber):~~[Man(barber)

     & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]]

      Quant, 7

Removing the double negation, we see that, since the law itself is self-contradictory, no such man can exist!

9     ~EXIST(barber):[Man(barber)

     & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]]

      Rem DNeg, 8