SMULLYAN'S DRINKER PRINCIPLE
****************************
"[T]here exists someone such that whenever he (or she) drinks, everybody drinks. It comes ultimately from the strange principle that a false proposition implies any proposition. [i.e. the principle of vacuous truth]."
Smullyan's Informal Proof
-------------------------
"Either it is true that everybody drinks or it isn't. Suppose it is true that everybody drinks. Then take any person--call him Jim. Since everybody drinks and Jim drinks, then it is true that if Jim drinks then everybody drinks. So, there is at least one person namely Jim-such that if he drinks then everybody drinks.
"Suppose, however, that it is not true that everybody drinks; what then? Well, in that case there is at least one person-call him Jim-who doesn't drink. Since it is false that Jim drinks, then it is true that if Jim drinks, everybody drinks. So again there is a person--namely Jim--such that if he drinks, everybody drinks."
--"What is the name of this book?" pp. 209-210
Formal Theorem (in DC Proof)
----------------------------
EXIST(a):U(a) => EXIST(a):[U(a) & [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
Where U is an arbitrary unary predicate analagous to the implicit domain of discourse in First-Order Predicate Logic.
The following machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com
By Dan Christensen
2021-11-14
The non-empty domain of discourse analagous to the implicit domain of discourse in First-Order Predicate Logic.
1 EXIST(a):U(a)
Premise
"Either it is true that everybody drinks or it isn't." (Two cases to consider)
2 ALL(b):[U(b) => Drinker(b)] | ~ALL(b):[U(b) => Drinker(b)]
Or Not
"Suppose it is true that everybody drinks." (Case 1)
3 ALL(b):[U(b) => Drinker(b)]
Premise
"Then take any person--call him Jim."
4 U(jim)
E Spec, 1
"Since everybody drinks and Jim drinks..."
5 U(jim) => Drinker(jim)
U Spec, 3
6 Drinker(jim)
Detach, 5, 4
"If Jim drinks then everybody drinks."
7 Drinker(jim)
Premise
8 ALL(b):[U(b) => Drinker(b)]
Copy, 3
9 Drinker(jim) => ALL(b):[U(b) => Drinker(b)]
4 Conclusion, 7
"So there is at least one person, namely Jim, such that if he drinks then everybody drinks."
10 U(jim)
& [Drinker(jim) => ALL(b):[U(b) => Drinker(b)]]
Join, 4, 9
Case 1
As Required:
11 ALL(b):[U(b) => Drinker(b)]
=> EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
4 Conclusion, 3
"Suppose, however, that it is not true that everybody drinks"
12 ~ALL(b):[U(b) => Drinker(b)]
Premise
13 ~~EXIST(b):~[U(b) => Drinker(b)]
Quant, 12
14 EXIST(b):~[U(b) => Drinker(b)]
Rem DNeg, 13
15 EXIST(b):~~[U(b) & ~Drinker(b)]
Imply-And, 14
16 EXIST(b):[U(b) & ~Drinker(b)]
Rem DNeg, 15
"In that case there is at least one person--call him Jim--who doesn't drink."
17 U(jim) & ~Drinker(jim)
E Spec, 16
18 U(jim)
Split, 17
19 ~Drinker(jim)
Split, 17
Since it is false that Jim drinks, then it is [vacuously] true that if Jim drinks,
everybody drinks.
20 Drinker(jim)
Premise
21 ~Drinker(jim) => ALL(b):[U(b) => Drinker(b)]
Arb Cons, 20
Vacuously true:
22 ALL(b):[U(b) => Drinker(b)]
Detach, 21, 19
[T]here is a person--namely Jim--such that if he drinks, everybody drinks."
23 Drinker(jim) => ALL(b):[U(b) => Drinker(b)]
4 Conclusion, 20
"So again there is a person--namely Jim--such that if he drinks, everybody drinks."
24 U(jim)
& [Drinker(jim) => ALL(b):[U(b) => Drinker(b)]]
Join, 18, 23
Case 2
As Required:
25 ~ALL(b):[U(b) => Drinker(b)]
=> EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
4 Conclusion, 12
Joining results...
26 [ALL(b):[U(b) => Drinker(b)]
=> EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]]
& [~ALL(b):[U(b) => Drinker(b)]
=> EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]]
Join, 11, 25
By cases, we have:
27 EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
Cases, 2, 26
As Required:
28 EXIST(a):U(a)
=> EXIST(a):[U(a)
& [Drinker(a) => ALL(b):[U(b) => Drinker(b)]]]
4 Conclusion, 1