The law of excluded middle
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-16.
Last modified on 2023-09-14.
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
- 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).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).