Martin Escardo, 2-4 May 2022 Roughly, we show that, for any family β of ordinals indexed by ordinals, EM → sup β ⊴ ∑ β → WEM where EM is the principle of excluded middle and WEM is the weak principle of excluded middle (excluded middle for negated propositions). The problem is that the sum doesn't always exist constructively. So we need a more precise formulation of the above, which we give below. We assume univalence in this module, which is needed for the development of the large ordinal of small ordinals, and, in particular, the ordering _⊴_ between ordinals and its properties. Other local assumptions belonging to HoTT/UF are discussed below. \begin{code} {-# OPTIONS --safe --without-K #-} open import UF.Univalence module Ordinals.SupSum (ua : Univalence) where open import MLTT.Spartan open import Notation.CanonicalMap open import Ordinals.Equivalence open import Ordinals.Maps open import Ordinals.OrdinalOfOrdinals ua open import Ordinals.OrdinalOfOrdinalsSuprema ua open import Ordinals.Type open import Ordinals.Underlying open import UF.ClassicalLogic open import UF.FunExt open import UF.PropTrunc open import UF.Size open import UF.Subsingletons open import UF.UA-FunExt private fe : FunExt fe = Univalence-gives-FunExt ua fe' : Fun-Ext fe' {𝓤} {𝓥} = fe 𝓤 𝓥 pe : PropExt pe = Univalence-gives-PropExt ua open import Ordinals.Arithmetic fe \end{code} Our construction of suprema of families of ordinals needs the assumption of set quotients, or, equivalently, propositional truncations and set replacement. But because the existence of propositional truncations follows from excluded middle, which we assume for our next theorem, we only need to assume set replacement to formulate the next theorem, in addition to excluded middle. Also, sums of ordinal-indexed families of ordinals don't always exist (see the module OrdinalsShulmanTaboo). They do exist, for example, for ordinals with a largest element (which, constructively, are not necessarily limit ordinals), or for all ordinals if we assume the principle of excluded middle. \begin{code} module sup-bounded-by-sum-under-em {𝓤 : Universe} (em : Excluded-Middle) (sr : Set-Replacement (fe-and-em-give-propositional-truncations fe em)) where open sums-assuming-EM (em {𝓤}) open suprema (fe-and-em-give-propositional-truncations fe em) sr sup-bounded-by-sum : (α : Ordinal 𝓤) (β : ⟨ α ⟩ → Ordinal 𝓤) → sup β ⊴ ∑ α β sup-bounded-by-sum α β = sup-is-lower-bound-of-upper-bounds β (∑ α β) bound where bound : (x : ⟨ α ⟩) → β x ⊴ ∑ α β bound x = ≼-gives-⊴ (β x) (∑ α β) m where f : ⟨ β x ⟩ → ⟨ ∑ α β ⟩ f y = x , y fop : is-order-preserving (β x) (∑ α β) f fop y z l = inr (refl , l) m : β x ≼ ∑ α β m = order-preserving-gives-≼ em (β x) (∑ α β) (f , fop) \end{code} We also formulate the following immediate consequence for use in another module, where Ordinalᵀ 𝓤 is the type of topped ordinals in the universe 𝓤, that is, the ordinals that have a largest element. \begin{code} open import Ordinals.ToppedType fe open import Ordinals.ToppedArithmetic fe renaming (∑ to ∑ᵀ) sup-bounded-by-sumᵀ : (τ : Ordinalᵀ 𝓤) (υ : ⟨ τ ⟩ → Ordinalᵀ 𝓤) → sup (λ x → [ υ x ]) ⊴ [ ∑ᵀ τ υ ] sup-bounded-by-sumᵀ τ υ = sup-bounded-by-sum [ τ ] (λ x → [ υ x ]) \end{code} This is the end of the anonymous module that assumes the principle of excluded middle. We now prove a weak converse of this consequence, namely that weak excluded middle follows from the assumption that sups are bounded by sums of topped-ordinals indexed by topped-ordinals. In order to formulate this, we need to speak of suprema, which are available if we assume propositional truncations and set replacement (or, equivalently set quotients). \begin{code} module _ {𝓤 : Universe} (pt : propositional-truncations-exist) (sr : Set-Replacement pt) where open import Ordinals.ToppedType fe open import Ordinals.ToppedArithmetic fe open suprema pt sr sup-bounded-by-sum-gives-WEM : ({𝓤 : Universe} (τ : Ordinalᵀ 𝓤) (υ : ⟨ τ ⟩ → Ordinalᵀ 𝓤) → sup (λ x → [ υ x ]) ⊴ [ ∑ τ υ ]) → {𝓤 : Universe} → WEM 𝓤 sup-bounded-by-sum-gives-WEM ϕ {𝓤} = γ where open import Ordinals.OrdinalOfTruthValues fe 𝓤 (pe 𝓤) open Omega (pe 𝓤) open import Ordinals.ArithmeticProperties ua τ = 𝟚ᵒ υ : ⟨ 𝟚ᵒ ⟩ → Ordinalᵀ (𝓤 ⁺) υ = cases (λ ⋆ → 𝟙ᵒ) (λ ⋆ → Ωᵒ) l : sup (λ x → [ υ x ]) ⊴ [ ∑ τ υ ] l = ϕ τ υ m : Ωₒ ⊴ sup (λ x → [ υ x ]) m = sup-is-upper-bound (λ x → [ υ x ]) (inr ⋆) o : Ωₒ ⊴ [ ∑ τ υ ] o = ⊴-trans Ωₒ (sup (λ x → [ υ x ])) [ ∑ τ υ ] m l p : [ ∑ τ υ ] ＝ (𝟙ₒ +ₒ Ωₒ) p = alternative-plus 𝟙ᵒ Ωᵒ q : Ωₒ ⊴ (𝟙ₒ +ₒ Ωₒ) q = transport (Ωₒ ⊴_) p o γ : WEM 𝓤 γ = ⊴-add-taboo q \end{code} Added 21st May 2022. Unfortunately, the above is not very useful in the generality it is proved. The reason is that in other modules we have sups and sums constructed under different assumptions, and although the assumptions are propositions and hence we can transport using propositional extensionality, this becomes to cumbersome to even write down, let alone prove. Hence we will repeat the above (short) code with the two assumptions we need. \begin{code} module _ {𝓤 : Universe} (em : Excluded-Middle) (pt : propositional-truncations-exist) (sr : Set-Replacement pt) where open suprema pt sr open import Ordinals.ToppedType fe open import Ordinals.ToppedArithmetic fe sup-bounded-by-sumᵀ : (τ : Ordinalᵀ 𝓤) (υ : ⟨ τ ⟩ → Ordinalᵀ 𝓤) → sup (λ x → [ υ x ]) ⊴ [ ∑ τ υ ] sup-bounded-by-sumᵀ τ υ = γ where bound : (x : ⟨ τ ⟩) → [ υ x ] ⊴ [ ∑ τ υ ] bound x = ≼-gives-⊴ [ υ x ] [ ∑ τ υ ] m where f : ⟨ υ x ⟩ → ⟨ ∑ τ υ ⟩ f y = x , y fop : is-order-preserving [ υ x ] [ ∑ τ υ ] f fop y z l = inr (refl , l) m : [ υ x ] ≼ [ ∑ τ υ ] m = order-preserving-gives-≼ em [ υ x ] [ ∑ τ υ ] (f , fop) γ : sup (λ x → [ υ x ]) ⊴ [ ∑ τ υ ] γ = sup-is-lower-bound-of-upper-bounds (λ x → [ υ x ]) [ ∑ τ υ ] bound open import Ordinals.TrichotomousType fe open import Ordinals.TrichotomousArithmetic fe sup-bounded-by-sum₃ : (τ : Ordinal₃ 𝓤) (υ : ⟨ τ ⟩ → Ordinal₃ 𝓤) → sup (λ x → [ υ x ]) ⊴ [ ∑³ τ υ ] sup-bounded-by-sum₃ τ υ = γ where bound : (x : ⟨ τ ⟩) → [ υ x ] ⊴ [ ∑³ τ υ ] bound x = ≼-gives-⊴ [ υ x ] [ ∑³ τ υ ] m where f : ⟨ υ x ⟩ → ⟨ ∑³ τ υ ⟩ f y = x , y fop : is-order-preserving [ υ x ] [ ∑³ τ υ ] f fop y z l = inr (refl , l) m : [ υ x ] ≼ [ ∑³ τ υ ] m = order-preserving-gives-≼ em [ υ x ] [ ∑³ τ υ ] (f , fop) γ : sup (λ x → [ υ x ]) ⊴ [ ∑³ τ υ ] γ = sup-is-lower-bound-of-upper-bounds (λ x → [ υ x ]) [ ∑³ τ υ ] bound \end{code}