The Barber ParadoxThis is a paradox first formulated by Bertrand Russell as a simple analogy to his famous set-theoretic paradox which undermined the very foundations of mathematics in his day. It went something as follows: In some strange land, it was decreed that in each village, there must be a barber, a man in that village who was to shave those and only those men in the village who do not shave themselves. Following is a formal proof resolving this paradox. The notation is a follows: Man(x) = x is a man the village Shaves(x,y) = x shaves y & = AND => = IMPLIES <=> = IF-AND-ONLY-IF (IFF) ~ = NOT ALL(x): = the universal quantifier, for all x ... EXIST(x): = the existential quantifer, there exists an x such that...

Suppose we define the barber as follows... 1 Man(barber) & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]] Premise Splitting this statement... The barber is a man in the village. 2 Man(barber) Split, 1 If x is a man in the village, then the barber shaves x if and only if x does not shave himself. 3 ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]] Split, 1 Applying the definition of the barber to the barber himself... 4 Man(barber) => [Shaves(barber,barber) <=> ~Shaves(barber,barber)] U Spec, 3 Since the barber is a man in village, we obtain the following contradiction... 5 Shaves(barber,barber) <=> ~Shaves(barber,barber) Detach, 4, 2

By contradiction, we obtain... 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 quantifier... 8 ~EXIST(barber):~~[Man(barber) & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]] Quant, 7 Removing the double negation, we obtain the following theorem that there cannot exist a barber as defined above: 9 ~EXIST(barber):[Man(barber) & ALL(x):[Man(x) => [Shaves(barber,x) <=> ~Shaves(x,x)]]] Rem DNeg, 8