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 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)
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
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).
- 2023-09-14. Egbert Rijke and Fredrik Bakke. Symmetric core of a relation (#754).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).