The Barber Paradox Revisited
             Why We Need Set Theory

                                                                           ŠAnna Vasilkova

Here, we will consider simple variations of the famous Barber Paradox (3 versions) and demonstrate the need for set theory in a very simple and direct way.

Version 1

The original Barber Paradox stated that the fabled barber is a man in a village who is required to shave those and only those men living there who do not shave themselves. It asks, does the barber shave himself or not? Either way, we arrive at a contradiction, so we can only conclude that no such barber can exist. Here is the original formalization of this scenario:

     Suppose we define the Shaves relation as follows where Shaves(barber,a) means the barber shaves a. 

      1     ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]

     Apply Universal Specifcation setting a=barber to obtain the contradiction... 

      2     Shaves(barber,barber) <=> ~Shaves(barber,barber)
            U Spec, 1 

We conclude that no such barber can exist. 

3     ~EXIST(barber):ALL(a):[Shaves(barber,a) <=> ~Shaves(a,a)]
4 Conclusion, 1

In this rather cartoonish formalization, we are quantifying over all objects in the universe. We are potentially shaving everything from black holes in space to the number 5.

Version 2

To make it just a bit more realistic, we might consider restricting our attention somewhat to the men living in the village. This will lead to an important insight that is not apparent in the original formalization.

     Suppose the barber is a man in the village. 

      1     Man(barber)

          Define the shaving relation as follows... 

            2     ALL(a):[Man(a) => [Shaves(barber,a) <=> ~Shaves(a,a)]]

          Apply Universal Specification setting a=barber in the previous line. 

            3     Man(barber) => [Shaves(barber,barber) <=> ~Shaves(barber,barber)]
                  U Spec, 2 

          Since the barber is a man in the village, we obtain the following contradiction... 

            4     Shaves(barber,barber) <=> ~Shaves(barber,barber)
                  Detach, 3, 1 

     The "definition" on line 2 results on a contradiction, so it must be false. 

      5     ~ALL(a):[Man(a) => [Shaves(barber,a) <=> ~Shaves(a,a)]]
4 Conclusion, 2 


6     ALL(barber):[Man(barber)
     => ~ALL(a):[Man(a) => [Shaves(barber,a) <=> ~Shaves(a,a)]]]

4 Conclusion, 1 

Or equivalently...

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

Thus, if this shaving relation holds for all the men in the village, then the barber cannot be a man in the village (perhaps a women).

We can now ask, is the converse true,  i.e. if the barber is not a man in the village, can this shaving relation still hold? By pure logic alone, we cannot prove the converse:

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

It is not even true in general, e.g. this statement would be false if the barber is not a man in the village and does not shave someone who does not shave himself.

Version 3

Using set theory, however, we can, formally prove:

     & barber
e v
     & Set(m)
     & ALL(a):[a
e m => a e v]
     => [EXIST(s):ALL(a):[a
e m => [(barber,a) e s <=> ~(a,a) e s]]
     <=> ~barber
e m]]


See  formal proof with commentary (81 lines)