Bedrock凝縮を通して構造を移す
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ本章では、初等的な Skolem 包が Mostowski 崩壊の後にどのような集合になるかを調べます。順序数の添字 lam において必要な仮定を与えると、崩壊像はある順序数 β が添字づける Lset β と同一視されます。この結論は β と lam を比較せず、そのような添字の最小のものを選ばず、基数評価も与えません。証明はまず、構成可能段階の関係を有界な一階論理式で記述し、崩壊の前後で読めるようにします。
{-# OPTIONS --cubical --safe --guardedness #-}
定理は ℓ-suc ℓ における排中律をパラメータとします。この一つの古典的仮定は、順序数段階、Skolem 包、階層の記述、十分な段階について先に得られた結果へ渡されます。ここでの議論は選択原理を導入しません。存在論理式の充足と、強化された十分さが与える局所的な段階の証人は命題的切り詰めのままなので、行き先が再び命題である場合にだけ使われます。
open import Base.Prelude open import Base.Classical using ( LEM )
ここで宇宙レベルとこの古典的パラメータを固定します。以下の集合はすべて、レベル ℓ の周囲の累積階層に属します。構成可能段階、Skolem 包、崩壊像も同じ累積階層の集合です。完全な初等性は、非有界な存在量化を含む論理式を移します。段階の絶対性、初等性、崩壊同型から作られた有界なインターフェースは、崩壊を通る Δ₀ の移送を外に示します。この二つの使い方を分けることが、凝縮の証明では欠かせません。
module L.GCH.CondensationTransfer {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
以下で作る二つの問い合わせに必要なのは、対象言語の所属、等号、連言、非有界な存在量化だけです。論理式を周囲の階層、段階、Skolem 包の間で移すとき、その定数のアルファベットは変わります。mapFo は既存の定数を付け替え、embed は定数を含まない論理式を新しい定数アルファベット上の論理式とみなします。どちらも変数の位置や論理構造を変えません。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import FOL.Manipulation.ConstantMapping using ( mapFo; embed ) import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
構成可能階層では、順序数の添字 d と、それが添字づける段階 Lset d を常に区別しなければなりません。lam が順序数なら、Lset lam の要素は構成可能です。逆に、順序数 d が Lset lam に属するなら、階数の比較によって d ∈ lam が得られます。下向きの特徴づけ Lset-out が述べるのは、段階の要素が、ある c ∈ lam に対する 𝒟ₒ (Lset c) から単に来るということだけであり、誕生段階を一つ選んで保持するわけではありません。さらに、厳密な添字関係 β ∈ α があれば、単調性によって Lset β の要素を Lset α へ移せます。
open import L.Constructible {ℓ} using ( IsOrd; isL; Lset; Lset-out; Lset-mono; Lset→isL; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( mem-ord; suc-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc; ord∈Lset→∈ ) open import L.Axioms.Basic {ℓ} using ( Lset-suc )
中心となる論理式は levelFo(a,p,z) です。その Δ₀ の証拠により、有界絶対性を使い、崩壊に沿って移送できます。健全性は、a、p、z が構成可能であるとき、充足から a ≡ Lset p が従うことを述べます。補助的な上界 z は一意である必要がありません。完全性は、γ が十分で、p が順序数であり、p ∈ γ であるとき、特定の三つ組 (Lset p,p,Lset γ) が論理式を満たすことを与えます。周囲の理論は、Skolem 包上の移送と、そのような三つ組を作るための局所的な十分な添字を供給します。
open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; Δ₀-isOrdAt; module Amb ; module Frame; _⊨ₚ_; embed-map; isOrd-at-p ) open import L.GCH.HierarchyDescription {ℓ} lem using ( levelFo; Δ₀-levelFo; level-sound; level-complete ) open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate; Adequate; Lset∈suc )
有限ベクトルは論理式を評価する環境を記録し、積は証明で必要となる所属と等しさの事実を組み合わせます。この章に現れるいくつかの存在は、命題的切り詰めのもとにあります。構成子 ∣_∣₁ は明示的な局所証人を切り詰めの中へ入れ、PT.rec と PT.map はそれを別の命題を得るためにだけ使います。とくに、強化された十分さが与える局所的な十分な添字が、大域的に選ばれた族になることはありません。
open import Cubical.Data.Vec using ( _∷_; [] ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Foundations.HLevels using ( isProp× ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
d が順序数なら、集合論的後続 sucV d は次の順序数添字です。また、後続段階の等式 Lset (sucV d) ≡ 𝒟ₒ (Lset d) もこの添字を使います。この二つの事実は関係していますが、後続の添字と、その添字における段階は別の集合です。空集合が別に現れるのは、Skolem 包の構成が、周囲の添字にすでに属する予備の要素を必要とするためです。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; module InfinitySet ) open InfinitySet {ℓ} using ( sucV )
命題値の階層構造を開くと、台 S と周囲の所属の記法 _∈ˢ_ が定まります。山括弧 ⟨_⟩ は、その真理値が運ぶ証明の型を取り出します。したがって、d ∈ˢ lam、構成可能段階への所属、崩壊像への所属は周囲の集合論における主張であり、論理式の内部で使う対象言語の原子 _∈̇_ とは区別されます。
open hPropStructure 𝒮ᵥ
周囲の意味論は、長さ n の環境を表す記法 S ^ n を与えます。論理式のスロットはこのようなベクトルから読まれ、新しく束縛された存在の証人は先頭に置かれて、以前のスロットを外側へずらします。そのため、後で三重に入れ子になった証人は、外側から z、p、a の順に導入されても、最終的には (a,p,z) の順に読まれます。
module SemVᵃ = FOL.Semantics 𝒮ᵥ open SemVᵃ using ( _^_ )
階層の証人を特定する論理式
論理式 isOrd-at-p は、三項環境の中央のスロットだけを使います。第一の連言支は p が推移的であることを述べ、第二の連言支は p の各要素が推移的であることを述べます。ここに示す二つの関数は、その二つの有界な節を IsOrd p の二つの成分へ展開します。隣の値 a と z はこの補題では何の役割も果たしません。また、この補題は levelFo の残りを読み取らず、a を構成可能段階と同一視することもありません。
isOrd-at-p-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ isOrd-at-p ⟩ → IsOrd p isOrd-at-p-out a p z h = ( λ {x₁} {y} y∈x₁ x₁∈p → h .fst x₁ x₁∈p y y∈x₁ ) , ( λ b b∈p {x₁} {y} y∈x₁ x₁∈b → h .snd b b∈p x₁ x₁∈b y y∈x₁ )
崩壊を通して階層の情報を移す
順序数 lam と、Skolem 包を含む周囲の構成可能段階 Lset lam を固定します。この添字は集合論的後続について閉じ、生成集合 X の各要素はこの段階に属します。また ∅ ∈ lam は、Skolem 包の構成に必要な既定の要素を与えます。この最初の仮定群の最後は完全な初等性です。パラメータが包から取られるなら、非有界量化子を含む論理式も含め、すべての論理式は包と周囲の段階で同じ真理値をもちます。
module Condense (lam : S) (ordλ : IsOrd lam) (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩) (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩) (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
さらに二つの仮定が、局所的な段階と構成可能な崩壊値を与えます。Superadequate lam は、各 d ∈ lam が、γ ∈ lam を満たすある十分な順序数添字 γ に単に含まれることを述べます。命題的切り詰めは、特定の γ も最小のものも保持しません。仮定 pixL は各点についての主張です。崩壊像の各要素が構成可能であると言うだけで、崩壊像そのものが構成可能な集合であることも、それを特定の段階と同一視することも、まだ述べていません。
(sup : Superadequate lam) (pixL : (x : S) → ⟨ x ∈ˢ HullStage.C.πX lam ordλ succλ X X⊆L ∅∈λ ⟩ → ⟨ isL x ⟩) where
ここからは三つの構造を同時に使います。Lset lam 上の周囲の構造、Skolem 包の要素を台とする構造、そして推移的な崩壊像です。包の要素は、基礎となる集合と、それが M に属するという証明をともに携えます。有界な論理式は最初の二つの構造の間で読め、崩壊を通して双方向に移せます。個々の所属の事実も崩壊の向こうへ送れます。これらの Δ₀ インターフェースを使うのは、完全な初等性によって非有界な存在問い合わせを処理した後だけです。
module F = Frame lam ordλ succλ X X⊆L ∅∈λ using (module A; module Carry; module HS) module A = F.A using (SM; module SemM; inL) module Mse = A.SemM.At A.SM id using (_⊨_) module HS = F.HS using (module ASt; module C; module Condense; module H; M) module Cy = F.Carry elem using (atL; atM; member-push; push; pull)
包含 Hull⊆L は、Skolem 包の要素から周囲の段階へ渡る基本的な橋です。x ∈ M ならば x ∈ Lset lam が成り立ちます。この事実は A.inL が必要とする段階への所属の証拠を与え、後では isLλ を通して、包から返された各証人を構成可能な集合にします。これは包が段階に各点で含まれるという主張であり、包そのものが段階の要素であるという主張ではありません。
open HS.H using ( Hull⊆L )
以上のデータから定まる Skolem 包を M と書きます。Hull⊆L により、その各要素は Lset lam に属します。しかし、この記法だけから M 全体の構成可能性や新たな閉性が従うわけではありません。したがって、以下で崩壊を使うたびに、その引数が M に属するという前提を保ちます。
M : S M = HS.M
Mostowski 崩壊写像を π、その推移的な像を πX と書きます。Skolem 包の要素上で、π は所属関係を保存し、有界な真理を像における読みに移します。ここからの課題は、πX に十分な段階の閉性と被覆の性質を示し、この推移的集合がちょうど一つの段階 Lset β であることを導くことです。
π : S → S π = HS.C.π
lam が順序数なので、Lset lam への所属から構成可能性が得られます。補助関数 isLλ は、まさにこの含意をまとめたものです。Skolem 包の問い合わせから返された三つの成分すべてにこれを適用してから level-sound を使います。levelFo の充足だけでは、その健全性定理が要求する構成可能性の仮定は得られないからです。
isLλ : (x : S) → ⟨ x ∈ˢ Lset lam ⟩ → ⟨ isL x ⟩ isLλ = Lset→isL lam ordλ
次の二つの基本的な所属の補題が、周囲の段階に置く証人を準備します。まず d ∈ lam とします。後続についての閉性から sucV d ∈ lam が得られ、段階全体 Lset d は Lset (sucV d) の一つの要素であり、Lset-mono がその要素を Lset lam へ移します。結論 Lset d ∈ Lset lam は集合の間の所属であり、一つの段階が別の段階に各点で含まれるという意味ではありません。
Lset∈Lλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩ Lset∈Lλ d d∈λ = Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (Lset∈suc d)
さらに d が順序数なら、ord∈Lset-suc は添字 d 自身を Lset (sucV d) に入れ、同じ単調性の一歩がそれを Lset lam へ移します。二つの補題を合わせると、d と Lset d という別々の段階要素が得られます。周囲の段階の内部で階層の論理式を証明するときには両方が必要であり、どちらの所属も、その出発点となった添字関係 d ∈ lam と混同してはなりません。
ord∈Lλ : (d : S) → IsOrd d → ⟨ d ∈ˢ lam ⟩ → ⟨ d ∈ˢ Lset lam ⟩ ord∈Lλ d od d∈λ = Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (ord∈Lset-suc d od)
Skolem 包の要素 d について、順序数性を崩壊の向こうへ送れます。Amb.isOrdAt-in は、定数を含まない有界な論理式 isOrdAt によって IsOrd d を表します。Cy.push はこの Δ₀ の真理を包の環境から π d を含む環境へ移し、Amb.isOrdAt-out が結果を IsOrd (π d) として読み取ります。有界性の証拠がこの移送を制御し、Cy.push がまとめている比較は、最終的には Skolem 包の初等的な包含と崩壊同型に基づきます。
ord-push : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd d → IsOrd (π d) ord-push d d∈M od = Amb.isOrdAt-out (π d) (Cy.push Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in d od))
同じ有界な記述は逆向きにも移せます。IsOrd (π d) から出発すると、Cy.pull が isOrdAt の真理をもとの Skolem 包の要素へ戻し、それを IsOrd d として読み取れます。したがって、崩壊は M の要素について順序数性を保存し、反映します。これは仮定 d ∈ M のもとでの局所的な同値であり、任意の周囲の集合に対する π の振る舞いを述べるものではありません。
ord-pull : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd (π d) → IsOrd d ord-pull d d∈M oπd = Amb.isOrdAt-out d (Cy.pull Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in (π d) oπd))
最初の存在問い合わせは、指定された段階 Lset d を Skolem 包の内部で取り戻すためのものです。三つの非有界な存在量化によって環境 (a,d′,z) が得られます。埋め込まれた核は levelFo(a,d′,z) を要求し、第二の連言支の等式が、返された中央の座標を d′ ≡ dM として固定します。Δ₀ なのは levelFo だけです。その外側の問い合わせ findA は有界ではないので、証人を周囲の段階から Skolem 包へ移すには、Δ₀ 絶対性だけでなく完全な初等性を使います。この等式が findA と後の問い合わせ findP を分けます。後者が返す添字 p′ は、外側で準備した p と等しい必要がありません。
findA : A.SM → Formula A.SM 0 findA dM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))))
補題 stageA は、後で初等性によって Skolem 包へ引き戻す周囲の証人を作ります。順序数 d を含む十分な添字 γ、基礎にある集合が d に等しい包の代表 dM、そして d、Lset d、Lset γ がそれぞれ Lset lam の要素であるという証拠を受け取ります。完全性が levelFo(Lset d,d,Lset γ) を与え、有界絶対性がこの核を段階の構造で読み、対象言語の等式には dM の基礎にある集合から d へのパスを使います。その後、三つの非有界な存在の節は、命題的切り詰めのもとで Lset γ、d、Lset d によって順に証明されます。ここでは γ が最小であるとは主張しません。
stageA : (d γ : S) (od : IsOrd d) (adγ : Adequate γ) (d∈γ : ⟨ d ∈ˢ γ ⟩) → (dM : A.SM) → fst dM ≡ d → ⟨ d ∈ˢ Lset lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩ → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findA dM) ⟩ stageA d γ od adγ d∈γ dM ed d∈ Ld∈ Lγ∈ =
周囲で用いる証人は、十分な上界 Lset γ、指定された添字 d、そしてその段階 Lset d です。最終的な環境は (Lset d,d,Lset γ) となるので、完全性が段階の記述の連言支を与えます。等式の連言支には sym ed が必要です。問い合わせは返された添字が dM の解釈に等しいことを求めますが、ed はその解釈を d と同一視する逆向きのパスだからです。各存在証人は命題的切り詰めのもとに置かれ、この三つ組を正準的に選ぶことなく、その存在だけを保ちます。
∣ (Lset γ , Lγ∈) , ∣ (d , d∈) , ∣ (Lset d , Ld∈) , (sat , sym ed) ∣₁ ∣₁ ∣₁ where δ : HS.ASt.SL ^ 3 δ = (Lset d , Ld∈) ∷ (d , d∈) ∷ (Lset γ , Lγ∈) ∷ []
段階の記述に関する完全性が、ここでの数学的な核を与えます。γ が十分であり、d が順序数で、d ∈ γ なので、三つ組 (Lset d,d,Lset γ) は周囲の階層で levelFo を満たします。十分さは記述に使う表を共通の上界に入れ、順序数性は d を正当な段階の添字にし、d ∈ γ はその添字を上界の下に置きます。残る課題は、この同じ Δ₀ の事実を Lset lam 上の構造で読むことです。
amb : ⟨ (Lset d ∷ d ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ amb = level-complete γ adγ d od d∈γ
次に、周囲での真理を Lset lam 上の段階構造での真理として表します。この時点ではまだ Skolem 包へ移していません。Cy.atL を逆向きに使うと、Δ₀ 論理式 levelFo を、その段階の三つの要素のもとで読めます。続いてパス embed-map が、内容を持たない定数の改名を embed levelFo と同一視します。周囲の問い合わせは Skolem 包の要素を定数として使いますが、levelFo 自身の定数域は空だからです。したがって sat は stageA が必要とする埋め込まれた核をちょうど与えます。完全な初等性を使うのは、非有界な問い合わせ全体を組み立てた後です。
sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩ sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo)) (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
第二の問い合わせも段階の記述を満たす三つ組 (u,a,z) を求めますが、付加条件が異なります。中央の座標を指定された添字と同一視する代わりに、yM と名づけられた Skolem 包の要素が第一座標 u に属することを要求します。したがって求めるのは、y を含む正しく記述された構成可能段階であり、その添字は固定されません。被覆の議論に必要なのは、まさにこの条件です。
findP : A.SM → Formula A.SM 0 findP yM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))))
補題 stageP は、この所属の問い合わせに対する周囲の証人を準備します。順序数 p、p を含む十分な段階 γ、y を名づける Skolem 包の要素 yM、および y ∈ Lset p から始めます。さらに三つの所属の仮定が p、Lset p、Lset γ をそれぞれ Lset lam に入れるので、三つの存在証人をすべて段階構造で使えます。ここで p は、一つの外部証人を作るためだけに使われます。findP には中央の座標を固定する等式がないため、後で初等性が返す内部の添字は別の p′ でもかまいません。
stageP : (y p γ : S) (op : IsOrd p) (adγ : Adequate γ) (p∈γ : ⟨ p ∈ˢ γ ⟩) → (yM : A.SM) → fst yM ≡ y → ⟨ y ∈ˢ Lset p ⟩ → ⟨ p ∈ˢ Lset lam ⟩ → ⟨ Lset p ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩ → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findP yM) ⟩ stageP y p γ op adγ p∈γ yM ey y∈Lp p∈ Lp∈ Lγ∈ =
同じ周囲の三つ組 (Lset p,p,Lset γ) が段階の記述を証明しますが、最後の連言支は今度は yM の解釈が Lset p に属することを記録します。この平行な構成により、二つの問い合わせの数学的な違いが明確になります。findA は指定された添字を保ち、findP は指定された点の所属を保ちます。したがって第二の場合、完全な初等性は別の内部添字を返してもかまいません。
∣ (Lset γ , Lγ∈) , ∣ (p , p∈) , ∣ (Lset p , Lp∈) , (sat , mem) ∣₁ ∣₁ ∣₁ where δ : HS.ASt.SL ^ 3 δ = (Lset p , Lp∈) ∷ (p , p∈) ∷ (Lset γ , Lγ∈) ∷ []
完全性が、二つの問い合わせに共通する核を与えます。γ の十分さ、p の順序数性、および p ∈ γ から、三つ組 (Lset p,p,Lset γ) が周囲の階層で levelFo を満たすことを示します。完全性が何を示し、何を示さないかを区別する必要があります。この外側で準備した特定の三つ組を検証しますが、公式を満たすすべての三つ組が p を使うとは述べず、後で得る内部の添字を一意にもしません。
amb : ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ amb = level-complete γ adγ p op p∈γ
前の問い合わせと同じく、この時点での移送は周囲の階層と Lset lam 上の段階構造との間だけで行われます。Cy.atL の逆向きは、levelFo の Δ₀ の証拠を使い、三つの基礎集合での周囲の充足を、それらの段階内の表示での充足として読みます。続いて embed-map のパスが、定数を持たない核を、周囲の Skolem 包の問い合わせが使う定数域へ移します。これは stageP が必要とする第一の連言支です。この有界な一歩では、非有界な量化子を一つも移していません。
sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩ sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo)) (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
残る連言支は、yM の解釈が Lset p に属することを述べます。その基礎集合は fst yM であり、パス ey : fst yM ≡ y によって、与えられた所属 y ∈ Lset p を逆向きにその解釈へ移せます。この小さな書き換えが、添字を固定せずに指定された点を問い合わせへ入れます。後で初等性が三つ組 (u,p′,z) を返すとき、保持される結論は y ∈ u であり、p′ と現在の p の間の等式はありません。
mem : ⟨ fst (A.inL yM) ∈ˢ Lset p ⟩ mem = subst (λ w → ⟨ w ∈ˢ Lset p ⟩) (sym ey) y∈Lp
集合 d に対して、Witness d は命題的切り詰めのもとで三つの事実を記録します。ある上界 z が Skolem 包に属し、指定された段階 Lset d が Skolem 包に属し、さらに (Lset d,d,z) が周囲の階層で levelFo を満たすことです。この型自体は任意の d に対して作れますが、以下の構成には IsOrd d と d ∈ M の両方が必要です。包みを切り詰めたままにしても、後で必要となる命題値の閉性と等式の結論には十分であり、十分な上界を選択済みのデータとして扱うこともありません。
Witness : S → Type (ℓ-suc ℓ) Witness d = ∥ Σ[ z ∈ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩ × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ ) ∥₁
構成はまず、Skolem 包の要素 d を周囲の段階へ入れます。Hull⊆L から d ∈ Lset lam が得られます。しかし強化された十分さが受け取るのは、構成可能段階の任意の要素ではなく、順序数 lam の要素です。次に示す局所的な事実 d∈λ が、まさにこの隔たりを埋めます。それが得られると、sup d d∈λ は d より上の十分な段階を供給するだけです。行き先の Witness d 自体が命題なので、外側の PT.rec はこの命題的に切り詰められた供給を利用できます。
witness : (d : S) → IsOrd d → ⟨ d ∈ˢ M ⟩ → Witness d witness d od d∈M = PT.rec squash₁ step1 (sup d d∈λ) where d∈Lλ : ⟨ d ∈ˢ Lset lam ⟩ d∈Lλ = Hull⊆L d d∈M
添字への所属を取り戻すため、d ∈ Lset lam に段階の反映補題を適用します。その仮定を見ると、この一歩が成り立つ理由が明確です。モジュールのパラメータにより lam は順序数であり、呼び出し側の仮定により d も順序数です。この二つの順序数性のもとでのみ、lam での段階への d の所属から d ∈ lam が従います。これは順序数の添字どうしの比較であり、任意の集合に対する一般的な階数原理ではありません。
d∈λ : ⟨ d ∈ˢ lam ⟩
d∈λ = ord∈Lset→∈ lam ordλ d od d∈Lλ
ここで後続についての閉性により、添字の関係を stageA が必要とする第二の段階所属へ変えます。d ∈ lam から、先の補題 Lset∈Lλ は Lset d ∈ Lset lam を与えます。このとき段階 Lset d 全体が、外側の段階の一つの要素として現れます。これと d∈Lλ を合わせると、d に関係する二つの座標が準備できます。最後の上界 Lset γ の所属は、強化された十分さが γ を供給した後で別に導きます。
Ld∈Lλ : ⟨ Lset d ∈ˢ Lset lam ⟩ Ld∈Lλ = Lset∈Lλ d d∈λ
強化された十分さは、命題的切り詰めのもとで、γ ∈ lam、d ∈ γ、Adequate γ を満たす添字 γ を返します。そのような三つ組ごとに step1 は Witness d を構成します。まず周囲の段階で問い合わせ全体を立て、初等性によってその切り詰められた存在の答えを Skolem 包の中で得て、その答えを切り詰められた証人の目標へだけ除去します。したがって、除去子の内部では一時的な γ を使えますが、γ の選択が定理のデータとして外へ出ることはありません。
step1 : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ d ∈ˢ γ ⟩ × Adequate γ) → Witness d step1 (γ , γ∈λ , d∈γ , adγ) = PT.rec squash₁ takeZ hullSat where Lγ∈Lλ : ⟨ Lset γ ∈ˢ Lset lam ⟩
与えられた関係 γ ∈ lam から、最後の周囲の段階への所属が得られます。γ に Lset∈Lλ を適用すると Lset γ ∈ Lset lam となります。これで Lset d、d、Lset γ はすべて段階構造の正当な要素となり、stageA の完全性の証人をそこで述べられます。この γ の使用には、最小性も一意性も必要ありません。
Lγ∈Lλ = Lset∈Lλ γ γ∈λ
固定添字の問い合わせが名づける定数は、単なる周囲の集合ではなく、Skolem 包の台の要素でなければなりません。d と、与えられた d ∈ M の証明を組にすると dM : A.SM が得られます。その基礎集合は定義により d そのものなので、stageA に渡す等式の証明は反射律です。この包装は新しい代表を作らず、崩壊も使いません。既存の Skolem 包の要素を、初等性が述べられている言語で提示するだけです。
dM : A.SM dM = d , d∈M
ここで findA に完全な初等性を使います。先の stageA の呼び出しは、改名された問い合わせが Lset lam 上の段階構造で成り立つことを示しました。elem の対称方向は、その充足を Skolem 包の構造へ移します。elem は任意の論理式に適用できるため、この一歩では三つの非有界な存在量化子も一緒に移せます。したがって、Δ₀ の核 levelFo にだけ用いた Cy.atL とは区別しなければなりません。得られる hullSat は、適切な三つ組が Skolem 包に存在することだけを述べます。
hullSat : ⟨ [] Mse.⊨ findA dM ⟩ hullSat = subst ⟨_⟩ (sym (elem 0 (findA dM) [])) (stageA d γ od adγ d∈γ dM refl d∈Lλ Ld∈Lλ Lγ∈Lλ)
findA の答えを必要な証人へ変えるため、外側の二つの座標 z と d′ が除去子の中ですでに展開されたとします。すると最も内側の存在量化子は、Skolem 包の要素 a、(a,d′,z) での埋め込まれた核の充足、および等式 fst d′ ≡ d を与えます。補助関数 finishA は、この切り詰められていない分岐を、M 内の上界、指定された Lset d の M への所属、および (Lset d,d,fst z) での周囲の充足へ変換します。この変換が使うのは健全性であり、存在証人の一意性ではありません。
finishA : (z d' : A.SM) → Σ[ a ∈ A.SM ] ( ⟨ (a ∷ d' ∷ z ∷ []) Mse.⊨ embed levelFo ⟩ × (fst d' ≡ d) ) → Σ[ w ∈ S ] ( ⟨ w ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
まず、埋め込まれた核を周囲の階層で読み直します。levelFo は Δ₀ なので、有界な比較 Cy.atM は Skolem 包の構造における (a,d′,z) での充足を、基礎集合 (fst a,fst d′,fst z) での周囲の充足と同一視します。この有界な一歩は、存在証人を展開した後に得られた核だけに作用します。非有界な問い合わせを除去するものでも、それだけで第一の座標を構成可能段階と同一視するものでもありません。
× ⟨ (Lset d ∷ d ∷ w ∷ []) ⊨ₚ levelFo ⟩ ) finishA z d' (a , sat , ed) = fst z , snd z , Ld∈M , amb' where amb : ⟨ (fst a ∷ fst d' ∷ fst z ∷ []) ⊨ₚ levelFo ⟩ amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (a ∷ d' ∷ z ∷ [])) sat
levelFo の健全性定理は、三つの基礎集合がそれぞれ構成可能であることを要求します。三つとも Skolem 包の要素なので、Hull⊆L によりそれぞれ Lset lam に属します。さらに lam が順序数であるため、isLλ がこれら三つの所属を必要な構成可能性の証明へ変えます。この別々の仮定と周囲での充足 amb を level-sound に渡すと、fst a は Lset (fst d′) と同一視されます。公式の充足だけでは、この同一視を正当化できません。
ea : fst a ≡ Lset d
ea = level-sound (fst a) (fst d') (fst z)
(isLλ (fst a) (Hull⊆L (fst a) (snd a)))
(isLλ (fst d') (Hull⊆L (fst d') (snd d')))
(isLλ (fst z) (Hull⊆L (fst z) (snd z))) amb
ここで findA の等式の連言支が、意図された役割を果たします。健全性から fst a ≡ Lset (fst d′) が得られ、ed : fst d′ ≡ d に Lset を作用させると Lset (fst d′) ≡ Lset d が得られます。二つのパスを合成すれば ea : fst a ≡ Lset d です。したがって、返された第一の座標は、もともと指定した添字での段階です。この等式の連言支がなければ、同じ健全性の議論から分かるのは、返された何らかの添字での段階だということだけです。
∙ cong Lset ed
返された座標 a は、Skolem 包への所属 snd a をすでに伴っています。この命題を ea に沿って移すと Lset d ∈ M が得られます。これが、指定された Skolem 包の順序数 d に対して求めていた閉性です。これは、強化された十分さ、完全な初等性、有界絶対性、および段階の記述の健全性から導かれます。M に対する別の閉性公理を仮定しておらず、この部分の議論では Mostowski 崩壊もまだ使っていません。
Ld∈M : ⟨ Lset d ∈ˢ M ⟩ Ld∈M = subst (λ w → ⟨ w ∈ˢ M ⟩) ea (snd a)
証人の包みには、向きの整った段階の記述も残す必要があります。(fst a,fst d′,fst z) での周囲の充足から始め、中央の座標を ed に沿って移し、第一の座標を ea に沿って移します。すると (Lset d,d,fst z) での充足が得られ、これはちょうど Witness d の第三のフィールドです。これを snd z および新しく得た Lset d ∈ M と合わせると、切り詰められていない一つの分岐ができ、後で命題的切り詰めの中へ戻されます。
amb' : ⟨ (Lset d ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩ amb' = subst (λ v → ⟨ (v ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩) ea (subst (λ p → ⟨ (fst a ∷ p ∷ fst z ∷ []) ⊨ₚ levelFo ⟩) ed amb)
z と d′ を固定すると、最も内側の存在量化子が保つのは、適切な a が単に存在することだけです。明示的な各 a から finishA によって d に対する必要な切り詰められた証人が得られるので、切り詰めの内部で写すことで必要な存在性だけを保てます。選ばれた a が外へ現れることはなく、残る座標も同じ命題的な制限のもとで扱われます。
takeD : (z : A.SM) → Σ[ d' ∈ A.SM ] ⟨ (d' ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM)) ⟩ → Witness d takeD z (d' , hd) = PT.map (finishA z d') hd
最も外側の証人 z がすでに固定された後、次の切り詰めが隠しているのは中央の座標 d′ です。これを命題 Witness d へ除去し、局所的な各 d′ を先の構成へ渡します。step1 ですでに用いた外側の除去が、証人 z を処理します。したがって、強化された十分さと三つの存在量化子から得られる証人は、すべて命題である結論の内部にとどまります。十分な上界も包内の三つ組も、大域的なデータとして選ばれません。
takeZ : Σ[ z ∈ A.SM ]
⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))) ⟩
→ Witness d
takeZ (z , hz) = PT.rec squash₁ (takeD z) hz
ここで、崩壊と構成可能段階の局所的な整合性を述べられます。d が Skolem 包の順序数なら、commute は Lset d が再び包に属することと、この段階を崩壊すると Lset (π d) が得られることを同時に証明します。証明は Witness d を命題の積へ除去します。包への所属は命題を値にとり、周囲の二つの集合の等しさも、周囲の累積階層が h-集合であるため命題です。したがって、その積は命題的切り詰めを除去できる正当な目標です。
commute : (d : S) → IsOrd d → (d∈M : ⟨ d ∈ˢ M ⟩) → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d)) commute d od d∈M = PT.rec (isProp× (snd (Lset d ∈ˢ M)) (isSetS (π (Lset d)) (Lset (π d)))) go (witness d od d∈M)
証人を局所的に開くと、Lset d が包に属するという成分が、最初の結論をそのまま与えます。残る二つのデータ、包の要素 z と levelFo(Lset d,d,z) の充足は、等式の証明に使うために残します。この分担は commute の二つの結論に対応しています。d が添字づける段階について Skolem 包が閉じていることは Witness d から直接得られますが、その段階と崩壊との整合性は、段階の有界な記述からさらに証明する必要があります。
where go : Σ[ z ∈ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩ × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ ) → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d)) go (z , z∈M , Ld∈M , amb) = Ld∈M , eq
等式の証明では、まず有界な記述を崩壊の向こうへ移します。環境は、Skolem 包の三つの要素 Lset d、d、z と、それぞれの所属の証明からなります。levelFo は定数を含まない Δ₀ 論理式なので、Cy.push は各座標をその崩壊値で置き換え、levelFo(π (Lset d),π d,π z) の充足を与えます。これは先に順序数性へ使ったのと同じ局所的な Δ₀ 移送を、今度は構成可能段階を記述する三変数の論理式へ適用したものです。
where pushed : ⟨ (π (Lset d) ∷ π d ∷ π z ∷ []) ⊨ₚ levelFo ⟩ pushed = Cy.push Δ₀-levelFo ((Lset d , Ld∈M) ∷ (d , d∈M) ∷ (z , z∈M) ∷ []) amb
移送された論理式を健全性によって読むには、崩壊された三つの座標がすべて構成可能でなければなりません。各座標は Skolem 包の要素の崩壊なので、πX-intro によって崩壊像に属し、点ごとの仮定 pixL が必要な構成可能性の証明を与えます。これにより健全性は、崩壊された第一座標を、第二座標が添字づける構成可能段階と同一視できます。
π (Lset d) ≡ Lset (π d)。
補助的な値 π z はこの記述を検証するために必要ですが、得られる等式には現れません。
eq : π (Lset d) ≡ Lset (π d) eq = level-sound (π (Lset d)) (π d) (π z) (pixL (π (Lset d)) (HS.C.πX-intro (Lset d) Ld∈M)) (pixL (π d) (HS.C.πX-intro d d∈M)) (pixL (π z) (HS.C.πX-intro z z∈M))
移送された充足は、以上の健全性の議論における最後の前提です。その結論は commute の仮定とともに読む必要があります。この等式が成り立つのは、Skolem 包に属する順序数 d についてです。これは演算 π と Lset の間の大域的な等式ではありません。この局所性で十分なのは、以下の二つの適用では、まず関係する包内の順序数を取り戻し、その後で整合性の等式を使うからです。
pushed
抽象的な凝縮の議論が要求する第一の性質は、崩壊像が自身の順序数に対応する段階について閉じていることです。崩壊像の順序数 δ が与えられたとき、levelIn は Lset δ もその像に属することを示さなければなりません。要素の特徴づけ πX-member は、命題的切り詰めのもとで、π d ≡ δ を満たす Skolem 包の要素 d を与えます。目標そのものが所属命題 Lset δ ∈ πX なので、この命題的に切り詰められた原像を局所的に開けます。
levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ HS.C.πX ⟩ → ⟨ Lset δ ∈ˢ HS.C.πX ⟩ levelIn δ oδ δ∈πX = PT.rec (snd (Lset δ ∈ˢ HS.C.πX)) go (HS.C.πX-member δ δ∈πX) where go : Σ[ d ∈ S ] (⟨ d ∈ˢ M ⟩ × (π d ≡ δ)) → ⟨ Lset δ ∈ˢ HS.C.πX ⟩
このような原像 d が得られれば、求める像への所属は Lset d から導けます。実際、Lset d が Skolem 包に属するという証明を πX-intro に渡すと、π (Lset d) が崩壊像に属するという証明が得られます。最後の輸送では、整合性の等式 π (Lset d) ≡ Lset (π d) に続いて、原像の等式 π d ≡ δ に Lset を施した等式を使います。残る課題は、d が順序数であり、Lset d が包に属することを示すことです。
go (d , d∈M , e) = subst (λ w → ⟨ w ∈ˢ HS.C.πX ⟩) (cm .snd ∙ cong Lset e) (HS.C.πX-intro (Lset d) (cm .fst)) where od : IsOrd d
整合性の補題を使う前に、原像の順序数性を復元します。仮定 IsOrd δ を π d ≡ δ に沿って逆向きに輸送すると IsOrd (π d) が得られ、ord-pull がこの事実を崩壊の手前へ反映して IsOrd d を与えます。議論の順序に注意してください。原像の記述だけから分かるのは、d が Skolem 包の要素だということです。その順序数性は、δ の順序数性と、有界な順序数論理式に対する反映から得られます。
od = ord-pull d d∈M (subst IsOrd (sym e) oδ)
これで commute の仮定がすべて揃いました。その第一成分は Lset d を Skolem 包に入れ、第二成分は π (Lset d) ≡ Lset (π d) を与えます。後者を、e : π d ≡ δ に Lset を施した cong Lset e と合成すると、この崩壊された段階は Lset δ と同一視され、輸送によって求める像への所属が得られます。したがって、崩壊像が順序数 δ を含むなら Lset δ も含みます。順序数でない集合や像の外の順序数について、閉性を主張しているわけではありません。
cm : ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d)) cm = commute d od d∈M
第二の性質は被覆です。Skolem 包の各要素 y に対して、π y ∈ Lset γ を満たす順序数 γ が崩壊像の中に単に存在することを求めます。その順序数、像への所属、そしてこの段階への所属は、一つの命題的切り詰めのもとに保たれます。したがって各 y には被覆する段階が存在しますが、そのような段階の族を選ぶことも、添字の最小性や lam との大小関係を主張することもありません。
cover : (y : S) → ⟨ y ∈ˢ M ⟩ → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁ cover y y∈M = PT.rec squash₁ go (Lset-out lam y (Hull⊆L y y∈M)) where Goal : Type (ℓ-suc ℓ)
目標 Goal 自体が命題的切り詰めです。この点は二度使われます。Lset-out が与える y の分解と、強化された十分さが与える十分な添字は、共通の行き先が命題なので、ともに局所的に利用できます。どちらの段階でも最終的な被覆の添字は固定されません。その添字は、所属の問い合わせ findP に対する内部の答えから得られます。
Goal = ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
構成は、まず構成可能階層の中で y の位置を定めることから始まります。Skolem 包の各要素は Lset lam に属するので、Lset-out は命題的切り詰めのもとで、y が Lset c の定義可能部分集合となる添字 c ∈ lam を与えます。p = sucV c と置きます。後続に関する閉性によって p を lam に戻すと、強化された十分さは、p を含む十分な添字 γ ∈ lam を、やはり切り詰めのもとで与えます。準備した添字 p は y を含む外側の段階を用意しますが、Skolem 包が後で返す添字そのものではありません。
go : Σ[ c ∈ S ] (⟨ c ∈ˢ lam ⟩ × ⟨ y ∈ˢ 𝒟ₒ (Lset c) ⟩) → Goal go (c , c∈λ , y∈D) = PT.rec squash₁ go₂ (sup p p∈λ) where p : S p = sucV c
最初の補助事実は、lam の後続に関する閉性の仮定を c ∈ lam に適用し、p = sucV c に対する p ∈ lam を得ます。この関係には二つの用途があります。一方では p に強化された十分さを適用し、他方では、後で作る周囲の証人において、順序数 p と段階 Lset p の両方を Lset lam の中へ置きます。添字に関するこの一つの閉性の仮定が、これらすべてを支えています。
p∈λ : ⟨ p ∈ˢ lam ⟩
p∈λ = succλ c c∈λ
準備した添字は順序数でもなければなりません。lam は順序数で c ∈ lam なので、mem-ord から IsOrd c が得られ、フォン・ノイマン後続についての順序数の閉性から IsOrd (sucV c)、すなわち IsOrd p が従います。ここでは後続の二つの役割を区別しています。succλ は後続を外側の添字に入れ、suc-ord はその後続自体が順序数であることを示します。
op : IsOrd p op = suc-ord (mem-ord {A = lam} ordλ c c∈λ)
誕生段階の情報は y ∈ 𝒟ₒ (Lset c) を与えます。後続段階の等式は、この定義可能冪集合の段階を Lset (sucV c) と同一視するので、輸送によって y ∈ Lset p が得られます。これが c からその後続へ進む理由です。分解によって y は c の段階上の定義可能部分集合として位置づけられますが、findP が必要とするのは構成可能段階への通常の所属です。
y∈Lp : ⟨ y ∈ˢ Lset p ⟩ y∈Lp = subst (λ w → ⟨ y ∈ˢ w ⟩) (sym (Lset-suc c)) y∈D
強化された十分さの証人を局所的に開くと、添字 γ ∈ lam、関係 p ∈ γ、性質 Adequate γ が得られます。これらは、外側で準備した添字 p に完全性を適用するために必要な仮定そのものです。組 yM = (y,y∈M) はここで y を包の台の要素とみなし、findP の定数パラメータとして使えるようにします。ここからの構成では、先のように指定された添字を固定する問い合わせではなく、y の所属を固定する問い合わせを使います。
go₂ : Σ[ γ ∈ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ p ∈ˢ γ ⟩ × Adequate γ) → Goal go₂ (γ , γ∈λ , p∈γ , adγ) = PT.rec squash₁ takeZ hullSat where yM : A.SM yM = y , y∈M
十分な添字 γ における完全性は、三つ組 (Lset p,p,Lset γ) を使って findP の周囲での答えを作り、先に得た所属が y をその第一座標に入れます。必要な三つの台への所属は、ord∈Lλ p、Lset∈Lλ p、Lset∈Lλ γ がそれぞれ与えます。findP は非有界な存在量化を含むので、この答え全体を Skolem 包へ移すには完全な初等性を使います。その結果、yM が正しく記述されたある段階に属するという、包内部の存在主張が得られます。
hullSat : ⟨ [] Mse.⊨ findP yM ⟩
hullSat = subst ⟨_⟩ (sym (elem 0 (findP yM) []))
(stageP y p γ op adγ p∈γ yM refl y∈Lp
(ord∈Lλ p op p∈λ) (Lset∈Lλ p p∈λ) (Lset∈Lλ γ γ∈λ))
内部の主張を局所的に開くと、Skolem 包の三つの要素 u、a、z が得られます。それらの基礎集合は levelFo(fst u,fst a,fst z) を満たし、同じ答えは y ∈ fst u も記録しています。ここから、崩壊像に属し、その段階が π y を含む順序数を得なければなりません。局所的な各答えから明示的な依存和を作れますが、その和はただちに命題的切り詰めのもとへ戻されるので、被覆の添字が選択済みのデータとして外へ出ることはありません。
finishP : (z a : A.SM) → Σ[ u ∈ A.SM ] ( ⟨ (u ∷ a ∷ z ∷ []) Mse.⊨ embed levelFo ⟩ × ⟨ y ∈ˢ fst u ⟩ ) → Σ[ β ∈ S ] (IsOrd β × ⟨ β ∈ˢ HS.C.πX ⟩
出力の証人は、局所的に β = π p′ とします。ここで p′ は、包の中央の座標 a の基礎にある集合です。p′ が順序数だと分かれば、ord-push により π p′ も順序数となり、a が持つ p′ ∈ M の証明から、πX-intro によって π p′ が崩壊像に入ります。残る成分は π y ∈ Lset (π p′) です。これを得るには、まず論理式への答えを周囲の階層で読み、その後で所属を局所的な整合性の等式と結びつけます。
× ⟨ π y ∈ˢ Lset β ⟩) finishP z a (u , sat , y∈u) = π p′ , ord-push p′ (snd a) op′ , HS.C.πX-intro p′ (snd a) , πy∈ where amb : ⟨ (fst u ∷ fst a ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
内部の充足の証明が扱うのは、包の構造における embed levelFo です。その核 levelFo は Δ₀ 論理式なので、Cy.atM はこの証明を、同じ三つの基礎集合 (fst u,fst a,fst z) における levelFo の周囲での充足として読みます。この段階では、どの座標も崩壊されません。その役割は、Skolem 包の内部意味論を離れ、isOrd-at-p-out と level-sound を適用できる周囲での主張を取り戻すことです。
amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (u ∷ a ∷ z ∷ [])) sat
Skolem 包の内部で返された中央の座標を p′ = fst a とします。これは、周囲で準備した後続 p = sucV c と等しい必要がありません。周囲の三つ組は findP yM が充足可能であることを示しましたが、findP が固定するのは yM の第一座標への所属だけであり、中央の座標を固定する等式は含みません。したがって完全な初等性が命題的切り詰めのもとで与えるのは、ある内部添字 p′ にすぎず、残りの証明はこの返された添字を使います。
p′ : S p′ = fst a
ただし、返された添字が順序数であることは分かります。周囲での充足 amb の第一の連言支は、中央の座標について読む三つの枠を持つ順序数の記述です。その連言支に読みの補題 isOrd-at-p-out を適用すると、IsOrd p′ が得られます。この結論が述べるのは内部の原像の添字 p′ です。Goal で使う順序数はその崩壊 π p′ であり、こちらの順序数性は別に ord-push から得ます。
op′ : IsOrd p′ op′ = isOrd-at-p-out (fst u) p′ (fst z) (amb .fst)
ここで健全性により、内部の答えの第一座標を特定します。u、a、z はいずれも Skolem 包の要素なので、Hull⊆L はそれらの基礎にある集合を Lset lam に入れ、isLλ がそれぞれの構成可能性を証明します。これら三つの前提を amb と合わせると、fst u ≡ Lset p′ が得られます。したがって、答えに記録された y ∈ fst u を y ∈ Lset p′ へ輸送できます。補助的な上界 fst z は一意である必要がなく、p′ と準備した p の間の等式も使いません。健全性は、返された順序数の添字だけから段階の値を定めます。
u≡ : fst u ≡ Lset p′ u≡ = level-sound (fst u) p′ (fst z) (isLλ (fst u) (Hull⊆L (fst u) (snd u))) (isLλ p′ (Hull⊆L p′ (snd a))) (isLλ (fst z) (Hull⊆L (fst z) (snd z))) amb
健全性から得た等式 u≡ は、返された段階の値 fst u を Lset p′ と同一視します。この等式に沿って、すでに得られた所属 y∈u を移せば、y ∈ Lset p′ が従います。ここで行うのは所属の右辺にある集合の置換だけであり、返された添字 p′ と先に用意した添字 p の間には何の関係も課していません。
y∈Lp′ : ⟨ y ∈ˢ Lset p′ ⟩
y∈Lp′ = subst (λ v → ⟨ y ∈ˢ v ⟩) u≡ y∈u
返された中央の座標は、局所的な交換定理に必要なデータをちょうど与えます。その基礎集合が p′ であり、op′ はそれが順序数であることを、snd a はそれが包に属することを示します。したがって commute p′ op′ (snd a) から、Lset p′ ∈ M と等式 π (Lset p′) ≡ Lset (π p′) の両方が得られます。この定理は包の中の順序数に対する局所的な主張であり、ここではその条件が満たされています。
cm : ⟨ Lset p′ ∈ˢ M ⟩ × (π (Lset p′) ≡ Lset (π p′)) cm = commute p′ op′ (snd a)
y∈Lp′ の両端は包の要素です。y については y∈M が、Lset p′ については cm .fst がその所属を与えます。そこで member-push によりこの所属を崩壊の後へ移し、π y ∈ π (Lset p′) を得ます。さらに cm .snd に沿って右辺の集合を置換すると、π y ∈ Lset (π p′) となります。先に示した π p′ の順序数性と像への所属と合わせれば、これは finishP が求める覆いの証人です。
πy∈ : ⟨ π y ∈ˢ Lset (π p′) ⟩ πy∈ = subst (λ w → ⟨ π y ∈ˢ w ⟩) (cm .snd) (Cy.member-push (Lset p′) y (cm .fst) y∈M y∈Lp′)
z と a を固定すると、最後の存在量化子は適切な u が単に存在することだけを述べます。明示的な各答えから、上で構成した順序数 π p′、その崩壊像への所属、および π y ∈ Lset (π p′) の証明が定まります。この構成を命題的切り詰めの内部で写すことにより、問い合わせへの特定の答えを選ぶことなく、被覆する順序数の存在を保てます。
takeA : (z : A.SM) → Σ[ a ∈ A.SM ] ⟨ (a ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero)) ⟩ → Goal takeA z (a , ha) = PT.map (finishP z a) ha
残る二つの存在の層も同じ制限に従います。z を固定した後、行き先 Goal が命題なので中央の証人 a を使えます。外側の除去も同様に z を扱います。したがって内部の答えの三つの座標は、すべて局所的にだけ利用できます。結果は各 Skolem 包の要素に被覆する順序数が存在することを示しますが、そのような順序数を選ぶ関数は作りません。
takeZ : Σ[ z ∈ A.SM ]
⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))) ⟩
→ Goal
takeZ (z , hz) = PT.rec squash₁ (takeA z) hz
ここまでで示した二つの性質が、崩壊像を決定します。その順序数要素全体の集合を β とします。像の推移性と、順序数の要素も順序数であることから、β は順序数です。x ∈ πX なら、被覆によって、順序数 γ ∈ πX を添字とするある Lset γ に x が属します。したがって γ ∈ β であり、単調性から x ∈ Lset β が従います。逆に x ∈ Lset β をある δ ∈ β のところで分解します。像の要素 δ に被覆を適用すると、δ ∈ γ を満たす順序数 γ ∈ β が得られます。すると x ∈ Lset γ であり、levelIn は Lset γ を推移的な崩壊像に入れるので、x ∈ πX です。外延性から πX ≡ Lset β が得られます。
module Cn = HS.Condense levelIn cover using (condenses)
こうして、IsOrd β と HS.C.πX ≡ Lset β を満たす明示的な集合 β が得られます。この証人は命題的切り詰めの中にはありません。崩壊像の順序数要素全体からなる集合そのものだからです。この結論は Condense の構造的な仮定をすべて使い、その古典的なパラメータは LEM (ℓ-suc ℓ) だけです。β と外側の添字 lam の比較、基数評価、単射は与えません。それらには後の章で導入する追加の構成が必要です。
condenses : Σ[ β ∈ S ] (IsOrd β × (HS.C.πX ≡ Lset β)) condenses = Cn.condenses