---
title: "構成可能階層と構成可能宇宙"
module: L.Constructible
lang: ja
site: "Bedrock"
description: "構成可能階層と構成可能宇宙"
stage: "構成可能段階と公理"
reading_order: 25
canonical: https://bedrock.institute/ja/L.Constructible.html
html: L.Constructible.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Constructible.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Definability]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Constructible.md, https://bedrock.institute/zh/L.Constructible.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
```

本章は固定した宇宙レベル `ℓ` で累積階層 V の内部を扱う。その台 `S` は、外延的で整礎的な所属関係をもつ集合からなる。対応する構造では等式と所属を命題値の関係として読み、`⟨ x ∈ˢ A ⟩` のような式は通常の所属証明の型を表す。以下の構成はこの環境で行う。

```agda
module L.Constructible {ℓ : Level} where
```

```agda
open import FOL.ZFStructure using ( ZFStructureₕ; _↾_; module hPropView )
open import FOL.Syntax using ( Formula )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( union-family-in; union-family-out )
open import L.Definability {ℓ} using ( module DefOf )
```

構成可能階層は空集合から始まり、定義可能冪集合を繰り返し施し、極限点では和集合を取る。できあがる各段階は推移的で、塔は添字の所属に沿って単調である。いくつかの段階に現れる集合の全体がクラス `L` を与え、周囲の構造をそこへ制限した集合論的構造が伴う。

この章の仕事の大部分は、ひとつの設計判断が担う。塔の添字には独立した順序数の型ではなく**集合そのもの**を使い、正則性公理が許す所属に沿った再帰で進める。つまり `Lset α = ⋃ { Def (Lset β) ∣ β ∈ α }` である。このただ一本の等式が零・後者・極限を同時にカバーし、フォン・ノイマン順序数の上ではまさにゲーデルの塔になる。定義そのものは任意の集合を添字として受け入れ、添字が順序数であるという要求は、クラス `L` を定義する場所で初めて課される。これと並行して帰納的述語 `isLayer`、すなわち「段階であること」が走る。その構成子こそ塔の閉包原理であり、二つの見方は章全体で協調する。

構成を進める数学的な材料は三つある。第一に、所属に沿った整礎再帰である。階層の章の原理 `∈-induction` は、`∈ˢ` に沿った再帰で集合上の関数を定義することを可能にし、塔そのものがまさにこれで定義される。第二に、添字族の和集合と、その和への所属を両方向に読む二つのモデル補題である。第三に、定義可能性の章の演算子 `Def A` であり、内側の世界 `(A, ∈)` で `A` のパラメータによって定義される `A` の部分集合を集めるもので、これを段階ごとに施すことが階層を上へ伸ばす原動力になる。一階述語論理式の構文、とりわけ型 `Formula` は、まさにこの演算子のために構文の章から引き継がれる。

階層の集合は小さな族によって表現され、本章はその表現を通して要素を読む。集合 `α` に対して `⟪ α ⟫` はその要素の小さな添字型であり、`⟪ α ⟫↪` は添字をふたたび集合へ埋め込み、`∈ₛ⟪ α ⟫↪ m` は `m` の指す要素が `α` に属することを証明する。橋渡し `∈∈ₛ` は階層固有の所属 `∈` と構造的な所属 `∈ˢ` を双方向に結び、`sett X f` は `X` 上の `f` の値を要素とする集合を作る。これらと並んで、命題的切り詰め `∥ _ ∥₁` とその導入 `∣ _ ∣₁` が「単に存在する」を与える。切り詰められた主張の要素は、証人が存在すると主張するのであって、それを名指しはしない。

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

基本の構成は所属の特徴づけとともに使える。空集合には `∅-empty`、非順序対には `pairing-ax`、二項和と添字族の和には `union-ax` が対応する。レベル `ℓ-suc ℓ` の命題が真理値を直接与える。`hPropView 𝒮ᵥ` を開くと、周囲の構造のフィールドが使えるようになる。`∈ˢ` は所属の命題を与え、`∈ᵗ` はその証明の基礎型を取り出す。本章のすべての主張はこの命題値の設定のなかで述べられる。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; _∪_ )
```

設定が整ったところで、定義可能冪集合の演算子に作業用の名前が与えられる。`𝒟 A` は定義可能性の章の `Def A` そのものであり、制限構造の上で `A` の有限個のパラメータによって定義される `A` の部分集合を集めたものである。この演算子の数学的内容、すなわちその要素がすべて `A` の部分集合であることや、推移的な `A` に対して `A ⊆ 𝒟 A` が成り立つことは、すでにそこで確立済みであり、ここでは本書を通して使われる短い記号を与えるだけである。

