THE BARBER PARADOX/THEOREM

**************************

 

In an village with a resident barber, that barber can shave those and only those men in the village who do not shave themselves if and only if that barber is not a man.

 

   ALL(v):ALL(barber):ALL(m):[Set(v)

   & barber e v

   & Set(m)

   & ALL(a):[a e m => a e v]

 

   => [EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

   <=> ~barber e m]]

 

where

 

   v = the set of all villagers

   m = the set of all men in the village

   s = the shaving relation on v, a set of ordered pairs, (x,y) e s means x shaves y

 

This proof makes use of the Cartesian Product Axiom (line 18) and the Subset Axioms (line 26).

 

 

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

   

    PROOF

    *****

   

    Suppose...

 

      1     Set(v)

         & barber e v

         & Set(m)

         & ALL(a):[a e m => a e v]

            Premise

 

    v = the set of all villagers

 

      2     Set(v)

            Split, 1

 

    The barber is a resident of the village

 

      3     barber e v

            Split, 1

 

      4     Set(m)

            Split, 1

 

    The set of men is a subset of the villagers

 

      5     ALL(a):[a e m => a e v]

            Split, 1

 

        

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

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

        

         Suppose...

 

            6     barber e m

                  Premise

 

            

             Prove: ~EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            

             Suppose to the contrary...

 

                  7     EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

                        Premise

 

                  8     ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

                        E Spec, 7

 

                  9     ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

                        Split, 8

 

                  10   ALL(a):[a e m => [(barber,a) e s <=> ~(a,a) e s]]

                        Split, 8

 

                  11   barber e m => [(barber,barber) e s <=> ~(barber,barber) e s]

                        U Spec, 10

 

             Obtain the contradiction...

 

                  12   (barber,barber) e s <=> ~(barber,barber) e s

                        Detach, 11, 6

 

         As Required:

 

            13   ~EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

                  4 Conclusion, 7

 

    As Required:

 

      14   barber e m

         => ~EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            4 Conclusion, 6

 

    Obtain the contra-positive

 

      15   ~~EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            Contra, 14

 

    '=>'

   

    As Required:

 

      16   EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            Rem DNeg, 15

 

        

         '<='

        

         Prove: ~barber e m

         => EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

        

         Suppose...

 

            17   ~barber e m

                  Premise

 

         Apply the Cartesian Product Axiom

 

            18   ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

                  Cart Prod

 

            19   ALL(a2):[Set(v) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e v & c2 e a2]]]

                  U Spec, 18

 

            20   Set(v) & Set(v) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e v & c2 e v]]

                  U Spec, 19

 

            21   Set(v) & Set(v)

                  Join, 2, 2

 

            22   EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e v & c2 e v]]

                  Detach, 20, 21

 

            23   Set'(v2) & ALL(c1):ALL(c2):[(c1,c2) e v2 <=> c1 e v & c2 e v]

                  E Spec, 22

 

         Define: v2   (the Cartesian product v*v)

 

            24   Set'(v2)

                  Split, 23

 

            25   ALL(c1):ALL(c2):[(c1,c2) e v2 <=> c1 e v & c2 e v]

                  Split, 23

 

         Apply the Subset Axiom

 

            26   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e v2 & [a=barber & b e m]]]

                  Subset, 24

 

            27   Set'(s) & ALL(a):ALL(b):[(a,b) e s <=> (a,b) e v2 & [a=barber & b e m]]

                  E Spec, 26

 

         Define: s  (a shaving relation such that the barber shaves every man in the village)

 

            28   Set'(s)

                  Split, 27

 

            29   ALL(a):ALL(b):[(a,b) e s <=> (a,b) e v2 & [a=barber & b e m]]

                  Split, 27

 

            

             Prove: ALL(a):[a e m => ~(a,a) e s]

            

             Suppose...

 

                  30   x e m

                        Premise

 

             Apply the definition of s

 

                  31   ALL(b):[(x,b) e s <=> (x,b) e v2 & [x=barber & b e m]]

                        U Spec, 29

 

                  32   (x,x) e s <=> (x,x) e v2 & [x=barber & x e m]

                        U Spec, 31

 

                  33   [(x,x) e s => (x,x) e v2 & [x=barber & x e m]]

                 & [(x,x) e v2 & [x=barber & x e m] => (x,x) e s]

                        Iff-And, 32

 

                  34   (x,x) e s => (x,x) e v2 & [x=barber & x e m]

                        Split, 33

 

                  35   (x,x) e v2 & [x=barber & x e m] => (x,x) e s

                        Split, 33

 

                  36   ~[(x,x) e v2 & [x=barber & x e m]] => ~(x,x) e s

                        Contra, 34

 

                  37   ~~[~(x,x) e v2 | ~[x=barber & x e m]] => ~(x,x) e s

                        DeMorgan, 36

 

             Sufficient: For ~(x,x) e s

 

                  38   ~(x,x) e v2 | ~[x=barber & x e m] => ~(x,x) e s

                        Rem DNeg, 37

 

                

                 Prove: ~[x=barber & x e m]

                

                 Suppose to the contrary...

 

                        39   x=barber & x e m

                              Premise

 

                        40   x=barber

                              Split, 39

 

                        41   x e m

                              Split, 39

 

                        42   barber e m

                              Substitute, 40, 41

 

                 Obtain the contradiction...

 

                        43   barber e m & ~barber e m

                              Join, 42, 17

 

             As Required:

 

                  44   ~[x=barber & x e m]

                        4 Conclusion, 39

 

                  45   ~(x,x) e v2 | ~[x=barber & x e m]

                        Arb Or, 44

 

                  46   ~(x,x) e s

                        Detach, 38, 45

 

         As Required:

 

            47   ALL(a):[a e m => ~(a,a) e s]

                  4 Conclusion, 30

 

            

             Prove: ALL(a):[a e m => (barber,a) e s]

            

             Suppose...

 

                  48   x e m

                        Premise

 

             Apply the definition of s

 

                  49   ALL(b):[(barber,b) e s <=> (barber,b) e v2 & [barber=barber & b e m]]

                        U Spec, 29

 

                  50   (barber,x) e s <=> (barber,x) e v2 & [barber=barber & x e m]

                        U Spec, 49

 

                  51   [(barber,x) e s => (barber,x) e v2 & [barber=barber & x e m]]

                 & [(barber,x) e v2 & [barber=barber & x e m] => (barber,x) e s]

                        Iff-And, 50

 

                  52   (barber,x) e s => (barber,x) e v2 & [barber=barber & x e m]

                        Split, 51

 

             Sufficient: For (barber,x) e s

 

                  53   (barber,x) e v2 & [barber=barber & x e m] => (barber,x) e s

                        Split, 51

 

             Apply the definition of v2

 

                  54   ALL(c2):[(barber,c2) e v2 <=> barber e v & c2 e v]

                        U Spec, 25

 

                  55   (barber,x) e v2 <=> barber e v & x e v

                        U Spec, 54

 

                  56   [(barber,x) e v2 => barber e v & x e v]

                 & [barber e v & x e v => (barber,x) e v2]

                        Iff-And, 55

 

                  57   (barber,x) e v2 => barber e v & x e v

                        Split, 56

 

                  58   barber e v & x e v => (barber,x) e v2

                        Split, 56

 

             Apply the definition of m

 

                  59   x e m => x e v

                        U Spec, 5

 

                  60   x e v

                        Detach, 59, 48

 

                  61   barber e v & x e v

                        Join, 3, 60

 

                  62   (barber,x) e v2

                        Detach, 58, 61

 

                  63   barber=barber

                        Reflex

 

                  64   barber=barber & x e m

                        Join, 63, 48

 

                  65   (barber,x) e v2 & [barber=barber & x e m]

                        Join, 62, 64

 

                  66   (barber,x) e s

                        Detach, 53, 65

 

         As Required:

 

            67   ALL(a):[a e m => (barber,a) e s]

                  4 Conclusion, 48

 

            

             Prove: ALL(a):[a e m => [(barber,a) e s <=> ~(a,a) e s]]

            

             Suppose...

 

                  68   x e m

                        Premise

 

                

                 Prove: (barber,x) e s => ~(x,x) e s

                

                 Suppose...

 

                        69   (barber,x) e s

                              Premise

 

                 Apply previous result

 

                        70   x e m => ~(x,x) e s

                              U Spec, 47

 

                        71   ~(x,x) e s

                              Detach, 70, 68

 

             As Required:

 

                  72   (barber,x) e s => ~(x,x) e s

                        4 Conclusion, 69

 

                

                 Prove: ~(x,x) e s => (barber,x) e s

                

                 Suppose...

 

                        73   ~(x,x) e s

                              Premise

 

                 Apply previous result

 

                        74   x e m => (barber,x) e s

                              U Spec, 67

 

                        75   (barber,x) e s

                              Detach, 74, 68

 

             As Required:

 

                  76   ~(x,x) e s => (barber,x) e s

                        4 Conclusion, 73

 

                  77   [(barber,x) e s => ~(x,x) e s]

                 & [~(x,x) e s => (barber,x) e s]

                        Join, 72, 76

 

                  78   (barber,x) e s <=> ~(x,x) e s

                        Iff-And, 77

 

         As Required:

 

            79   ALL(a):[a e m => [(barber,a) e s <=> ~(a,a) e s]]

                  4 Conclusion, 68

 

            

             Prove: ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

            

             Suppose...

 

                  80   (x,y) e s

                        Premise

 

             Apply definition of s

 

                  81   ALL(b):[(x,b) e s <=> (x,b) e v2 & [x=barber & b e m]]

                        U Spec, 29

 

                  82   (x,y) e s <=> (x,y) e v2 & [x=barber & y e m]

                        U Spec, 81

 

                  83   [(x,y) e s => (x,y) e v2 & [x=barber & y e m]]

                 & [(x,y) e v2 & [x=barber & y e m] => (x,y) e s]

                        Iff-And, 82

 

                  84   (x,y) e s => (x,y) e v2 & [x=barber & y e m]

                        Split, 83

 

                  85   (x,y) e v2 & [x=barber & y e m] => (x,y) e s

                        Split, 83

 

                  86   (x,y) e v2 & [x=barber & y e m]

                        Detach, 84, 80

 

                  87   (x,y) e v2

                        Split, 86

 

                  88   x=barber & y e m

                        Split, 86

 

             Apply definition of v2

 

                  89   ALL(c2):[(x,c2) e v2 <=> x e v & c2 e v]

                        U Spec, 25

 

                  90   (x,y) e v2 <=> x e v & y e v

                        U Spec, 89

 

                  91   [(x,y) e v2 => x e v & y e v]

                 & [x e v & y e v => (x,y) e v2]

                        Iff-And, 90

 

                  92   (x,y) e v2 => x e v & y e v

                        Split, 91

 

                  93   x e v & y e v => (x,y) e v2

                        Split, 91

 

                  94   x e v & y e v

                        Detach, 92, 87

 

         As Required:

 

            95   ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

                  4 Conclusion, 80

 

         Joining results...

 

            96   ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

                  Join, 95, 79

 

    '<='

   

    As Required:

 

      97   ~barber e m

         => EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            4 Conclusion, 17

 

    Joining results...

 

      98   [EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

         & [~barber e m

         => EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

            Join, 16, 97

 

    Apply Iff-And Rule

 

      99   EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

         <=> ~barber e m

            Iff-And, 98

 

As Required:

 

100  ALL(v):ALL(barber):ALL(m):[Set(v)

    & barber e v

    & Set(m)

    & ALL(a):[a e m => a e v]

    => [EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]

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

    <=> ~barber e m]]

      4 Conclusion, 1