Diaconescu’s theorem

Content created by Fredrik Bakke.

Created on 2025-01-07.
Last modified on 2025-01-07.

module foundation.diaconescus-theorem where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.axiom-of-choice
open import foundation.booleans
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.law-of-excluded-middle
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.identity-types

open import synthetic-homotopy-theory.suspensions-of-propositions
open import synthetic-homotopy-theory.suspensions-of-types

Idea

The axiom of choice implies the law of excluded middle. This is often referred to as Diaconescu’s theorem.

Theorem

We follow the proof given under Theorem 10.1.14 in [UF13].

Proof. Given a proposition P, then its suspension ΣP is a set with the property that (N ＝ S) ≃ ΣP, where N and S are the poles of ΣP. There is a surjection from the booleans onto the suspension f : bool ↠ ΣP such that f true ≐ N and f false ≐ S. Its fiber family is in other words an inhabited family over ΣP. Applying the axiom of choice to this family, we obtain a mere section s of f which thus exhibits P as a logical equivalent to f⁻¹ N ＝ f⁻¹ S. The latter is an equation of booleans, and the booleans have decidable equality so P must also be decidable.

instance-theorem-Diaconescu :
  {l : Level} (P : Prop l) →
  instance-choice₀
    ( suspension-set-Prop P)
    ( fiber map-surjection-bool-suspension) →
  is-decidable-type-Prop P
instance-theorem-Diaconescu P ac-P =
  rec-trunc-Prop
    ( is-decidable-Prop P)
    ( λ s →
      is-decidable-iff'
        ( ( iff-equiv (compute-eq-north-south-suspension-Prop P)) ∘iff
          ( ( λ p →
              ( inv (pr2 (s north-suspension))) ∙
              ( ap map-surjection-bool-suspension p) ∙
              ( pr2 (s south-suspension))) ,
            ( ap (pr1 ∘ s))))
        ( has-decidable-equality-bool
          ( pr1 (s north-suspension))
          ( pr1 (s south-suspension))))
    ( ac-P is-surjective-map-surjection-bool-suspension)

theorem-Diaconescu :
  {l : Level} → level-AC0 l l → LEM l
theorem-Diaconescu ac P =
  instance-theorem-Diaconescu P
    ( ac (suspension-set-Prop P) (fiber map-surjection-bool-suspension))

References

[UF13]
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.

Recent changes