---
title: "集合と交わる最初の段階"
module: L.Choice.FirstIntersectionStage
lang: ja
site: "Bedrock"
description: "集合と交わる最初の段階"
stage: "正準整列順序と選択公理"
reading_order: 72
canonical: https://bedrock.institute/ja/L.Choice.FirstIntersectionStage.html
html: L.Choice.FirstIntersectionStage.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/FirstIntersectionStage.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Axioms.Basic]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.Choice.FirstIntersectionStage.md, https://bedrock.institute/zh/L.Choice.FirstIntersectionStage.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 )
```

本章は、内部の選択の構成のための二つの材料を提供する。第一は最小段階についての補題である。順序数の性質がはじめて成立するとき、それは最小の段階で成立する。その段階が後者であるかどうかは自動ではない。性質は零順序数ではじめて成立するかもしれないからである。本章は、議論に必要な条件付きの形を証明する。最小の段階のほかに、切り出しが単に存在するならば、すなわちその下の順序数 `δ` で、後者 `sucV δ` ですでに性質が成立しているならば、最小の段階は後者であり、一意な直前の段階をもつ。第二の材料は上界の順序数である。構成可能な集合に対し、その集合、その要素、その要素の要素、そして塔の極限段階を同時に含む一つの順序数がある。

この材料に仕えるのは、二つの鍵による比較である。異なる段階ではじめて現れた二つの集合は、誕生の順序数だけによって比較され、それ以外の何ものによっても比較されない。同じ段階ではじめて現れた集合どうしだけが、その段階の中の名前によって比較される。第一の材料は、それぞれの誕生の順序数を、単なる存在ではなく確定した対象にする。第二の材料は、候補の族全体が必要とする材料が一つの段階の中に住むことを保証し、名前の比較に共通の場を与える。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
```

本章は一つの仮定のもとで進む。モデルのレベルの後続での排中律の実例であり、以下の主張はすべてその設定の中でなされる。

本章の問いは、はじめての出現についてのものである。構成可能な集合は、いつか塔に入る。塔の住む周囲の階層は反射しない所属をもち、だからどの順序数も自分自身を含まず、後者の性質も分かっている。順序数は自分の後者の中に坐り、後者の要素はその順序数の要素か、その順序数自身のどちらかである。

構成可能の側は、塔 `Lset` で答える。塔は順序数で添字づけられ、順序数は階層の集合であり、ホストの宇宙レベルではない。順序数性 `IsOrd` はそれ自体命題であり、塔には層の関係、外向きの分解、単調性があり、推移性が層の間で要素を運ぶ。

議論を支えるのは、比較と段階である。段階の下の順序数を段階そのものと比べることが、その段階がある後者を行き過ぎていないかの判定である。順序数の要素も後者もまた順序数である。各構成可能集合はその最初の順序数を携え、順序数性と所属とともに渡され、極小性は反駁として述べられる。二つの順序数には共通の上界がある。そして後者の恒等式は、次の段階がちょうど前の段階の定義可能な部分集合であると言う。何ものかが塔に入るのは、まさにこの一歩によってである。

議論は三つの命題の動きで書かれる。場合への分裂、空型で終わる反駁、そして存在することがだけ分かっている存在である。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
```

直前の段階は、順序数と命題的な証拠との対である。この種の対は第一成分で決まり、累積階層自身も集合なので、直前の段階の等しさは順序数成分の等しさに帰着する。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )
```

階層の無限の構成は、フォン・ノイマンの後者 `sucV` と、上界に含める極限段階 `ω` の両方を与える。

```agda
open hPropView 𝒮ᵥ
```

構造の所属 `∈ˢ` は、順序数性も段階も極小性もその中で述べられる関係である。

## 最小段階の直前の段階

問いは、何かが現れる最小の段階が後者であるか、そしてどの段階を後者とするかである。最小の段階だけでは後者とは限らない。性質は零からはじまるかもしれないからである。構成が産出するのは、「下に切り出しがある」という追加の仮定のもとでの、一意な直前の段階である。

後者は、それが後者とするものを決める。少なくとも順序数の間ではそうである。候補の直前の段階を別のものと比べると、それぞれが相手の後者に属するので、それぞれは相手の要素か等しいかのどちらかであり、二つの順序数が互いに要素であることはあり得ない。推移性から一方が自分自身の要素になるからである。そこで、与えられた順序数の直前の段階であることは命題になり、これこそが、単に存在するだけの直前の段階を確定したものとして読める理由である。

