Introduction

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

Here is a non-paradoxical variation of the Barber Paradox. If

the barber is a member of a set of men (e.g. those living in a

a town or village), then there DOES exist a relation 'shaves'

defined on that set of men such that, (a) the barber shaves

himself, and (b) for every man in that set, if he is not the

barber, then the barber shaves him if and only if he does

not shave himself. Such a relation is one that has the barber

shaving every man including himself. (Another possibility,

not shown here, is that every man shaves himself.)

Proof

-----

Suppose...

1     Set(men) & barber e men

Premise

2     Set(men)

Split, 1

3     barber e men

Split, 1

Apply Cartesian Product rule

4     ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) eb

<=> c1 e a1 & c2 e a2]]]

Cart Prod

5     ALL(a2):[Set(men) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b

<=> c1 e men & c2 e a2]]]

U Spec, 4

6     Set(men) & Set(men) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b

<=> c1 e men & c2 e men]]

U Spec, 5

7     Set(men) & Set(men)

Join, 2, 2

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

Detach, 6, 7

9     Set'(men2) & ALL(c1):ALL(c2):[(c1,c2) e men2 <=> c1 e men & c2 e men]

E Spec, 8

Define: men2  (the set ordered pairs of men)

10    Set'(men2)

Split, 9

11    ALL(c1):ALL(c2):[(c1,c2) e men2 <=> c1 e men & c2 e men]

Split, 9

Apply Subset rule

12    EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e men2 & a=barber]]

Subset, 10

13    Set'(shaves) & ALL(a):ALL(b):[(a,b) e shaves <=> (a,b) e men2 & a=barber]

E Spec, 12

Define: shaves

14    Set'(shaves)

Split, 13

15    ALL(a):ALL(b):[(a,b) e shaves <=> (a,b) e men2 & a=barber]

Split, 13

Prove: (barber,barber) e shaves

Apply def of shaves

16    ALL(b):[(barber,b) e shaves <=> (barber,b) e men2 & barber=barber]

U Spec, 15

17    (barber,barber) e shaves <=> (barber,barber) e men2 & barber=barber

U Spec, 16

18    [(barber,barber) e shaves => (barber,barber) e men2 & barber=barber]

& [(barber,barber) e men2 & barber=barber => (barber,barber) e shaves]

Iff-And, 17

19    (barber,barber) e shaves => (barber,barber) e men2 & barber=barber

Split, 18

Sufficient: For (barber,barber) e shaves

20    (barber,barber) e men2 & barber=barber => (barber,barber) e shaves

Split, 18

Apply def of men2

21    ALL(c2):[(barber,c2) e men2 <=> barber e men & c2 e men]

U Spec, 11

22    (barber,barber) e men2 <=> barber e men & barber e men

U Spec, 21

23    [(barber,barber) e men2 => barber e men & barber e men]

& [barber e men & barber e men => (barber,barber) e men2]

Iff-And, 22

24    (barber,barber) e men2 => barber e men & barber e men

Split, 23

Sufficient: (barber,barber) e men2

25    barber e men & barber e men => (barber,barber) e men2

Split, 23

26    barber e men & barber e men

Join, 3, 3

27    (barber,barber) e men2

Detach, 25, 26

28    barber=barber

Reflex

29    (barber,barber) e men2 & barber=barber

Join, 27, 28

As Required:

30    (barber,barber) e shaves

Detach, 20, 29

Prove:

ALL(a):[a e men

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

Suppose...

31    x e men

Premise

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

Suppose...

32    ~x=barber

Premise

'=>'

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

Suppose...

33    (barber,x) e shaves

Premise

Prove: ~(x,x) e shaves

Apply def of shaves

34    ALL(b):[(x,b) e shaves <=> (x,b) e men2 & x=barber]

U Spec, 15

35    (x,x) e shaves <=> (x,x) e men2 & x=barber

U Spec, 34

36    [(x,x) e shaves => (x,x) e men2 & x=barber]

& [(x,x) e men2 & x=barber => (x,x) e shaves]

Iff-And, 35

37    (x,x) e shaves => (x,x) e men2 & x=barber

Split, 36

38    (x,x) e men2 & x=barber => (x,x) e shaves

Split, 36

39    ~[(x,x) e men2 & x=barber] => ~(x,x) e shaves

Contra, 37

40    ~~[~(x,x) e men2 | ~x=barber] => ~(x,x) e shaves

DeMorgan, 39

Sufficient: For ~(x,x) e shaves

41    ~(x,x) e men2 | ~x=barber => ~(x,x) e shaves

Rem DNeg, 40

42    ~(x,x) e men2 | ~x=barber

Arb Or, 32

As Required:

43    ~(x,x) e shaves

Detach, 41, 42

'=>'

As Required:

44    (barber,x) e shaves => ~(x,x) e shaves

4 Conclusion, 33

'<='

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

Suppose...

45    ~(x,x) e shaves

Premise

Prove: (barber,x) e shaves

Apply def of shaves

46    ALL(b):[(barber,b) e shaves <=> (barber,b) e men2 & barber=barber]

U Spec, 15

47    (barber,x) e shaves <=> (barber,x) e men2 & barber=barber

U Spec, 46

48    [(barber,x) e shaves => (barber,x) e men2 & barber=barber]

& [(barber,x) e men2 & barber=barber => (barber,x) e shaves]

Iff-And, 47

49    (barber,x) e shaves => (barber,x) e men2 & barber=barber

Split, 48

Sufficient: (barber,x) e shaves

50    (barber,x) e men2 & barber=barber => (barber,x) e shaves

Split, 48

Prove: (barber,x) e men2

Apply def of men2

51    ALL(c2):[(barber,c2) e men2 <=> barber e men & c2 e men]

U Spec, 11

52    (barber,x) e men2 <=> barber e men & x e men

U Spec, 51

53    [(barber,x) e men2 => barber e men & x e men]

& [barber e men & x e men => (barber,x) e men2]

Iff-And, 52

54    (barber,x) e men2 => barber e men & x e men

Split, 53

55    barber e men & x e men => (barber,x) e men2

Split, 53

56    barber e men & x e men

Join, 3, 31

As Required:

57    (barber,x) e men2

Detach, 55, 56

58    barber=barber

Reflex

59    (barber,x) e men2 & barber=barber

Join, 57, 58

60    (barber,x) e shaves

Detach, 50, 59

'<='

As Required:

61    ~(x,x) e shaves => (barber,x) e shaves

4 Conclusion, 45

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

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

Join, 44, 61

63    (barber,x) e shaves <=> ~(x,x) e shaves

Iff-And, 62

As Required:

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

4 Conclusion, 32

As Required:

65    ALL(a):[a e men

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

4 Conclusion, 31

66    (barber,barber) e shaves

& ALL(a):[a e men

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

Join, 30, 65

As Required:

67    ALL(men):ALL(barber):[Set(men) & barber e men

=> EXIST(shaves):[(barber,barber) e shaves

& ALL(a):[a e men

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

4 Conclusion, 1