Drinker paradox
|
|
This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (February 2011) |
|
|
This article may contain original research. Please improve it by verifying the claims made and adding references. Statements consisting only of original research may be removed. More details may be available on the talk page. (February 2011) |
The drinker paradox is a theorem of classical predicate logic that states: There is someone in the pub such that, if he is drinking, everyone in the pub is drinking. The actual theorem is
The paradox was popularised by the mathematical logician Raymond Smullyan, who called it the "drinking principle" in his book What Is the Name of this Book?[1]
Contents |
[edit] Proof of the paradox
The paradox is valid 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.
The proof begins by recognizing it is true that either everyone in the pub is drinking (in this particular round of drinks), or at least one person in the pub isn't drinking.
On the one hand, suppose everyone is drinking. For any particular person, it can't 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.
Suppose, on the other hand, 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 true.
Either way, there is someone in the pub such that, if he is drinking, everyone in the pub is drinking. Hence the paradox.
[edit] Discussion
This proof illustrates several properties of classical predicate logic that do not always agree with ordinary language.
[edit] Non-empty domain
First, we didn't need to assume there was anyone in the pub. The assumption that the domain is non-empty is built into the inference rules of classical predicate logic.[2] 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
.
Nevertheless, free logic, which allows for empty domains, still has something like the drinker paradox in the form of the theorem:
Or in words:
- If there is anyone in the pub at all, then there is someone such that, if they are drinking, then everyone in the pub is drinking.
[edit] Excluded middle
The above proof begins by saying that either everyone is drinking, or someone is not drinking. This uses the validity of excluded middle for the statement
"everyone is drinking", which is always available in classical logic. If the logic does not admit arbitrary excluded middle—for example if the logic is intuitionistic—then the truth of
must first be established, i.e.,
must be shown to be decidable.[3]
[edit] Material versus indicative conditional
Most 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.
In natural language, on the other hand, typically "if...then..." is used as an indicative conditional.
[edit] Notes
- ^ Raymond Smullyan (1990). What is the Name of this Book. Penguin Books Ltd. chapter 14. ISBN 0-14-013511-1.
- ^ Martín Escardó; Paulo Oliva. Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox. Computability in Europe 2010. p. 2. http://www.cs.bham.ac.uk/~mhe/papers/dp.pdf.
- ^ Martin Abadi; Georges Gonthier; Benjamin Werner (1998). "Choice in Dynamic Linking". In Igor Walukiewicz. Foundations of Software Science and Computation Structures. Springer. p. 24. ISBN 3-540-21298-1.
[edit] References
- Coscoy, Yann; Kahn, Gilles; Théry, Laurent (1995), "Extracting text from proofs", Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, 902/1995, pp. 109–123, doi:10.1007/BFb0014048, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.8114&rep=rep1&type=pdf.
![\exists x.\ [D(x) \rightarrow \forall y.\ D(y)]. \,](http://upload.wikimedia.org/wikipedia/en/math/b/8/3/b83747eae94e4f3d13c6fc99c01a6339.png)
![\exists x.\ [x=x] \rightarrow \exists x.\ [D(x) \rightarrow \forall y.\ D(y)]](http://upload.wikimedia.org/wikipedia/en/math/7/5/3/7535ef2cc804da0b34a9089516c7d7fa.png)