最小の段階が直前の段階をもつには、二つの入力が要る。分けて見る価値がある。第一は最小の段階そのものである。性質が成立する順序数 `σ` であり、極小性は反駁として述べられる。より小さい順序数は性質をもたない、と。第二は `σ` での切り出しの単なる存在である。`σ` の下の順序数 `δ` で、その後者 `sucV δ` ですでに性質が成立しているもの。切り出しがあれば、極小性が「後者が厳密に下にとどまる」ことを排除し、行き過ぎない比較は一つの場合を残す。切り出された順序数の後者はちょうど `σ` である、と。ゆえに最小の段階は後者であり、切り出された順序数がその直前の段階である。切り出しなしには何も従わない。性質は零順序数ではじめて成立するかもしれず、零の下には順序数がそもそも存在しないからである。

```agda
IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)
```

順序数 `σ` の候補の直前の段階 `δ` とは、そのフォン・ノイマンの後者が `σ` 自身であるような順序数である。両方の半分が要る。順序数性は比較が使うものであり、等式は `δ` を `σ` に釘づけするものである。

```agda
private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → ⊥₀
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)
```

どの順序数も、自分の要素である順序数の要素にはなれない。推移性がこの所属を二歩の循環で `a` 自身へ運び、非反射性と衝突するからである。この二歩の不可能性こそ、二つの順序数が互いを含むことを禁じるものである。

```agda
  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → ⊥₀-rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)
```

所属の分岐はこう読む。`δ'` は `δ` の後者の要素であり、かつ `δ` は `δ'` の要素である。結論は `δ ≡ δ'` でなければならない。もし `δ'` が `δ` 自身の要素なら、二歩の循環が閉じてしまう。だから `δ'` は `δ` 自身であり、消去はまさにそれを返す。

```agda
ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')
```

後者の演算は順序数の上で単射である。後者の等式から、`δ` は `sucV δ'` の要素である。消去は二つの読みを示す。`δ` が `δ'` の要素なら、所属の分岐が循環を閉じて等式を与え、さもなくば `δ` ははじめから `δ'` である。後者は、それの後者とするものを決める。

```agda
  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')
```

消去に渡す二つの所属は、順序数が自分の後者の中に坐るという既存の事実から、等式とその逆向きに沿って輸送したものである。

```agda
isPropPredOf : (σ : S) → isProp (Σ[ δ ∶ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))
```

したがって、同じ順序数のどの二つの直前の段階も等しくなる。第一成分は単射性により一致し、残りのデータは命題なので、直前の段階の型全体が命題になる。これこそ、単に存在するだけの直前の段階を確定したものとして使える理由である。切り詰めを命題値の対象へほどくのは、つねに正当である。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module _ (P : S → hProp (ℓ-suc ℓ)) where
```

</summary>
<div class="submodule-fold-content">

最小段階の議論は、順序数の性質ごとに一度だけ書かれる。性質はパラメータであり、以下のどこでもその内側を読むことはない。

```agda
  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∶ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)
```

`σ` での切り出しとは、議論が動くデータである。`σ` より厳密に下の順序数 `δ` で、その後者がすでに性質を帯びているもの。切り出しが単に存在するだけでも、最小の段階が `δ` のはるか上にあることはあり得ない。性質はすでに `sucV δ` で成立しているからである。

```agda
  private
    below-case : (σ δ : S) → isLeastOrd P σ → IsOrd δ → ⟨ P (sucV δ) ⟩
               → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
    below-case σ δ least ordδ m s∈σ =
      ⊥₀-rec (least (sucV δ) (suc-ord ordδ) m s∈σ)
```

下の分岐は、後者が最小の段階より厳密に下にとどまる場合を扱う。極小性は反駁として述べられており、この分岐の仮定はその前提そのものなので、`least` がまず矛盾を与える。`⊥*-rec` がその矛盾を、この分岐が負うパス `sucV δ ≡ σ` へ消去する。

```agda
    same-case : (σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
    same-case σ δ e = e
```

等しい場合は何の仕事も要らない。この場合に渡されたのは、後者が最小の段階と等しいという同定そのものだからである。

```agda
    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∶ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)
```

`atCarve` は切り出しを確定した直前の段階に変える。証人 `δ` はそのまま残り、その順序数性は順序数 `σ` への所属から回復し、`sucV δ` を `σ` に釘づけする等式が場合分析の内容である。

```agda
      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ
```

`δ` の順序数性は順序数 `σ` から受け継がれる。順序数の要素は順序数だからである。

```agda
      suc≡σ : sucV δ ≡ σ
      suc≡σ = ⊎-rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)
