The law of excluded middle

module foundation.law-of-excluded-middle where

open import foundation.decidable-types

open import foundation-core.decidable-propositions
open import foundation-core.dependent-pair-types
open import foundation-core.negation
open import foundation-core.propositions
open import foundation-core.universe-levels

open import univalent-combinatorics.2-element-types

Idea

The law of excluded middle asserts that any proposition P is decidable.

Definition

LEM : (l : Level) → UU (lsuc l)
LEM l = (P : Prop l) → is-decidable (type-Prop P)

Properties

Given LEM, we obtain a map from the type of propositions to the type of decidable propositions

decidable-prop-Prop :
  {l : Level} → LEM l → Prop l → Decidable-Prop l
pr1 (decidable-prop-Prop lem P) = type-Prop P
pr1 (pr2 (decidable-prop-Prop lem P)) = is-prop-type-Prop P
pr2 (pr2 (decidable-prop-Prop lem P)) = lem P

The unrestricted law of excluded middle does not hold

abstract
  no-global-decidability :
    {l : Level} → ¬ ((X : UU l) → is-decidable X)
  no-global-decidability {l} d =
    is-not-decidable-type-UU-Fin-two-ℕ (λ X → d (pr1 X))