A formal proof that weak excluded middle holds from the familiar facts about real numbers.

wlem.agda

{-
  Weak excluded middle states that for every propostiion P, either ¬¬P or ¬P holds.

  We give a proof of weak excluded middle, relying just on basic facts about real numbers,
  which we carefully state, in order to make the dependence on them transparent.

  Some people might doubt the formalization. To convince yourself that there is no cheating, you should:

  * Carefully read the facts listed in the RealFacts below to see that these are all
    just familiar facts about the real numbers.

  * Verify that there are no postulates or holes (unproved statements).

  * Carefully read the statement of WLEM to see that it matches the informal statement.

  * Run the file with Agda.

  © 1 April 2023 -- Andrej Bauer
-}

open import Agda.Primitive
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary

module wlem where

  open Σ

  record RealsFacts : Set₁ where
    field
      ℝ : Set

      𝟘 : ℝ
      𝟙 : ℝ

      _<_ : ℝ → ℝ → Set

      𝟘<𝟙 : 𝟘 < 𝟙

      <-irref : ∀ {x} → ¬ (x < x)
      <-trans : ∀ {x y z} → x < y → y < z → x < z

      -- The following property is valid intuitionistically, see HoTT book Definition 11.2.7 (iv).
      cover : ∀ x → 𝟘 < x ⊎ x < 𝟙

      _≤_ : ℝ → ℝ → Set

      ≤-refl : ∀ {x} → x ≤ x
      ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
      ≤-antis : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y

      <⇒≤ : ∀ {x y} → x < y → x ≤ y

      <-≤⇒< : ∀ {x y z} → x < y → y ≤ z → x < z
      ≤-<⇒< : ∀ {x y z} → x ≤ y → y < z → x < z

    is-bound : ∀ (S : ℝ → Set) (x : ℝ) → Set
    is-bound S x = ∀ y → S y → y ≤ x

    is-inhabited : ∀ (S : ℝ → Set) → Set
    is-inhabited S = Σ[ x ∈ ℝ ] S x

    is-bounded : ∀ (S : ℝ → Set) → Set
    is-bounded S = Σ[ x ∈ ℝ ] is-bound S x

    is-supremum : ∀ (S : ℝ → Set) (x : ℝ) → Set
    is-supremum S x = is-bound S x × (∀ y → is-bound S y → x ≤ y)

    -- A bounded inhabited subset of reals has a supremum, see
    -- https://ncatlab.org/nlab/show/diff/MacNeille+real+number#completeness
    field
      sup : ∀ (S : ℝ → Set) → is-inhabited S → is-bounded S → ℝ
      sup-supremum : ∀ (S : ℝ → Set) (i : is-inhabited S) (b : is-bounded S) → is-supremum S (sup S i b)

    -- Some derived facts

    <⇒≢ : ∀ {x y} → x < y → x ≢ y
    <⇒≢ {x} {y} x<y x≡y = <-irref (subst (x <_) (sym x≡y) x<y)

    𝟘≤𝟙 : 𝟘 ≤ 𝟙
    𝟘≤𝟙 = <⇒≤ 𝟘<𝟙

    𝟘≢𝟙 : 𝟘 ≢ 𝟙
    𝟘≢𝟙 p = <-irref {x = 𝟙} (subst (_< 𝟙) p 𝟘<𝟙)

    ¬𝟙≤𝟘 : ¬ (𝟙 ≤ 𝟘)
    ¬𝟙≤𝟘 p = 𝟘≢𝟙 (≤-antis 𝟘≤𝟙 p)

  module _ (ℛ : RealsFacts) where
    open RealsFacts ℛ

    -- The main theorem
    WLEM : ∀ (P : Set) → ¬ ¬ P ⊎ ¬ P
    WLEM P = wlem-proof
      where
        -- Consider a proposition P.

        -- Let S := {x ∈ ℝ | x = 0 ∨ (x = 1 ∧ P) }
        S : ℝ → Set
        S x = (x ≡ 𝟘) ⊎ (x ≡ 𝟙 × P)

        -- S is inhabited by 0
        S-inhabited : is-inhabited S
        S-inhabited = 𝟘 , inj₁ refl

        -- S is bunded by 1
        S-bounded : is-bounded S
        S-bounded = 𝟙 , λ { _ (inj₁ refl) → 𝟘≤𝟙 ; _ (inj₂ (refl , _)) → ≤-refl}

        -- ¬P holds if, and only if, 0 is an upper bound for S
        ¬P⇒S≤𝟘 : ¬ P → is-bound S 𝟘
        ¬P⇒S≤𝟘 _ _ (inj₁ refl) = ≤-refl
        ¬P⇒S≤𝟘 ¬p _ (inj₂ (refl , p)) = ⊥-elim (¬p p)

        S≤𝟘⇒¬P : is-bound S 𝟘 → ¬ P
        S≤𝟘⇒¬P b p = ¬𝟙≤𝟘 (b 𝟙 (inj₂ (refl , p)))

        -- S is inhabited and bounded, so it has a supremum u
        u : ℝ
        u = sup S S-inhabited S-bounded

        -- If P holds then 1 ≤ u
        P⇒𝟙≤u : P → 𝟙 ≤ u
        P⇒𝟙≤u p = proj₁ (sup-supremum S S-inhabited S-bounded) 𝟙 (inj₂ (refl , p))

        -- If ¬p holds then u ≤ 0
        ¬P⇒u≤𝟘 : ¬ P → u ≤ 𝟘
        ¬P⇒u≤𝟘 ¬p = proj₂ (sup-supremum S S-inhabited S-bounded) 𝟘 (¬P⇒S≤𝟘 ¬p)

        -- Proof of WLEM
        wlem-proof : ¬ ¬ P ⊎ ¬ P
        wlem-proof with cover u
        -- either 0 < u or u < 1
        ... | inj₁ 𝟘<u =
           -- if 0 < u then ¬¬P: if ¬P were the case, we would get u ≤ 0 < u
           inj₁ (λ ¬p → <-irref {x = u} (≤-<⇒< (¬P⇒u≤𝟘 ¬p) 𝟘<u))
        ... | inj₂ u<𝟙 =
           -- if u < 1 then ¬P: if P were the case, we woudl get u < 1 ≤ u
           inj₂ λ p → <-irref (<-≤⇒< u<𝟙 (P⇒𝟙≤u p))