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