The law of excluded middle

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

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

module foundation.law-of-excluded-middle where

open import foundation-core.law-of-excluded-middle public
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

Properties

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