Struggling With My Drinker's Problem

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:

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:[1][2]

  1. 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.
  2. 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.[1][2] (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.

Stating it via Propositions-as-Types

Let's start with the hardest part, getting the theorem statement precisely and correctly:

Proving it: All or Counter-example

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":

We'll get back to the actual implementation later, let us first see if we can actually use this for the full proof.

Finishing the drinker

We need to case-split on the allOrCounterex result, let's create a continuation doing that:

De Morgan

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?

Law of Excluded Middle

What's missing is a way to get something out of thin air. The notorious law of excluded middle, a constructivist's nightmare:

Using lem, we can make our first case-splitting continuation on allOrCounterex and finish the proof:



In this post:

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.