この章を読むか、対話型目次と依存グラフで別のルートを選べます。

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

module L.GCH.BelowSuccessorCardinal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

後続基数は、もとの基数を真に上回る最初の基数である。δ が L の中で κ の後続基数であると仮定する。本章では、任意の順序数 α ∈ δ から κ への内部単射があることを証明する。証明は整礎帰納法と順序数の三分法を組み合わせる。排中律には二つの明確な役割がある。順序数の三分法を与えることと、κ ∈ α の場合に、α が基数でないことを、より小さい行き先が単に存在するという形へ変えることである。

宇宙レベルを一つ固定し、階層で使われる命題のレベルにおける排中律を仮定する。この古典的仮定は明示され、そのレベルも正確に定められている。証明では、まず順序数の三分法を通して使い、後に Ex を表す論理式を判定するためにもう一度使う。残りの材料は V、L、順序数、内部単射についての構造的事実である。

議論は二つの構造の間を行き来する。周囲の階層は整礎的な所属関係とその非反射性を与え、構成可能宇宙は順序数と基数の述語を与える。順序数の三分法が現在の順序数と κ を比較し、包含の符号化と単射の推移性が内部単射を構成して合成する。

例外となる分岐が与えるのは、切り詰められた証人だけである。そのため、証明は和型と空型で判定を場合分けし、命題的切り詰めで単なる存在を表し、整礎帰納法で所属関係を降りる。これらの論理形式は、命題的に切り詰められた結論 InjL と一致する。

import Cubical.Induction.WellFounded as WF

open hPropView 𝒮ᵥ using ( _∈ˢ_ )

周囲の階層の論域を SV.S と書く。所属に関する帰納法はこの型の上で行われる。その要素は V の集合であり、この時点では L に属する証明をまだ伴わない。

module SV = hPropView 𝒮ᵥ using ( S )

構成可能宇宙の論域を SL.S と書く。その要素は、周囲の集合とその構成可能性の証明からなる依存対である。SuccCardL、IsCardinalL、InjL はいずれもこの論域の要素について述べる。

module SL = hPropView 𝒮ʟ using ( S )
module Sem = FOL.Semantics 𝒮ʟ
module At = Sem.At SL.S id

δ が κ の後続基数であり、順序数 α が δ に属すると仮定する。目標 InjL α κ は、α から κ への内部単射が単に存在することを述べる。これは、κ の後続基数より小さい順序数の濃度はすべて κ 以下である、という主張の正確な形である。

below-succ-injects :
    (κ δ : SL.S) → SuccCardL δ κ
  → (α : SL.S) → IsOrd (α .fst) → ⟨ α .fst ∈ˢ δ .fst ⟩
  → InjL α κ

整礎帰納法は α の基礎となる集合に施される。述語 P a は、周囲の集合 a を考察中の順序数とみなすために必要なデータ、すなわち構成可能性の証明、順序数であること、δ に属することをちょうど補う。これらの仮定のもとで、(a , la) から κ への内部単射を要求する。

below-succ-injects κ δ (ordδ , _ , κ∈δ , least) α =
  WF.WFI.induction regularityV {P = P} step (α .fst) (α .snd)
  where
  P : SV.S → Type (ℓ-suc ℓ)
  P a = (la : ⟨ isL a ⟩) → IsOrd a → ⟨ a ∈ˢ δ .fst ⟩ → InjL (a , la) κ

