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
=> EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):[a e pub & 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
*****
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 pub & 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
Joining results...
16 x e pub & x e drinkers
Join, 3, 15
Generalizing...
As Required:
17 EXIST(a):[a e pub & a e drinkers]
E Gen, 16
Prove: ~ALL(a):[a e pub => a e drinkers]
Prove: ~y e drinkers
Apply definition of drinkers
18 y e drinkers <=> y e pub & ~y=y
U Spec, 9
19 [y e drinkers => y e pub & ~y=y]
& [y e pub & ~y=y => y e drinkers]
Iff-And, 18
20 y e drinkers => y e pub & ~y=y
Split, 19
21 y e pub & ~y=y => y e drinkers
Split, 19
22 ~[y e pub & ~y=y] => ~y e drinkers
Contra, 20
23 ~~[~y e pub | ~~y=y] => ~y e drinkers
DeMorgan, 22
24 ~y e pub | ~~y=y => ~y e drinkers
Rem DNeg, 23
Sufficient: For ~y e drinkers
25 ~y e pub | y=y => ~y e drinkers
Rem DNeg, 24
26 y=y
Reflex
27 ~y e pub | y=y
Arb Or, 26
As Required:
28 ~y e drinkers
Detach, 25, 27
Joining results...
29 y e pub & ~y e drinkers
Join, 4, 28
Generalizing...
As Required:
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
As Required:
34 ~ALL(a):[a e pub => a e drinkers]
Rem DNeg, 33
Combine results
35 EXIST(a):[a e pub & a e drinkers]
& ~ALL(a):[a e pub => a e drinkers]
Join, 17, 34
36 ~[EXIST(a):[a e pub & a e drinkers] => ~~ALL(a):[a e pub => a e drinkers]]
Imply-And, 35
As Required:
37 ~[EXIST(a):[a e pub & 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
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
Joining results...
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 pub & a e drinkers] => ALL(a):[a e pub => a e drinkers]]
Join, 46, 37
48 EXIST(drinkers):[Set(drinkers) & ALL(a):[a e drinkers => a e pub]
& ~[EXIST(a):[a e pub & 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 pub & a e drinkers] => ALL(a):[a e pub => a e drinkers]]]]
4 Conclusion, 1