Martin Escardo.

Excluded middle related things. Notice that this file doesn't
postulate excluded middle. It only defines what the principle of
excluded middle is.

In the Curry-Howard interpretation, excluded middle say that every
type has an inhabitant or os empty. In univalent foundations, where
one works with propositions as subsingletons, excluded middle is the
principle that every subsingleton type is inhabited or empty.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.ExcludedMiddle where

open import MLTT.Spartan

open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UniverseEmbedding

\end{code}

Excluded middle (EM) is not provable or disprovable. However, we do
have that there is no truth value other than false (โฅ) or true (โค),
which we refer to as the density of the decidable truth values.

\begin{code}

EM : โ ๐ค โ ๐ค โบ ฬ
EM ๐ค = (P : ๐ค ฬ ) โ is-prop P โ P + ยฌ P

excluded-middle = EM

lower-EM : โ ๐ฅ โ EM (๐ค โ ๐ฅ) โ EM ๐ค
lower-EM ๐ฅ em P P-is-prop = f d
where
d : Lift ๐ฅ P + ยฌ Lift ๐ฅ P
d = em (Lift ๐ฅ P) (equiv-to-prop (Lift-is-universe-embedding ๐ฅ P) P-is-prop)

f : Lift ๐ฅ P + ยฌ Lift ๐ฅ P โ P + ยฌ P
f (inl p) = inl (lower p)
f (inr ฮฝ) = inr (ฮป p โ ฮฝ (lift ๐ฅ p))

Excluded-Middle : ๐คฯ
Excluded-Middle = โ {๐ค} โ EM ๐ค

EM-is-prop : FunExt โ is-prop (EM ๐ค)
EM-is-prop {๐ค} fe = ฮ โ-is-prop
(ฮป {๐ค} {๐ฅ} โ fe ๐ค ๐ฅ)
(ฮป _ โ decidability-of-prop-is-prop (fe ๐ค ๐คโ))

LEM : โ ๐ค โ ๐ค โบ ฬ
LEM ๐ค = (p : ฮฉ ๐ค) โ p holds + ยฌ (p holds)

EM-gives-LEM : EM ๐ค โ LEM ๐ค
EM-gives-LEM em p = em (p holds) (holds-is-prop p)

LEM-gives-EM : LEM ๐ค โ EM ๐ค
LEM-gives-EM lem P i = lem (P , i)

WEM : โ ๐ค โ ๐ค โบ ฬ
WEM ๐ค = (P : ๐ค ฬ ) โ is-prop P โ ยฌ P + ยฌยฌ P

WEM-is-prop : FunExt โ is-prop (WEM ๐ค)
WEM-is-prop {๐ค} fe = ฮ โ-is-prop (ฮป {๐ค} {๐ฅ} โ fe ๐ค ๐ฅ)
(ฮป _ _ โ decidability-of-prop-is-prop (fe ๐ค ๐คโ)
(negations-are-props (fe ๐ค ๐คโ)))

\end{code}

Double negation elimination is equivalent to excluded middle.

\begin{code}

DNE : โ ๐ค โ ๐ค โบ ฬ
DNE ๐ค = (P : ๐ค ฬ ) โ is-prop P โ ยฌยฌ P โ P

EM-gives-DNE : EM ๐ค โ DNE ๐ค
EM-gives-DNE em P i ฯ = cases id (ฮป u โ ๐-elim (ฯ u)) (em P i)

double-negation-elim : EM ๐ค โ DNE ๐ค
double-negation-elim = EM-gives-DNE

fake-ยฌยฌ-EM : {X : ๐ค ฬ } โ ยฌยฌ (X + ยฌ X)
fake-ยฌยฌ-EM u = u (inr (ฮป p โ u (inl p)))

DNE-gives-EM : funext ๐ค ๐คโ โ DNE ๐ค โ EM ๐ค
DNE-gives-EM fe dne P isp = dne (P + ยฌ P)
(decidability-of-prop-is-prop fe isp)
fake-ยฌยฌ-EM

all-props-negative-gives-DNE : funext ๐ค ๐คโ
โ ((P : ๐ค ฬ ) โ is-prop P โ ฮฃ Q ๊ ๐ค ฬ , (P โ ยฌ Q))
โ DNE ๐ค
all-props-negative-gives-DNE {๐ค} fe ฯ P P-is-prop = I (ฯ P P-is-prop)
where
I : (ฮฃ Q ๊ ๐ค ฬ , (P โ ยฌ Q)) โ ยฌยฌ P โ P
I (Q , f , g) ฮฝ = g (three-negations-imply-one (double-contrapositive f ฮฝ))

