---
title: "L の内部における基数と符号化された単射"
module: L.Cardinal
lang: ja
site: "Bedrock"
description: "L の内部における基数と符号化された単射"
stage: "順序数，単射，基数"
reading_order: 89
canonical: https://bedrock.institute/ja/L.Cardinal.html
html: L.Cardinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Cardinal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Model, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Coding.Model, L.Coding.Injection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.Cardinal.md, https://bedrock.institute/zh/L.Cardinal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L の内部における基数と符号化された単射

`L` の内部で基数を論じるには、互いに関係する二種類の比較を区別する必要があります。ホストでは集合を提示する小さな型を実際の関数で比較できますが、`L` の内部で述べる主張は、それ自身が構成可能なグラフによって証されなければなりません。本章では両方の概念を展開し、それぞれの論理的な強さを明確に保ちます。具体的な関数とグラフの符号はデータを持ち、後で使う基数の比較は存在だけを保持します。

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

議論は基礎語彙の章で説明したホスト言語の中で行います。用いる古典的な原理は、`Type (ℓ-suc ℓ)` にある命題に対する排中律だけです。これは宇宙レベルで制限された仮定であり、無制限の排中律や選択原理ではありません。単射やグラフの符号の定義自体は証人を選びません。古典的な推論が働くのは、順序数の整列順序を構成するときと、後でその順序から最小元を得るときです。

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

そこで、宇宙レベルとこの排中律の実例を章全体のパラメータとして明示します。以下の構成はすべて同じ `lem` に相対しており、途中で別の公理を加えることはありません。ここでの目的は、後の基数論に必要な正確な概念と有界な順序を準備することです。基数代表や後続基数の存在を、この時点で主張するわけではありません。

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

以下では二つの数学的な場を同時に扱います。累積階層は周囲の集合と命題値の所属を与え、構成可能モデルは `L` に属する集合と、その上で解釈される関係を与えます。基本的な事実 `a ∈ sucV a` は、すべての集合が集合論的後続 `a ∪ {a}` に属すことを表し、後で有界な探索のための特定の点を与えます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( self∈sucV )
```

周囲の各集合には標準的な小さな提示もあります。そのインデックスは集合のすべての要素を名指し、`member` はインデックスを所属証明へ変え、`fiber` は所属からインデックスを復元します。順序対を使えば、集合で関係を表せます。構成可能な側では、モデルの要素は周囲の集合と、それが `L` に属すことの証明を組にしたものです。さらに `L` の推移性により、集合の構成可能性はその各要素へ受け継がれます。これらの事実が、小さな提示と構成可能なグラフの符号を結び付けます。

```agda
open import V.Presentation {ℓ} using ( member; fiber )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )
```

有界な探索には、順序数の所属が提示上に誘導する狭義の整列順序を使います。その三分性は最終的に `lem` を用い、整礎性は周囲の所属の正則性から得られます。ほかの材料は、一価性、正確な定義域、単射性というグラフの性質を対象言語で記述します。後で具体的なグラフの符号を命題的切り詰めによって隠すとき、順序に関する材料と論理式に関する材料を区別することが重要になります。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ} using ( SWO; module SWO )
open import L.Coding.Model {ℓ} using ( svAt; domAt )
open import L.Coding.Injection {ℓ} lem using ( injAt )
```

集合 `a` に対し、その要素を添字付ける小さな型を `⟪ a ⟫`、インデックスをそれが名指す要素へ送る写像を `⟪ a ⟫↪` と書きます。集合論的後続 `sucV a` は `a` のすべての要素と `a` 自身を含みます。したがって `a` が順序数なら、`⟪ sucV a ⟫` は、すべてのより小さい順序数を名指すインデックスと `a` を名指すインデックスを含む、小さな探索空間です。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

本書では、存在を命題的切り詰めによって意図的に弱めることがよくあります。`∥ X ∥₁` の要素は `X` に要素があることを主張しますが、具体的な要素は明らかにしません。反証を表す空型のような命題へは消去できますが、任意のデータへは消去できません。この規則により、後で `InjCode` に含まれる具体的なグラフの情報と、`InjL` が述べる単なる存在が厳密に区別されます。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
```

以下の記法は、主張がどちらの場に属すかを示します。周囲の構造では、`_∈ˢ_` は階層の生の集合どうしの命題値をもつ所属関係です。これに対して `S` は構成可能な構造の台であり、要素 `a : S` は、底にある周囲の集合 `fst a` と、その構成可能性を示す命題値の証明からなります。したがって `⟨ fst x ∈ˢ fst a ⟩` は底の周囲の集合に関するホスト側の命題であり、`x : S` 上の量化は構成可能集合だけにわたります。対象言語の構文は、以下で導入する充足関係を通して別に現れます。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )
```