```agda
open hPropView 𝒮ᵥ

𝒟 : S → S
𝒟 A = DefOf.Def A
```

## 推移的集合

階層の各段階は推移的である。空集合は推移的であり、定義可能冪集合は推移性を保存し、推移的集合の和も推移的である。これらの閉性は、後で層を作る構成子に一つずつ対応する。

(`𝒟` は前の章の `Def` に対する本書の短い記号で、この演算子に慣用される花文字に合わせたものである。)

集合 `A` が推移的であるとは、`A` の要素の要素が再び `A` の要素になることである。定義 `isTransV` は構造レベルの閉性条件 `Transitive` を「`A` と等しい集合のクラス」に具体化したものであり、したがって `isTransV A` の証明は文字どおり、`y ∈ˢ x` と `x ∈ˢ A` から `y ∈ˢ A` を与える関数である。宇宙に注意してほしい。この主張は台を量化するので `ℓ-suc ℓ` に存在する。推移性は命題であり、`isPropIsTransV` がこれを直接示する。二つの証明 `p` と `q` が与えられれば、その結論 `y ∈ˢ A` は構成により命題なので各点で一致し、立方の関数外延性がこの各点一致を `p` と `q` の間のパスへ組み立てる。最後の行は、空集合についての最初の閉性事実を宣言している。

```agda
isTransV : S → Type (ℓ-suc ℓ)
isTransV A = Transitive (λ x → x ∈ˢ A)

isPropIsTransV : (A : S) → isProp (isTransV A)
isPropIsTransV A p q i {x} {y} y∈x x∈A = ⟨ y ∈ˢ A ⟩isProp (p y∈x x∈A) (q y∈x x∈A) i

∅-trans : isTransV ∅
```

空集合の場合は空虚に成り立つ。`x ∈ˢ ∅` から `∈∈ₛ` を経て `∅` の本来の要素が取り出せ、`∅-empty` がそこから矛盾を導くので、`y ∈ˢ A` へ至る任意の含意が成り立つ。定義可能冪集合については、前の章の二つの補題を組み合わせる。`𝒟 A` の要素 `x` は定義可能な部分集合なので、`y ∈ x` なら `y ∈ A` が強制され (`Def∋⊆A`)、これに推移性の仮定 `Atr` を適用すれば、推移的な `A` に対する `A ⊆ 𝒟 A` (`A⊆Def`) によって `y` は `𝒟 A` に入る。最後に `⋃-trans` が和の原理を述べる。`x` の各要素が推移的ならば、`x` の要素の要素全体の集合 `⋃ x` も推移的である。

```agda
∅-trans {x} y∈x x∈∅ = ⊥₀-rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅))

𝒟-trans : ∀ {A} → isTransV A → isTransV (𝒟 A)
𝒟-trans {A} Atr {x} {y} y∈x x∈𝒟A =
  DefOf.Refine.A⊆Def A Atr y (DefOf.Def∋⊆A A x x∈𝒟A y y∈x)

⋃-trans : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isTransV y) → isTransV (⋃ x)
```

和の要素を見るには、まずそれが実際に要素であることを見なければならない。仮定 `u∈⋃x` は周囲の階層における所属であり、`∈∈ₛ` の第二の向きがそれを切り詰められたファイバー形式へ変換する。そして `union-ax` がその所属を特徴づける。すなわち `u ∈ ⋃ x` となるのは、`u ∈ w` なる `w ∈ x` が単に存在するとき、そしてそのときに限る。命題的切り詰めは本質的である。公理は途中の `w` を名指しせず、その存在を主張するだけだからである。したがって証明は切り詰めの内部で写像を行い、対 `w , (w∈ₛx , u∈ₛw)` が与えられる分岐では、二度の `∈∈ₛ` がファイバーのデータから使える仮定 `w∈x` と `u∈w` を復元する。

```agda
⋃-trans x mem {u} {v} v∈u u∈⋃x =
  ∈∈ₛ {a = v} {b = ⋃ x} .snd (union-ax x v .snd
    (map₁
      (λ { (w , (w∈ₛx , u∈ₛw)) →
        let w∈x = ∈∈ₛ {a = w} {b = x} .snd w∈ₛx
```

この分岐では、仮定 `mem w w∈x` が `w` の推移性を言うので、`v ∈ u` と `u ∈ w` から `v ∈ w` が得られる。第一の向きの `∈∈ₛ` で改めて変換すると、このデータは `union-ax` の正当なファイバーになり、命題的切り詰めの消去も、目標である「`v` の `⋃ x` への所属」が命題であるため正当である。二項和はこれに続く。`A ∪ B` は `⋃ ⁅ A , B ⁆` と定義されるので、`∪-trans` はこの対への `⋃-trans` の適用であり、残る義務は対の各要素が推移的であることで、これを供給するのが局所的な主張 `prem` である。