all-props-negative-gives-EM : funext ๐ค ๐คโ
โ ((P : ๐ค ฬ ) โ is-prop P โ ฮฃ Q ๊ ๐ค ฬ , (P โ ยฌ Q))
โ EM ๐ค
all-props-negative-gives-EM {๐ค} fe ฯ = DNE-gives-EM fe
(all-props-negative-gives-DNE fe ฯ)

fe-and-em-give-propositional-truncations : FunExt
โ Excluded-Middle
โ propositional-truncations-exist
fe-and-em-give-propositional-truncations fe em =
record {
โฅ_โฅ          = ฮป X โ ยฌยฌ X ;
โฅโฅ-is-prop   = ฮ -is-prop (fe _ _) (ฮป _ โ ๐-is-prop) ;
โฃ_โฃ          = ฮป x u โ u x ;
โฅโฅ-rec       = ฮป i u ฯ โ EM-gives-DNE em _ i (ยฌยฌ-functor u ฯ)
}

De-Morgan : โ ๐ค โ ๐ค โบ ฬ
De-Morgan ๐ค = (P Q : ๐ค ฬ )
โ is-prop P
โ is-prop Q
โ ยฌ (P ร Q) โ ยฌ P + ยฌ Q

EM-gives-De-Morgan : EM ๐ค
โ De-Morgan ๐ค
EM-gives-De-Morgan em A B i j =
ฮป (ฮฝ : ยฌ (A ร B)) โ
Cases (em A i)
(ฮป (a : A) โ Cases (em B j)
(ฮป (b : B) โ ๐-elim (ฮฝ (a , b)))
inr)
inl

\end{code}

But already weak excluded middle gives De Morgan:

\begin{code}

non-contradiction : {X : ๐ค ฬ } โ ยฌ (X ร ยฌ X)
non-contradiction (x , ฮฝ) = ฮฝ x

WEM-gives-De-Morgan : WEM ๐ค โ De-Morgan ๐ค
WEM-gives-De-Morgan wem A B i j =
ฮป (ฮฝ : ยฌ (A ร B)) โ
Cases (wem A i)
inl
(ฮป (ฯ : ยฌยฌ A)
โ Cases (wem B j)
inr
(ฮป (ฮณ : ยฌยฌ B) โ ๐-elim (ฯ (ฮป (a : A) โ ฮณ (ฮป (b : B) โ ฮฝ (a , b))))))

De-Morgan-gives-WEM : funext ๐ค ๐คโ โ De-Morgan ๐ค โ WEM ๐ค
De-Morgan-gives-WEM fe d P i = d P (ยฌ P) i (negations-are-props fe) non-contradiction

\end{code}

Is the above De Morgan Law a proposition? If it doesn't hold, it is
vacuously a proposition. But if it does hold, it is not a
proposition. We prove this by modifying any given ฮด : De-Mordan ๐ค to a
different ฮด' : De-Morgan ๐ค. Then we also consider a truncated version
of De-Morgan that is a proposition and is logically equivalent to
De-Morgan. So De-Morgan ๐ค is not necessarily a proposition, but it
always has split support (it has a proposition as a retract).

\begin{code}

De-Morgan-is-prop : ยฌ De-Morgan ๐ค โ is-prop (De-Morgan ๐ค)
De-Morgan-is-prop ฮฝ ฮด = ๐-elim (ฮฝ ฮด)

De-Morgan-is-not-prop : funext ๐ค ๐คโ โ De-Morgan ๐ค โ ยฌ is-prop (De-Morgan ๐ค)
De-Morgan-is-not-prop {๐ค} fe ฮด = IV
where
open import MLTT.Plus-Properties

wem : WEM ๐ค
wem = De-Morgan-gives-WEM fe ฮด

g : (P Q : ๐ค ฬ )
(i : is-prop P) (j : is-prop Q)
(ฮฝ : ยฌ (P ร Q))
(a : ยฌ P + ยฌยฌ P)
(b : ยฌ Q + ยฌยฌ Q)
(c : ยฌ P + ยฌ Q)
โ ยฌ P + ยฌ Q
g P Q i j ฮฝ (inl _) (inl v) (inl _) = inr v
g P Q i j ฮฝ (inl u) (inl _) (inr _) = inl u
g P Q i j ฮฝ (inl _) (inr _) _       = ฮด P Q i j ฮฝ
g P Q i j ฮฝ (inr _) _       _       = ฮด P Q i j ฮฝ

ฮด' : De-Morgan ๐ค
ฮด' P Q i j ฮฝ = g P Q i j ฮฝ (wem P i) (wem Q j) (ฮด P Q i j ฮฝ)

