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)] $.

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]}

## 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.

## Discussion Edit

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.

**Cite error:**

`<ref>`

tags exist, but no `<references/>`

tag was found