```The Barber Paradox

This 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
```
```

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

```