The Drinker's Paradox
A Tale of Three Paradoxes
(Last updated 2022-10-30, "See Also")


                                                      Russell and friends
                                 Photo Credit: The Official Website of The James Joyce Irish Pub, Prague

The Drinker's Theorem:  Consider the set of all drinkers in the world, and
the set of all people in a given pub (empty or otherwise). Then there
exists a person who, if her or she is drinking, then everyone in that pub
is drinking.

It doesn't matter how many people are there. Or how many are drinking. Or how few. No one needs to be taking their cues from some "lead drinker," but in every pub, in every town and village, it just happens! How is this possible?

There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Russell's Paradox (actually a theorem) is the key.

The Resolution of Russell's Paradox

We begin assuming that we have the set r of all things that are not elements of themselves:

1     ALL(a):[a e r <=> ~a e a]
Premise

Applying this definition to r itself, we obtain the following contradiction:

2     r e r <=> ~r e r
U Spec, 1

Therefore, no such set can exist and we have the theorem:

3     ~EXIST(r):ALL(a):[a e r <=> ~a e a]
4 Conclusion, 1

The Resolution of the Paradox of the Universal Set

We apply slight variation of the above theorem to resolve the so-called Paradox of the Universal Set to prove that no set can contain everything:

    ~EXIST(s):[Set(s) & ALL(a):a e s]

Or equivalently, every set must exclude something:

    ALL(s):[Set(s) => EXIST(a):~a e s]   (Formal proof, 28 lines)

The Drinker's Theorem

Again, consider the set (drinkers) of all drinkers in the world, and the set (pub) of all people in a given pub.  Then there exists a person who, if he or she is drinking, then everyone in that pub is drinking. More formally, this paradox can be stated as a provable theorem:

EXIST(x):[x e drinkers => ALL(a):[a e pub => a e drinkers]] (Formal proof, 10 lines)

This proof makes use of the previous result that every set excludes something.

Conclusion

As stated in the above disclaimer, this is not some profound truth about about set theory and logic. More an entertaining curiosity than anything else, this logical construct is highly unusual. In formal mathematical proofs, you will rarely if ever, see an existential quantifier applied to an implication like this.  Such a construct should set off alarm bells whenever you see it. Something weird and counter-intuitive  is probably happening.

The general principle as demonstrated in the above proof (see lines 4 to 6), is that for any set s, empty or not, we would have:

EXIST(x):[x e s => Q]  (Formal proof, 9 lines)

where Q is any logical proposition whatsoever, even a falsehood or a contradiction would do.  We could even have:

    EXIST(x):[x e s => ~x e s]

And this would be provably true! There is no need, however, to question our sanity or, worse, The Rules of Logic as some have suggested. It is important to understand what we have not proven here. In the Drinker's Paradox, we have not proven, as commonly misinterpreted (note the bracketing):

EXIST(x):[x e drinkers] => ALL(a):[a e pub => a e drinkers]

Now, this would be very profound indeed were it not for the obvious fact that this statement is not always true! Note that, here, the existential quantifier is not applied to the implication as in the wildly counter-intuitive Drinker's Paradox above.

See Also 

· The formalizing of Smullyan’s Original Drinkers Principle (New 2022-11-14)

DC Proof Homepage