有界部分集合が制御された段階に現れる

module At (κ : S) (oκ : IsOrd (κ .fst)) (cκ : IsCardinalL κ)
          (κ∉ω : ⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
          (y : S) (y⊆κ : (z : V ℓ) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩) where

κ が順序数であることと κ ∉ ω から、ω ⊆ κ が従う。有限 von Neumann 数項 # k はどれも ω に属するので、すべての k について # k ∈ κ である。これらの要素を、合併の符号化における有限のタグとして使う。

num∈κ : (k : ℕ) → ⟨ # k ∈ κ .fst ⟩
num∈κ k = ω⊆ (κ .fst) oκ κ∉ω (# k) (#∈ω k)

順序数 κ と、それを添字とする構成可能段階は別の集合である。そこで Lset κ を内部集合 Lκ としてまとめる。この段階が出発集合の主要部分となり、κ 自身は、その出発集合を符号化して入れる基数として残る。

Lκ : S
Lκ = LsetS (κ .fst) oκ

κ と y を一つの共通の段階へ入れるため、まず L の内部で両者の無順序対を作る。この対を含む推移的な段階は、その二つの要素も含むので、一度の出現段階の構成で両方を扱える。

private
  P₀ : S
  P₀ = pairʟ κ y

この無順序対が現れる、順序数である段階の添字 α₀ を取る。これは構成可能性から得られる扱いやすい添字にすぎず、α₀ がこの対の現れる最小の段階だとは主張していない。

  α₀ : V ℓ
  α₀ = stage (P₀ .fst) (P₀ .snd)

選んだ段階の添字 α₀ は順序数である。次にこれより真に上にある、十分性を強めた順序数を取るため、また後で順序数の推移性によって κ を α₀ の下から lam へ運ぶために、この事実が必要である。

  oα₀ : IsOrd α₀
  oα₀ = stage-ord (P₀ .fst) (P₀ .snd)

基数 κ は Lset α₀ に属する。κ は無順序対の要素であり、その対は Lset α₀ に属し、この段階は推移的だからである。ここで得たのは段階への所属であって、後で使う順序数への所属 κ ∈ α₀ ではない。

  κ∈Lα₀ : ⟨ κ .fst ∈ˢ Lset α₀ ⟩
  κ∈Lα₀ = layer-trans (Lset-layer α₀) {x = P₀ .fst} {y = κ .fst}
    (pairʟ-in κ y κ (inl refl)) (stage-mem (P₀ .fst) (P₀ .snd))

同じ推移性の議論により、無順序対のもう一つの要素を通して y も Lset α₀ に入る。κ と違い、y は順序数とは仮定されていない。したがって後では、この事実を段階の単調性によって Lset lam へ運び、y ∈ α₀ へ変換することはしない。

  y∈Lα₀ : ⟨ y .fst ∈ˢ Lset α₀ ⟩
  y∈Lα₀ = layer-trans (Lset-layer α₀) {x = P₀ .fst} {y = y .fst}
    (pairʟ-in κ y y (inr refl)) (stage-mem (P₀ .fst) (P₀ .snd))

ここで α₀ ∈ lam を満たす、十分性を強めた順序数 lam を明示的に取る。この真の拡張が、後の包と凝縮の議論に必要な閉性を与える。lam 自身は明示的なデータであるが、その強められた十分性が保証する局所的な十分な添字は、命題的切り詰めの内側にとどまる。

  sa = superadequate-above α₀ oα₀

この高い順序数を、コードでは lam、本文では λ と書く。その具体的な構成は以後使わず、順序数性、後続に関する閉性、強められた十分性、および α₀ より上にあるという事実だけを使う。

opaque
  lam : V ℓ
  lam = sa .fst

最初に保つ事実は、lam が順序数であることである。したがって lam は推移的であり、lam より下の順序数の所属をさらに上へ運べる。

  ordλ : IsOrd lam
  ordλ = sa .snd .fst

次に保つのは、順序数の後続に関する閉性である。d ∈ lam ならば sucV d ∈ lam でもある。この閉性は、有限 Skolem 構成が lam を添字とする段階の内部にとどまるための構造的仮定の一つである。

  succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
  succλ = sa .snd .snd .snd .fst .snd .fst

強められた十分性とは、各 d ∈ lam に対して、d ∈ γ ∈ lam を満たす十分な順序数 γ が単に存在することである。これは lam より下に局所的な十分な余地を与えるが、最小の γ も、そのような γ の族も選ばない。

  sup : Superadequate lam
  sup = sa .snd .snd .snd .snd

基数 κ は順序数の添字 lam に属する。κ と α₀ はともに順序数なので、まず κ ∈ Lset α₀ から κ ∈ α₀ が得られる。さらに α₀ ∈ lam と順序数 lam の推移性から、κ ∈ lam が従う。この結論は添字 lam への所属であり、段階 Lset lam への所属ではない。

  κ∈λ : ⟨ κ .fst ∈ˢ lam ⟩
  κ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ (κ .fst) oκ κ∈Lα₀) (sa .snd .snd .fst)

一方、y について必要なのは、段階 Lset lam への所属である。α₀ ∈ lam から、段階の単調性により Lset α₀ ⊆ Lset lam が得られる。これを先の y ∈ Lset α₀ に適用すると、y ∈ Lset lam となる。y が順序数であるという仮定は必要ない。

  y∈Lλ : ⟨ y .fst ∈ˢ Lset lam ⟩
  y∈Lλ = Lset-mono {α = lam} {β = α₀} (sa .snd .snd .fst) y∈Lα₀

y の周囲の各要素は Lset κ に属する。部分集合の仮定により z ∈ y から z ∈ κ が得られる。κ は順序数なので、このような z も順序数であり、自身の後続段階に属し、累積性によって z ∈ Lset κ となる。したがって y ⊆ κ から、出発集合を推移的にするために必要な段階への包含が得られる。

y⊆Lκ : (z : V ℓ) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ Lset (κ .fst) ⟩
y⊆Lκ z hz = ord⊆Lset (κ .fst) oκ z (y⊆κ z hz)

Lset lam の内部で、出発集合 X = Lset κ ∪ {y} を作る。これは y を含み、しかも推移的である。Lset κ に由来する要素は、その推移的な段階にとどまる。また y の要素は、仮定により κ に属し、したがって Lset κ に属する。この推移性こそが、後で崩壊に y を固定させる。

module UK = UnionKit (κ .fst) lam (y .fst) oκ ordλ κ∈λ y⊆Lκ y∈Lλ κ∉ω
  using ( X; X⊆Lλ; ∅∈λ; Lα∈X; x∈X; X-mem; sgl≡; Xtr )

以下では、この Lset κ の推移的な拡張を X と書く。覚えておくべき二つの性質は互いに補い合う。y ∈ X によって、位置を定めたい集合が包に入り、推移性によって、崩壊がその集合を変えない。

X : V ℓ
X = UK.X

数え上げのため、タグ 0 ∈ κ を用いて、単元集合 {y} とその κ への符号化された単射を内部で構成し、それを Lκ と内部で合併する。こうして同じ集合 Lset κ ∪ {y} の符号化された提示が得られ、その二つの部分には、タグ付き合併の議論に必要な単射がすでに備わっている。

module Pt = Point κ (num∈κ ) y using ( Y; Y-out; Y-in; injL )
module U = Union2 Lκ Pt.Y using ( D; out; in₁; in₂ )

この内部で構成した合併を Xʟ と書く。これは X と同じ数学的な合併を表すが、その構成には、κ への符号化された単射を示すために必要な内部データが伴っている。

Xʟ : S
Xʟ = U.D

Xʟ と X を同一視するため、両者の要素を二方向に比較する。順方向では、内部で符号化された合併への所属から、命題的切り詰めのもとで、Lset κ の要素である場合と、符号化された単元集合の要素である場合に分かれる。どちらからも X への所属が従う。X への所属は命題なので、この除去は正当である。

Xʟ-eq : Xʟ .fst ≡ X
Xʟ-eq = extensionalV {a = Xʟ .fst} {b = X} (λ z → ⇔toPath (fwd z) (bwd z))
  where
  fwd : (z : V ℓ) → ⟨ z ∈ˢ Xʟ .fst ⟩ → ⟨ z ∈ˢ X ⟩
  fwd z h = rec₁ ((z ∈ˢ X) .snd) go (U.out zS h)

段階の側の場合、左の包含によって、その要素は X に入る。z を一時的に構成可能集合としてまとめられるのは、L の推移性による。z は構成可能集合 Xʟ の要素なので、z 自身も構成可能である。

    where
    zS : S
    zS = z , isL-trans {x = Xʟ .fst} {y = z} h (Xʟ .snd)
    go : ⟨ z ∈ˢ Lset (κ .fst) ⟩ ⊎ ⟨ z ∈ˢ Pt.Y .fst ⟩ → ⟨ z ∈ˢ X ⟩
    go (inl hz) = UK.Lα∈X z hz

単元集合の側では、符号化された要素は、すでに X に属すると分かっている y に等しくなる。逆方向では、X への所属が、やはり命題的切り詰めのもとで Lset κ の側と単元集合の側に分かれる。行き先である Xʟ への所属は命題なので、この二度目の除去も正当である。

    go (inr hz) = subst (λ w → ⟨ w ∈ˢ X ⟩) (sym (Pt.Y-out zS hz)) UK.x∈X
  bwd : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Xʟ .fst ⟩
  bwd z h = rec₁ ((z ∈ˢ Xʟ .fst) .snd) go (UK.X-mem z h)
    where
    go : ⟨ z ∈ˢ Lset (κ .fst) ⟩ ⊎ ⟨ z ∈ˢ ⁅ y .fst ⁆s ⟩ → ⟨ z ∈ˢ Xʟ .fst ⟩

逆方向の二つの場合は、Xʟ の二つの成分へそれぞれ入る。Lset κ の要素は、その段階から構成可能性を受け継いで左側に入り、{y} の要素は、まず y と同一視されてから、符号化された単元集合の側に入る。こうして外延性により Xʟ .fst ≡ X が得られ、切り詰められた場合分けはどちらも保持されない。

    go (inl hz) = U.in₁ (z , isL-trans {x = Lset (κ .fst)} {y = z} hz (Lκ .snd)) hz
    go (inr hz) = subst (λ w → ⟨ w ∈ˢ Xʟ .fst ⟩) (sym (UK.sgl≡ z hz)) (U.in₂ y Pt.Y-in)

始集合は構成可能である。内部の写しが構成可能で、二つの写しの底の集合が等しいからである。

X-isL : ⟨ isL X ⟩
X-isL = subst (λ w → ⟨ isL w ⟩) Xʟ-eq (Xʟ .snd)

X とこの構成可能性の証明を組にして、XS : S とする。台となる周囲の集合は依然としてちょうど X であり、この包装は InjL が要求する内部の定義域を与えるだけである。

XS : S
XS = X , X-isL

無限基数の平方法則により、符号化された単射 κ × κ ↪ κ の存在が命題的切り詰めのもとで得られる。その仮定は冒頭で固定した事実、すなわち κ が順序数であり内部の基数であり、ω の要素ではないことに一致する。全単射も、特定の単射のグラフも得られない。

pairκ : InjL (prodL κ) κ
pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (κ .fst) (κ .snd) oκ cκ κ∉ω

二つの成分の単射をタグ付き合併の構成に入れると、符号化された単射 Xʟ ↪ κ × κ が得られる。タグ #0 と #1 が、段階の側と単元集合の側を区別する。これを平方法則の単射と合成して Xʟ ↪ κ を得た後、Xʟ .fst ≡ X に沿って定義域を構成可能な包装 XS へ移す。こうして必要な符号化された単射 X ↪ κ が、引き続き命題的切り詰めのもとで得られる。

base : InjL XS κ
base = move Xʟ XS κ κ Xʟ-eq refl
  (injl-trans Xʟ (prodL κ) κ
    (tag-union κ (num∈κ ) (num∈κ ) Lκ Pt.Y (stage-counted κ Lκ oκ κ∉ω refl) Pt.injL)
    pairκ)

M を、Lset lam の内部で X が生成する Skolem 包とする。この包に対する Tarski-Vaught の定理により、M は凝縮に必要な意味で初等的である。推移的集合 X 全体が出発集合なので、これは y を含み、後でその崩壊が y を固定する、同じ一つの包である。

elem = HullElemDown.elem lam ordλ X UK.X⊆Lλ UK.∅∈λ

包の数え上げ定理は、X ↪ κ を Skolem 閉包の有限段階へ順に伝え、さらにそれらの合併へ伝える。その結果、符号化された単射 M ↪ κ の存在が命題的切り詰めのもとで得られる。したがって、この包は凝縮を適用するのに必要な初等性をもち、その大きさも引き続き κ によって制御される。

hull↪κ = Count.hull↪κ lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL κ oκ cκ κ∉ω base

凝縮は明示的な順序数 β を与え、M の崩壊像を Lset β と同一視する。さらに Lset β と M を構成可能集合としてまとめ、逆崩壊から得られる符号化された単射 Lset β ↪ M の存在を命題的切り詰めのもとで与える。ここで β は段階の添字であり、Lset β がそれによって添字づけられる段階である。

module St = Site lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ elem sup X-isL
  using ( β; oβ; ext; Lβ; βL; hullL; Lβ↪M )

ここからは、一つの包の構成について三つの側面を使う。包 M、包含 X ⊆ M、そして像を πX とする崩壊写像 π である。対応する不動点定理は、M の推移的部分集合に適用できる。これらの事実から、まず崩壊が y を変えないことを示し、次に同じ y を凝縮によって同一視された段階へ入れる。

module HS = HullStage lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( M )
module HSH = HullStage.H lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ using ( X⊆M )
module HSC = HullStage.C lam ordλ succλ X UK.X⊆Lλ UK.∅∈λ
  using ( πX; π; fixes; πX-intro )

集合 y は Skolem 包 M に属する。y は始点集合 X に入っており、X の各要素は X から生成された包に属するからである。

y∈M : ⟨ y .fst ∈ˢ HS.M ⟩
y∈M = HSH.X⊆M (y .fst) UK.x∈X

崩壊は y を固定する。始点の集合 X が推移的で包の中にあるため、崩壊の写像は X のすべての要素の上で恒等であり、y もその一つである。

πy : HSC.π (y .fst) ≡ y .fst
πy = HSC.fixes X
  (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
  UK.Xtr (y .fst) UK.x∈X

y は包に属するので、崩壊像は π(y) を含む。凝縮によってこの像は構成可能段階 Lset β と同一視され、不動点の等式 π(y) = y から y ∈ Lset β が従う。ここで崩壊は y を別の集合に置き換えたのではなく、もとの y を制御された構成可能段階の中に位置づけている。

y∈Lβ : ⟨ y .fst ∈ˢ Lset St.β ⟩
y∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πy
  (subst (λ w → ⟨ HSC.π (y .fst) ∈ˢ w ⟩) St.ext (HSC.πX-intro (y .fst) y∈M))

順序数 β は、三つの符号化された単射の鎖によって κ へ単射する。順序数の所属による β から Lset β への包含、制限された逆崩壊による Lset β から包 M への単射、そして包の計数による M から κ への単射である。この鎖が与えるのは符号化された単射であり、裸の順序数の比較ではない。

β↪κ : InjL St.βL κ
β↪κ = injl-trans St.βL St.Lβ κ
  (inclusion-coded St.βL St.Lβ (λ z hz → ord⊆Lset St.β St.oβ z hz))
  (injl-trans St.Lβ St.hullL κ St.Lβ↪M hull↪κ)

局所的な証人は、構成可能順序数 β、その順序数性、y が段階 Lset β に属するという事実、そして符号化された単射 β ↪ κ をまとめる。ここで返されるのは段階の添字 β であり、Lset β は y が位置づけられた構成可能段階である。この二つは区別される。

result : Σ[ b ∶ S ] (IsOrd (b .fst) × ⟨ y .fst ∈ˢ Lset (b .fst) ⟩ × InjL b κ)
result = St.βL , St.oβ , y∈Lβ , β↪κ