```agda
            u∈w = ∈∈ₛ {a = u} {b = w} .snd u∈ₛw
        in w , (w∈ₛx , ∈∈ₛ {a = v} {b = w} .fst (mem w w∈x v∈u u∈w)) })
      (union-ax x u .fst (∈∈ₛ {a = u} {b = ⋃ x} .fst u∈⋃x))))

∪-trans : ∀ {A B} → isTransV A → isTransV B → isTransV (A ∪ B)
∪-trans {A} {B} tA tB = ⋃-trans ⁅ A , B ⁆ prem
```

義務 `prem` が問うのは、対の各 `y` が推移的かどうかである。対の所属は「単に」の形で特徴づけられる。すなわち `y ∈ ⁅ A , B ⁆` となるのは、`y` が `A` であるか `y` が `B` であることが単に成り立つときであり、選ばれた選言肢ではなく命題的切り詰めによって与えられる。消去の目標は命題 `isTransV y` であり、各分岐は `y` を `A` ないし `B` と同一視する等式 `p` を伴う。推移性は集合の等しさで不変なので、`subst isTransV (sym p)` が既知の証明 `tA` ないし `tB` をその等式に沿って型 `isTransV y` へ輸送する。

```agda
  where
  prem : (y : S) → ⟨ y ∈ˢ ⁅ A , B ⁆ ⟩ → isTransV y
  prem y y∈ = rec₁ (isPropIsTransV y)
    (λ { (inl p) → subst isTransV (sym p) tA
       ; (inr p) → subst isTransV (sym p) tB })
```

`prem` の最後の行が命題的切り詰めされた所属を `pairing-ax` に通して場合分けを完成させ、二項の場合が終わる。族の形式 `setUnion-trans` は小さな添字族を一度に扱う。型 `X : Type ℓ` と関数 `f : X → S` が与えられれば、集合 `sett X f` の要素は値 `f x` であり、各 `f x` は仮定により推移的である。ここでも添字集合への所属は命題的切り詰めされており、証明が受け取るのは対 `x , fx≡y`、すなわち添字と、その値を `y` と同一視するパスである。

```agda
    (pairing-ax A B y .fst (∈∈ₛ {a = y} {b = ⁅ A , B ⁆} .fst y∈))

setUnion-trans : (X : Type ℓ) (f : X → S) → ((x : X) → isTransV (f x))
               → isTransV (⋃ (sett X f))
setUnion-trans X f hf = ⋃-trans (sett X f)
  (λ y → rec₁ (isPropIsTransV y)
```

ここでも輸送が帳簿づけを担う。`subst isTransV fx≡y (hf x)` は `f x` の推移性の証明を同一視に沿って `y` へ移し、`isTransV y` が命題であるため命題的切り詰めの消去が許される。これで閉包原理、空集合、定義可能冪集合、そして一般・二項・添字付きの三形態の和、がそろった。以下で証明する、すべての層が推移的であることの帰納は一行の振り分けとなり、各構成子がここで証明した対応する補題と結ぶ。

```agda
    (λ { (x , fx≡y) → subst isTransV fx≡y (hf x) }))
```

## 順序数の述語

構成可能階層の添字として働くのはフォン・ノイマン順序数であり、整礎で外延的な宇宙の内部では、古典的な定義はわずかなものに縮む。すなわち**順序数**とは、推移的な集合からなる推移的な集合である。整礎性と外延性は定義に書き込む必要がない。階層が至る所でそれらを保証するからである。線形性は後の章で証明される古典的な定理であって、概念そのものの一部ではない。この章ではこの述語とその命題性を記録し、順序数の理論は必要になったときに専用の章で展開される。

したがって `IsOrd A` は二つの命題の積である。`A` が推移的であり、かつ `A` の各要素が推移的である、という二つである。`isPropIsOrd A` は、命題が積と依存関数に関して閉じていることを使い、両成分の命題性を合わせる。この証明書は `isL` の定義で明示的に使われ、`(IsOrd α , isPropIsOrd α)` が「段階の添字は順序数である」という真理値を与える。

```agda
IsOrd : S → Type (ℓ-suc ℓ)
IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x)

isPropIsOrd : (A : S) → isProp (IsOrd A)
isPropIsOrd A = isProp× (isPropIsTransV A)
                  (isPropΠ λ x → isPropΠ λ _ → isPropIsTransV x)
```

## 層

`isLayer A` は塔の閉包性を五つの構成子で記録する。空集合は層であり、層に `𝒟` を適用したものも層である。和集合については、要素がすべて層である集合、二つの層、小さく添字付けられた層の族、という三つの形を受け入れる。すべての層について性質を証明するときの帰納法の場合分けは、この五つである。特に各場合は、前節で証明した推移性の補題の一つに対応する。