```

`δ ∈ σ` のもとで、`suc∈or≡` はその後者に二つの可能性だけを残す。`σ` より厳密に下にとどまるか、`σ` と等しいかである。極小性が前者を退けるので、後者が必要な等式を与える。

```agda
  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∶ S ] IsPredOf σ δ
  predOf σ ordσ least = rec₁ (isPropPredOf σ) (atCarve σ ordσ least)
```

`predOf` は、存在することだけ分かっている切り出しを消費し、直前の段階を返す。切り詰められた入力は「直前の段階の型が命題である」という事実へ消去されるので、仮の切り出しの間で選択が行われることはない。切り詰めがどの切り出しを渡しても、答えは同じ確定した直前の段階である。

```agda
  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁
```

`carveAt` は、最小の段階の要素 `z` から切り出しを作る。そこには、`z` がどこかの後者の段階で現れるなら、性質はすでにそこで成立するという観察が伴う。これは塔への下降の形そのものである。段階への出現とは、より前の段階の定義可能冪集合の内側への出現であり、後者の恒等式により、どの定義可能冪集合も後者の段階である。

```agda
  carveAt σ z z∈Lσ k = map₁
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)
```

</div>
</details>

塔は `z` の所属を切り詰めた形で分解する。`σ` の下のある段階 `δ` で、`z` が `Lset δ` の定義可能冪集合の中にある、というものである。写像は切り詰めの内側だけで行われる。後者の恒等式を逆向きに読んで、`z` を `𝒟ₒ (Lset δ)` から `Lset (sucV δ)` へ運び、観察 `k` がその後者で発火し、できた切り出しが切り詰めへ注入し戻される。

## 集合の下方全体を収める一つの段階

この節では、段階の推移性と順序数の上界から、集合の要素、その要素の要素、そして極限段階 `ω` を同時に含む一つの層を得る。

構成にはもう一つ、上界が要る。それを得るのに比較は関わらない。段階は推移的であり、集合の段階はすでにその要素を、その次にはその要素の要素を収めている。最初の段階も他の段階と同じ段階なので、それで足りる。

もう一つ確定すべき順序数は、塔の極限段階である。先の比較は対象言語で書かれ、各アリティの無定数の論理式 `Formula ⊥* n` の符号は、いずれも `Lset ω` に属する。そのような符号は自由変数をもち得るので、これらは文ではなく論理式である。後者の段階の要素の完全な名前は、符号より多くを語る。アリティと、より前の段階から取ったパラメータのベクトルも名指すのである。ここで作る界が覆うのは符号のほうで、`ω ∈ β` と単調性が `Lset ω` を `Lset β` へ持ち上げる。パラメータが界の下にあるのは別の理由によるもので、次の事実がまさにそれを記録する。集合の要素とその要素の要素が同じ層に落ちる、と。

```agda
stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)
```

段階は推移的であり、`a` の最初の段階もまた段階である。だから `a` の要素 `x` は、塔の `a` 自身の段階での層の中にある。推移性が所属を、集合からその集合を収める層へ運ぶのである。

```agda
stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)
```

推移性を二度適用すれば、二層下まで届く。`a` の要素の要素も同じ層の中にある。それは `x` に属し、`x` はその層に属するからである。

```agda
stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∶ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)
```

支配されなければならない二つの順序数は、極限段階 `ω` と集合自身の最初の段階である。`bound2` は両方の上にある一つの順序数を、その順序数性の証明とともに返す。

```agda
bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)
```

塔の単調性が、二層下の事実を最初の段階から、界順序数の段階へ引き上げる。今や一つの層が、`a` とその要素、その要素の要素、そして比較が読む論理式の符号を同時に収める。

## まとめ

本章の再利用可能な成果は、最小段階が後者である場合のその一意な直前の段階と、選択の構成を支えるのに十分な上界順序数である。最小段階の補題は条件付きであり、その条件こそが内容である。順序数の性質の最小の段階を `σ` とすると、性質は零順序数ではじめて成立してもよく、そのときは下に切り出すべきものが何もない。`σ` での切り出しが単に存在するならば、すなわち `σ` の下の順序数で、その後者がすでに性質をもつものがあれば、`carveAt` がそれを作り、`predOf` が `isPropPredOf` で切り詰めを閉じて、それを一意な直前の段階に変える。後者がその後者とするものを決める理由は `ord-suc-inj` である。`stageBound` が上界の順序数を供給する。それは集合自身の段階の上にあり、したがってその要素やそのまた要素の上にあり、塔の極限段階、すなわち論理式の符号が住む段階の上にもある。