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-04-11.

module where
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


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


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


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

  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