この述語は台を添字とする帰納的な族であり、構成子は段階の生成規則として読める。基底の場合は、空集合が段階であること。`𝒟` による閉包は、`A` が段階ならその定義可能冪集合も段階であることで、後者ステップに対応する。一般の和の構成子は極限ステップに対応する。`x` の要素がすべて、切り詰めなしに層であるなら、`⋃ x` も層である。二項和の構成子は、`A` と `B` の層の証明から直接 `A ∪ B` を扱う。各構成子は、前節の推移性の補題の一つを `isTransV` を `isLayer` に置き換えた形に対応し、この平行性こそが次の証明を即座にする。

```agda
data isLayer : S → Type (ℓ-suc ℓ) where
  ∅-layer        : isLayer ∅
  𝒟-layer        : ∀ {A} → isLayer A → isLayer (𝒟 A)
  union-layer    : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isLayer y) → isLayer (⋃ x)
  union₂-layer   : ∀ {A B} → isLayer A → isLayer B → isLayer (A ∪ B)
```

小さな添字族の構成子が全体を完成させる。型 `X : Type ℓ` と族 `f : X → S` に対し、すべての値が層なら、和 `⋃ (sett X f)` も層である。極限段階は、まさにこの構成子を通して前段階の族から組み立てられる。次に帰納である。`layer-trans`、すなわちすべての層が推移的であることを示すには、層を帰納的な引数として受け取るので、場合はその構成子で定まる。空集合の場合はそのまま `∅-trans` である。`𝒟` の場合は `𝒟-trans` を適用し、その前提は下の層に対する帰納仮定 `layer-trans lA` である。

```agda
  setUnion-layer : (X : Type ℓ) (f : X → S)
                 → ((x : X) → isLayer (f x)) → isLayer (⋃ (sett X f))

layer-trans : ∀ {A} → isLayer A → isTransV A
layer-trans ∅-layer = ∅-trans
layer-trans (𝒟-layer {A} lA) = 𝒟-trans {A} (layer-trans lA)
```

三つの和の場合も同じように直接に振り分けられる。一般の和の場合は、要素ごとの帰納仮定を `⋃-trans` に渡す。この補題は `x` の各要素 `y` に対する `y` の推移性の証明を要求するが、構成子の前提 `mem` がまさにそれを切り詰めなしで供給するため、命題的切り詰めの消去は必要ない。二項の場合は二つの帰納仮定に対する `∪-trans` である。族の場合は各点の帰納仮定を伴う `setUnion-trans` である。こうしてこの節は、構造的再帰だけで塔のすべての段階が推移的集合であることを確立する。本章の後半でクラス `L` の推移性を示す際に用いられる事実である。

```agda
layer-trans (union-layer x mem) = ⋃-trans x (λ y y∈x → layer-trans (mem y y∈x))
layer-trans (union₂-layer lA lB) = ∪-trans (layer-trans lA) (layer-trans lB)
layer-trans (setUnion-layer X f hf) = setUnion-trans X f (λ x → layer-trans (hf x))
```

## 階層

いよいよ塔そのものを、所属に沿った再帰で構成する。まず二つの技術的な措置を施す。`𝒟` を展開すると論理式上の大きな `sett` になり、再帰の仕組みそのものも到達可能性の消去子へ展開される。露出したままだと両者がその後の変換に割り込むため、`opaque` によって `𝒟ₒ` と塔を不透明にし、明示的に展開するブロックの内側でのみ開き、`Lset-compute` を塔の宣言された展開式とする。ステップは、添字 `α` の要素 `β` にわたって再帰値に `𝒟ₒ` を施したものの和集合を取り、計算規則は命題としてのパスとして成り立つ。

まず演算子を `opaque` ブロックの内側で `𝒟ₒ` として包み直し、`Def` の込み入った定義が、補題が明示的に展開を求めない限り姿を現さないようにする。ステップ関数 `LsetStep` は添字集合 `α` と、`α` の各要素 `β` に対する再帰値 `rec β` を受け取る。ここでの所属は、構造的な所属の命題を型として読む `∈ᵗ` を通して現れる。本体は、小さな添字 `m : ⟪ α ⟫` を、`m` の指す要素 `⟪ α ⟫↪ m` での再帰値に `𝒟ₒ` を施したものへ写す族を作り、その和集合を取る。この和を添字型にわたって展開すれば、意図された読みはまさに `⋃ { 𝒟ₒ (Lset β) ∣ β ∈ α }` であり、一本の等式が零・後者・極限を等しく扱う。`α` が空なら和は空、後者なら古典的な次のステップを繰り返し、極限ならすべての前段階を一度に集める。

