# The law of excluded middle

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

Created on 2022-02-16.

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))