Martin Escardo, 1st April 2024. Three versions of the Drinker Paradox, one of which is equivalent to the principle of excluded middle. \begin{code} {-# OPTIONS --safe --without-K #-} open import UF.FunExt open import UF.PropTrunc module Taboos.DrinkerParadox (fe : Fun-Ext) (pt : propositional-truncations-exist) where open PropositionalTruncation pt open import MLTT.Spartan open import UF.ClassicalLogic open import UF.SubtypeClassifier \end{code} The so-called Drinker Paradox says that in every non-empty pub X there is a person x₀ such that if x₀ drinks then everybody drinks, for any notion of drinking. \begin{code} DP : (𝓤 : Universe) → 𝓤 ⁺ ̇ DP 𝓤 = (X : 𝓤 ̇ ) → ¬ is-empty X → (drinks : X → Ω 𝓤) → ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) \end{code} This implies double negation elimination and hence excluded middle. \begin{code} DP-gives-DNE : DP 𝓤 → DNE 𝓤 DP-gives-DNE {𝓤} dp P P-is-prop ν = III where X : 𝓤 ̇ X = P X-is-non-empty : ¬ is-empty X X-is-non-empty = ν anything-you-like : Ω 𝓤 anything-you-like = ⊥ drinks : X → Ω 𝓤 drinks x = anything-you-like I : ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) I = dp X X-is-non-empty drinks II : (Σ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds)) → P II = pr₁ III : P III = ∥∥-rec P-is-prop II I DP-gives-EM : DP 𝓤 → EM 𝓤 DP-gives-EM dp = DNE-gives-EM fe (DP-gives-DNE dp) \end{code} As indicated in the above proof, it doesn't matter what "drinks" is taken to be. Any drinking predicate will do. Conversely, excluded middle gives DP. \begin{code} EM-gives-DP : EM 𝓤 → DP 𝓤 EM-gives-DP em X X-is-non-empty drinks = V where X-is-inhabited : ∥ X ∥ X-is-inhabited = non-empty-is-inhabited pt em X-is-non-empty I : (∃ x ꞉ X , ¬ (drinks x holds)) + ((x : X) → (drinks x holds)) I = ∃-not+Π pt em (λ (x : X) → drinks x holds) (λ (x : X) → holds-is-prop (drinks x)) II : (Σ x₀ ꞉ X , ¬ (drinks x₀ holds)) → Σ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) II (x₀ , x₀-is-sober) = x₀ , (λ (x₀-is-not-sober : drinks x₀ holds) → 𝟘-elim (x₀-is-sober x₀-is-not-sober)) III : ((x : X) → (drinks x holds)) → X → Σ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) III a x₀ = x₀ , λ (_ : drinks x₀ holds) → a IV : type-of I → ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) IV (inl e) = ∥∥-functor II e IV (inr a) = ∥∥-functor (III a) X-is-inhabited V : ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) V = IV I \end{code} Now consider the following two variations, where we instead require that the pub is assumed to be respectively pointed and inhabited. \begin{code} pointed-DP : (𝓤 : Universe) → 𝓤 ⁺ ̇ pointed-DP 𝓤 = (X : 𝓤 ̇ ) → X → (drinks : X → Ω 𝓤) → ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) inhabited-DP : (𝓤 : Universe) → 𝓤 ⁺ ̇ inhabited-DP 𝓤 = (X : 𝓤 ̇ ) → ∥ X ∥ → (drinks : X → Ω 𝓤) → ∃ x₀ ꞉ X , (drinks x₀ holds → (x : X) → drinks x holds) \end{code} These two variations are weaker than the original version. \begin{code} pointed-DP-gives-inhabited-DP : inhabited-DP 𝓤 → pointed-DP 𝓤 pointed-DP-gives-inhabited-DP idp X x₀ = idp X ∣ x₀ ∣ DP-gives-pointed-DP : DP 𝓤 → pointed-DP 𝓤 DP-gives-pointed-DP dp X x = dp X (λ (e : X → 𝟘) → e x) \end{code} I don't know whether excluded middle can be proved from any of these two weaker variations, or, equivalently, whether each of these two variations imply the original. There are more variations. For example, we can consider the particular case where the drinking predicate is decidable, or we can replace ∃ by Σ. These two modifications together are indeed one of our definitions of compactness in TypeTopology.CompactTypes.