```agda
opaque
  𝒟ₒ : S → S
  𝒟ₒ A = 𝒟 A

LsetStep : (α : S) → (∀ β → β ∈ᵗ α → S) → S
LsetStep α rec = ⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (rec (⟪ α ⟫↪ m) (mem m))))
```

補助関数 `mem` が本体に必要な変換を供給する。添字 `m` の指す `α` の要素は `⟪ α ⟫↪ m` であり、`∈ₛ⟪ α ⟫↪ m` がこの集合が小さな表現で `α` に属することを証明する。そして `∈∈ₛ` がそれを、`rec` が期待する型としての所属 `∈ᵗ` へ変換する。塔そのものはただ一度の呼び出しである。`Lset` はステップ関数に `∈-induction` を適用したものとして定義される。これは所属に沿った整礎再帰であり、その正当性は階層の章の正則性の定理が一度に与える。再帰の添字は集合 `α` そのものであり、素の定義は添字の順序数性を要求しない。順序数性が課されるのは、この階層を使う場所においてである。

```agda
  where
  mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
  mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)

opaque
  Lset : S → S
```

`𝒟ₒ` と `Lset` はそれぞれ固有の `opaque` ブロックで包まれるため、両者の Agda の項は型検査のあいだ抽象的なままである。再帰の仕組みの内側、つまりある到達可能性の消去子で何が展開されようと、それが後の変換に漏れ出すことはない。盲目的な展開の代わりとなるのが、宣言された計算規則である。`Lset-compute` は、`Lset α` が `α` と再帰値 `λ β _ → Lset β` にステップを適用したものに等しいことを、命題としてのパスとして述べる。これは階層の章の `∈-induction-compute` をこのステップで実例化した恰好であり、この等式は定義的に成り立つとは限らない。明示的に述べておくことで、以後の証明は再帰の仕組みを開く代わりに、この一本の制御された等式で `Lset α` を書き換えられる。

```agda
  Lset = ∈-induction LsetStep

opaque
  unfolding Lset
  Lset-compute : (α : S) → Lset α ≡ LsetStep α (λ β _ → Lset β)
  Lset-compute = ∈-induction-compute LsetStep
```

塔のすべての値は層である。まず `Lset-compute` で一度展開し、各要素に帰納仮定を適用し、`𝒟ₒ-layer` で一段上げ (不透明な定義が展開されるのはまさにここだけである)、最後に `setUnion-layer` によって族の和が再び層であると結論する。

演算子から述語への橋渡しは一行で済む。`𝒟ₒ` を展開するブロックの内側では、`𝒟ₒ-layer` という主張は文字どおり構成子 `𝒟-layer` である。`𝒟ₒ A` は `𝒟 A` へ簡約されるからである。本章で不透明な包みの内側を見る必要があるのはここだけで、これ以後は演算子のすべての使用が抽象的なままで済む。目標 `Lset-layer` は、塔がまるごと帰納的述語の内側に落ちること、すなわちすべての段階 `Lset α` が層であることを言う。その証明自体が、塔を定義したのと同じ原理である所属帰納の適用である。

```agda
opaque
  unfolding 𝒟ₒ
  𝒟ₒ-layer : ∀ {A} → isLayer A → isLayer (𝒟ₒ A)
  𝒟ₒ-layer = 𝒟-layer

Lset-layer : (α : S) → isLayer (Lset α)
```

この帰納のステップ関数は `α` と、`α` の各要素 `β` に対して `Lset β` が層であることを与える帰納仮定 `IH` を受け取る。`Lset` は不透明なので、目標 `isLayer (Lset α)` は構成子と直接照合できず、まず輸送されなければならない。等式 `Lset-compute α` が `Lset α` をステップの和集合と同一視し、`subst isLayer (sym (Lset-compute α))` がそのパスに沿って目標を正しい向きへ移すので、目標は `isLayer (⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))))` になる。これはまさに塔のステップ関数が作った族である。

```agda
Lset-layer = ∈-induction step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → isLayer (Lset β)) → isLayer (Lset α)
  step α IH = subst isLayer (sym (Lset-compute α))
    (setUnion-layer ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))
```

残りの義務は族の構成子に正確にはまる。`setUnion-layer` は族と、その各値に対する層の証明を要求する。添字 `m` に対する値は `Lset (⟪ α ⟫↪ m)` での `𝒟ₒ` であり、局所的な補助 `mem` によって型としての所属へ変換されたうえでその要素に適用した帰納仮定 `IH` が `isLayer (Lset (⟪ α ⟫↪ m))` を与え、`𝒟ₒ-layer` がそれを定義可能冪集合の一段へ引き上げる。`Lset` の不透明な包みは宣言された等式を通してのみ開かれ、`𝒟ₒ` の包みは `𝒟ₒ-layer` の内側でのみ開かれるので、帰納全体が塔の意図された読みのレベルで進む。前節と合わせれば、すべての段階は推移的な層である。

