I've recently stumbled upon the Drinker's Problem:
The drinker paradox (also known as the drinker's theorem, the drinker's principle, or the drinking principle) is a theorem of classical predicate logic which can be stated as "There is someone in the pub such that, if he is drinking, then everyone in the pub is drinking." It 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?
Lovely book name. For people who love Greek letters, here's the formal problem definition:
The non-formal verbal proof is remarkably simple to understand. Here's the quote from Wikipedia:
- 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 everybodydrinks, everybody includes that person.
- Otherwise at least one person is not drinking. For any nondrinking person, the statement if that particular person is drinking, then everyone in the pub is drinking is formally true: its antecedent ("that particular person is drinking") is false, therefore the statement is 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. (These kinds of statements are said to be vacuously true.)
In this post, I will:
- articulate a bit on the "paradoxical" part of the problem
- describe my way of proving it constructively in cubicaltt
- mention few things which were discovered as a pleasant surprise as I went along
There are few peculiar things about this paradox. First, it isn't really a paradox, there's only a paradox-ish part about it. The part is that linguistically, it seems like the person is causing everyone else to drink somehow, whereas in reality, what is stated is that you can always find a person, such that it just so happens that everyone else is drinking along. To make a similar statement not involving conscious agents: "every day, I can find a person, such that, if that person is up, then the sun is up". This doesn't mean that the sun follows some person's actions. What we see is a principle named Correlation does not imply causation.
Let's start with the hardest part, getting the theorem statement precisely and correctly:
Ais the type of all drinkers
Dis the property meaning "is drinking"
- : I didn't have the
x : Apresent at first, it was needed later as I went along, but it makes total sense, since we need the bar to have at least one person, otherwise the theorem wouldn't make sense. In other words, our type must be inhabited
- : I will return you a specific person
- : and a function, which states, that given a fact that person is drinking
- : for any person in the bar
- : I will prove that that person is drinking
Not knowing what else can I do, I decided to follow the verbal proof, stated in the beginning. So, we need to begin by stating "either everyone is drinking, or there's someone who is not":
- : the "impossible", or "absurd" type, we cannot construct its value. Copied from prelude.ctt
- : negation in constructive mathematics is done via giving a function that returns absurd given that value. Copied from prelude.ctt
- : good old
Eithertype. Copied from prelude.ctt
- : notice how all this function needs is the type and the property, no "real values" (it should work for non-inhabited types)
-  you either get
inlwith "for all
x:A, I'll prove they're drinking"
- : or you get
inrwith specific person
x:A, and a proof they aren't (
neg (D x))
We'll get back to the actual implementation later, let us first see if we can actually use this for the full proof.
We need to case-split on the
allOrCounterex result, let's create a continuation doing that:
- : We'll need this in our proof. Given an absurd value (which can never be constructed!), I can prove anything. This is akin to saying "which is impossible becuase earlier we've shown the opposite xyz, leading to contradiction" in your verbal proof. Copied from prelude.ctt
- : function's signature is copied from
drinker, and we only add the first parameter in its return type
- : here's that parameter, which is an alpha-renamed result from
- : branch when everybody's drinking
- : then any person can suite as a proof, so let's take the inhabitant
- : we're not interested in the fact he is drinking (we know that)
- : we're just passing the
allDto prove that everyone's drinking
- : in "not everyone's drinking" case, where we get a specific person and a proof they're not drinking
- : we return that person as "the answer"
- : most interesting part. We need to prove "if that person's drinking, everybody else does", but we've got our "they are not drinking" value, so we pass "that person is drinking" (
y) to the "that person is not drinking" function (
pair.2), and get an absurd, from which we can prove anything (via
This was satisfying already, but now there is another problem that's bugging: the whole "either everyone is drinking, or somebody is not" sounds terrifically obvious to the listener, but is this a fundamental claim? Doesn't sound like an axiom or a law to me, it feels like we can break this down a bit more.
I started searching for the drinker's solution on the internet, and came up to the post called Seemingly impossible constructive proofs, which had another one, called Seemingly impossible functional programs before it. It seemed unrelated at first, but I decided to give the "functional programs" one a go before I switch to the main thing. It turned out rewarding, indeed.
In that post, something that caught my eye was this:
An implementation of "for every", using "for some". It also explicitly links the De Morgan's Laws page.
Now, I was aware of the whole De Morgan thing related to conjunctions, disjunctions and negations, but completely forgot (or did I not know?) about its use for the quantifiers! Here are the laws for conjunction and disjunction:
And here they are for quantifiers:
And it makes total sense when you think about it. "All things hold" is the same as "not (some thing doesn't)". "Some thing holds" is the same as "not (all thing do)".
- : if we were to have a "not everyone's drinking" statement
- : then we could turn it into a "there exists a person, for whom we'd give a proof they're not drinking"
This gives us a hint on how to get from "not everyone's drinking" branch to a useful dependent pair, but not a complete solution yet. What's missing?
What's missing is a way to get something out of thin air. The notoriouf law of excluded middle, a constructivist's nightmare:
lem, we can made our first case-splitting continuation on
allOrCounterex and finish the proof:
- : "everyone's drinking" branch fits ideally as is
- : "not (everyone's drinking)" is translated via
deMorganintroduced earlier, precisely matching what we need
- : we use
lem, passing a type meaning "everyone's drinking", which constructs the
orwe split upon
In this post:
- we've seen the usage of absurd type
N0, the notion of negation (
neg), "prove by absurdity" (
efq), good old
- introduced an explicit use of LEM only when we needed it
- introduced De Morgan's law for quantifiers, jumping from "forall" statement to "there exists" one
- had an exercise in proving things constructively and formally
Well, that's one drinking problem less in my life. Pass that scotch&beer, let's celebrate! 🥃🍺
Full source code can be found in drinker.ctt.
Please send your feedback in Issues or PRs in this blog's repo.