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

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