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.