Introduction

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

Here we prove that if a barber is a member of a set of men (e.g. those living

in a a town or village), then there does NOT exist a relation 'shaves' defined

on that set of men such that the barber shaves those and only those men who do

not shave themselves.

Proof

-----

Suppose the barber is a man in the village

1     barber e men

      Premise

     Suppose further that there exists a relation 'shaves' defined on the men in

     the village such that the barber shaves those and only those men who do not

     shave themselves

      2     EXIST(shaves):ALL(x):[x e men

          => [(barber,x) e shaves <=> ~(x,x) e shaves]]

            Premise

     Removing the existential quantifier, we have the definition of 'shaves'

      3     ALL(x):[x e men

          => [(barber,x) e shaves <=> ~(x,x) e shaves]]

            E Spec, 2

     Apply the definition to the barber himself

      4     barber e men

          => [(barber,barber) e shaves <=> ~(barber,barber) e shaves]

            U Spec, 3

     We obtain the contradiction...

      5     (barber,barber) e shaves <=> ~(barber,barber) e shaves

            Detach, 4, 1

By contradiction, there cannot exist a relation 'shaves' defined on the men

in the village such that the barber shaves those and only those men who do

not shave themselves

6     ~EXIST(shaves):ALL(x):[x e men

     => [(barber,x) e shaves <=> ~(x,x) e shaves]]

      4 Conclusion, 2