構成可能な構造には、命題値をもつ点ごとの部分集合関係もあります。`⟨ a ⊆ˢ b ⟩` の証明は、各 `x : S` について、`x` が `a` に属するという証明を `x` が `b` に属するという証明へ送ります。したがって、その量化は構成可能な台にわたります。`L` の推移性により、これは底にある集合について通常の部分集合関係として読めます。`a` と `b` が順序数なら、これは両者の非狭義の順序です。そのため、後続基数の最小性は包含を結論とし、狭義の比較は所属で表します。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( _⊆ˢ_ )
```

充足の記号 `_⊨_` は、構成可能な構造における解釈を表すものとして固定します。判断 `γ ⊨ φ` では、環境 `γ` は `S` の要素を並べるため、`φ` の非有界量化子は構成可能集合にわたります。これが `InjCode` の最初の三条件の意味です。それらは `L` の内部で成り立つ対象言語の主張であり、その証明自体はホストで扱われます。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

まず、ホストレベルだけで単射を定義します。`X ↪ Y` の要素は関数 `f : X → Y` とその単射性の証明からなり、その証明は `f x` と `f y` の等しさから `x` と `y` の等しさが従うことを述べます。関数は具体的なデータなので、この対から射影できます。全射性や逆関数は含まれず、集合、構成可能性の証明、充足の判断、切り詰めもこの定義には現れません。後では、二つの周囲の集合を表す小さな提示型が典型的な始域と終域になります。

```agda
_↪_ : Type ℓ → Type ℓ → Type ℓ
X ↪ Y = Σ[ f ∈ (X → Y) ] ((x y : X) → f x ≡ f y → x ≡ y)
```

ここで、底にある集合が順序数である構成可能集合 `α` を固定します。後で必要な大きさの順序数を探すには、`sucV (fst α)` の標準的な提示の中で探索すれば十分です。この集合は `α` のすべての要素と `α` 自身を含むので、探索空間は小さな型であると同時に自然な始点を持ちます。ここでの定義が作るのは、この順序付けられた探索空間です。候補の述語を与えて最小元を選ぶのは後の議論です。

```agda
module LeastCardInjL (α : S) (oα : IsOrd (fst α)) where
```

最初に、この集合論的後続自身が `L` に属すことを示します。`oα` に順序数の後続を二度適用すると、`sucV (sucV (fst α))` が順序数だと分かります。順序数が次の構成可能な段階に属すという定理により、`sucV (fst α)` はこの明示された段階に入り、ある段階への所属からその構成可能性が得られます。したがって、この証明は後続を含む具体的な段階を示しており、構成可能性が一般に `sucV` について閉じているという性質を仮定してはいません。

```agda
  hSucα : ⟨ isL (sucV (fst α)) ⟩
  hSucα = Lset→isL (sucV (sucV (fst α))) (suc-ord (suc-ord oα)) (sucV (fst α))
            (ord∈Lset-suc (sucV (fst α)) (suc-ord oα))
```

提示の各インデックス `m` は `sucV (fst α)` の要素を名指します。この後続は構成可能であり、`L` は推移的なので、名指された要素も構成可能です。そこで `up` は、`m` が名指す底の集合を保ち、この事実から得た証明を添えて `S` の要素を作ります。この写像はこの有界な提示上だけで定義され、任意の周囲の集合を構成可能集合へ変えるものではありません。

```agda
  up : ⟪ sucV (fst α) ⟫ → S
  up m = ⟪ sucV (fst α) ⟫↪ m
       , isL-trans (member (sucV (fst α)) m) hSucα
