The law of excluded middle

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-16.
Last modified on 2024-10-15.

module foundation.law-of-excluded-middle where
Imports 
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.decidable-propositions
open import foundation-core.negation
open import foundation-core.propositions

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)

prop-LEM : (l : Level) → Prop (lsuc l)
prop-LEM l = Π-Prop (Prop l) (is-decidable-Prop)

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-2-Element-Type (λ X → d (pr1 X))

Recent changes