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.