```

順序数の所属によって、これらのインデックスを順序付けます。順序数 `sucV (fst α)` に `ordSWO` を適用すると、`⟪ sucV (fst α) ⟫` 上の狭義の整列順序 `w` が得られます。この比較は名指された集合どうしの所属に従い、三分性は `lem` に依存し、整礎性は正則性から従います。この値を不透明にする指定は、後の証明での展開を制御するだけであり、関係、その法則、あるいは法則が依存する仮定を変えません。

```agda
  opaque
    w : SWO (⟪ sucV (fst α) ⟫)
    w = ordSWO (sucV (fst α)) (suc-ord oα)
```

パス `w-lt` が、この順序の利用可能な記述を与えます。インデックス `m` と `n` に対し、`w` のもとで `m` が `n` に先行するという命題は、`m` が名指す集合が `n` の名指す集合に属すという命題と同一視されます。これは命題型どうしの等しさであり、集合どうしの等しさではありません。後の証明はこのパスに沿って、インデックスの比較と順序数の所属の間で証拠を両方向に移せます。その際、整列順序を展開する必要はありません。

```agda
  opaque
    unfolding w
    w-lt : (m n : ⟪ sucV (fst α) ⟫)
         → SWO._<∙_ w m n ≡ ⟨ ⟪ sucV (fst α) ⟫↪ m ∈ˢ ⟪ sucV (fst α) ⟫↪ n ⟩
    w-lt m n = refl
```

この探索空間には、`fst α` を名指す特定のインデックスがあります。証明 `self∈sucV (fst α)` は順序数がその集合論的後続に属すことを与え、`fiber` はその所属を、インデックスとその像を記述する等式の組へ変えます。階層の所属は命題値ですが、提示写像は埋め込みなので、そのファイバー自体が命題です。したがって選択原理を用いずに、切り詰めをこの一意なファイバーへ消去できます。`self` はこうして復元されたインデックスであり、順序数そのものではありません。

```agda
  self : ⟪ sucV (fst α) ⟫
  self = fiber (sucV (fst α)) (self∈sucV (fst α)) .fst
```

付随する等式は、`self` が何を名指すかを正確に述べます。提示写像によるその像は `fst α` に等しくなります。この等式は底にある周囲の集合どうしのものであり、対応する `S` の要素どうしの等しさまでは主張しません。後者には構成可能性の証明も同一視する必要があるからです。`self` と `self-eq` を合わせると、後の探索で `α` の性質を調べるための具体的なインデックスが得られます。

```agda
  self-eq : ⟪ sucV (fst α) ⟫↪ self ≡ fst α
  self-eq = fiber (sucV (fst α)) (self∈sucV (fst α)) .snd
```

## 内部の単射と後続基数

具体的な構成可能集合 `F` は、まず `L` の内部での三つの充足条件によって、`a` から `b` への単射を符号化します。第一の条件は、対の形をした項目が一価であること、つまり同じ入力が異なる二つの出力を持たないことを述べます。第二の条件は、定義域が正確に `a` であることを両方向に述べます。対の形をした各項目の第一成分は `a` に属し、`a` の各要素には出力が単に存在します。第三の条件はグラフの単射性、つまり出力が同じ二つの項目の入力が等しいことを述べます。三つの判断では、環境の第一項が `F`、第二項が `a` であり、すべての非有界量化子は `S` にわたります。

```agda
InjCode : S → S → S → Type (ℓ-suc ℓ)
InjCode F a b =
    ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩
```

第四の条件はホストで直接述べられます。任意の `x,y : S` に対し、底にある集合の順序対が底のグラフに属すなら、底にある出力は `b` に属します。したがって `b` は値の終域となる上界であり、`b` のすべての要素が値として取られるとは述べません。また `InjCode` は、`F` のすべての要素が順序対であるとも主張しません。その条件が調べるのは対の形をした要素だけなので、別の形をした余分な要素は符号から読み出される関数に影響しません。このホストレベルの値域条件は、先の三つの対象言語における充足の判断と区別する必要があります。

```agda
  × ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst b ⟩)
