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 everybody drinks, 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:
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"
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
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":
Eithertype. Copied from prelude.ctt
inlwith "for all
x:A, I'll prove they're drinking"
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:
drinker, and we only add the first parameter in its return type
allDto prove that everyone's 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)". "Something holds" is the same as "not (all thing do)".
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 notorious law of excluded middle, a constructivist's nightmare:
lem, we can make our first case-splitting continuation on
allOrCounterex and finish the proof:
deMorganintroduced earlier, precisely matching what we need
lem, passing a type meaning "everyone's drinking", which constructs the
orwe split upon
In this post:
N0, the notion of negation (
neg), "prove by absurdity" (
efq), good old
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.