Drinker paradox
The drinker paradox (also known as drinker's principle or (the) drinking principle) is a theorem of classical predicate logic, usually stated in natural language as: There is someone in the pub such that, if he is drinking, everyone in the pub is drinking. The actual theorem is
where D is an arbitrary predicate and P is an arbitrary set. The paradox was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his 1978 book What Is the Name of this Book?[1]
Proofs
The proof begins by recognizing it is true that either everyone in the pub is drinking, or at least one person in the pub is not drinking. Consequently, there are two cases to consider:[1][2]
- Suppose everyone is drinking. For any particular person, it cannot be wrong to say that if that particular person is drinking, then everyone in the pub is drinking — because everyone is drinking. Because everyone is drinking, then that one person must drink because when ' that person ' drinks ' everybody ' drinks, everybody includes that person.[1][2]
- Suppose that at least one person is not drinking. For any particular nondrinking person, it still cannot be wrong to say that if that particular person is drinking, then everyone in the pub is drinking — because that person is, in fact, not drinking. In this case the condition is false, so the statement is vacuously true due to the nature of material implication in formal logic, which states that "If P, then Q" is always true if P (the condition or antecedent) is false.[1][2]
Either way, there is someone in the pub such that, if he is drinking, everyone in the pub is drinking. A slightly more formal way of expressing the above is to say that, if everybody drinks, then anyone can be the witness for the validity of the theorem. And if someone does not drink, then that particular non-drinking individual can be the witness to the theorem's validity.[3]
The proof above is essentially model-theoretic (can be formalized as such). A purely syntactic proof is possible and can even be mechanized (in Otter for example), but only for an equisatisfiable rather than an equivalent negation of the theorem.[4] Namely, the negation of the theorem is
which is equivalent with the prenex normal form
By Skolemization the above is equisatisfiable with
The resolution of the two clauses and results in an empty set of clauses (i.e. a contradiction), thus proving the negation of the theorem is unsatisfiable. The resolution is slightly non-straightforward because it involves a search based on Herbrand's theorem for ground instances that are propositionally unsatisfiable. The bound variable x is first instantiated with a constant d (making use of the assumption that the domain is non-empty), resulting in the Herbrand universe:[5]
One can sketch the following natural deduction:[4]
Or spelled out:
- Instantiating x with d yields which implies
- x is then instantiated with f(d) yielding which implies .
Observe that and unify syntactically in their predicate arguments. An (automated) search thus finishes in two steps:[5]
The proof by resolution given here uses the law of excluded middle, the axiom of choice, and non-emptiness of the domain as premises.[4]
Explanation of paradoxality
The paradox is ultimately based on the principle of formal logic that the statement is true whenever A is false, i.e., any statement follows from a false statement[1] (ex falso quodlibet).
What important to the paradox is that the conditional in classical (and intuitionistic) logic is the material conditional. It has the property that is true if B is true or if A is false (in classical logic, but not intuitionistic logic, this is also a necessary condition).
So as it was applied here, the statement "if he is drinking, everyone is drinking" was taken to be correct in one case, if everyone was drinking, and in the other case, if he was not drinking — even though his drinking may not have had anything to do with anyone else's drinking.
On the other hand, in natural language, typically "if...then..." is used as an indicative conditional.
History and variations
Smullyan in his 1978 book attributes the naming of "The Drinking Principle" to his graduate students.[1] He also discusses variants (obtained by replacing D with other, more dramatic predicates):
- "there is a woman on earth such that if she becomes sterile, the whole human race will die out." Smullyan writes that this formulation emerged from a conversation he had with philosopher John Bacon.[1]
- A "dual" version of the Principle: "there is at least one person such that if anybody drinks, then he does."[1]
As "Smullyan's ‘Drinkers’ principle" or just "Drinkers' principle" it appears in H.P. Barendregt's "The quest for correctness" (1996), accompanied by some machine proofs.[2] Since then it has made regular appearance as an example in publications about automated reasoning; it is sometimes used to contrast the expressiveness of proof assistants.[4][5][6]
Non-empty domain
The paradox implicitly assumes there was someone in the pub. The assumption that the domain is non-empty is built into the inference rules of classical predicate logic.[7] We can deduce from , but of course if the domain were empty (in this case, if there were nobody in the pub), the proposition is not well-formed for any closed expression .
In the setting with empty domains allowed, the drinker paradox must be formulated as follows:[7]
A set P satisfies
if and only if it is non-empty.
Or in words:
- If there is anyone in the pub at all, then there is someone such that, if he is drinking, then everyone in the pub is drinking.
See also
References
- ^ a b c d e f g h Raymond Smullyan (1978). What is the Name of this Book? The Riddle of Dracula and Other Logical Puzzles. Prentice Hall. chapter 14. How to Prove Anything. (topic) 250. The Drinking Principle. pp. 209-211. ISBN 0-13-955088-7.
{{cite book}}
: Unknown parameter|nopp=
ignored (|no-pp=
suggested) (help) - ^ a b c d H.P. Barendregt (1996). "The quest for correctness". Images of SMC Research 1996 (PDF). Stichting Mathematisch Centrum. pp. 54–55. ISBN 978-90-6196-462-9.
- ^ Peter J. Cameron (1999). Sets, Logic and Categories. Springer. p. 91. ISBN 978-1-85233-056-9.
- ^ a b c d Marc Bezem , Dimitri Hendriks (2008) Clausification in Coq
- ^ a b c J. Harrison (2008). "Automated and Interactive Theorem Proving". In Orna Grumberg, Tobias Nipkow, Christian Pfaller (ed.). Formal Logical Methods for System Security and Correctness. IOS Press. pp. 123–124. ISBN 978-1-58603-843-4.
{{cite book}}
: CS1 maint: multiple names: editors list (link) - ^ Freek Wiedijk. 2001. Mizar Light for HOL Light. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '01), Richard J. Boulton and Paul B. Jackson (Eds.). Springer-Verlag, London, UK, 378-394.
- ^ a b Martín Escardó; Paulo Oliva. "Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox" (PDF). Computability in Europe 2010: 2.
{{cite journal}}
: Cite journal requires|journal=
(help)