THEOREM
*******
A "non-paradoxical" version of the Drinker's Theorem
****************************************************
ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~ALL(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
=> [EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
where:
pub = set of people in a pub
drinkers = subset of pub that are drinking
This proof was written with the aid of the author's DC Proof 2.0 software
available at http://www.dcproof.com
PROOF
*****
Prove: ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Suppose...
1 Set(pub) & x e pub & y e pub & ~x=y
Premise
pub is the set of people in the a pub
2 Set(pub)
Split, 1
x is a person in the pub
3 x e pub
Split, 1
y is a person in the pub
4 y e pub
Split, 1
x and y are distinct
5 ~x=y
Split, 1
Prove: EXIST(a):[a e drinkers]
Construct the subset drinkers (excluding only y)
Apply Subset Axiom
6 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pub & ~a=y]]
Subset, 2
7 Set(drinkers) & ALL(a):[a e drinkers <=> a e pub & ~a=y]
E Spec, 6
Define: drinkers (the set of drinkers in the pub -- excludes only y)
8 Set(drinkers)
Split, 7
Only y is not a drinker
9 ALL(a):[a e drinkers <=> a e pub & ~a=y]
Split, 7
Prove: x e drinkers
Apply definition of drinkers
10 x e drinkers <=> x e pub & ~x=y
U Spec, 9
11 [x e drinkers => x e pub & ~x=y]
& [x e pub & ~x=y => x e drinkers]
Iff-And, 10
12 x e drinkers => x e pub & ~x=y
Split, 11
Sufficient: For x e drinkers
13 x e pub & ~x=y => x e drinkers
Split, 11
14 x e pub & ~x=y
Join, 3, 5
As Required:
15 x e drinkers
Detach, 13, 14
As Required:
16 EXIST(a):a e drinkers
E Gen, 15
Prove: ~y e drinkers
Apply definition of drinkers
17 y e drinkers <=> y e pub & ~y=y
U Spec, 9
18 [y e drinkers => y e pub & ~y=y]
& [y e pub & ~y=y => y e drinkers]
Iff-And, 17
19 y e drinkers => y e pub & ~y=y
Split, 18
20 y e pub & ~y=y => y e drinkers
Split, 18
21 ~[y e pub & ~y=y] => ~y e drinkers
Contra, 19
Prove: ~[y e pub & ~y=y]
Suppose to the contrary...
22 y e pub & ~y=y
Premise
23 y e pub
Split, 22
24 ~y=y
Split, 22
25 y=y
Reflex
26 y=y & ~y=y
Join, 25, 24
As Required:
27 ~[y e pub & ~y=y]
4 Conclusion, 22
28 ~y e drinkers
Detach, 21, 27
29 y e pub & ~y e drinkers
Join, 4, 28
30 EXIST(a):[a e pub & ~a e drinkers]
E Gen, 29
31 ~ALL(a):~[a e pub & ~a e drinkers]
Quant, 30
32 ~ALL(a):~~[a e pub => ~~a e drinkers]
Imply-And, 31
33 ~ALL(a):[a e pub => ~~a e drinkers]
Rem DNeg, 32
34 ~ALL(a):[a e pub => a e drinkers]
Rem DNeg, 33
35 EXIST(a):a e drinkers
& ~ALL(a):[a e pub => a e drinkers]
Join, 16, 34
36 ~[EXIST(a):a e drinkers => ~~ALL(a):[a e pub => a e drinkers]]
Imply-And, 35
37 ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]
Rem DNeg, 36
Prove: ALL(a):[a e drinkers => a e pub]
Suppose...
38 m e drinkers
Premise
Apply definition of drinkers
39 m e drinkers <=> m e pub & ~m=y
U Spec, 9
40 [m e drinkers => m e pub & ~m=y]
& [m e pub & ~m=y => m e drinkers]
Iff-And, 39
41 m e drinkers => m e pub & ~m=y
Split, 40
42 m e pub & ~m=y => m e drinkers
Split, 40
43 m e pub & ~m=y
Detach, 41, 38
44 m e pub
Split, 43
As Required:
45 ALL(a):[a e drinkers => a e pub]
4 Conclusion, 38
46 Set(drinkers) & ALL(a):[a e drinkers => a e pub]
Join, 8, 45
47 Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]
Join, 46, 37
Generalizing...
48 EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]
E Gen, 47
As Required:
49 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
4 Conclusion, 1
Switch quantifiers
50 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~ALL(drinkers):~[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Quant, 49
51 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~ALL(drinkers):~~[Set(drinkers) & ALL(a):[a e drinkers => a e pub] => ~~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Imply-And, 50
52 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~ALL(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub] => ~~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Rem DNeg, 51
As Required:
53 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~ALL(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub] => [EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Rem DNeg, 52
54 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> ~~EXIST(drinkers):~[Set(drinkers) & ALL(a):[a e drinkers => a e pub] => [EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Quant, 53
55 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):~[Set(drinkers) & ALL(a):[a e drinkers => a e pub] => [EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Rem DNeg, 54
56 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):~~[Set(drinkers) & ALL(a):[a e drinkers => a e pub] & ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Imply-And, 55
57 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub] & ~[EXIST(a):a e drinkers => ALL(a):[a e pub => a e drinkers]]]]
Rem DNeg, 56
58 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub] & ~~[EXIST(a):a e drinkers & ~ALL(a):[a e pub => a e drinkers]]]]
Imply-And, 57
Or equivalently...
59 ALL(pub):ALL(x):ALL(y):[Set(pub) & x e pub & y e pub & ~x=y
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub] & [EXIST(a):a e drinkers & ~ALL(a):[a e pub => a e drinkers]]]]
Rem DNeg, 58