```agda
      (λ m → 𝒟ₒ-layer (IH (⟪ α ⟫↪ m) (mem m))))
    where
    mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
    mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)
```

## 段階の比較

塔についてさらに二つの事実がある。第一は演算子の所属に名前を与える。`𝒟ₒ A` は `A` の定義可能部分集合の集合なので、それに属することは構成上「ある `defSet φ` である、と単に」であり、論理式を一つ、外延的な等式とともに示せば、集合を演算子の中へ置くのにちょうど十分である。第二は塔を一度展開し、和集合を両方向から読む。段階とは、添字の要素にわたる前段階の `𝒟ₒ` の和集合であり、したがって段階に属することは、ある前段階の `𝒟ₒ` に属することに他ならない。これは二つの独立な方向として述べられる。単調性はその後、別個の構成ではなく帰結として従う。

`𝒟ₒ` を展開するブロックの内側では、`𝒟ₒ A` への所属は `Def` の定義的性質に帰着する。`𝒟ₒ A` の要素とは、`A` の小さな要素の上でのアリティ 1 の論理式 `φ` が選び出す `A` の部分集合であり、実際の集合はパス `DefOf.defSet A φ ≡ x` によって特定される。周囲の階層での所属は命題的に切り詰められているため、主張には命題的切り詰めが冠される。断言されるのはそのような論理式が単に存在することであって、一つが選ばれていることではない。以下の二つの補題は、この同値をそれぞれ一方向ずつ述べるものである。ここでは導入の方向が宣言され、切り詰められた定義データを所属へ取る。

```agda
opaque
  unfolding 𝒟ₒ
  𝒟ₒ-intro : (A x : S)
           → ∥ Σ[ φ ∶ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁
           → ⟨ x ∈ˢ 𝒟ₒ A ⟩
```

証明の本体は両方向とも恒等写像である。`𝒟ₒ` を展開すれば、命題的に切り詰められた定義データの要素はもともと要素であり、逆に反転の補題 `𝒟ₒ-inv` は所属を同じ切り詰められたデータとして返す。したがって `𝒟ₒ-intro` と `𝒟ₒ-inv` の対は、直前述べたインターフェイスそのものである。段階における `DefOf.defSet` を論理式からの写像として読み、反転によって要素の定義論理式を取り戻す。どちらも「単に存在する」のレベルで働くため、標準的な論理式が選ばれることはない。`𝒟ₒ A` の要素は単に何らかの定義可能部分集合であるだけであり、この二方向が言うのはそれだけである。

```agda
  𝒟ₒ-intro A x p = p

  𝒟ₒ-inv : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
         → ∥ Σ[ φ ∶ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁
  𝒟ₒ-inv A x p = p
```

塔を後の議論で使うために、さらに二つの事実を示す。第一は演算子の所属に名前を与える。`𝒟ₒ A` は `A` の定義可能部分集合の集合なので、それに属することは構成上「ある `defSet φ` である、と単に」であり、論理式を一つ、外延的な等式とともに示せば、集合を演算子の中へ置くのにちょうど十分である。第二は塔を一度展開し、和集合を両方向から読む。段階とは、添字の要素にわたる前段階の `𝒟ₒ` の和集合であり、したがって段階に属することは、ある前段階の `𝒟ₒ` に属することに他ならない。これは、証明がそう使うために、二つの独立な方向として述べられる。単調性はその後、別個の構成ではなく帰結として従う。

最初の補題は、段階がその固有の定義可能冪集合に含まれるという包含である。`Lset-layer β` が段階 `Lset β` が層であることを言い、`layer-trans` がそれを推移的にするので、定義可能性の章の細分の評価 `A⊆Def` がそのまま適用され、`x ∈ Lset β ⟹ x ∈ 𝒟ₒ (Lset β)` が得られる。双対の `𝒟ₒ∋⊆` は、演算子が細分するだけで要素を失わないことを再確認する。`𝒟ₒ A` の各要素は `A` の部分集合なので、その要素の要素も依然 `A` にある。最後に `stageFam` が、塔のステップの下にある族に名前を与える。`α` の小さな表現の添字 `m` に対して、対応する段階は `m` の指す要素での `Lset` に `𝒟ₒ` を施したものである。

