THEOREM Dual of Smullyan's
Drinkers' Principle
*******
EXIST(a):U(a)=> EXIST(a):[U(a)&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]
"There is someone such that if anybody at all drinks, then
he does, too."
"[Two cases to consider:] either there is at least one
person who drinks or there isn't.
"If there isn't [case 2 here],then
take any person-call him Jim. Since it is false that someone drinks, then it is
true that if someone drinks then Jim drinks.
"On the other hand, if there is someone who drinks [case 1
here], then take any person who drinks--call him Jim.
"Then it is true that someone drinks and it is true that
Jim drinks, hence it is true that if someone drinks then Jim drinks."
--R. Smullyan, "What is the name
of this book?" p.211
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof.com
Dan Christensen
2023-05-05
PROOF
*****
Suppose...
1 EXIST(a):U(a)
Premise
Two cases:
"Either there is at least one person who drinks or there
isn't."
2 EXIST(b):[U(b) &
Drinker(b)] | ~EXIST(b):[U(b) & Drinker(b)]
Or Not
Case 1: "There is someone who drinks"
Prove: EXIST(b):[U(b) &
Drinker(b)]
=> EXIST(a):[U(a) & [EXIST(b):[U(b) & Drinker(b)] =>
Drinker(a)]]
Suppose...
3 EXIST(b):[U(b) &
Drinker(b)]
Premise
"Take any person who drinks--call him Jim"
4 U(jim) & Drinker(jim)
E Spec, 3
5 U(jim)
Split, 4
6 Drinker(jim)
Split, 4
"Then it is true that someone drinks and it is true
that Jim
drinks, hence it is true that if
someone drinks then Jim
drinks."
7 EXIST(b):[U(b) &
Drinker(b)] => Drinker(jim)
Arb Ante, 6
8 U(jim)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(jim)]
Join, 5, 7
Case 1
As Required:
9 EXIST(b):[U(b) &
Drinker(b)]
=>
EXIST(a):[U(a)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]
4 Conclusion, 3
Case 2
Prove: ~EXIST(b):[U(b) &
Drinker(b)]
=> EXIST(a):[U(a) & [EXIST(b):[U(b) & Drinker(b)] =>
Drinker(a)]]
Suppose nobody is a drinker
10 ~EXIST(b):[U(b) & Drinker(b)]
Premise
"Take any person--call him Jim."
11 U(jim)
E Spec, 1
"Since it is false that someone drinks, then it is true
that if someone drinks then
Jim drinks. "
12 ~~ALL(b):~[U(b) & Drinker(b)]
Quant, 10
13 ALL(b):~[U(b) & Drinker(b)]
Rem DNeg, 12
14 ALL(b):~~[U(b) => ~Drinker(b)]
Imply-And, 13
15 ALL(b):[U(b) => ~Drinker(b)]
Rem DNeg, 14
16 U(jim) =>
~Drinker(jim)
U Spec, 15
17 ~Drinker(jim)
Detach, 16, 11
Prove: EXIST(b):[U(b) &
Drinker(b)] => Drinker(jim)
Suppose...
18 EXIST(b):[U(b) & Drinker(b)]
Premise
19 ~EXIST(b):[U(b) & Drinker(b)] =>
Drinker(jim)
Arb Cons, 18
Vacuously true:
20 Drinker(jim)
Detach, 19, 10
As Required:
21 EXIST(b):[U(b) & Drinker(b)] =>
Drinker(jim)
4 Conclusion, 18
22 U(jim)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(jim)]
Join, 11, 21
Case 2
As Required:
23 ~EXIST(b):[U(b) & Drinker(b)]
=>
EXIST(a):[U(a)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]
4 Conclusion, 10
24 [EXIST(b):[U(b) & Drinker(b)]
=>
EXIST(a):[U(a)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]]
&
[~EXIST(b):[U(b) & Drinker(b)]
=>
EXIST(a):[U(a)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]]
Join, 9, 23
Apply Cases Rule
25 EXIST(a):[U(a)
&
[EXIST(b):[U(b) & Drinker(b)] => Drinker(a)]]
Cases, 2, 24
As Required:
26 EXIST(a):U(a) => EXIST(a):[U(a) & [EXIST(b):[U(b) &
Drinker(b)] => Drinker(a)]]
4 Conclusion, 1