The drinker paradox 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?
Proofs of the paradox 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: 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.
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 is false.
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.
The proof above is essentially model-theoretic.
A purely syntactic proof is possible and can even be mechanized, but only for an equisatisfiable
rather than an equivalent negation of the theorem.
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, 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, resulting in the Herbrand
universe:
One can sketch the following natural deduction:
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 search thus finishes in two steps:
The proof by resolution given here uses the law of excluded middle, the axiom of choice,
and non-emptiness of the domain as premises.
Discussion This proof illustrates several properties
of classical predicate logic that do not always agree with ordinary language.
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.
Material versus indicative conditional Most important to the paradox is that the
conditional in classical logic is the material conditional.
It has the property that is true if B is true or if A is false.
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.
Non-empty domain It is not necessary 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 from , but of course if the domain were empty, the proposition is not
well-formed for any closed expression . Nevertheless, if we allow empty domains we
still have 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 he is drinking, then everyone in the pub is drinking.
Temporal aspects Although not discussed in formal terms by
Smullyan, he hints that the verb "drinks" is also ambiguous by citing a postcard written
to him by two of his students, which contains the following dialogue:
Logician / I know a fellow who is such that whenever he drinks, everyone does.Student
/ I just don't understand.
Do you mean, everyone on earth?Logician / Yes, naturally.Student / That sounds crazy!
You mean as soon as he drinks, at just that moment, everyone does?Logician / Of course.Student
/ But that implies that at some time, everyone was drinking at once.
Surely that never happened!
History and variations Smullyan in his 1978 book attributes the naming
of "The Drinking Principle" to his graduate students.
He also discusses variants: "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.
A "dual" version of the Principle: "there is at least one person such that if anybody
drinks, then he does."
As "Smullyan's ‘Drinkers’ principle" or just "Drinkers' principle" it appears in H.P.
Barendregt's "The quest for correctness", accompanied by some machine proofs.
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.
See also List of paradoxes
Reification Temporal logic