```agda
  Lset⊆𝒟ₒ : (β x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩
  Lset⊆𝒟ₒ β x = DefOf.Refine.A⊆Def (Lset β) (layer-trans (Lset-layer β)) x

  𝒟ₒ∋⊆ : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  𝒟ₒ∋⊆ A = DefOf.Def∋⊆A A

stageFam : (α : S) → ⟪ α ⟫ → S
```

次に、段階への所属を上から特徴づける。`Lset-in` の主張は、`δ` が `α` の要素であり `x` が `𝒟ₒ (Lset δ)` に属するなら、`x` はすでに `Lset α` に属する、ということである。証明はまず計算規則で `Lset α` を一度書き換え、目標を和集合 `⋃ (sett ⟪ α ⟫ (stageFam α))` への所属に変える。そして `union-family-in` を呼ぶ。これはモデル章の補題で、添字 `i` と `f i` の要素 `x` を受け取り、添字付きの和の要素を返す。供給される添字は `fib .fst`、すなわち `⟪ α ⟫` のうち要素 `δ` を名指す元である。

```agda
stageFam α m = 𝒟ₒ (Lset (⟪ α ⟫↪ m))

Lset-in : (α δ x : S) → ⟨ δ ∈ˢ α ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-in α δ x δ∈α x∈𝒟ₒδ =
  subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-compute α))
    (union-family-in ⟪ α ⟫ (stageFam α) (fib .fst) x
```

名前 `fib` はファイバーの計算の略記である。構造的な所属 `δ∈α` は命題的に切り詰められているが、`∈-asFiber` がそれを埋め込み `⟪ α ⟫↪` のファイバーへ変換する。つまり添字 `i` と `⟪ α ⟫↪ i ≡ δ` というパスの対である。証明の内側ではこの同一視に沿って輸送が行われる。`x∈𝒟ₒδ` は `Lset δ` について述べているが、`union-family-in` が必要とするのは `stageFam α (fib .fst)` の要素であり、これは `𝒟ₒ (Lset (⟪ α ⟫↪ (fib .fst)))` に等しいので、`subst` がパス `sym (fib .snd)` を横断して仮定を移す。`δ∈α` が切り詰められたものであることはここでは問題にならない。`∈-asFiber` が実際にそこからファイバー表現を構成したからである。

```agda
      (subst (λ δ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) (sym (fib .snd)) x∈𝒟ₒδ))
  where
  fib = ∈-asFiber {a = δ} {b = α} δ∈α

Lset-out : (α x : S) → ⟨ x ∈ˢ Lset α ⟩
         → ∥ Σ[ δ ∶ S ] (⟨ δ ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) ∥₁
```

下向きの方向 `Lset-out` は命題的切り詰めを避けられず、それを率直に述べる。`Lset α` の要素 `x` は、ある前駆から単に来ている。すなわち `δ ∈ α` かつ `x ∈ 𝒟ₒ (Lset δ)` なる `δ` が単に存在するということである。証明はここでも計算規則で `Lset α` を書き換え、`union-family-out` を適用して、`⟪ α ⟫` の添字 `m` でその位置の族の値に `x` が属することが単に成り立つことを得る。そして切り詰めの内部で写像を行う。対 `(m , hx)` は、段階 `⟪ α ⟫↪ m`、`∈∈ₛ` による `α` への構造的な所属、そして `hx` になる。結果が切り詰められた証人になるのは、和集合の公理が標準的な前駆を名指さないからにほかならない。分岐の内側で構成した一つは局所的なデータであって、選ばれた関数ではない。

```agda
Lset-out α x x∈Lα = map₁
  (λ { (m , hx) → ⟪ α ⟫↪ m
    , (∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m) , hx) })
  (union-family-out ⟪ α ⟫ (stageFam α) x
    (subst (λ w → ⟨ x ∈ˢ w ⟩) (Lset-compute α) x∈Lα))
```

単調性はこれで、別個の構成ではなく特徴づけの短い帰結になる。`β ∈ α` かつ `x ∈ Lset β` なら、まず `Lset⊆𝒟ₒ` が `x` を `𝒟ₒ (Lset β)` へ引き上げる。段階が推移的であることを使う。次に包含 `β ∈ α` とともに `Lset-in` を適用して、`x` を `Lset α` へ運ぶ。厳密な形に注意してほしい。単調性が要求するのは `β` が `α` の部分集合であることではなく要素であることであり、これは塔が要素にわたる和集合を取って伸びる仕方と一致する。

```agda
Lset-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-mono {α} {β} β∈α {x} x∈Lβ = Lset-in α β x β∈α (Lset⊆𝒟ₒ β x x∈Lβ)
```

## クラス L とその構造