I : (i : is-prop ๐) (h : ยฌ ๐) โ wem ๐ i ๏ผ inl h
I i h = Iโ (wem ๐ i) refl
where
Iโ : (a : ยฌ ๐ + ยฌยฌ ๐) โ wem ๐ i ๏ผ a โ wem ๐ i ๏ผ inl h
Iโ (inl u) p = transport (ฮป - โ wem ๐ i ๏ผ inl -) (negations-are-props fe u h) p
Iโ (inr ฯ) p = ๐-elim (ฯ h)

ฮฝ : ยฌ (๐ ร ๐)
ฮฝ (p , q) = ๐-elim p

II : (i j : is-prop ๐) โ ฮด' ๐ ๐ i j ฮฝ โ  ฮด ๐ ๐ i j ฮฝ
II i j = IIโ
where
m n : ยฌ ๐ + ยฌ ๐
m = ฮด ๐ ๐ i j ฮฝ
n = g ๐ ๐ i j ฮฝ (inl ๐-elim) (inl ๐-elim) m

IIโ : ฮด' ๐ ๐ i j ฮฝ ๏ผ n
IIโ = apโ (ฮป -โ -โ โ g ๐ ๐ i j ฮฝ -โ -โ m)
(I i ๐-elim)
(I j ๐-elim)

