Drinker paradox
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
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?

# Proof of the paradox
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
This proof illustrates several properties of classical predicate logic which do not always agree with ordinary language.

## 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. 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.
Nevertheless, free logic, which allows for empty domains, still has something like the drinker paradox in the form of the theorem:
Or in words:

## 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 S = "everyone is drinking", which is always available in classical logic. If the logic does not admit arbitrary excluded middlefor example if the logic is intuitionisticthen the truth of S \or \neg S must first be established, i.e., S must be shown to be decidable.
As a simple example of one such decision procedure, if there are finitely many customers in the pub, one can simply check that everyone in the pub drinks, or find one person who doesn't drink. But if S is given no semantics, then there is no proof of the drinker paradox in intuitionistic logic. Indeed, assuming the drinking principle over infinite domains leads to various classically valid but intuitionistically unacceptable conclusions.
For instance, it would allow for a simple solution of Goldbach's conjecture, which is one of the oldest unsolved problems in mathematics. It asks whether all even numbers greater than two can be expressed as the sum of two prime numbers. Applying the drinking principle, it would follow that there exists an even number greater than two, such that, if it is the sum of two primes, then all even numbers greater than two are the sum of two primes. However, the fundamental property of a constructive proof is that when a number with a certain property is proven to exist, the actual number is specified. It would then suffice to check whether that particular number is the sum of two primes, which has a finite decision process. If it were not, then obviously it would be a refutation of the conjecture. But if it were, then all of them would be, and the conjecture would be proven.
Nevertheless, intuitionistic (free) logic still has something like the drinker paradox in the form of the theorem:
If we take N(x) to be \neg D(x), that is, x is not drinking, then in words this reads:
In classical logic this would be equivalent to the previous statement, from which it can be derived by two transpositions.

## 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 A \rightarrow B 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 or she is drinking, then everyone is drinking" was taken to be correct in one case, if everyone was drinking, and in the other case, if he or she was not drinking  even though his or her 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.