```

`InjL a b` は、四つの条件をどの具体的なグラフが満たすかを忘れます。これは `F` と `InjCode F a b` からなる依存対の命題的切り詰めなので、`L` の内部に `a` から `b` への符号化された単射が単に存在することだけを述べます。特定のグラフやホストレベルの関数を射影することはできません。これを局所的に開けるのは目標が命題である場合だけです。後で単射を合成したり変換したりする構成は、そのような枝の中でグラフを使い、得られたグラフを再び命題的切り詰めに入れます。向きも主張の一部であり、`InjL a b` だけから `InjL b a` は何も分かりません。

```agda
InjL : S → S → Type (ℓ-suc ℓ)
InjL a b = ∥ Σ[ F ∈ S ] InjCode F a b ∥₁
```

`κ` が順序数であるとき、基数性は始順序数であることによって表されます。von Neumann 順序数の各要素 `δ` はより小さい順序数であり、`IsCardinalL κ` は、`InjCode F κ δ` を満たす構成可能なグラフが存在するという命題的切り詰めを反証します。直前の記法で言えば、排除されるのは `InjL κ δ` であり、`InjL δ κ` ではありません。これらは内部の符号化された単射を表す命題であって、ホストレベルの型 `_↪_` の実例ではなく、その切り詰めから後者のホストレベルの単射を一般に取り出すこともできません。この定義は一般の構成可能集合についても形成でき、`κ` が順序数であるという証明を含みません。後の使用箇所では `IsOrd (fst κ)` を別に与えてから、始順序数として解釈します。反証の行き先は空型なので、必要となる命題的切り詰めの消去は正当です。

```agda
IsCardinalL : S → Type (ℓ-suc ℓ)
IsCardinalL κ =
  (δ : S) → ⟨ fst δ ∈ fst κ ⟩
          → (∥ Σ[ F ∈ S ] InjCode F κ δ ∥₁ → Empty.⊥)
```

`SuccCardL δ κ` の引数の順序では、`δ` が候補となる後続基数であり、`κ` がそれより下にある対象です。最初の三条件は、`δ` の底にある集合が順序数であること、`δ` が始順序数を表す述語を満たすこと、そして `κ ∈ δ`、すなわち順序数の文脈で `δ` が `κ` より真に大きいことを述べます。これらは与えられた対の性質を記述するだけで、そのような `δ` を作るものではなく、`κ` 自身が順序数や基数であることも要求しません。定義の最後の条件が、さらに大域的な最小性を加えます。ここに `sucV` は現れません。後続基数は集合論的後続 `κ ∪ {κ}` ではありません。

```agda
SuccCardL : S → S → Type (ℓ-suc ℓ)
SuccCardL δ κ =
    IsOrd (fst δ)
  × IsCardinalL δ
  × ⟨ fst κ ∈ fst δ ⟩
```

最後のフィールドは、`κ` より大きい内部順序数基数全体の中での最小性を表します。基礎集合が順序数で、`IsCardinalL c` を満たし、`κ` を含む任意の `c : S` を与えると、このフィールドは内部の包含 `δ ⊆ˢ c` を返します。第一のフィールドによって `δ` も順序数であることが分かっているので、ここで包含は順序数の非狭義の比較です。すなわち、`δ` はそのようなすべての `c` 以下です。結論が所属ではなく包含になっているのは、`c` が `δ` 自身である場合も扱う必要があるからです。`S` 上の量化と `_⊆ˢ_` はどちらも構成可能な台に対するものなので、これは `L` に見える候補の中での最小性です。このフィールドが `κ` について仮定するのは `κ ∈ c` だけです。`κ` 自身の順序数性と内部基数性は、この述語を用いる各定理で仮定されます。

このフィールドは単射のグラフを構成しません。`InjCode F a b` は特定の構成可能な符号 `F` と単射の四条件を保持しますが、`InjL a b` は `∥ Σ[ F ∈ S ] InjCode F a b ∥₁` という命題的切り詰めです。したがって、`IsCardinalL c` と `c` の順序数性を合わせた仮定は、`c` からその要素であるより小さな順序数への `InjL` 単射が存在しないことを述べます。`SuccCardL δ κ` 自体は、固定された対 `δ, κ` に関する切り詰められていない性質です。適切な `δ` の存在を証明せず、特定の `δ` も選びません。後の `succCardExists` は、`κ` が順序数である内部基数であり、有限順序数ではないとき、そのような `δ` の存在を命題的切り詰めの下で証明します。そこで用いる古典的仮定は、このモジュールのパラメータ `LEM (ℓ-suc ℓ)` だけです。集合論的後続 `sucV` はこの定義に現れません。

```agda
  × ((c : S) → IsOrd (fst c) → IsCardinalL c → ⟨ fst κ ∈ fst c ⟩
             → ⟨ δ ⊆ˢ c ⟩)
```