---
title: "後続基数より小さい順序数をその基数へ単射する"
module: L.GCH.BelowSuccessorCardinal
lang: ja
site: "Bedrock"
description: "後続基数より小さい順序数をその基数へ単射する"
stage: "GCH の証明"
reading_order: 108
canonical: https://bedrock.institute/ja/L.GCH.BelowSuccessorCardinal.html
html: L.GCH.BelowSuccessorCardinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/BelowSuccessorCardinal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Cardinal, L.DefinableInjection, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.BelowSuccessorCardinal.md, https://bedrock.institute/zh/L.GCH.BelowSuccessorCardinal.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

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

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

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

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Cardinal {ℓ} lem using ( InjL; SuccCardL; IsCardinalL )
open import L.DefinableInjection {ℓ} lem using ( injLAt; module InjLAt )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

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

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

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

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

```agda
import Cubical.Induction.WellFounded as WF

open hPropView 𝒮ᵥ using ( _∈ˢ_ )
```

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

```agda
module SV = hPropView 𝒮ᵥ using ( S )
```

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

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

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

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

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

```agda
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` の各要素で利用でき、これは三分法の第三の分岐が必要とするものである。

```agda
  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` で述べられる。

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

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

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

```agda
    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` を通してこの論理式に排中律を適用する。充足するなら必要な単なる証人があり、反証されるなら任意の要素と単射が矛盾を導く。これは `α'` が基数であるという条件にほかならない。

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

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

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

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

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

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

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

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

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

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

```agda
    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` が三分法を得る箇所と、`κ` より上の分岐が切り詰められた小さい行き先を得る箇所である。