module 1Lab.Classical where

The law of excluded middle🔗

While we do not assume any classical principles in the 1Lab, we can still state them and explore their consequences.

The law of excluded middle (LEM) is the defining principle of classical logic, which states that any proposition is either true or false (in other words, decidable). Of course, assuming this as an axiom requires giving up canonicity: we could prove that, for example, any Turing machine either halts or does not halt, but this would not give us any computational information.

LEM : Type
LEM =  (P : Ω)  Dec  P 

Note that we cannot do without the assumption that is a proposition: the statement that all types are decidable is inconsistent with univalence.

An equivalent statement of excluded middle is the law of double negation elimination (DNE):

DNE : Type
DNE =  (P : Ω)  ¬ ¬  P    P 

We show that these two statements are equivalent propositions.

LEM-is-prop : is-prop LEM
LEM-is-prop = hlevel!

DNE-is-prop : is-prop DNE
DNE-is-prop = hlevel!

LEM→DNE : LEM  DNE
LEM→DNE lem P = Dec-elim _  p _  p)  ¬p ¬¬p  absurd (¬¬p ¬p)) (lem P)

DNE→LEM : DNE  LEM
DNE→LEM dne P = dne (el (Dec  P ) hlevel!) λ k  k (no λ p  k (yes p))

LEM≃DNE : LEM  DNE
LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM

Weak excluded middle🔗

The weak law of excluded middle (WLEM) is a slightly weaker variant of excluded middle which asserts that every proposition is either false or not false.

WLEM : Type
WLEM =  (P : Ω)  Dec (¬  P )

As the name suggests, the law of excluded middle implies the weak law of excluded middle.

LEM→WLEM : LEM  WLEM
LEM→WLEM lem P = lem (P →Ω ⊥Ω)

The weak law of excluded middle is also a proposition.

WLEM-is-prop : is-prop WLEM
WLEM-is-prop = hlevel!

The axiom of choice🔗

The axiom of choice is a stronger classical principle which allows us to commute propositional truncations past Π types.

Axiom-of-choice : Typeω
Axiom-of-choice =
   { ℓ'} {B : Type } {P : B  Type ℓ'}
   is-set B  (∀ b  is-set (P b))
   (∀ b   P b )
    (∀ b  P b) 

Like before, the assumptions that is a set and is a family of sets are required to avoid running afoul of univalence.

An equivalent and sometimes useful statement is that all surjections between sets merely have a section. This is essentially jumping to the other side of the fibration equivalence.

Surjections-split : Typeω
Surjections-split =
   { ℓ'} {A : Type } {B : Type ℓ'}  is-set A  is-set B
   (f : A  B)
   is-surjective f
    (∀ b  fibre f b) 

We show that these two statements are logically equivalent1.

AC→Surjections-split : Axiom-of-choice  Surjections-split
AC→Surjections-split ac Aset Bset f =
  ac Bset (fibre-is-hlevel 2 Aset Bset f)

Surjections-split→AC : Surjections-split  Axiom-of-choice
Surjections-split→AC ss {P = P} Bset Pset h = ∥-∥-map
  (Equiv.to (Π-cod≃ (Fibre-equiv P)))
  (ss (Σ-is-hlevel 2 Bset Pset) Bset fst λ b 
    ∥-∥-map (Equiv.from (Fibre-equiv P b)) (h b))

We can show that the axiom of choice implies the law of excluded middle; this is sometimes known as the Diaconescu-Goodman-Myhill theorem2.

Given a proposition we consider the suspension of the type is a set with two points and a path between them if and only if holds.

Since admits a surjection from the booleans, the axiom of choice merely gives us a section

module _ (split : Surjections-split) (P : Ω) where
  section :  ((x : Susp  P )  fibre 2→Σ x) 
  section = split Bool-is-set (Susp-prop-is-set hlevel!) 2→Σ 2→Σ-surjective

But a section is always injective, and the booleans are discrete, so we can prove that is also discrete. Since the path type in is equivalent to this concludes the proof.

  Discrete-ΣP : Discrete (Susp  P )
  Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set hlevel! _ _))
     f  Discrete-inj (fst  f) (right-inverse→injective 2→Σ (snd  f))
                        Discrete-Bool)
    section

  AC→LEM : Dec  P 
  AC→LEM = Dec-≃ (Susp-prop-path hlevel!) Discrete-ΣP

  1. they are also propositions, but since they live in Typeω we cannot easily say that↩︎

  2. not to be confused with Diaconescu’s theorem in topos theory↩︎