INTRODUCTION
************
Russell's original Barber scenario:
barber e men & ALL(a):[a e men => [(barber,a) e shaves <=> ~(a,a) e shaves]]
where
men is the set of men in town
barber is a man in town
(x,y) e shaves mean x shaves y
This leads to the well known contradiction: (barber,barber) e shaves <=> ~(barber,barber) e shaves
Therefore, we have:
~[barber e men & ALL(a):[a e men => [(barber,a) e shaves <=> ~(a,a) e shaves]]]
The multiple barber scenario:
ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
where
barbers is a subset of men
Here, we establish that
ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
<=> ALL(a):[a e barbers => ~(a,a) e shaves]
i.e. the barbers cannot shave themselves, but they must shave each other
We make the following assumptions about the sets of men, barbers and shaves:
1. barbers is a subset of men.
2. If a man shaves, a unique man in the village (possible he himself) shaves him.
3. If a man does not shave himself, then a barber will shave him.
Note that we will obtain a contradiction if, as in the original scenario, there is only one barber.
(This proof was written with the aid the authors DC Proof 2.0 software available free at http://www.dcproof.com )
AXIOMS
******
men is a set
1 Set(men)
Axiom
barbers is a set
2 Set(barbers)
Axiom
barbers is a subset of men
3 ALL(a):[a e barbers => a e men]
Axiom
shaves is a set of ordered pairs of men
4 Set'(shaves)
Axiom
5 ALL(a):ALL(b):[(a,b) e shaves => a e men & b e men]
Axiom
If a man does not shave himself, then there exists a barber who will shave him.
6 ALL(a):[a e men => [~(a,a) e shaves => EXIST(b):[b e barbers & (b,a) e shaves]]]
Axiom
Uniqueness of shavers
7 ALL(a):ALL(b):ALL(c):[a e men & b e men & c e men => [(a,b) e shaves & (c,b) e shaves => a=c]]
Axiom
PROOF
*****
'=>'
Prove: ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]
Suppose...
8 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
Premise
Prove: ALL(a):[a e barbers => ~(a,a) e shaves]
Suppose...
9 x e barbers
Premise
Prove: ~(x,x) e shaves
Supose to the contrary...
10 (x,x) e shaves
Premise
11 x e men => [EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves]
U Spec, 8
12 x e barbers => x e men
U Spec, 3
13 x e men
Detach, 12, 9
14 EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves
Detach, 11, 13
15 x e barbers & (x,x) e shaves
Join, 9, 10
16 EXIST(b):[b e barbers & (b,x) e shaves]
E Gen, 15
17 ~(x,x) e shaves
Detach, 14, 16
18 (x,x) e shaves & ~(x,x) e shaves
Join, 10, 17
As Required:
19 ~(x,x) e shaves
4 Conclusion, 10
As Required:
20 ALL(a):[a e barbers => ~(a,a) e shaves]
4 Conclusion, 9
As Required:
21 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]
4 Conclusion, 8
'<='
Prove: ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
Suppose...
22 ALL(a):[a e barbers => ~(a,a) e shaves]
Premise
Prove: ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
=> ~(a,a) e shaves]]
Suppose...
23 x e men
Premise
'=>'
Prove: EXIST(b):[b e barbers & (b,x) e shaves]
=> ~(x,x) e shaves
Suppose...
24 EXIST(b):[b e barbers & (b,x) e shaves]
Premise
25 y e barbers & (y,x) e shaves
E Spec, 24
26 y e barbers
Split, 25
27 (y,x) e shaves
Split, 25
Two cases:
28 x=y | ~x=y
Or Not
Case 1
Prove: x=y => ~(x,x) e shaves
Suppose...
29 x=y
Premise
30 x e barbers => ~(x,x) e shaves
U Spec, 22
31 x e barbers
Substitute, 29, 26
32 ~(x,x) e shaves
Detach, 30, 31
As Required:
33 x=y => ~(x,x) e shaves
4 Conclusion, 29
Case 2
Prove: ~x=y => ~(x,x) e shaves
Suppose...
34 ~x=y
Premise
35 ALL(b):ALL(c):[x e men & b e men & c e men => [(x,b) e shaves & (c,b) e shaves => x=c]]
U Spec, 7
36 ALL(c):[x e men & x e men & c e men => [(x,x) e shaves & (c,x) e shaves => x=c]]
U Spec, 35
37 x e men & x e men & y e men => [(x,x) e shaves & (y,x) e shaves => x=y]
U Spec, 36
38 ALL(b):[(y,b) e shaves => y e men & b e men]
U Spec, 5
39 (y,x) e shaves => y e men & x e men
U Spec, 38
40 y e men & x e men
Detach, 39, 27
41 y e men
Split, 40
42 x e men
Split, 40
43 x e men & x e men
Join, 42, 42
44 x e men & x e men & y e men
Join, 43, 41
45 (x,x) e shaves & (y,x) e shaves => x=y
Detach, 37, 44
46 ~x=y => ~[(x,x) e shaves & (y,x) e shaves]
Contra, 45
47 ~[(x,x) e shaves & (y,x) e shaves]
Detach, 46, 34
48 ~~[(x,x) e shaves => ~(y,x) e shaves]
Imply-And, 47
49 (x,x) e shaves => ~(y,x) e shaves
Rem DNeg, 48
50 ~~(y,x) e shaves => ~(x,x) e shaves
Contra, 49
51 (y,x) e shaves => ~(x,x) e shaves
Rem DNeg, 50
52 ~(x,x) e shaves
Detach, 51, 27
As Required:
53 ~x=y => ~(x,x) e shaves
4 Conclusion, 34
54 [x=y => ~(x,x) e shaves] & [~x=y => ~(x,x) e shaves]
Join, 33, 53
55 ~(x,x) e shaves
Cases, 28, 54
As Required:
56 EXIST(b):[b e barbers & (b,x) e shaves]
=> ~(x,x) e shaves
4 Conclusion, 24
As Required:
57 ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
=> ~(a,a) e shaves]]
4 Conclusion, 23
As Required:
58 ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
=> ~(a,a) e shaves]]
4 Conclusion, 22
59 [ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]]
& [ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
=> ~(a,a) e shaves]]]
Join, 21, 58
As Required:
60 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
<=> ALL(a):[a e barbers => ~(a,a) e shaves]
Iff-And, 59
'=>'
Prove: ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]
Suppose...
61 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
Premise
Prove: ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
Suppose...
62 x e men
Premise
Apply premise
63 x e men => [EXIST(b):[b e barbers & (b,x) e shaves] <=> ~(x,x) e shaves]
U Spec, 61
64 EXIST(b):[b e barbers & (b,x) e shaves] <=> ~(x,x) e shaves
Detach, 63, 62
65 [EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves]
& [~(x,x) e shaves => EXIST(b):[b e barbers & (b,x) e shaves]]
Iff-And, 64
66 EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves
Split, 65
As Required:
67 ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
4 Conclusion, 62
68 ALL(a):[a e barbers => ~(a,a) e shaves]
Detach, 21, 67
'=>'
As Required:
69 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]
4 Conclusion, 61
'<='
Prove: ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
Suppose...
70 ALL(a):[a e barbers => ~(a,a) e shaves]
Premise
Prove: ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
Suppose...
71 x e men
Premise
Apply previous result
72 [ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]] => ALL(a):[a e barbers => ~(a,a) e shaves]]
& [ALL(a):[a e barbers => ~(a,a) e shaves] => ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]]
Iff-And, 60
73 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]] => ALL(a):[a e barbers => ~(a,a) e shaves]
Split, 72
74 ALL(a):[a e barbers => ~(a,a) e shaves] => ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
Split, 72
75 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] => ~(a,a) e shaves]]
Detach, 74, 70
76 x e men => [EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves]
U Spec, 75
77 EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves
Detach, 76, 71
Apply axiom
78 x e men => [~(x,x) e shaves => EXIST(b):[b e barbers & (b,x) e shaves]]
U Spec, 6
79 ~(x,x) e shaves => EXIST(b):[b e barbers & (b,x) e shaves]
Detach, 78, 71
80 [EXIST(b):[b e barbers & (b,x) e shaves] => ~(x,x) e shaves]
& [~(x,x) e shaves => EXIST(b):[b e barbers & (b,x) e shaves]]
Join, 77, 79
81 EXIST(b):[b e barbers & (b,x) e shaves]
<=> ~(x,x) e shaves
Iff-And, 80
As Required:
82 ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
<=> ~(a,a) e shaves]]
4 Conclusion, 71
As Required:
83 ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
<=> ~(a,a) e shaves]]
4 Conclusion, 70
84 [ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
=> ALL(a):[a e barbers => ~(a,a) e shaves]]
& [ALL(a):[a e barbers => ~(a,a) e shaves]
=> ALL(a):[a e men
=> [EXIST(b):[b e barbers & (b,a) e shaves]
<=> ~(a,a) e shaves]]]
Join, 69, 83
85 ALL(a):[a e men => [EXIST(b):[b e barbers & (b,a) e shaves] <=> ~(a,a) e shaves]]
<=> ALL(a):[a e barbers => ~(a,a) e shaves]
Iff-And, 84