集合が**構成可能**であるとは、塔のある順序数段階がそれを含むことである。順序数の上限を定義に意図的に書き込むのは、後の理論が段階の順序数を取り出す必要があるためであり、この形はそれを構成によって直接与える。順序数性が課されるのはまさにこの定義の箇所であることに注意してほしい。塔 `Lset` そのものは任意の集合を添字として受け付ける。`L` は推移的クラスである。段階は推移的であり、証人となる順序数は動かない。

このクラスは部分型ではなく真理値である。`isL x` は、すべての集合 `α` にわたる索引付きの選言 `∃[ x ] P x` として定義され、その各項は `IsOrd α` と `x ∈ˢ Lset α` の連言である。したがって添字付き選言の意味により、`isL x` の要素は単に、順序数 `α` と段階 `α` への `x` の所属の対である。構成可能集合に標準的な段階が付属することはない。量詞は台全体にわたるため、証人はこの「単に存在する」の形でしか得られない。クラスを命題値の述語として扱うことが、まもなくそれを構造へ制限できる理由である。

```agda
isL : S → hProp (ℓ-suc ℓ)
isL x = ∃[ α ∶ S ] ((IsOrd α , isPropIsOrd α) ⊓ (x ∈ˢ Lset α))

isL-trans : Transitive isL
isL-trans {x} {y} y∈x x∈L = rec₁ ((isL y) .snd)
  (λ { (α , (ordα , x∈Lα)) →
```

クラスの推移性は、段階の閉性からただちに従う。`y ∈ x` と `isL x` の要素が与えられ、命題的に切り詰められたものを命題 `isL y` へ消去する。証人は対 `(α , ordα , x∈Lα)` であり、段階 `Lset α` は `layer-trans (Lset-layer α)` により推移的集合なので、二つの仮定 `y∈x` と `x∈Lα` から `y ∈ Lset α` が得られる。同じ順序数 `α` が結論を改めて証明するので、クラスは要素の要素について閉じている。結論を `∣ _ ∣₁` で改めて切り詰めるのは、目標 `isL y` それ自体が切り詰められた存在式だからであって、どの選択を取り消す必要があったからではない。

```agda
    ∣ α , (ordα , layer-trans (Lset-layer α) y∈x x∈Lα) ∣₁ })
  x∈L
```

ある順序数段階に属すること**こそ**定義そのものなので、この方向の橋は構成子そのものである。この橋に名前を与えるのは、引用しやすくするためである。

段階 `α` の順序数の証人 `oα` と所属 `x∈Lα` が与えられれば、証明は三つの成分、順序数、その順序数性、所属、を一つの命題的に切り詰められた対へまとめる。計算されるものは何もない。この補題の内容は、`isL x` の定義にある存在式が、まさに手元のデータによって証明されるということである。信頼の向きに注意してほしい。この補題は `α` の順序数性を仮定として受け取る。定義上の `Lset` は任意の集合を添字として受け付けるため、選んだ添字が本当に順序数であることは呼び出し側が知っていなければならないからである。

```agda
Lset→isL : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ isL x ⟩
Lset→isL α oα x x∈Lα = ∣ α , (oα , x∈Lα) ∣₁
```

最後に、構成可能クラスを一つの構造として捉える。`𝒮ᵥ` を命題値のクラス `isL` に制限して得られるのが `𝒮ʟ` である。その元は構成可能性の証明を伴う集合であり、等式と所属は制限を通して受け継がれる。これが後に L についての論理式を解釈する構造になる。これを ZFC のモデルと示すには、続く各章の公理ごとの議論が別に必要である。

一行で十分である。制限 `_↾_` は周囲の構造とクラス `isL` を受け取り、`isL` を満たす証拠と対になった集合を要素とする構造を作る。等号と所属は第一射影に沿って読まれるため、周囲のものと一致する。`isL` は `hProp` の真理値であり、クラスは推移的であると証明済みなので、制限された構造は同じ枠組みのなかで問題なく定義される。まだ開いている問題、すなわち後の章の主題は、この構造が ZF と ZFC の公理を満たすかどうかである。制限そのものはそれについて何も主張しない。

```agda
𝒮ʟ : ZFStructureₕ (ℓ-suc ℓ)
𝒮ʟ = 𝒮ᵥ ↾ isL
```

## まとめ

塔 `Lset` は所属再帰で定義され、`isLayer` は定義可能性の演算と三種類の和集合構成に関する閉包性を記録する。層の証拠に対する構造的再帰と対応する補題から `layer-trans` が得られる。集合が `isL` に属するとは、ある順序数 `α` に対して `Lset α` に単に属することである。このクラスは推移的であり、周囲の構造をそこへ制限すると `𝒮ʟ` が得られる。残る課題は、この構造が ZFC を満たすことを公理ごとに証明することである。