The law of excluded middle

Content created by Louis Wasserman.

Created on 2026-02-05.
Last modified on 2026-02-05.

module foundation-core.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

Idea

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

Definition

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

LEM : UUω
LEM = {l : Level} → level-LEM l

prop-level-LEM : (l : Level) → Prop (lsuc l)
prop-level-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} → 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

Recent changes