κ ∈ δ であり δ が順序数なので、κ 自身も順序数である。したがって帰納段階では、a と κ の基礎となる集合に順序数の三分法を適用できる。帰納仮定は a の各要素で利用でき、これは三分法の第三の分岐が必要とするものである。

  ordκ : IsOrd (κ .fst)
  ordκ = mem-ord {A = δ .fst} ordδ (κ .fst) κ∈δ

  step : (a : SV.S) → (∀ a' → ⟨ a' ∈ˢ a ⟩ → P a') → P a
  step a ih la orda a∈δ = go (ord-tri a orda (κ .fst) ordκ)
    where

周囲の集合 a と証明 la を対にして、L の対応する要素 α' を得る。これにより、整礎帰納法は単純な論域 SV.S 上で行いながら、濃度に関する主張は本来の論域 SL.S で述べられる。

    α' : SL.S
    α' = a , la

κ ∈ a の分岐を考える。もし α' が L-基数なら、SuccCardL δ κ の最小性により δ は α' に含まれる。a ∈ δ なので a ∈ a が従い、所属の非反射性に反する。したがってこの分岐では α' は基数ではありえない。

型 Ex は、ここで必要な非基数性を肯定的に表す。すなわち、α' が内部単射するような γ ∈ α' が単に存在する、という主張である。

    not-card : ⟨ κ .fst ∈ˢ a ⟩ → IsCardinalL α' → ⊥₀
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

    Ex : Type (ℓ-suc ℓ)
    Ex = ∥ Σ[ γ ∶ SL.S ] (⟨ γ .fst ∈ˢ a ⟩ × InjL α' γ) ∥₁

    exFo : Formula SL.S 1
    exFo = ∃̇ ((var zero ∈̇ var (suc zero))
             ∧̇ injLAt (suc zero) zero)

    exFill : Ex → ⟨ (α' ∷ []) At.⊨ exFo ⟩
    exFill = map₁ (λ { (γ , γ∈a , inj) → γ , γ∈a
      , InjLAt.fill (suc zero) zero (γ ∷ α' ∷ []) inj })

    exRead : ⟨ (α' ∷ []) At.⊨ exFo ⟩ → Ex
    exRead = map₁ (λ { (γ , γ∈a , sat) → γ , γ∈a
      , InjLAt.read (suc zero) zero (γ ∷ α' ∷ []) sat })

    exDecision : Dec Ex
    exDecision = mapDec exRead (λ ns e → ns (exFill e))
      (FOL.Semantics.decideSatisfaction 𝒮ʟ id lem (α' ∷ []) exFo)

論理式 exFo は候補 γ を束縛し、γ ∈ α' と論理式 injLAt α' γ を連言して、ちょうど Ex を表す。写像 exFill と exRead が命題的切り詰めのもとで両方向を証明する。その後、decideSatisfaction を通してこの論理式に排中律を適用する。充足するなら必要な単なる証人があり、反証されるなら任意の要素と単射が矛盾を導く。これは α' が基数であるという条件にほかならない。

    some-γ : ⟨ κ .fst ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide exDecision
      where
      decide : Dec Ex → Ex

反証の分岐は not-card と矛盾するため、どちらの結果からも Ex が得られる。この段階で排中律が与えるのは場合分けである。切り詰めを取り除くことも、特定の γ を選ぶこともない。

      decide (yes e) = e
      decide (no ¬e) =
        ⊥₀-rec (not-card κ∈a (λ γ γ∈a inj → ¬e ∣ γ , γ∈a , inj ∣₁))

Ex の切り詰め前の内容は、γ ∈ a と α' から γ への内部単射からなる。順序数の要素は順序数であり、δ は推移的なので、γ は再び帰納述語を満たす。帰納仮定が γ から κ への単射を与え、内部単射の推移性が二つを合成する。

    from-γ : Σ[ γ ∶ SL.S ] (⟨ γ .fst ∈ˢ a ⟩ × InjL α' γ) → InjL α' κ
    from-γ (γ , γ∈a , α↪γ) =
      injl-trans α' γ κ α↪γ

γ で帰納仮定を使うには、P の三つの条件をすべて与える。構成可能性は γ の第二成分であり、順序数であることは γ ∈ a と a の順序数性から従い、δ への所属は γ ∈ a ∈ δ と順序数 δ の推移性から従う。

        (ih (γ .fst) γ∈a (γ .snd)
            (mem-ord {A = a} orda (γ .fst) γ∈a)
            (ordδ .fst γ∈a a∈δ))

三分法の第一の分岐は a ∈ κ である。順序数は推移的なので、a の各要素は κ の要素でもある。この包含を符号化すれば、α' から κ への内部単射が得られる。

    go : Tri a (κ .fst) → InjL α' κ
    go (inl a∈κ)       =
      inclusion-coded α' κ (λ z z∈a → ordκ .fst z∈a a∈κ)

等しい場合には、a ≡ κ .fst に沿って同じ包含を移送すれば、必要な単射が得られる。残る κ ∈ a の場合には、先に得た切り詰められた証人を InjL α' κ へ消去する。InjL 自身が命題なので、この消去は正当である。

    go (inr (inl e))   =
      inclusion-coded α' κ (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) e z∈a)
    go (inr (inr κ∈a)) = rec₁ squash₁ from-γ (some-γ κ∈a)

これで順序数の三分法の三つの分岐がすべて閉じる。したがって、後続基数 δ より小さい任意の順序数は、その基数 κ へ内部単射する。所属の整礎性により、証明は γ へ降りられる。排中律は二箇所で使われる。ord-tri が三分法を得る箇所と、κ より上の分岐が切り詰められた小さい行き先を得る箇所である。

後続基数より小さい順序数をその基数へ単射する