IIโ : (m' : ยฌ ๐ + ยฌ ๐)
โ m ๏ผ m'
โ g ๐ ๐ i j ฮฝ (inl ๐-elim) (inl ๐-elim) m' โ  m
IIโ (inl x) p q = +disjoint
(inl x      ๏ผโจ p โปยน โฉ
m          ๏ผโจ q โปยน โฉ
inr ๐-elim โ)
IIโ (inr x) p q = +disjoint
(inl ๐-elim ๏ผโจ q โฉ
m          ๏ผโจ p โฉ
inr x      โ)

IIโ : ฮด' ๐ ๐ i j ฮฝ โ  m
IIโ = transport (_โ  m) (IIโ โปยน) (IIโ m refl)

III : ฮด' โ  ฮด
III e = II ๐-is-prop ๐-is-prop IIIโ
where
IIIโ : ฮด' ๐ ๐ ๐-is-prop ๐-is-prop ฮฝ ๏ผ ฮด ๐ ๐ ๐-is-prop ๐-is-prop ฮฝ
IIIโ = ap (ฮป - โ - ๐ ๐ ๐-is-prop ๐-is-prop ฮฝ) e

IV : ยฌ is-prop (De-Morgan ๐ค)
IV i = III (i ฮด' ฮด)

module _ (pt : propositional-truncations-exist) where

open PropositionalTruncation pt

truncated-De-Morgan : โ ๐ค โ ๐ค โบ ฬ
truncated-De-Morgan ๐ค = (P Q : ๐ค ฬ )
โ is-prop P
โ is-prop Q
โ ยฌ (P ร Q) โ ยฌ P โจ ยฌ Q

truncated-De-Morgan-is-prop : FunExt โ is-prop (truncated-De-Morgan ๐ค)
truncated-De-Morgan-is-prop fe = ฮ โ-is-prop (ฮป {๐ค} {๐ฅ} โ fe ๐ค ๐ฅ)
(ฮป P Q i j ฮฝ โ โจ-is-prop)

De-Morgan-gives-truncated-De-Morgan : De-Morgan ๐ค โ truncated-De-Morgan ๐ค
De-Morgan-gives-truncated-De-Morgan d P Q i j ฮฝ = โฃ d P Q i j ฮฝ โฃ

truncated-De-Morgan-gives-WEM : FunExt โ truncated-De-Morgan ๐ค โ WEM ๐ค
truncated-De-Morgan-gives-WEM {๐ค} fe t P i = III
where
I : ยฌ (P ร ยฌ P) โ ยฌ P โจ ยฌยฌ P
I = t P (ยฌ P) i (negations-are-props (fe ๐ค ๐คโ))

II : ยฌ P โจ ยฌยฌ P
II = I non-contradiction

III : ยฌ P + ยฌยฌ P
III = exit-โฅโฅ
(decidability-of-prop-is-prop (fe ๐ค ๐คโ)
(negations-are-props (fe ๐ค ๐คโ)))
II

truncated-De-Morgan-gives-De-Morgan : FunExt โ truncated-De-Morgan ๐ค โ De-Morgan ๐ค
truncated-De-Morgan-gives-De-Morgan fe t P Q i j ฮฝ =
WEM-gives-De-Morgan (truncated-De-Morgan-gives-WEM fe t) P Q i j ฮฝ

\end{code}

The above shows that weak excluded middle, De Morgan and truncated De
Morgan are logically equivalent (https://ncatlab.org/nlab/show/De%20Morgan%20laws).

\begin{code}

double-negation-is-truncation-gives-DNE : ((X : ๐ค ฬ ) โ ยฌยฌ X โ โฅ X โฅ) โ DNE ๐ค
double-negation-is-truncation-gives-DNE f P i u = exit-โฅโฅ i (f P u)

non-empty-is-inhabited : EM ๐ค โ {X : ๐ค ฬ } โ ยฌยฌ X โ โฅ X โฅ
non-empty-is-inhabited em {X} ฯ =
cases
(ฮป (s : โฅ X โฅ)
โ s)
(ฮป (u : ยฌ โฅ X โฅ)
โ ๐-elim (ฯ (contrapositive โฃ_โฃ u))) (em โฅ X โฅ โฅโฅ-is-prop)

โ-not+ฮ  : EM (๐ค โ ๐ฅ)
โ {X : ๐ค ฬ }
โ (A : X โ ๐ฅ ฬ )
โ ((x : X) โ is-prop (A x))
โ (โ x ๊ X , ยฌ (A x)) + (ฮ  x ๊ X , A x)
โ-not+ฮ  {๐ค} {๐ฅ} em {X} A is-prop-valued =
Cases (em (โ x ๊ X , ยฌ (A x)) โ-is-prop)
inl
(ฮป (u : ยฌ (โ x ๊ X , ยฌ (A x)))
โ inr (ฮป (x : X) โ EM-gives-DNE
(lower-EM (๐ค โ ๐ฅ) em)
(A x)
(is-prop-valued x)
(ฮป (v : ยฌ A x) โ u โฃ (x , v) โฃ)))

โ+ฮ -not : EM (๐ค โ ๐ฅ)
โ {X : ๐ค ฬ }
โ (A : X โ ๐ฅ ฬ )
โ ((x : X) โ is-prop (A x))
โ (โ x ๊ X , A x) + (ฮ  x ๊ X , ยฌ (A x))
โ+ฮ -not {๐ค} {๐ฅ} em {X} A is-prop-valued =
Cases (em (โ x ๊ X , A x) โ-is-prop)
inl
(ฮป (u : ยฌ (โ x ๊ X , A x))
โ inr (ฮป (x : X) (v : A x) โ u โฃ x , v โฃ))

not-ฮ -implies-โ-not : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
โ EM (๐ค โ ๐ฅ)
โ ((x : X) โ is-prop (A x))
โ ยฌ ((x : X) โ A x)
โ โ x ๊ X , ยฌ A x
not-ฮ -implies-โ-not {๐ค} {๐ฅ} {X} {A} em i f =
Cases (em E โ-is-prop)
id
(ฮป (u : ยฌ E)
โ ๐-elim (f (ฮป (x : X) โ EM-gives-DNE
(lower-EM ๐ค em)
(A x)
(i x)
(ฮป (v : ยฌ A x) โ u โฃ x , v โฃ))))
where
E = โ x ๊ X , ยฌ A x

\end{code}

Added by Tom de Jong in August 2021.

\begin{code}

not-ฮ -not-implies-โ : {X : ๐ค ฬ } {A : X โ ๐ฅ ฬ }
โ EM (๐ค โ ๐ฅ)
โ ยฌ ((x : X) โ ยฌ A x)
โ โ x ๊ X , A x
not-ฮ -not-implies-โ {๐ค} {๐ฅ} {X} {A} em f = EM-gives-DNE em (โ A) โฅโฅ-is-prop ฮณ
where
ฮณ : ยฌยฌ (โ A)
ฮณ g = f (ฮป x a โ g โฃ x , a โฃ)

\end{code}

Added by Martin Escardo 26th April 2022.

\begin{code}

Global-Choice' : โ ๐ค โ ๐ค โบ ฬ
Global-Choice' ๐ค = (X : ๐ค ฬ ) โ is-nonempty X โ X

Global-Choice : โ ๐ค โ ๐ค โบ ฬ
Global-Choice ๐ค = (X : ๐ค ฬ ) โ X + is-empty X

Global-Choice-gives-Global-Choice' : Global-Choice ๐ค โ Global-Choice' ๐ค
Global-Choice-gives-Global-Choice' gc X ฯ = cases id (ฮป u โ ๐-elim (ฯ u)) (gc X)

Global-Choice'-gives-Global-Choice : Global-Choice' ๐ค โ Global-Choice ๐ค
Global-Choice'-gives-Global-Choice gc X = gc (X + ยฌ X)
(ฮป u โ u (inr (ฮป p โ u (inl p))))
\end{code}

Global choice contradicts univalence.