I've recently stumbled upon the Drinker's Problem:

The

drinker paradox(also known as thedrinker's theorem, thedrinker's principle, or thedrinking 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 bookWhat 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]

- 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 whenthat persondrinkseverybodydrinks, 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 drinkingis 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:

- articulate a bit on the "paradoxical" part of the problem
- describe my way of proving it with Curry–Howard correspondence (or Brouwer-Heyting-Kolmogorov interpretation, if you like) 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:

`drinker`

` (A : U) -- [1]`

` (D : A -> U) -- [2]`

` (x : A) -- [3]`

` : ( (x : A) -- [4]`

` * ((y : D x) -- [5]`

` -> (z : A) -- [6]`

` -> D z -- [7]`

` )`

` )`

` = undefined`

**[1]**:`A`

is the type of all drinkers**[2]**:`D`

is the property meaning "is drinking"**[3]**: I didn't have the`x : A`

present 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****[4]**: I will return you a specific person**[5]**: and a function, which states, that given a fact that person is drinking**[6]**: for any person in the bar**[7]**: 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":

`x``data N0 = -- [1]`

``

`-- [2]`

`neg (A : U) : U = A -> N0`

``

`-- [3]`

`data or (A B : U)`

` = inl (a : A)`

` | inr (b : B)`

``

`-- [4]`

`allOrCounterex`

` (A : U)`

` (D : A -> U)`

` : (or ((x : A) -> D x) -- [5]`

` ((x : A) * (neg (D x))) -- [6]`

` )`

` = undefined`

**[1]**: the "impossible", or "absurd" type, we cannot construct its value. Copied from prelude.ctt**[2]**: negation in "propositions-as-types" mathematics is done via giving a function that returns absurd given that value. Copied from prelude.ctt**[3]**: good old`Either`

type. Copied from prelude.ctt**[4]**: notice how all this function needs is the type and the property, no "real values" (it should work for non-inhabited types)**[5]**you either get`inl`

with "for all`x:A`

, I'll prove they're drinking"**[6]**: or you get`inr`

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

`xxxxxxxxxx`

`-- [1]`

`efq (A : U) : N0 -> A = split {}`

``

`-- [2]`

`drinkerC1`

` (A : U)`

` (D : A -> U)`

` (x : A)`

` : (or ((q : A) -> D q) -- [3]`

` ((q : A) * (neg (D q))))`

` ->`

` ( (x : A)`

` * ((y : D x)`

` -> (z : A)`

` -> D z`

` )`

` )`

` = split`

` inl allD -> -- [4]`

` ( x -- [5]`

` , (\(_ : D x) -> -- [6]`

` \(z : A) -> -- [7]`

` allD z))`

` inr pair -> -- [8]`

` ( pair.1 -- [9]`

` , \(y : D pair.1) ->`

` \(z : A) ->`

` efq (D z) (pair.2 y)) -- [10]`

``

`drinker ... = drinkerC1 A D x (allOrCounterex A D)`

**[1]**: 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 because earlier we've shown the opposite xyz, leading to contradiction" in your verbal proof. Copied from prelude.ctt**[2]**: function's signature is copied from`drinker`

, and we only add the first parameter in its return type**[3]**: here's that parameter, which is an alpha-renamed result from`allOrConterex`

**[4]**: branch when everybody's drinking**[5]**: then any person can suite as a proof, so let's take the inhabitant**[6]**: we're not interested in the fact he is drinking (we know that)**[7]**: we're just passing the`allD`

to prove that everyone's drinking**[8]**: in "not everyone's drinking" case, where we get a specific person and a proof they're not drinking**[9]**: we return that person as "the answer"**[10]**: the 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`efq`

)

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:

`xxxxxxxxxx`

`> forevery p = not(forsome(\a -> not(p a)))`

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)".

`xxxxxxxxxx`

`deMorgan`

` (A : U)`

` (D : A -> U)`

` : (neg ((x : A) -> D x)) -- [1]`

` -> ( (x : A) -- [2]`

` * (neg (D x)))`

` = undefined`

**[1]**: if we were to have a "not everyone's drinking" statement**[2]**: 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 notorious law of excluded middle, a constructivist's nightmare:

`xxxxxxxxxx`

`lem (A : U)`

` : or A (neg A)`

` = undefined`

Using `lem`

, we can make our first case-splitting continuation on `allOrCounterex`

and finish the proof:

`xxxxxxxxxx`

`allOrCounterexC1`

` (A : U)`

` (D : A -> U)`

` : (lem : or ((x : A) -> D x)`

` (neg ((x : A) -> D x)))`

` -> (or ((x : A) -> D x)`

` ((x : A) * (neg (D x))))`

` = split`

` inl f -> inl f -- [1]`

` inr f -> inr (deMorgan A D f) -- [2]`

``

`allOrCounterex ...`

` = allOrCounterexC1 A D `

` (lem ((x : A) -> D x)) -- [3]`

**[1]**: "everyone's drinking" branch fits ideally as is**[2]**: "not (everyone's drinking)" is translated via`deMorgan`

introduced earlier, precisely matching what we need**[3]**: we use`lem`

, passing a type meaning "everyone's drinking", which constructs the`or`

we split upon

Voila!

In this post:

- we've seen the usage of absurd type
`N0`

, the notion of negation (`neg`

), "prove by absurdity" (`efq`

), good old`or`

type - 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 via "propositions as types" concept, 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.