--- title: "内部の段階順序関係" module: L.Choice.InternalWellOrder lang: ja site: "Bedrock" description: "内部の正準整列順序" stage: "正準整列順序と選択公理" reading_order: 83 canonical: https://bedrock.institute/ja/L.Choice.InternalWellOrder.html html: L.Choice.InternalWellOrder.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/InternalWellOrder.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.OrderTable, L.Choice.StageOrderAdequacy, L.Choice.NameComparisonAdequacy, L.Choice.EarliestDisagreement, L.Coding.HierarchySequence, L.Coding.DefinablePowerSet, L.Coding.Model, L.Coding.CodeSet, L.Hierarchy, L.WellOrder.Base, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/en/L.Choice.InternalWellOrder.md, https://bedrock.institute/zh/L.Choice.InternalWellOrder.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 内部の段階順序関係 各構成可能段階では、`orderAt` がその要素上のホスト側の狭義整列順序をすでに与えています。この章の課題は、その基礎となる比較を `L` で解釈される論理式からも使えるようにすることです。各順序数段階について、順序対の所属が `relOf (orderAt α oα)` と対ごとに両方向で対応する関係集合を得ます。ここで新しい整列順序を構成することも、この関係が整列順序であると述べる対象言語の論理式を証明することもありません。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` この章では二つの水準を一貫して区別します。整列順序はホスト理論の数学的構造ですが、`L` の内部でそれを表すものは、一階言語から指すことのできる集合でなければなりません。 ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` 構成は任意の宇宙レベルで行い、表示された後続レベルでの排中律だけを仮定します。後で得られる関係集合が引き継ぐのは、ちょうどこの仮定です。 ```agda module L.Choice.InternalWellOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` 一回の比較ステップを内部で記述するには、変数と定数を、所属・等号・連言・存在量化で結べば十分です。以下の六つの存在束縛は、同じ論理構成子を繰り返し用いたものです。 ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} ``` この関係は順序数段階を添字とします。そのため、証人は構成可能集合として同定され、後続段階への所属は直前の段階上での定義可能性と結び付けられなければなりません。 ```agda using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; Lset-suc ) open import L.Choice.FirstIntersectionStage {ℓ} lem using ( stageBound ) ``` 意味論的な目標には二つの水準があります。`orderAt δ od` は、`Lset δ` の要素上のホスト側の狭義整列順序です。その再帰的記述で用いる同じ誕生段階のステップについて、`Under δ (stepOrder δ od) u v` は、`u` と `v` が `Lset (sucV δ)` に属することと、そこから得られる二要素が `stepOrder δ od` で関係づけられることを記録します。`Lset δ` 上の最小名が、このホスト側のステップを以下で構成する論理式へ結び付けます。 ```agda open import L.Choice.StageOrders {ℓ} lem using ( Mem; New; relOf; carry; orderAt; Under ; stepAt-fill; stepAt-read; IsLeastName; leastNameOf ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming ) open import L.Choice.NameComparison {ℓ} lem using ( StepAt ) ``` 再帰的な順序表には、妥当なステップ記述から関係集合を作る仕組みがすでにあります。残る仕事は、具体的な論理式を一つ与えてその意味論的な二方向を証明し、抽象的なステップ引数への順序表の依存を取り除くことです。 ```agda open import L.Choice.OrderTable {ℓ} lem using ( IsRel; ixRel-fill; ixRel-rep ) open import L.Choice.StageOrderAdequacy {ℓ} lem using ( CodesAt; CodesAt-in; CodesAt-out; stepOrder; module Ordered ; towerS; towerS-fst; powS; powS-fst; sh2; sh3; StpOut; StpIn ) open import L.Choice.NameComparisonAdequacy {ℓ} lem using ( module At ) ``` この論理式は、段階の塔、その定義可能部分集合、段階における表の値、塔上のコードという四つの変動する対象を同定しなければなりません。これらの同定条件により、任意の充足する割り当てを意図した数学的データへ戻せます。 ```agda open import L.Choice.EarliestDisagreement {ℓ} lem using ( codeOrder; codeOrder-fill; codeOrder-rep ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) ``` さらに二つの証人は固定された定数です。コード上の比較関係と、空のアルファベットに対するコード集合です。これらは順序表から得る変動する関係値とともに、最小名を比較するための補助関係と領域を与えます。 ```agda open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) ``` 充足関係は構成可能集合の命題的構造で解釈されます。したがって、各存在節は命題的に切り詰められた依存対を生みます。証人は証明を支えますが、命題の外で選択済みのデータとして取り出すことはできません。 ```agda import FOL.Absoluteness open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) ``` 比較は後続段階の要素の間で行われます。段階を小さい型で表示することで、ホスト側の整列順序をその要素に作用させられます。`sucV` は、比較される二対象を位置付ける後続順序数を記録します。 ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV ) ``` ここから先、論理式は `L` が備える一階構造で解釈されます。したがって、スロットに置く要素は、その基礎集合と、その集合が構成可能であるという命題の両方を含みます。 ```agda open hPropStructure 𝒮ʟ ``` 以下では、この解釈を `γ ⊨ φ` と書きます。絶対性によって、同定論理式を基礎集合についての具体的事実として読めるため、後で証人を読み解くことができます。 ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## 記述が束縛する要素 六つの枠のずらしは、すべての変数を、ステップの論理式の六つの証人の向こう側へ運びます。 ```agda private sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i))))) ``` 六つの証人をすべて束縛した後、`StepAt` はそのうち五つを直接参照します。塔 `tw`、表の関係 `rl`、コード集合 `cs`、コード順序 `ro`、空のアルファベットのコード集合 `c0` です。定義可能冪集合の証人 `pw` は周囲の所属条件で使われ、`StepAt` には渡されません。 ```agda iTow iRel iCod iOrd iNil : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) iTow = suc (suc (suc (suc (suc zero)))) iRel = suc (suc (suc zero)) iCod = suc (suc zero) ``` 最も内側の二つの添字は `ro` と `c0` を選びます。新たな束縛を導入するのではなく、すでに束縛された二つの証人が、完全に拡張された環境のどこにあるかを記録するだけです。 ```agda iOrd = suc zero iNil = zero ``` ## ステップの論理式 `Stp d f u v` の六つの証人は、依存関係に従う順序で導入されます。最初は `d` が指す段階の塔であり、次はその定義可能冪集合です。後者への所属条件が、`u` と `v` の指す対象を後続段階で比較できることを保証します。 ```agda opaque Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n Stp d f u v = ∃̇ ( LsetGraphAt zero (suc d) ∧̇ ∃̇ ( DefAt zero (suc zero) ``` 第三の証人は、その段階で順序表に記録された値 `rl` であり、第四の証人は塔上のコード集合です。最後の二証人は対象言語の等号で制約される変数で、それぞれ正準なコード順序と空のアルファベットに対するコード集合に固定されます。 ```agda ∧̇ ( (var (sh2 u) ∈̇ var zero) ∧̇ ( (var (sh2 v) ∈̇ var zero) ∧̇ ∃̇ ( appAt (sh3 f) (sh3 d) zero ∧̇ ∃̇ ( CodesAt zero (sh3 zero) ∧̇ ∃̇ ( (var zero ≐ con codeOrder) ``` 最内部では、`StepAt` は七つの意味論的スロットを見ます。上で選んだ五つの補助証人と、六つの束縛を越えてずらされた二つの元の対象です。そこで述べるのは両者の最小名の比較であり、表現された関係が `L` の内部で整列順序の論理式を満たすという主張ではありません。 ```agda ∧̇ ∃̇ ( (var zero ≐ con (AllCodes ∅ʟ)) ∧̇ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ) ) ) ) ) ) ) ) ``` ## 六つの束縛を層ごとに扱う 読みのモジュールは、四つの枠・環境・そして解読された段階の順序数性を固定します。ホストの順序がその順序数性を必要とするからです。 ```agda module Reading {n : ℕ} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) where private δ : V ℓ δ = fst (lookup d γ) ``` ホストの順序は、段階の提示の上に運ばれます。要素の狭義の順序が、小さな索引型の上で使えるのです。 ```agda ordW : SWO ⟪ Lset δ ⟫ ordW = carry (Lset δ) (orderAt δ od) ``` `Lset (sucV δ)` にある集合の名前は `Lset δ` 上で作られ、その直前の段階に移された順序 `ordW` に関してのみ最小名として区別されます。述語 `IsLeastName` は、その名前が与えられた集合を表すことと、それより小さい別の名前がないことの両方を記録します。これが、後続段階の集合と `StepAt` が用いる名前比較との正確な橋渡しです。 ```agda module NM = Naming (Lset δ) ordW ``` 意味論的な目標は、命題的に切り詰められた `Under` の主張です。そこには二つの後続段階への所属とステップ比較が含まれますが、存在論理式を読むことで分かるのは、そのような証拠が存在することだけです。名前や六つの束縛対象をデータとして選ぶことはありません。 ```agda Goal : Type (ℓ-suc ℓ) Goal = ∥ Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ ``` 六つの証人で環境をすべて拡張した後、`StepHolds tw pw rl cs ro c0` は、最内部の `StepAt` 論理式が充足されることそのものです。これは六つの存在の層の内側にある最後の意味論的条件です。各層の証人を命題的切り詰めの下に置くのは周囲の束縛子であり、`StepHolds` 自体ではありません。 ```agda opaque StepHolds : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) StepHolds tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ⟩ ``` 最内部のペイロードは、`c0` を固定する等式とステップの充足そのものを含みます。これらはペイロード内では通常の連言の証拠であり、命題的切り詰めは外側の存在層によって導入されます。 ```agda Six : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) Six tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con (AllCodes ∅ʟ)) ⟩ × StepHolds tw pw rl cs ro c0 ``` 一層外では、`ro` が正準なコード順序に固定され、適切な `c0` の存在は命題的に切り詰められます。等式は意図した基礎集合を定めますが、証明が選択済みの存在証人を公開することはありません。 ```agda Five : (tw pw rl cs ro : S) → Type (ℓ-suc ℓ) Five tw pw rl cs ro = ⟨ (ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con codeOrder) ⟩ × ∥ (Σ[ c0 ∈ S ] Six tw pw rl cs ro c0) ∥₁ ``` コード集合の条件は、束縛された塔上の `cs` を特徴付けます。論理式を読むとき、その妥当性と先に得た塔の同定から `cs` の基礎集合が定まります。残る内側の証人は、なお命題的切り詰めの下にあります。 ```agda Four : (tw pw rl cs : S) → Type (ℓ-suc ℓ) Four tw pw rl cs = ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ × ∥ (Σ[ ro ∈ S ] Five tw pw rl cs ro) ∥₁ ``` 順序表の適用条件は、`rl` が復号された段階で記録された何らかの値であることを述べます。読み出す向きでは、`rl` はそこで記録された任意の値であり得るため、後の関係仮定はそのすべての値を全称的に扱う必要があります。埋める向きでは、与えられた特定の `rl` を使います。 ```agda Three : (tw pw rl : S) → Type (ℓ-suc ℓ) Three tw pw rl = ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ × ∥ (Σ[ cs ∈ S ] Four tw pw rl cs) ∥₁ ``` 定義可能冪集合の条件が `pw` を同定し、続く二つの連言が比較対象をともにそこへ置きます。`tw` と `pw` が同定されれば、これらの所属は `Lset (sucV δ)` への所属となり、`Under` が必要とする二つの領域成分を与えます。 ```agda Two : (tw pw : S) → Type (ℓ-suc ℓ) Two tw pw = ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ( ⟨ fst (lookup u γ) ∈ fst pw ⟩ × ( ⟨ fst (lookup v γ) ∈ fst pw ⟩ ``` 二つの所属の後、残るペイロードは表の値 `rl` の切り詰められた存在から始まります。最終目標 `Goal` 自体が命題なので、再利用できる証人の選択を取り出すことなく、各切り詰めをこの目標へ消去できます。 ```agda × ∥ (Σ[ rl ∈ S ] Three tw pw rl) ∥₁ ) ) ``` 最外部のペイロードは、段階グラフを満たす証人 `tw` から始まります。順序数性により、この記述は基礎集合の水準で一意なので、任意の充足する `tw` を `Lset δ` と同定できます。後続するすべての証人の入れ子の存在は、命題的に切り詰められたままです。 ```agda One : (tw : S) → Type (ℓ-suc ℓ) One tw = ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ × ∥ (Σ[ pw ∈ S ] Two tw pw) ∥₁ ``` ## 段階におけるステップの妥当性 六つの束縛要素のうち `StepAt` に入るのは五つだけであり、`pw` はその外側にある二つの所属条件で使われます。そこで `Slots` は、塔と符号集合を意図した対象と同一視し、`rl` が対ごとの表現性 `IsRel δ rl` をもつと仮定し、`ro` と `c0` を必要な二つの定数に固定します。これらは、先に証明した名前比較の妥当性定理が必要とする条件そのものです。 ```agda module Slots (tw pw rl cs ro c0 : S) (qtw : fst tw ≡ Lset δ) (hrel : IsRel δ rl) (qcs : fst cs ≡ fst (AllCodes (LsetS δ od))) (qro : fst ro ≡ fst codeOrder) ``` 整合の内部では、名前づけの妥当性が段階のもとで具体化され、その局所の一歩の比較が、コードの順序と関係の値のもとで開かれます。関係の表現の両方向が供給されます。 ```agda (qc0 : fst c0 ≡ fst (AllCodes ∅ʟ)) where private module A6 = At (Lset δ) (snd (LsetS δ od)) ordW module L6 = A6.Least codeOrder rl codeOrder-rep codeOrder-fill (ixRel-rep δ od rl hrel) (ixRel-fill δ od rl hrel) ``` これらの保証により、名前比較の定理を完全に拡張された環境で具体化できます。その七つの意味論的スロットは、比較される二対象と、`iTow`、`iRel`、`iCod`、`iOrd`、`iNil` が選ぶ五つの補助証人からなります。 ```agda module St = L6.Step iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) qro refl (Σ≡Prop (λ x → snd (isL x)) qtw) qcs qc0 ``` 第一の対象について、`LeastFst t` は「`t` がその最小名である」という主張の局所的な形です。そこに含まれる表示の等式は、`IsLeastName` の対応する等式とは逆向きです。以下の変換補題は、その等式を反転しながら同じ最小性の主張を保ちます。 ```agda LeastFst : NM.Name → Type (ℓ-suc ℓ) LeastFst = St.LeastOf (sh6 u) ``` `LeastSnd` は第二の対象について同じ橋渡しを与えます。`StepAt` は最小名の存在だけを述べるのではなく、一方の最小名を他方と比較するので、二つの述語を並行に保つことが必要です。 ```agda LeastSnd : NM.Name → Type (ℓ-suc ℓ) LeastSnd = St.LeastOf (sh6 v) ``` 公開された述語 `IsLeastName` と妥当性定理は、解釈の等式を互いに逆向きに述べます。パスの対称性で第一の対象の等式を変換し、極小性条件も各競合名の等式を同様に反転して移します。 ```agda leastFst-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup u γ)) → LeastFst t leastFst-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 第二の対象の変換も同じ形です。変わるのは等式の向きだけであり、最小性の数学的内容は保たれます。 ```agda leastSnd-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup v γ)) → LeastSnd t leastSnd-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 読み出す向きでは、同じ対称性によって第一の対象の `IsLeastName` を回復します。パスを二度反転すれば元の向きに戻るので、この変換で情報は失われません。 ```agda leastFst-out : (t : NM.Name) → LeastFst t → IsLeastName δ ordW t (fst (lookup u γ)) leastFst-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 第二の最小名述語も同じ方法で読み戻され、ホスト側のステップ補題に渡せる二つの通常の最小名の事実が得られます。 ```agda leastSnd-out : (t : NM.Name) → LeastSnd t → IsLeastName δ ordW t (fst (lookup v γ)) leastSnd-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 最内部の論理式に対する二つの意味論的な向きは、意図的に非対称です。二つの具体的な最小名とその比較が与えられると、`holds-in` は `StepHolds` を証明します。逆に `holds-out` が `StepHolds` から返すのは、適切な二つの最小名とその比較が存在することの命題的切り詰めだけであり、選ばれた名前の組が論理式の外へ出ることはありません。 ```agda opaque unfolding StepHolds ``` 内向きでは、`t₁` と `t₂` についての局所的な最小名の事実と `t₁ ≺ₙ t₂` を合わせると、最内部の論理式に必要な意味論的内容がすべて揃います。名前比較の妥当性定理は、まさにこの三つの事実を `StepHolds` へ移します。 ```agda holds-in : (t₁ t₂ : NM.Name) → LeastFst t₁ → LeastSnd t₂ → NM._≺ₙ_ t₁ t₂ → StepHolds tw pw rl cs ro c0 holds-in = St.StepAt-fill ``` 逆に、最内部の充足を読むと、命題的切り詰めの下で二つの最小名とその名前比較が得られます。この切り詰めは本質的です。結果は適切な名前の存在を述べますが、選択済みの一対を公開しません。 ```agda holds-out : StepHolds tw pw rl cs ro c0 → ∥ Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] (LeastFst t₁ × (LeastSnd t₂ × NM._≺ₙ_ t₁ t₂)) ∥₁ holds-out = St.StepAt-read ``` ## 束縛を読み解く 全体の読み出しは、充足する割り当てが与えるどの六証人に対しても働かなければなりません。最初の仮定は、`tw` が復号された段階のグラフ記述を満たし、`pw` がその上の定義可能冪集合の記述を満たし、第一の比較対象が `pw` に属することを述べます。後で一意性と妥当性を使い、これらを具体的な段階についての事実へ変換します。 ```agda private atAll : (tw pw rl cs ro c0 : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ ``` 続く仮定は、第二の所属、順序表の適用、コード集合の記述を与えます。特に、関係についての前提は、順序表が `δ` で記録するすべての `r` に及びます。読み出す向きでは、存在論理式がそのどの `rl` を束縛していてもよいからです。ここで最後に現れる等式は、`ro` を正準なコード順序に固定します。 ```agda → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → fst ro ≡ fst codeOrder ``` 外向きの議論は、ここで最内側の条件に到達します。六つの存在証人を同定すると、`atAll` は `StepAt` の充足から、二つの最小の名前とその名前比較が単に存在することを読み出します。次の議論をこの命題的切り詰めの上で写すことで、切り詰めの外へ名前を選び出すことなく、名前比較を必要なホスト側の `Under` 比較へ変換します。 ```agda → fst c0 ≡ fst (AllCodes ∅ʟ) → StepHolds tw pw rl cs ro c0 → Goal atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep = PT.map atNames (K.holds-out hstep) where ``` 塔の同定の等式が、論理式で束縛された塔が、入力の順序数での構成可能な段階に等しいことを、層の妥当性の補題で読み出します。 ```agda qtw : fst tw ≡ Lset δ qtw = Lset-only zero (suc d) (tw ∷ γ) hg od ``` 定義可能な部分集合の同定が、束縛された集合がその段階の定義可能冪集合であることを、塔の等式に沿って述べます。 ```agda qpw : fst pw ≡ 𝒟ₒ (Lset δ) qpw = subst ⟨_⟩ (DefAt-stage δ od zero (suc zero) (pw ∷ tw ∷ γ) qtw) hdef ``` 後続の段階への所属は、二度の輸送によって復元されます。最初の輸送が、構成可能な層の後続の恒等式を使って、定義可能冪集合と後続の段階を同一視します。二つ目の輸送が、束縛された集合がその定義可能冪集合と等しいという等式に沿って書き換えます。二つ合わせて、比較される対象を後続の段階 `Lset (sucV δ)` の中に置きます。 ```agda inSuc : (x : V ℓ) → ⟨ x ∈ fst pw ⟩ → ⟨ x ∈ Lset (sucV δ) ⟩ inSuc x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (Lset-suc δ)) (subst (λ z → ⟨ x ∈ z ⟩) qpw h) ``` 最初の比較の候補は、枠 `u` の基礎の集合であり、復元の補題によって後続の段階の要素として提示されます。 ```agda a : New δ a = fst (lookup u γ) , inSuc (fst (lookup u γ)) hu ``` 二つ目の比較の候補は、枠 `v` の基礎の集合で、同様に提示されます。 ```agda b : New δ b = fst (lookup v γ) , inSuc (fst (lookup v γ)) hv ``` 適用論理式の充足は、`rl` が表の `δ` に記録された値であることを述べます。外向きの仮定 `vals` は、そのように記録されたすべての値を意図的に対象とするため、`Stp` の内部で選ばれたこの証人についても `IsRel δ rl` を与えます。これは可能な表の証人すべてに対する健全性の条件であり、表の値の一意性を主張するものではありません。 ```agda hrel : IsRel δ rl hrel = vals rl (subst ⟨_⟩ (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ pw ∷ tw ∷ γ)) happ) ``` 符号集合の記述を外向きに読むと、`cs` は `AllCodes (LsetS δ od)`、すなわち現在の段階 `Lset δ` 上の符号集合と同一視されます。比較される対象は後続段階に属しますが、その名前は直前の段階に関して作られるので、ここでの符号集合は `sucV δ` ではなく `δ` で添字づけられます。 ```agda qcs : fst cs ≡ fst (AllCodes (LsetS δ od)) qcs = cong fst (CodesAt-out (LsetS δ od) zero (sh3 zero) (cs ∷ rl ∷ pw ∷ tw ∷ γ) qtw hcs) ``` 塔、段階関係、符号集合、二つの固定された符号対象がすべて同定されたので、`Slots` は六つの証人を、すでに証明された名前比較の妥当性定理へ接続します。この共通の具体化により、残りの議論では最内側の論理式と対応する最小名のデータを相互に読み替えられます。 ```agda module K = Slots tw pw rl cs ro c0 qtw hrel qcs qro qc0 ``` 名前の妥当性定理が返す命題的切り詰めの内部で、`t₁` と `t₂` を比較される二つの集合の最小名とし、`t₁ ≺ₙ t₂` とします。目標の `Under` は最後の比較だけでなく、二つの集合がともに `Lset (sucV δ)` に属することも記録します。この二つの所属成分は、すでに `a` と `b` によって得られています。 ```agda atNames : Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] ( K.LeastFst t₁ × ( K.LeastSnd t₂ × NM._≺ₙ_ t₁ t₂ ) ) → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) atNames (t₁ , (t₂ , (l₁ , (l₂ , lt)))) = a .snd ``` 二つの最小名についての外向きの読みは、局所的な述語を `IsLeastName` へ戻します。続いて `stepAt-fill` は、これらの最小名の比較から、それらが表す新しい要素の間の `stepOrder δ od` 関係が従うことを示します。直前に得た二つの所属と合わせて、`Under` が完成します。 ```agda , ( b .snd , stepAt-fill δ ordW a b t₁ t₂ (K.leastFst-out t₁ l₁) (K.leastSnd-out t₂ l₂) lt ) ``` ## 束縛を組み立てる 逆向きの議論では、実際の表の値 `rl` と、それが表の `δ` に記録され、必要な段階関係を表すことの証拠を固定します。さらに、`Under` 比較が含む二つの後続段階への所属も固定します。外向きの場合と異なり、この構成では具体的な局所表の値が手元にあるため、それを `Stp` の三番目の存在証人として使えます。 ```agda module Pack (rl : S) (hpr : ⟨ pr δ (fst rl) ∈ fst (lookup f γ) ⟩) (hrel : IsRel δ rl) (hx : ⟨ fst (lookup u γ) ∈ Lset (sucV δ) ⟩) (hy : ⟨ fst (lookup v γ) ∈ Lset (sucV δ) ⟩) where ``` 組み立てる議論では、`Stp` が定める順序で六つの証人を使います。すなわち `towerS δ od`、`powS δ od`、与えられた表の値 `rl`、`AllCodes (LsetS δ od)`、`codeOrder`、`AllCodes ∅ʟ` です。特に第四の証人は現在の段階 `Lset δ` 上の符号集合であり、その後続段階に属するのは比較される二つの対象です。 ```agda private module K = Slots (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) (towerS-fst δ od) hrel refl refl refl ``` 最初の比較の候補は、後続の段階での所属によって提示されます。 ```agda a : New δ a = fst (lookup u γ) , hx ``` 二つ目の比較の候補も同じように提示されます。 ```agda b : New δ b = fst (lookup v γ) , hy ``` 固定されたホスト側の整列順序 `ordW` に関して、各新要素には最小名があるので、最初の候補から名前とその `IsLeastName` の証明の組が得られます。これは論理式を満たすための明示的で局所的な証人であり、`Stp` が名前を一意に定めると主張するものではありません。 ```agda n₁ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup u γ)) n₁ = leastNameOf δ ordW a ``` 同じ定理から、二つ目の候補についても最小名が得られます。局所的に選んだ二つの名前を比較し、`StepAt` の内向きの妥当性定理へ渡します。その論理式の存在の意味論と、それを囲む `Stp` の六つの存在束縛子によって、名前は再び隠されます。この構成が選ばれた名前の組を外へ出すことはありません。 ```agda n₂ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup v γ)) n₂ = leastNameOf δ ordW b ``` 最初の証人には `towerS δ od` を取ります。その定義定理は、これが拡張された環境で `LsetGraphAt` を満たし、したがって第一の束縛子が要求する `Lset δ` を基礎集合にもつことを示します。 ```agda hg : ⟨ (towerS δ od ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ hg = Lset-defines zero (suc d) (towerS δ od ∷ γ) od (towerS-fst δ od) ``` 二つ目の証人は `powS δ od` であり、その基礎集合は定義可能部分集合の集合 `𝒟ₒ (Lset δ)` です。`DefAt-stage` が与える等式は `DefAt` の充足を特徴づけます。この特徴づけに沿って `powS-fst` を輸送すると、必要な充足の主張が得られます。ここで使うのはこの段階の定義可能部分集合の集合であり、完全な冪集合ではありません。 ```agda hdef : ⟨ (powS δ od ∷ towerS δ od ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hdef = subst ⟨_⟩ (sym (DefAt-stage δ od zero (suc zero) (powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od))) (powS-fst δ od) ``` `Stp` の二つの所属の連言を満たすため、ここで必要なのは後続段階から選ばれた定義可能部分集合の対象へ向かう向きです。等式 `Lset-suc δ` により、`Lset (sucV δ)` への所属を `𝒟ₒ (Lset δ)` への所属へ書き換え、さらに `powS-fst` により、それを `powS δ od` の基礎となる集合への所属へ書き換えます。 ```agda inPow : (x : V ℓ) → ⟨ x ∈ Lset (sucV δ) ⟩ → ⟨ x ∈ fst (powS δ od) ⟩ inPow x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (powS-fst δ od)) (subst (λ z → ⟨ x ∈ z ⟩) (Lset-suc δ) h) ``` 適用の充足は、表の項目の証明から、適用の符号化の妥当性に沿って運ばれます。 ```agda happ : ⟨ (rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ powS δ od ∷ towerS δ od ∷ γ))) hpr ``` 第四の証人について、`CodesAt` の内向きの読みは、`AllCodes (LsetS δ od)` が塔 `Lset δ` 上の符号集合の記述を満たすことを示します。後続段階上の符号集合は必要ありません。 ```agda hcs : ⟨ (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ hcs = CodesAt-in (LsetS δ od) zero (sh3 zero) (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od) refl ``` ホスト側の `stepOrder` 比較を仮定します。すでに選んだ二つの最小名は、内向きの等式の向きを調整すると、局所的な最小名述語を満たします。残るのは、ホスト側の比較を最内側の `StepAt` 論理式が要求する名前比較へ変換することだけです。 ```agda hstep : relOf (stepOrder δ od) a b → StepHolds (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) hstep cmp = K.holds-in (n₁ .fst) (n₂ .fst) (K.leastFst-in (n₁ .fst) (n₁ .snd)) (K.leastSnd-in (n₂ .fst) (n₂ .snd)) ``` 定理 `stepAt-read` は、`n₁` と `n₂` の最小性の証明を使って、ちょうどこの変換を行います。得られた名前比較を `holds-in` に渡すと、最内側の充足が証明されます。この議論は既存のホスト側の `stepOrder` を用いるのであり、新しい整列順序を構成するものではありません。 ```agda (stepAt-read δ ordW a b (n₁ .fst) (n₂ .fst) (n₁ .snd) (n₂ .snd) cmp) ``` 対象言語の六つの存在量化は、依存対の命題的切り詰めが六重に入れ子になったものとして解釈されます。`packAll` は `towerS δ od` とその `LsetGraphAt` の証明から、この入れ子を組み始めます。証明の内部では具体的な証人を構成しますが、最も外側の存在の境界では、その命題的切り詰めだけが直ちに残ります。 ```agda packAll : relOf (stepOrder δ od) a b → ∥ (Σ[ tw ∈ S ] One tw) ∥₁ packAll cmp = ∣ towerS δ od , ( hg , ∣ powS δ od ``` 第二の証人は `powS δ od` であり、`DefAt` の充足と、後続段階から輸送した二つの所属が付随します。第三の証人は与えられた表の値 `rl` であり、その順序対の所属証明から必要な `appAt` の充足が得られます。したがって、埋める向きでは、表から値を選ぶのではなく、呼び出し側がすでに与えた特定の関係値を使います。 ```agda , ( hdef , ( inPow (fst (lookup u γ)) hx , ( inPow (fst (lookup v γ)) hy , ∣ rl , ( happ ``` 符号の集合の充足のあとに、符号の順序の要素とその同定の等式が続き、さらに空のアルファベットの符号の集合が続きます。 ```agda , ∣ AllCodes (LsetS δ od) , ( hcs , ∣ codeOrder , ( refl , ∣ AllCodes ∅ʟ ``` 最後の包み込みでは、空のアルファベットの符号集合、それを同定する等式、最内側のステップ論理式の充足を挿入します。六つの切り詰めをすべて閉じることで `Stp` が証明されますが、選んだ塔、関係、符号、名前の証人は後の利用者へ公開されません。 ```agda , ( refl , hstep cmp ) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ ) ) ) ∣₁ ) ∣₁ ``` ## 二つの読み 二つの読みは、再帰的な表が必要とする正確なインターフェースを与え、その型が本質的な非対称性を記録します。外向きは、その段階で記録されたすべての関係値を扱わなければならず、返すのは `∥ Under ... ∥₁` だけです。内向きは、指定された一つの記録済みの値とその `IsRel` の証明、さらに切り詰められていない `Under` の比較を受け取り、そこから `Stp` の充足を構成します。 ```agda opaque unfolding Stp StepHolds ``` 外向きの読みでは、表の `δ` に記録されたすべての値が必要な段階関係を表すと仮定します。`Stp` の充足が与える存在証人は命題的に切り詰められているため、`read` は六つの切り詰めを一つずつ、同じく命題的に切り詰められた `Goal` へ除去します。 ```agda read : ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → ⟨ γ ⊨ Stp d f u v ⟩ → Goal read vals = PT.rec PT.squash₁ (λ { (tw , (hg , hpw)) → PT.rec PT.squash₁ (λ { (pw , (hdef , (hu , (hv , hrl)))) → PT.rec PT.squash₁ ``` 除去は束縛子の順、すなわち塔、定義可能部分集合の集合、表の値、符号集合、符号順序、空のアルファベットの符号集合の順に進みます。各段階の証人は次の切り詰めを扱う継続の内部でだけ利用でき、選択された六つ組が返されることはありません。 ```agda (λ { (rl , (happ , hcs)) → PT.rec PT.squash₁ (λ { (cs , (hcs , hro)) → PT.rec PT.squash₁ (λ { (ro , (qro , hc0)) → PT.rec PT.squash₁ (λ { (c0 , (qc0 , hstep)) → atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep }) ``` 六つの証人とその条件が局所的にすべて揃うと、`atAll` は命題的に切り詰められた `Under` 比較を返します。その後、入れ子の除去子が構文とは逆の順で閉じられ、対象言語の存在量化が要求する切り詰めの境界が保たれます。 ```agda hc0 }) hro }) hcs }) hrl }) hpw }) ``` 内向きの読み出しは、特定の表の値と、その所属と関係の証明と、二つの所属の証明とホスト側の比較を消費して、すべてを六重の存在量化の中にまとめます。 ```agda fill : (r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ fill r hpr hrel (hx , (hy , cmp)) = Pack.packAll r hpr hrel hx hy cmp ``` ステップの論理式の外向きの読み出しが、最初の妥当性の方向として書き出されます。充足が、切り詰められたステップの比較を含意する、というものです。 ```agda stp-out : StpOut Stp stp-out = Reading.read ``` ## フレームを具体化する ステップの論理式の内向きの読み出しが、二つ目の妥当性の方向として書き出されます。正しい関係をもつ特定の表の値とホスト側の比較が合わせて、論理式の充足を含意する、というものです。 ```agda stp-in : StpIn Stp stp-in = Reading.fill ``` `Stp` とこの二つの読みを抽象的な構成へ与えることで、段階順序の表が完全に具体化されます。とくに各順序数段階について内部集合 `relL` と `relL-fill`、`relL-rep` が得られ、`orderAt` のホスト側の関係と、対応する順序対が `relL` に属することを要素ごとに相互変換できます。ここで得られるのは関係グラフの表現であり、`relL` が整列順序の論理式を満たすという対象言語の主張は証明されていません。 ```agda open Ordered Stp stp-out stp-in public ``` ## 上界順序数における順序 構成可能集合 `a` に対し、`stageBound` は `ω` と `a` が最初に現れる段階の両方より上にある順序数を選びます。したがって `Lset boundOrd` は、`a` の要素と、さらにそれらの要素を含むのに十分高く、後の横断集合の議論に必要な局所的な論域となります。選ばれた上界はこの目的には十分ですが、`a` に対する最小の上界または一意に定まる上界だとは主張しません。 ```agda module Bound (a : V ℓ) (p : ⟨ isL a ⟩) where boundOrd : V ℓ boundOrd = stageBound a p .fst ``` 同じ上界の結果は、`boundOrd` が順序数であることも証明します。この証明により、すでに構成されているホスト側の族 `orderAt` を段階 `Lset boundOrd` に特殊化できます。 ```agda boundOrd-ord : IsOrd boundOrd boundOrd-ord = stageBound a p .snd .fst ``` この添字で内部の関係対象を得るには、表の構成は添字自身が構成可能であることも必要とします。順序数は自分自身の後続段階に属するので、`boundOrd ∈ Lset (sucV boundOrd)` が、`Lset→isL` によって `isL boundOrd` を示すための証人になります。 ```agda boundOrd-isL : ⟨ isL boundOrd ⟩ boundOrd-isL = Lset→isL (sucV boundOrd) (suc-ord boundOrd-ord) boundOrd (ord∈Lset-suc boundOrd boundOrd-ord) ``` 表現する関係は、すでに存在するホスト側の狭義整列順序 `orderAt boundOrd boundOrd-ord` であり、その台は `Mem (Lset boundOrd)` です。整列順序の構造はこの `SWO` 値が持っており、以下の行はその二項関係を `L` の内部の集合として実現するだけです。 ```agda boundOrder : SWO (Mem (Lset boundOrd)) boundOrder = orderAt boundOrd boundOrd-ord ``` 表は、選ばれた順序数におけるこの内部集合を `relL` として与えます。したがって `orderL` はモデルの要素であり、その要素は関係グラフの順序対を表します。これは新しい整列順序の構成ではなく、整列順序の公理を対象理論の内部で満たすという証明も、ここでは付与されません。 ```agda orderL : S orderL = relL boundOrd boundOrd-isL boundOrd-ord ``` 順方向の表現補題は、ホスト側の比較 `relOf boundOrder x y` から、符号化された順序対 `pr (fst x) (fst y)` を `orderL` に入れます。これにより、既存の `SWO` の関係とその内部グラフとの要素ごとの対応の一方向が得られます。 ```agda orderL-fill : (x y : Mem (Lset boundOrd)) → relOf boundOrder x y → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ orderL-fill = relL-fill boundOrd boundOrd-isL boundOrd-ord ``` 逆に、符号化された順序対が `orderL` に属することから、ホスト側の比較を復元できます。`orderL-fill` と `orderL-rep` を合わせると、どの順序対が内部の関係グラフに現れるかが要素ごとに正確に特徴づけられます。これらは、そのグラフを表す集合の一意性を主張せず、それが整列順序であることを対象言語の内部で証明するものでもありません。 ```agda orderL-rep : (x y : Mem (Lset boundOrd)) → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ → relOf boundOrder x y orderL-rep = relL-rep boundOrd boundOrd-isL boundOrd-ord ``` ## まとめ 狭義整列順序そのものは、`Mem (Lset α)` 上のホスト側の構造 `orderAt α oα` です。集合 `relL α hα oα` は、その二項関係を関係グラフとして表す `L` の要素であり、`relL-fill` と `relL-rep` は、各要素対についてその表現の二方向を証明します。六つの束縛子をもつ論理式とその妥当性の読みは、この関係グラフを後の対象言語の論理式から利用できるようにしますが、新しい整列順序も、対象言語における整列順序の主張も証明しません。