Back to Coq Main Page

Predicate Logic: Drinker's Theorem

This example included in the official Coq documentation: see Paradoxes of classical predicate calculus.

"In any nonempty bar there is a person such that, if s/he drinks, then everyone else in that bar also drinks."

See Wikipedia: Drinker Paradox for a longer discussion. In fact, it is not a paradox, but rather simple theorem. It sounds unusual, because most if-then statements usually mean some causal relationship between the condition and the conclusion. In the drinker theorem there is no such relationship: We do not need any assumptions on how one person's drinking affects what other people do.

Human-readable Proof

We consider two cases.

• If we assume that everyone is drinking, then select anybody (note that the bar is nonempty). The conclusion of the theorem will be true.
• If there are non-drinking people in the bar, then select anyone among them. In this case the condition is wrong: the person we selected does NOT drink. Therefore the whole implication will be also true, since false implies anything.

Computer-verified Proof

Denote D - the set of all people in the bar; P - drinker predicate (takes value "true" for those who drink, takes value "false" otherwise). There is at least one person in the bar, denote it by d, we do not know, if d drinks or not.