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