|This article is still under construction|
Please post comments, questions and suggestions on the talk page, not in the article itself. Thank you.
The drinker paradox is a theorem of classical predicate logic that can be stated: there is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking. The actual theorem is
- $ \exists x.\ [D(x) \rightarrow \forall y.\ D(y)] $.
Proof of the paradox Edit
The proof begins by recognising 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.
Suppose, on the other hand, at least one person isn't drinking. For that particular person, it still can't 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.
Either way, there is someone in the pub such that, if he or she is drinking, then everyone in the pub is drinking. Hence the paradox.
This proof illustrates several properties of classical predicate logic which do not always agree with ordinary language.
Non-empty domain Edit
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. We can deduce $ D(x) $ from $ \forall x D(x) $, but of course if the domain were empty (in this case, if there were nobody in the pub) then the proposition $ D(x) $ is not well-formed for any closed expression $ x $.
- If there is anyone in the pub at all, then there is someone such that, if he or she is drinking, then everyone in the pub is drinking.
Excluded middle Edit
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 $ S = $ "everyone is drinking", which is always available in classical logic.
<ref>tags exist, but no
<references/>tag was found