---
title: "Skolem 包を構成して崩壊させる"
module: L.GCH.SkolemHull
lang: ja
site: "Bedrock"
description: "Skolem 包を構成して崩壊させる"
stage: "GCH の証明"
reading_order: 105
canonical: https://bedrock.institute/ja/L.GCH.SkolemHull.html
html: L.GCH.SkolemHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SkolemHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, FOL.Manipulation.ConstantOccurrences, FOL.Semantics, FOL.Manipulation.ParameterAbstraction, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, V.Hierarchy, V.Presentation, V.Collapse, V.Smallness, L.Axioms.Basic, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Rank, L.WellOrder.Base, L.Choice.StageOrders, L.Coding.CodeConstructibility]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.SkolemHull.md, https://bedrock.institute/zh/L.GCH.SkolemHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Skolem 包を構成して崩壊させる

本章は、構成可能段階の中の始集合の Skolem 包を作り、包が段階の中で初等的であることを示し、所属を保つ全単射によって推移的集合へ崩壊させ、充足関係と有界論理式が崩壊を越えてどう移るかを整理します。重要なのは、包そのものはコードで与えられた像にすぎず、推移性は Mostowski 崩壊の後に初めて得られる、という点です。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

本章は古典論理に依拠し、仮定はここで入ります。包の構成は問いの充足可能性を判定し、外延性の証明は両方向で所属を判定し、初等性の移送は二重否定を除去します。これらの段階はどれも排中律を消費します。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

モジュールは宇宙レベル `ℓ` を固定し、本書の常の形式に従って古典的な仮定を明示的に受け取ります。`ℓ-suc ℓ` での排中律が引数として渡され、大域的に仮定されることはなく、本章の各定理はどのレベルの実例を使うかを正確に記録します。

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

対象言語は本書の一階の言語です。論理式は項から等号と所属で作られ、命題の結合子、非有界と有界の量化子の下で閉じています。述語 `Δ₀` は、すべての量化子が有界である論理式を選び出します。

```agda
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure; _↾_ )
open import FOL.Syntax using
  ( Formula; Term; con; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊥̇
  ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
```

述語 `Δ₀` は論理式の構造に沿う帰納的な証拠です。その構成子は原子式・結合子・有界量化子を覆いますが、非有界量化子に対応する構成子はありません。この証拠が後の絶対性の議論を支え、`countFo` と `constantsFo` は定数の各出現を記録します。

```agda
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Absoluteness
import FOL.Manipulation.ConstantOccurrences
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )
```

パラメータ抽象は定数の出現を追加の環境変数で置き換え、定数写像と定数改名は意味を保って定数アルファベットを変えます。`renameTm` は文脈写像に沿って変数の位置を改名し、これにより以下で `suc` による弱化が得られます。周囲の階層は外延性とともに開かれます。同じ要素をもつ集合は等しい、という性質です。

```agda
open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm; mapFo-comp; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀; ⊨-map )
open import FOL.Manipulation.Renaming using ( renameTm )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
```

提示は、埋め込みをもつ小さな型で集合の要素を索引づけ、その繊維が提示された要素を名指します。崩壊は任意の台 `X` から推移的な像を構成し、崩壊写像を `X` 上で単射にするために制限された所属関係の外延性を用います。Δ₀ の小ささは、有界に定義できるクラスを集合へ分離します。空集合は各定義可能性後続に属し、`Lset-suc` は後続添字の段階を直前の段階の定義可能冪集合と同一視します。

```agda
open import V.Presentation {ℓ} using ( member; fiber )
open import V.Collapse {ℓ} using ( module Collapse; isExt; isTrans )
open import V.Smallness {ℓ} using ( separateFromSmall; module Δ₀Small )
open import L.Axioms.Basic {ℓ} using ( ∅∈𝒟ₒ; Lset-suc )
open import L.Constructible {ℓ}
```

構成可能な段階 `Lset α` は推移的であり、その構成は指数について単調なので、より大きな指数はより大きな段階を与えます。包の議論で繰り返し使う順序数の事実は、順序数の要素が順序数であること、`ω` が順序数であること、数項が `ω` に属すること、空集合が順序数であることです。

```agda
  using ( 𝒮ʟ; isTransV; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ
        ; layer-trans; Lset-layer )
open import L.Ordinal {ℓ} using ( mem-ord; ω-ord; #∈ω; ∅-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈; rank-Lset )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
```

整列順序には最小要素の選択子が伴います。述語を満たす要素の存在の切り詰められた主張から、述語を満たし整列順序で最小の要素を返します。段階の所属のランクによる特徴づけと、段階の台に制限した段階の順序がこの選択子に入力を供給し、和と単元を符号化する仕組みが、後で使う有限の始集合を作ります。

```agda
open import L.Rank {ℓ} using ( rank-fix )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; leastOf )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt )
open import L.Coding.CodeConstructibility {ℓ} using ( cup-out; cup-inl; cup-inr; sgl-out )
```

本章の環境は台の要素のベクトルであり、その演算は成分ごとに行われます。関数を環境へ写すこと、索引で参照すること、要素を一つ加えて延ばすこと、そして連結です。第二成分が命題である対は、要素を、決して区別しない証拠とともに記録します。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( Vec; map; lookup; _∷_; []; _++_ )
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_; _,_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
```

空型は矛盾を表します。`Empty.rec` はその要素から任意の目標へ消去し、`isProp⊥` は目標が矛盾であるとき命題的切り詰めの消去を可能にします。存在論理式の充足と提示された集合への所属は命題的切り詰めで表され、証人を選ばずに存在だけを保持します。

```agda
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

累積階層は添字型と評価で集合を提示します。包では有限木型 `Code` を添字型とし、論理式は証人コードの一部ですが、それ自体がコードなのではありません。構成は、空集合、和、非順序対と一元集合の構成、そして無限順序数とその後続を供給します。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; _∪_; ⁅_,_⁆; ⁅_⁆s; union-ax; pairing-ax; module InfinitySet
        ; SetPackage; SingletonPackage )  -- lint-agda: keep (SetPackage via record projection)
open InfinitySet using ( ω; sucV )
```

小さな所属の関係 `_∈ₛ_` と、周囲の所属 `_∈ˢ_` への橋 `∈∈ₛ` は、集合の提示された読みと、階層の中での読みをつなぎます。提示が内部的に記録することは、宇宙で成り立つことと同じです。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; extensionality )
```

周囲の構造を開くことで、修飾のない等号と所属の記号は周囲の関係を表します。一方、制限された各構造は固有の意味論的解釈をもちます。

```agda
open hPropStructure 𝒮ᵥ
```

`SemV` は、以下で充足関係を具体化するときに使う固定長の周囲環境を与えます。定数が `𝒮ʟ` を動く論理式では、出現回数によって定数を含まない場合を識別できます。そのとき `erase` は、充足を変えずに定数領域を空の型へ置き換えます。

```agda
module SemV = FOL.Semantics 𝒮ᵥ using ( _^_; module At )
open SemV using ( _^_ )
module CS = hPropStructure 𝒮ʟ using ( S )
module Cnt = FOL.Manipulation.ConstantOccurrences.ZeroOccurrences CS.S using ( erase; erase-inv )
```

空の定数領域では、`Δ₀-small` は各有界論理式の各環境での真理値が一段低い宇宙の命題と同値であることを示します。分出にはさらに `separateFromSmall` を適用する必要があります。そして項代数が始まります。構造、その台を周囲の宇宙へ写す写像、そして台の上の整列順序を引数とするのです。

```agda
module D0 = Δ₀Small {ℓc = ℓ-suc ℓ} {K = ⊥* {ℓ-suc ℓ}} (λ b → Empty.rec* b)
  using ( Δ₀-small )
module TermAlgebra (𝒮 : ZFStructure (ℓ-suc ℓ))
                   (toSet : ZFStructure.S 𝒮 → V ℓ)
                   (wo : SWO (ZFStructure.S 𝒮))
```

残りの引数は、既定の要素 `junk` と、`K` で索引づけられた基底の生成元の族です。`K` を始集合の提示と同一視するのは、後の包の実例です。既定の値は簿記のためのもので、後の構成がそれを調べることはありません。

```agda
                   (junk : ZFStructure.S 𝒮)
                   {K : Type ℓ} (emb : K → ZFStructure.S 𝒮) where
```

ここで隠すのは引数構造の修飾されていない Agda 名 `_∈ˢ_` だけであり、充足関係 `_⊨₀_` の原子的所属は引き続き `𝒮` によって解釈されます。台の名前を替えるのは、本章が周囲の台を指すときの曖昧さをなくすためです。

```agda
  open ZFStructure 𝒮 hiding ( _∈ˢ_ ) renaming ( S to S𝒮 )
```

項代数の充足は、自明に空な定数領域のもとで述べられます。評価される論理式は、定数記号を使わずに作られたものだけで、純粋な所属と等号の言語であり、充足は命題値です。この節の各問いと閉包の主張は、すべてこの読みを用います。

```agda
  private module Sem = FOL.Semantics 𝒮
  open Sem using () renaming ( _^_ to _^𝒮_ )
  module At0 = Sem.At (⊥* {ℓ}) Empty.rec* using ( _⊨_ )
  _⊨₀_ : {n : ℕ} → S𝒮 ^𝒮 n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
  _⊨₀_ = At0._⊨_
```

コードは、基底の生成元の上の有限な木の代数を作ります。基のコードは生成元を名指し、証人のコードは、アリティが `suc k` の問いと `k` 個の引数のコードを記録します。`Code` は帰納型なので各コードは有限木であり、`cs` の各成分はその直接の引数部分木です。各部分木は基コードでも証人コードでもかまいません。

```agda
  data Code : Type ℓ where
    base : K → Code
    wit  : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec Code k → Code
```

`Sat k ψ vs` は、任意の引数のベクトル `vs` のもとで `ψ` を満たす要素の単なる存在です。閉包の定理は後に `vs` をコードの値として特殊化します。充足可能性は切り詰められた存在として述べられ、証人を産み出すことなく、存在を主張するだけです。

```agda
  Sat : (k : ℕ) → Formula (⊥* {ℓ}) (suc k) → Vec S𝒮 k → Type (ℓ-suc ℓ)
  Sat k ψ vs = ∥ Σ[ a ∈ S𝒮 ] ⟨ (a ∷ vs) ⊨₀ ψ ⟩ ∥₁
```

この切り詰められた存在が与えられれば、`search` は、引数 `wo` として渡された特定の狭義整列順序のもとで最小の充足要素を返します。最小とはその整列順序での最小のことであり、所属に関する極小でもランクの比較でもありません。

```agda
  search : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec S𝒮 k)
         → Sat k ψ vs → S𝒮
  search k ψ vs w = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vs) ⊨₀ ψ) w .fst
```

コードのベクトルは成分ごとに評価され、単一のコードの評価と相互に定義されます。証人のコードの引数の値は、その成分のコードの値です。

```agda
  mutual
    vals : {m : ℕ} → Vec Code m → Vec S𝒮 m
    vals [] = []
    vals (c ∷ cs') = val c ∷ vals cs'
```

充足可能な証人のコードは最小の充足要素へ評価され、充足しない証人のコードは `junk` へ評価されます。すべてのコードが像に値を供給するため、`junk` が包の中に現れることもあります。しかし `val-wit` が示すのは、充足可能性が与えられれば `junk` は無関係だということです。

```agda
    val : Code → S𝒮
    val (base m) = emb m
    val (wit k ψ cs) = Sum.rec (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

この小さな補題は、命題の目標に要素があると分かったとき、古典的な判定がどのように使われるかを記録します。判定が左枝なら、命題性によりその要素は `x` と同一視され、消去結果は `f x` になります。右枝なら、その否定は `x` と矛盾するため、その場合は不可能です。

```agda
  sum-stuck : {X : Type (ℓ-suc ℓ)} (x : X) (px : isProp X)
            → (f : X → S𝒮) (g : (X → Empty.⊥) → S𝒮) (s : X ⊎ (X → Empty.⊥))
            → Sum.rec f g s ≡ f x
  sum-stuck x px f g (Sum.inl x') = sym (cong f (px x x'))
  sum-stuck x px f g (Sum.inr h)  = Empty.rec (h x)
```

証人コードに格納された問いの充足可能性の証拠が与えられると、この補題は、そのコードの値が探索の最小の充足要素と同一視されることを示します。既定の枝は反証され、証人のある枝が探索を実行します。

```agda
  val-wit : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
          → (w : Sat k ψ (vals cs)) → val (wit k ψ cs) ≡ search k ψ (vals cs) w
  val-wit k ψ cs w = sum-stuck w squash₁ (search k ψ (vals cs)) (λ _ → junk)
                       (lem (Sat k ψ (vals cs) , squash₁))
```

コードのベクトルの評価は、その上で評価を写すことと同じであり、簡単な再帰で示されます。これにより、後の主張は環境の再帰的な形と写した形の間を自由に行き来できます。

```agda
  vals≡map : {m : ℕ} (cs : Vec Code m) → vals cs ≡ map val cs
  vals≡map [] = refl
  vals≡map (c ∷ cs') = cong₂ _∷_ refl (vals≡map cs')
```

包の提示は、階層が集合を提示するのと同じ仕方です。コードの族と評価によります。包はすべてのコードの値の像であり、異なるコードが同じ値に評価されうるので、提示は要素を重複して持ちえます。したがって包の中の所属は、コードの存在の切り詰められた主張にすぎず、包が推移的であることや、最小の閉じた集合であることは、本章では主張されません。

```agda
  Hull : V ℓ
  Hull = sett Code (λ c → toSet (val c))
```

提示の中の所属は直接です。どのコードの値も包の要素であり、その証人はそのコード自身です。

```agda
  inHull : (c : Code) → ⟨ toSet (val c) ∈ˢ Hull ⟩
  inHull c = ∣ c , refl ∣₁
```

こうして、充足可能な符号化された問いはどれも、包の中に充足する証人をもちます。この定理が主張するのはこの閉包の性質であり、包のすべての要素を成功した最小の証人として特徴づけるものではありません。

```agda
  closed : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k)
         → Sat k ψ (vals cs)
         → ∥ Σ[ a ∈ S𝒮 ]
              (⟨ toSet a ∈ˢ Hull ⟩ × ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩) ∥₁
  closed k ψ cs w = ∣ a , a∈H , sat ∣₁
```

証人を改めて探す必要はありません。項代数がすでに割り当てた値、すなわち探索が返した最小の充足要素がそれです。

```agda
    where
    a : S𝒮
    a = search k ψ (vals cs) w
```

選択子は `a` と `IsLeast` の二成分、すなわち `a` が問いを満たす証明と、それより真に小さい充足要素がない証明を返します。この行は前者を射影します。

```agda
    pa : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    pa = leastOf wo {ℓ'' = ℓ-suc ℓ} lem (λ a → (a ∷ vals cs) ⊨₀ ψ) w .snd .fst
```

証人が包に属することは、まさにこの問いのために作られた証人のコードから来ます。その値は `val-wit` によって探索の結果と同一視され、すべてのコードの値は包の中にあります。

```agda
    a∈H : ⟨ toSet a ∈ˢ Hull ⟩
    a∈H = subst (λ z → ⟨ toSet z ∈ˢ Hull ⟩) (val-wit k ψ cs w)
            (inHull (wit k ψ cs))
```

充足は記録された成分であり、閉包の節はこれで完成です。

```agda
    sat : ⟨ (a ∷ vals cs) ⊨₀ ψ ⟩
    sat = pa
```

## 台の写像に沿って充足関係を移す

包が作られ閉じたので、本章は二つ目の作業、構造の間の充足の移送に移ります。移送は、周囲の台の上の二つの述語に対して述べられます。

```agda
module SatTransfer (MA MB : S → hProp (ℓ-suc ℓ)) where
```

源の台は、周囲の台の各要素と、それが第一の述語を満たすことの証明の対です。その論理式は、このような対のもとでのみ読まれます。

```agda
  SA : Type (ℓ-suc ℓ)
  SA = Σ[ x ∈ S ] ⟨ MA x ⟩
```

目標の台は、第二の述語に対する同じ構成であり、そこの充足は同じ論理式の目標の読みです。

```agda
  SB : Type (ℓ-suc ℓ)
  SB = Σ[ x ∈ S ] ⟨ MB x ⟩
```

源の構造は、対になった台のもとで論理式を読みます。項の辞書は変数を対の要素として評価し、充足は命題値です。

```agda
  module SemA = FOL.Semantics (𝒮ᵥ ↾ MA)
    using ( module At )
  module SemB = FOL.Semantics (𝒮ᵥ ↾ MB)
    using ( module At )
  open SemA.At SA id renaming ( _⊨_ to _⊨ᴬ_ ; ⟦_⟧ to ⟦_⟧ᴬ )
```

目標の構造は、反対側で同じことを行い、固有の充足と固有の項の辞書をもちます。

```agda
  open SemB.At SB id renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```

移送は二つの原理で組織されます。一致とは、すべての論理式と環境に対して、左の充足と写された環境での写された論理式の充足が等しい、という命題の等式です。次に述べる証人の原理は存在量化の逆向きを支えます。目標側の存在が成り立つとき、その像が行列を充足する `q : SA` が単に存在すればよいのです。

```agda
  Agree : (SA → SB) → Type (ℓ-suc (ℓ-suc ℓ))
  Agree g = (n : ℕ) (φ : Formula SA n) (δ : SA ^ n)
          → (δ ⊨ᴬ φ) ≡ (map g δ ⊨ᴮ mapFo g φ)
  Witness : (SA → SB) → Type (ℓ-suc ℓ)
  Witness g = (n : ℕ) (φ : Formula SA (suc n)) (δ : SA ^ n)
```

この `q` が、すでに選ばれた目標側の証人の逆像である必要はありません。この原理が主張するのは、その像が行列を充足する内側の点の存在の切り詰められた主張であり、これがまさに存在量化の逆方向が消費する形です。

```agda
            → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ φ) ⟩
            → ∥ Σ[ q ∈ SA ] ⟨ (g q ∷ map g δ) ⊨ᴮ mapFo g φ ⟩ ∥₁
```

移送のモジュールは、写像と原子的な仮定を受け取ります。原子的な所属と等号には、`g` を越えた双方向の一致が必要です。そうして初めて、帰納の中の所属と等号のアトムが命題のパスになります。

```agda
  module Along (g : SA → SB)
    (at∈ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ∈̇ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ∈̇ u)))
    (at≐ : (n : ℕ) (t u : Term SA n) (δ : SA ^ n)
         → (δ ⊨ᴬ (t ≐ u)) ≡ (map g δ ⊨ᴮ mapFo g (t ≐ u)))
```

証人の原理が第三の仮定であり、移送のデータはこれでそろいます。

```agda
    (wit : Witness g) where
```

最初の弱化補題は源の構造で述べられます。`suc` による改名は各既存変数を環境の新しい先頭要素の後へずらすため、`x ∷ δ` での評価は `δ` での評価に戻り、定数は影響を受けません。

```agda
    private
      renA : {n : ℕ} (t : Term SA n) (x : SA) (δ : SA ^ n)
           → ⟦ renameTm suc t ⟧ᴬ (x ∷ δ) ≡ ⟦ t ⟧ᴬ δ
      renA (con c) x δ = refl
      renA (var i) x δ = refl
```

同じ弱めは目標の構造でも成立します。次の主張は、写しと弱めの比較を始めます。

```agda
      renB : {n : ℕ} (t : Term SB n) (x : SB) (δ : SB ^ n)
           → ⟦ renameTm suc t ⟧ᴮ (x ∷ δ) ≡ ⟦ t ⟧ᴮ δ
      renB (con c) x δ = refl
      renB (var i) x δ = refl
      mapTm-ren : {n : ℕ} (t : Term SA n)
```

写しと弱めは項の上で交換します。これは定義的なことで、弱めた項の写しは、改名された各成分を順に弱めます。

```agda
                → mapTm g (renameTm suc t) ≡ renameTm suc (mapTm g t)
      mapTm-ren (con c) = refl
      mapTm-ren (var i) = refl
```

写して弱めた項を任意の目標点 `x` と写された環境で評価した値は、写された項を写された環境で評価した値と一致します。

```agda
      renG : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
           → ⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ) ≡ ⟦ mapTm g t ⟧ᴮ (map g δ)
      renG t x δ = cong (λ u → ⟦ u ⟧ᴮ (x ∷ map g δ)) (mapTm-ren t)
                 ∙ renB (mapTm g t) x (map g δ)
```

項に対する所属は弱めで変わらず、その形は有界の場合が消費するものです。次の補題が、副条件の移送そのものを述べます。

```agda
      memRen : {n : ℕ} (t : Term SA n) (x : SB) (δ : SA ^ n)
             → (fst x ∈ˢ fst (⟦ mapTm g (renameTm suc t) ⟧ᴮ (x ∷ map g δ)))
             ≡ (fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memRen t x δ = cong (λ s → fst x ∈ˢ fst s) (renG t x δ)
      memPath : {n : ℕ} (t : Term SA n) (q : SA) (δ : SA ^ n)
```

有界量化子の副条件は、写像を越えて移ります。連鎖は、源の構造で弱めることから始まり、ずらした環境のもとで所属の原子的な仮定を適用します。

```agda
              → (fst q ∈ˢ fst (⟦ t ⟧ᴬ δ))
              ≡ (fst (g q) ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)))
      memPath {n} t q δ =
        cong (λ s → fst q ∈ˢ fst s) (sym (renA t q δ))
        ∙ at∈ (suc n) (var zero) (renameTm suc t) (q ∷ δ)
```

連鎖は、目標の構造での弱めで終わります。これで、どの有界の場合の副条件も、写像の両側で読めます。

```agda
        ∙ memRen t (g q) δ
```

古典的な段階は一度だけまとめられます。命題に対する二重否定の除去は排中律から従います。全称の場合の順方向では、目標側の反例を仮定し、それを否定された行列の存在証人として包み、`Witness` で内側へ引き戻して矛盾を導きます。最後に `dne` が必要な目標側の真理を与えます。

```agda
      dne : (P : hProp (ℓ-suc ℓ)) → (((⟨ P ⟩) → Empty.⊥) → Empty.⊥) → ⟨ P ⟩
      dne P h = Sum.rec (λ p → p)
        (λ (np : ⟨ P ⟩ → Empty.⊥) → Empty.rec (h np)) (lem P)
```

帰納は十の場合を通って始まります。最初の二つは仮定そのものであり、`at∈` と `at≐` です。命題の結合子は成分ごとに運ばれます。命題の上の合取・選言・含意は成分で決まるからです。

```agda
    agree : Agree g
    agree n (t ∈̇ u) δ = at∈ n t u δ
    agree n (t ≐ u) δ = at≐ n t u δ
    agree n (φ ∧̇ ψ) δ = cong₂ _⊓_ (agree n φ δ) (agree n ψ δ)
    agree n (φ ∨̇ ψ) δ = cong₂ _⊔_ (agree n φ δ) (agree n ψ δ)
```

含意も同じく成分ごとに運ばれ、偽は一定です。存在の節は同値で始まります。順方向は、内側での存在の充足が、写された環境のもとで写された存在の充足へ写ることを述べます。

```agda
    agree n (φ ⇒̇ ψ) δ = cong₂ _⇒_ (agree n φ δ) (agree n ψ δ)
    agree n ⊥̇ δ = refl
    agree n (∃̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩ → ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩
```

順方向は内側の証人の切り詰めを消去して証人を写します。逆方向こそ、証人の原理が働く場所です。外側の充足を証人の原理に渡すと、その像が行列を充足する内側の点が返り、一致がその充足を運び戻します。

```agda
      fwd = PT.rec (snd (map g δ ⊨ᴮ mapFo g (∃̇ ψ)))
        (λ { (q , hq) → ∣ g q , subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hq ∣₁ })
      bwd : ⟨ map g δ ⊨ᴮ mapFo g (∃̇ ψ) ⟩ → ⟨ δ ⊨ᴬ (∃̇ ψ) ⟩
      bwd h = PT.map (λ { (q , hq) →
        q , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) hq }) (wit n ψ δ h)
```

全称の節が古典的な部分です。順方向は、すべての内側の点が行列を充足すると仮定し、外側の点 `x` を固定して、`x` が像の中で行列を充足することを示します。証明は二重否定の除去から始まり、ここで排中律が移送に入ります。

```agda
    agree n (∀̇ ψ) δ = ⇔toPath fwd bwd
      where
      fwd : ((q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x = dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

もし `x` が失敗するなら、写された環境は `x` で否定された行列を充足します。その否定に証人の原理を施すと、像が否定を充足する内側の点が返り、その点での一致が、すべての内側の点が行列を充足するという仮定と矛盾します。

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) (h q))) })
          (wit n (¬̇ ψ) δ ∣ x , (λ yes → lift (nx yes)) ∣₁)
      bwd : ((x : SB) → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
```

逆方向は直接です。すべての内側の点は外側の台へ写るからです。有界全称は、補助の論理式で始まります。それは、名前を替えた上界への所属と、行列の否定を連言したもので、「上界には属するが行列は成立しない」という古典的な読みです。

```agda
      bwd h q = subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (h (g q))
    agree n (∀̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ¬̇ ψ
```

順方向は、上界の中のすべての内側の点が行列を充足するなら、写された上界に属するすべての外側の点が写された行列を充足する、と述べます。証明は再び二重否定の除去から始まり、外側の点が失敗すると仮定します。

```agda
      fwd : ((q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩)
          → (x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
          → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩
      fwd h x hx =
        dne ((x ∷ map g δ) ⊨ᴮ mapFo g ψ) λ nx →
```

証人の原理を補助の論理式に施すと、内側の点 `q` が返ります。その像は上界に属しますが、行列を反証します。像の上界への所属は、弱めと `memPath` を通して運び戻され、一致が行列の内側での充足を像へ持ち上げて、失敗と矛盾します。

```agda
        PT.rec isProp⊥ (λ { (q , hq) →
          lower (hq .snd (subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ))
            (h q (subst ⟨_⟩ (sym (memPath t q δ))
                    (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst)))))) })
          (wit n mat δ ∣ x , (subst ⟨_⟩ (sym (memRen t x δ)) hx
```

補助の適用は証人の記録で閉じ、その第二成分は像における行列の失敗、すなわち否定された行列です。逆方向は、像のもとの外側の充足と内側の副条件から、内側の行列の充足が出ることを述べます。

```agda
            , (λ yes → lift (nx yes))) ∣₁)
      bwd : ((x : SB) → ⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                   → ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩)
          → (q : SA) → ⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ → ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩
      bwd h q hq =
```

逆方向は、内側の点の像のもとで外側の充足を適用します。副条件は `memPath` で、行列は一致で運ばれます。有界存在は、副条件と行列自身を連言した補助の行列で始まります。

```agda
        subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ)))
          (h (g q) (subst ⟨_⟩ (memPath t q δ) hq))
    agree n (∃̇∈ t ψ) δ = ⇔toPath fwd bwd
      where
      mat : Formula SA (suc n)
```

補助の行列は、副条件と行列の連言であり、順方向は、内側の証人の対が外側の証人の対へ写ると述べます。証明は、切り詰めの上の一回の写しです。

```agda
      mat = (var zero ∈̇ renameTm suc t) ∧̇ ψ
      fwd : ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
          → ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
      fwd = PT.map (λ { (q , hq , hψ) →
```

二つの成分は別々に運ばれます。副条件は `memPath` で、行列は一致によって運ばれます。逆方向はその逆を述べ、外側の証人の対が内側の対を与えます。

```agda
        g q , (subst ⟨_⟩ (memPath t q δ) hq ,
               subst ⟨_⟩ (agree (suc n) ψ (q ∷ δ)) hψ) })
      bwd : ∥ Σ[ x ∈ SB ] (⟨ fst x ∈ˢ fst (⟦ mapTm g t ⟧ᴮ (map g δ)) ⟩
                        × ⟨ (x ∷ map g δ) ⊨ᴮ mapFo g ψ ⟩) ∥₁
          → ∥ Σ[ q ∈ SA ] (⟨ fst q ∈ˢ fst (⟦ t ⟧ᴬ δ) ⟩ × ⟨ (q ∷ δ) ⊨ᴬ ψ ⟩) ∥₁
```

逆方向は、補助の形で読んだ外側の対に証人の原理を走らせ、内側の点とその像の対を得ます。成分は、弱めと `memPath`、そして一致によって運び戻されます。

```agda
      bwd h = PT.map (λ { (q , hq) →
        q , ( subst ⟨_⟩ (sym (memPath t q δ))
                (subst ⟨_⟩ (memRen t (g q) δ) (hq .fst))
            , subst ⟨_⟩ (sym (agree (suc n) ψ (q ∷ δ))) (hq .snd)) })
        (wit n mat δ (PT.map (λ { (x , hx , hψ) →
```

二つの成分が有界存在の移送を閉じ、十場合の帰納が完了します。

```agda
          x , (subst ⟨_⟩ (sym (memRen t x δ)) hx , hψ) }) h))
```

## 段階内部の Tarski-Vaught 判定条件

順序数の指数 `α` に対し、段階 `Lset α` を周囲の構造とすれば、上の移送からその内部での初等性が得られます。

```agda
module AtStage (α : S) (ordα : IsOrd α) where
```

段階は推移的です。その理由は正確にはこうです。`Lset-layer α` が `α` における層の推移性の証明を与え、`layer-trans` がそれを `Lset α` の推移性へ変えます。順序数性の仮定はここでは使われず、下の整列順序のために取ってあります。

```agda
  Ltr : isTransV (Lset α)
  Ltr = layer-trans (Lset-layer α)
```

推移性により、有界論理式は `Lset α` の内部と宇宙全体とで絶対的になります。したがって、段階に制限した構造を Tarski-Vaught の議論の外側の意味論として使えます。

```agda
  module AbsL = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ Lset α) Ltr
    using ( SM; 𝒮M; _⊨ᵐ_; ⟦_⟧ᵐ; abs₀ )
```

段階の台は、`Lset α` に属する要素の型です。以下のどの包の要素も、どの段階での読みも、この型の中にあります。

```agda
  SL : Type (ℓ-suc ℓ)
  SL = AbsL.SM
```

前章の段階の順序は、この台の上の整列順序に制限されます。この段階に含まれる台 `M` を固定し、段階への包含を仮定します。

```agda
  wL : SWO SL
  wL = orderAt α ordα
  module AtM (M : S) (M⊆L : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ x ∈ˢ Lset α ⟩) where
```

部分構造の台は、周囲の台の要素と、それが `M` に属することの証明の対です。論理式はこのような対のもとでのみ読まれます。

```agda
    SM : Type (ℓ-suc ℓ)
    SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

部分構造の意味論は、周囲の意味論の `M` への制限です。項は制限の内側で評価され、充足は命題値です。

```agda
    module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
      using ( module At )
    open SemM.At SM id renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

段階への包含は、台の各要素をその段階での所属と対にします。これは包含の仮定が供給します。

```agda
    inL : SM → SL
    inL c = fst c , M⊆L (fst c) (snd c)
```

初等性は、この包含のもとで充足が変わらないことを、台のすべての論理式と環境に対して述べます。これは命題の間のパスであり、二つの原子式についての合同性と証人の原理がこの形で合成されます。

```agda
    Elementary : Type (ℓ-suc (ℓ-suc ℓ))
    Elementary = (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
               → (δ ⊨ᵐ φ) ≡ (map inL δ AbsL.⊨ᵐ (mapFo inL φ))
```

Tarski-Vaught の判定条件は、初等性の証人の形です。段階がある環境の像のもとで存在の論理式を充足するなら、台のある要素の像がそこで行列を充足します。充足が命題値なので、単に存在すれば足ります。

```agda
    TarskiVaught : Type (ℓ-suc ℓ)
    TarskiVaught = (n : ℕ) (φ : Formula SM (suc n)) (δ : SM ^ n)
                 → ⟨ map inL δ AbsL.⊨ᵐ (mapFo inL (∃̇ φ)) ⟩
                 → ∥ Σ[ q ∈ SM ] ⟨ (inL q ∷ map inL δ) AbsL.⊨ᵐ (mapFo inL φ) ⟩ ∥₁
```

各点での包含は環境の参照と可換です。これは項の一致に必要な変数の場合です。

```agda
    private
      lookup-inL : {n : ℕ} (i : Fin n) (δ : SM ^ n)
                 → lookup i (map inL δ) ≡ inL (lookup i δ)
      lookup-inL zero (c ∷ δ) = refl
      lookup-inL (suc i) (c ∷ δ) = lookup-inL i δ
```

項は包含の両側で一致します。台の項は、部分構造で読んでも、写して段階で読んでも、同じ底の要素に評価されます。定数は固定的で、変数は参照に従います。そして移送の仕組みが、二つの所属の述語のもとで具体化されます。

```agda
      tm-agree : (n : ℕ) (t : Term SM n) (δ : SM ^ n)
               → fst (⟦ t ⟧ᵐ δ) ≡ fst (AbsL.⟦ mapTm inL t ⟧ᵐ (map inL δ))
      tm-agree n (con c) δ = refl
      tm-agree n (var i) δ = sym (cong fst (lookup-inL i δ))
    module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ Lset α)
```

初等性は、共有の帰納を具体化して得られます。二つの原子式の場合は、今証明した充足関係の合同性から得られ、証人の原理がちょうど Tarski-Vaught の実例で、ブールと量化子の場合は共有の本体が運びます。二つの合同性と判定条件を除けば、段階に固有のことは何も使われません。

```agda
    TV→elem : TarskiVaught → Elementary
    TV→elem tv = Tr.Along.agree inL
      (λ n t u δ → cong₂ _∈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      (λ n t u δ → cong₂ _≈ˢ_ (tm-agree n t δ) (tm-agree n u δ))
      tv
```

## 始集合を最小の証人について閉じる

始集合 `X` がこの段階に含まれ、指数 `α` が空集合を含むと仮定します。空集合が `Lset α` に属するのは、`∅` が順序数 `α` の中にあり、基底の層で符号化されているからです。

```agda
  module Hull (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
               (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
    ∅∈Lsetα : ⟨ ∅ ∈ˢ Lset α ⟩
    ∅∈Lsetα = Lset-in α ∅ ∅ ∅∈α (∅∈𝒟ₒ ∅)
```

始集合の提示の埋め込みは、段階の台の中に着地します。各索引は `X` の要素を名指し、包含の仮定がその要素が段階 `Lset α` に属することを証明します。

```agda
    inStg : ⟪ X ⟫ → SL
    inStg m = ⟪ X ⟫↪ m , X⊆L (⟪ X ⟫↪ m) (member X m)
```

項代数は、段階の制限された構造のもとで具体化されます。台は第一射影で宇宙へ写され、証人の探索は段階の整列順序を使い、既定の値は空集合、基のコードは `X` の提示で索引づけられます。包はこうして段階の中で育ちます。

```agda
    module T = TermAlgebra AbsL.𝒮M fst wL (∅ , ∅∈Lsetα) {K = ⟪ X ⟫} inStg
    open T using ( Code; base; val; Hull; inHull )
```

包は段階の中にあります。すべての要素はあるコードの値であり、コードの値は項代数自身の型づけによって段階 `Lset α` の要素です。証明は切り詰められた提示を消去し、同一視に沿って輸送します。

```agda
    Hull⊆L : (x : S) → ⟨ x ∈ˢ Hull ⟩ → ⟨ x ∈ˢ Lset α ⟩
    Hull⊆L x x∈H = PT.rec (snd (x ∈ˢ Lset α)) go x∈H
      where
      go : Σ[ c ∈ Code ] (fst (val c) ≡ x) → ⟨ x ∈ˢ Lset α ⟩
      go (c , q) = subst (λ z → ⟨ z ∈ˢ Lset α ⟩) q (snd (val c))
```

所属は、切り詰められた存在としてしか読み戻せません。包の要素はあるコードの値ですが、コードは選ばれません。異なるコードが同じ値に評価しうるので、これが提示の正直な形です。

```agda
    hull-member : (x : S) → ⟨ x ∈ˢ Hull ⟩
                → ∥ Σ[ c ∈ Code ] (fst (val c) ≡ x) ∥₁
    hull-member x x∈H = x∈H
```

逆方向には切り詰めは要りません。提示自身の導入規則により、どのコードの値も要素です。

```agda
    val-in-Hull : (c : Code) → ⟨ fst (val c) ∈ˢ Hull ⟩
    val-in-Hull c = inHull c
```

始集合は要素ごとに包に入ります。`X` の要素 `x` は索引によって提示され、`x` における提示の繊維がその索引を返します。

```agda
    module XInM (x : S) (x∈X : ⟨ x ∈ˢ X ⟩) where
      mx : ⟪ X ⟫
      mx = fiber X x∈X .fst
```

繊維は、提示された要素を `x` と同一視するパスを運び、所属を運ぶときの道すじになります。

```agda
      x≡val : ⟪ X ⟫↪ mx ≡ x
      x≡val = fiber X x∈X .snd
```

その索引での基のコードは、提示された要素、すなわち `x` へ評価されます。輸送によって、`x` の包の中の所属が着地します。

```agda
      inM : ⟨ x ∈ˢ Hull ⟩
      inM = subst (λ z → ⟨ z ∈ˢ Hull ⟩) x≡val (inHull (base mx))
```

一度組み立てれば、始集合の包への包含は一つの補題になります。

```agda
    X⊆M : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Hull ⟩
    X⊆M x x∈X = XInM.inM x x∈X
```

## 充足関係は崩壊同型で不変である

同型の前後で充足関係を比較するため、集合 `M`、`PM` と、`M` の要素を `PM` の要素へ送る台の写像 `p` を固定します。

```agda
module IsoInv (M : S) (PM : S)
  (p : S → S)
  (p∈ : (x : S) → ⟨ x ∈ˢ M ⟩ → ⟨ p x ∈ˢ PM ⟩)
```

閉性の条件 `p∈` に加えて、写像 `p` には四つの仮定を置きます。`iso-fwd` は所属を保存し、`iso-bwd` は所属を反映し、最後の二つの引数は `M` 上の単射性と終域 `PM` への全射性を述べます。

```agda
  (iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩)
  (iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
           → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩)
  (p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ M ⟩) (y∈ : ⟨ y ∈ˢ M ⟩)
```

写像 `p` は `M` 上で単射であり、`PM` へ単に全射です。保存と反映と合わせて、これらはまさに二つの構造の間の所属の同型のデータです。

```agda
          → p x ≡ p y → x ≡ y)
  (surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
        → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (p y ≡ z)) ∥₁)
  where
```

源の台は、`M` の各要素とその所属の証明を対にします。本章のどの制限された構造とも同じです。

```agda
  SM : Type (ℓ-suc ℓ)
  SM = Σ[ x ∈ S ] ⟨ x ∈ˢ M ⟩
```

終域の台は、`PM` の各要素とその所属の証明を対にします。

```agda
  SPM : Type (ℓ-suc ℓ)
  SPM = Σ[ x ∈ S ] ⟨ x ∈ˢ PM ⟩
```

同型は、対になった台へ持ち上がります。底の要素に `p` を施し、像の中での所属を証明するのです。

```agda
  g : SM → SPM
  g m = p (fst m) , p∈ (fst m) (snd m)
```

始域の意味論は、`M` に制限した構造で項と論理式を解釈します。

```agda
  module SemM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ M))
    using ( module At )
  module SemPM = FOL.Semantics (𝒮ᵥ ↾ (λ x → x ∈ˢ PM))
    using ( module At )
  open module Mse = SemM.At SM id public renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

終域の意味論は、`PM` に制限した構造で写された項と論理式を解釈します。

```agda
  open module Pse = SemPM.At SPM id public renaming ( _⊨_ to _⊨ᵖᵐ_ ; ⟦_⟧ to ⟦_⟧ᵖᵐ )
```

全射は対になった台へ持ち上がります。終域 `PM` のすべての要素は `M` のある点の像であり、底の要素の等しさは、`PM` への所属が命題であるため、対の等しさへ持ち上がります。

```agda
  surj' : (p' : SPM) → ∥ Σ[ q ∈ SM ] (g q ≡ p') ∥₁
  surj' (z , z∈) = PT.map (λ { (y , y∈ , e) →
    (y , y∈) , Σ≡Prop (λ w → (w ∈ˢ PM) .snd) e }) (surj z z∈)
```

一般の充足関係の移送定理を、`M` と `PM` への所属述語に適用できます。所属の保存と反映が、その所属原子式の場合を与えます。

```agda
  module Tr = SatTransfer (λ x → x ∈ˢ M) (λ x → x ∈ˢ PM)
```

写像 `p` は環境に各索引ごとに施されるので、参照は一度に一つずつ簡約できます。

```agda
  private
    lookup-g : {n : ℕ} (i : Fin n) (δ : SM ^ n)
             → p (fst (lookup i δ)) ≡ fst (lookup i (map g δ))
    lookup-g zero (m ∷ δ) = refl
    lookup-g (suc i) (m ∷ δ) = lookup-g i δ
```

項は写像 `p` のもとで一致します。`M` の項の値に `p` を施すことは、写された項を写された環境で評価することと等しくなります。定数は固定的で、変数は参照に従います。所属の原子式がここで述べられます。

```agda
    tm-agree : {n : ℕ} (t : Term SM n) (δ : SM ^ n)
             → p (fst (⟦ t ⟧ᵐ δ)) ≡ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ))
    tm-agree (con m) δ = refl
    tm-agree (var i) δ = lookup-g i δ
    at∈ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
```

原子項の所属は両方向に移ります。順方向は、内側の所属を項の等式に沿って運び、所属を保存する `iso-fwd` に渡します。

```agda
        → (δ ⊨ᵐ (t ∈̇ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ∈̇ u))
    at∈ n t u δ = ⇔toPath
      (λ h → subst (λ z → ⟨ fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ∈ˢ z ⟩) (tm-agree u δ)
        (subst (λ z → ⟨ z ∈ˢ p (fst (⟦ u ⟧ᵐ δ)) ⟩) (tm-agree t δ)
          (iso-fwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
```

順方向の輸送は、`p` を施した後の所属に着地します。逆方向は、同型を通してその所属を反映し、項の等式に沿って内側の所属を復元します。

```agda
            (snd (⟦ t ⟧ᵐ δ)) h)))
      (λ h → iso-bwd (fst (⟦ u ⟧ᵐ δ)) (fst (⟦ t ⟧ᵐ δ)) (snd (⟦ u ⟧ᵐ δ))
        (snd (⟦ t ⟧ᵐ δ))
        (subst (λ z → ⟨ p (fst (⟦ t ⟧ᵐ δ)) ∈ˢ z ⟩) (sym (tm-agree u δ))
          (subst (λ z → ⟨ z ∈ˢ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ)) ⟩)
```

逆方向が所属の節を閉じます。項の等式に導かれた同型を通した反映が、内側の所属をちょうど返します。等号の原子式と証人の原理は、残りの仮定が扱います。

```agda
            (sym (tm-agree t δ)) h)))
```

アトムの項の等号は、等式の両辺に崩壊を施すことで移ります。順方向は、`M` における値の等式を取り、`cong` で `p` を施し、項の同約によって両辺を写された項へ運びます。

```agda
    at≐ : (n : ℕ) (t u : Term SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ (t ≐ u)) ≡ (map g δ ⊨ᵖᵐ mapFo g (t ≐ u))
    at≐ n t u δ = ⇔toPath
      (λ h → subst (λ z → z ≡ fst (⟦ mapTm g u ⟧ᵖᵐ (map g δ))) (tm-agree t δ)
        (subst (λ z → p (fst (⟦ t ⟧ᵐ δ)) ≡ z) (tm-agree u δ) (cong p h)))
```

逆方向は、単射性が活きる場所です。崩壊した両辺が等しいことから、`p-inj` がもとの値の等しさを取り戻します。二つの向きで、等号のアトムが命題の間のパスになります。

```agda
      (λ h → p-inj (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) (snd (⟦ t ⟧ᵐ δ))
        (snd (⟦ u ⟧ᵐ δ))
        (subst (λ z → z ≡ p (fst (⟦ u ⟧ᵐ δ))) (sym (tm-agree t δ))
          (subst (λ z → fst (⟦ mapTm g t ⟧ᵖᵐ (map g δ)) ≡ z)
            (sym (tm-agree u δ)) h)))
```

証人の原理は全射から作られます。像の中の外側の証人 `p'` は、単に、`M` のある `q` の崩壊です。その同一視に沿って充足を運ぶと、内側の証人と、像の中での充足が得られます。

```agda
    wit : Tr.Witness g
    wit n ψ δ h = PT.rec squash₁
      (λ { (p' , hp) → PT.map
        (λ { (q , gq≡p) →
          q , subst (λ z → ⟨ (z ∷ map g δ) ⊨ᵖᵐ mapFo g ψ ⟩) (sym gq≡p) hp })
```

全射の補題が逆像を供給し、二つの輸送が合わさって、移送の証人の原理になります。

```agda
        (surj' p') }) h
```

原子の場合と証人原理がそろうと、共有の帰納により、環境を崩壊で写し、定数を `g` で付け替えても充足関係が保たれることが分かります。

```agda
  agree : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
        → (δ ⊨ᵐ φ) ≡ (map g δ ⊨ᵖᵐ mapFo g φ)
  agree = Tr.Along.agree g at∈ at≐ wit
```

一致は、後で合成するために二つの片方向の形で記録されます。順方向には、内側の充足から、写された環境での写された論理式の充足が得られます。

```agda
  iso-inv : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
          → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩
  iso-inv n φ δ = subst ⟨_⟩ (agree n φ δ)
```

逆方向は、外側の充足を内側の充足へ戻します。本章は次に、外延性をもつ集合 `X` の崩壊のもとでこの不変性を具体化し、所属の同型と単射性を伴って崩壊を開きます。

```agda
  iso-inv-bwd : (n : ℕ) (φ : Formula SM n) (δ : SM ^ n)
              → ⟨ map g δ ⊨ᵖᵐ mapFo g φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
  iso-inv-bwd n φ δ = subst ⟨_⟩ (sym (agree n φ δ))
module CollapseIso (X : S) (Xext : isExt X) where
  module C = Collapse X using ( module InjExt; π; πX; πX-intro; πX-member )
```

`X` の外延性こそ、崩壊が必要とするものです。制限された構造は単射となり、`X` の上の所属と崩壊の像の上の所属の間の同型が使えるようになります。

```agda
  module CI = C.InjExt Xext using ( iso; π-inj )
```

目標の台は崩壊像 `πX` であり、その点はちょうど `X` の要素の崩壊値です。

```agda
  PM : S
  PM = C.πX
```

写像 `p` は各集合をその Mostowski 崩壊値へ送ります。

```agda
  p : S → S
  p = C.π
```

`X` の要素は像の中に着地します。これは、像に対する崩壊自身の導入規則によるものです。

```agda
  p∈ : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ p x ∈ˢ PM ⟩
  p∈ = C.πX-intro
```

所属は崩壊に沿って順方向に保存されます。`X` の中で `y` が `x` に属するなら、`y` の崩壊は `x` の崩壊に属します。これが所属の同型の第一成分です。

```agda
  iso-fwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ y ∈ˢ x ⟩ → ⟨ p y ∈ˢ p x ⟩
  iso-fwd x y x∈ y∈ = CI.iso x y x∈ y∈ .fst
```

所属は逆方向にも反映されます。崩壊された所属は、`X` の中の本当の所属から生じたものに限ります。二つの向き合わせて、崩壊が所属について忠実であることが言えます。

```agda
  iso-bwd : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
          → ⟨ p y ∈ˢ p x ⟩ → ⟨ y ∈ˢ x ⟩
  iso-bwd x y x∈ y∈ = CI.iso x y x∈ y∈ .snd
```

崩壊は `X` の上で単射です。崩壊が等しい二つの要素は等しい。所属への忠実さと単射性が、要素の上の同型の二つの半分です。

```agda
  p-inj : (x y : S) (x∈ : ⟨ x ∈ˢ X ⟩) (y∈ : ⟨ y ∈ˢ X ⟩)
        → p x ≡ p y → x ≡ y
  p-inj = CI.π-inj
```

像のすべての点は `X` の要素から来ます。全射は切り詰められており、証人を選ばずに逆像の存在を主張します。これがまさに、証人の原理が消費する形です。

```agda
  surj : (z : S) (z∈ : ⟨ z ∈ˢ PM ⟩)
       → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (p y ≡ z)) ∥₁
  surj = C.πX-member
```

外延的な集合 `X` では、崩壊は所属を保存かつ反映し、`X` 上で単射であり、`πX` のすべての点を覆います。

```agda
  module I = IsoInv X PM p p∈ iso-fwd iso-bwd p-inj surj
    using ( SM; SPM; g; surj'; iso-inv; iso-inv-bwd; _⊨ᵐ_; _⊨ᵖᵐ_; ⟦_⟧ᵐ; ⟦_⟧ᵖᵐ )
```

## Skolem 包は初等的である

したがって、`X` 上の構造と `πX` 上の構造の間で充足関係を双方向に移せます。

```agda
module HullElemDown (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩) (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

これを `Lset α` 内の Skolem 包に適用すると、初等性は Tarski-Vaught の証人条件に帰着します。

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α
    using ( module T; Hull⊆L; hull-member )
  M : S
  M = H.T.Hull
```

部分構造の仕組みは包のもとで具体化され、その論理式には周囲の読みが与えられます。包の台のすべての要素にはコードがあります。コードは切り詰められた提示によって存在し、値と包含の同一視は、段階の所属の命題値性によって持ち上がります。

```agda
  module A = ASt.AtM M H.Hull⊆L using ( Elementary; SM; module SemM; TV→elem; inL )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
  codeOf : (q : A.SM) → ∥ Σ[ c ∈ H.T.Code ] (H.T.val c ≡ A.inL q) ∥₁
  codeOf q = PT.map (λ { (c , e) → c , Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) e })
    (H.hull-member (fst q) (snd q))
```

コードは、一つの要素から有限の環境へ持ち上がります。空の環境は空のベクトルで符号化され、再帰の場合は、新しいコードを、すでに作られたコードの列に加えます。

```agda
  codeEnv : {n : ℕ} (δ : Vec A.SM n)
          → ∥ Σ[ ds ∈ Vec H.T.Code n ]
               (map H.T.val ds ≡ map A.inL δ) ∥₁
  codeEnv [] = ∣ [] , refl ∣₁
  codeEnv (q ∷ δ) = PT.map2
```

構成の場合は、二つの切り詰められた存在を一つに合成します。延びたコードのベクトルの評価は、包含された環境にちょうど等しくなります。

```agda
    (λ { (c , ec) (ds , eds) → c ∷ ds , cong₂ _∷_ ec eds })
    (codeOf q) (codeEnv δ)
```

成分ごとの写像は有限環境の連結も保ちます。したがって、自由変数の値と定数出現を置き換える値を、Tarski-Vaught の議論に用いる一つの符号化環境へまとめられます。

```agda
  inL-++ : {n m : ℕ} (δ : Vec A.SM n) (σ : Vec A.SM m)
          → map A.inL (δ ++ σ) ≡ map A.inL δ ++ map A.inL σ
  inL-++ [] σ = refl
  inL-++ (q ∷ δ) σ = cong (A.inL q ∷_) (inL-++ δ σ)
  tv : (n : ℕ) (ψ : Formula A.SM (suc n)) (δ : Vec A.SM n)
```

この主張は Tarski-Vaught の条件そのものです。段階が包含された環境のもとで存在の論理式を充足するなら、単に、包のある要素がそこで行列を充足します。証明はまず環境の符号化を消去し、探索の閉包へ進みます。

```agda
     → ⟨ map A.inL δ ASt.AbsL.⊨ᵐ (mapFo A.inL (∃̇ ψ)) ⟩
     → ∥ Σ[ q ∈ A.SM ]
          ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩ ∥₁
  tv n ψ δ h = PT.rec squash₁ takeEnvironment (codeEnv params)
    where
```

パラメータ抽象は各定数出現を追加の自由変数に置き換えます。得られる論理式は定数領域が空で、アリティが `countFo ψ` だけ増えますが、`ψ` の論理構造はすべて保たれます。

```agda
    bodyFo : Formula (⊥* {ℓ}) (suc (n + countFo ψ))
    bodyFo = absFo ψ
```

抽象された本体のための環境は、もとの環境に定数の出現を続けたものです。抽象は定数を余分な自由変数に変えるので、一つのベクトルが探索に必要なすべてを運びます。

```agda
    params : Vec A.SM (n + countFo ψ)
    params = δ ++ constantsFo ψ
```

この結合環境のコードが得られると、最小証人についての閉性から包内の証人が得られます。抽象後の論理式ともとのパラメータ付き論理式との意味論的同一視により、必要な Tarski-Vaught の証人が従います。

```agda
    takeEnvironment : Σ[ ds ∈ Vec H.T.Code (n + countFo ψ) ]
                        (map H.T.val ds ≡ map A.inL params)
                    → ∥ Σ[ q ∈ A.SM ]
                         ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                             (mapFo A.inL ψ) ⟩ ∥₁
```

探索の閉包は、符号化された環境のもとで走ります。その評価の記録に、符号化の等式と、連結の上の包含の分配を合成すると、コードの評価が包含された引数であることが得られます。

```agda
    takeEnvironment (ds , eds) = PT.map finish (H.T.closed _ bodyFo ds witness)
      where
      vals-env : H.T.vals ds
               ≡ map A.inL δ ++ map A.inL (constantsFo ψ)
      vals-env = H.T.vals≡map ds ∙ eds ∙ inL-++ δ (constantsFo ψ)
```

重要な同一視はこう述べます。符号化された環境のもと、裸の探索の意味論で読んだ抽象された本体は、包含された環境のもと、段階の意味論で読んだ本体と同じ命題だと。

```agda
      body-path : (b : ASt.SL)
                → ((b ∷ H.T.vals ds) H.T.⊨₀ bodyFo)
                ≡ ((b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ mapFo A.inL ψ)
      body-path b =
          cong (λ ε → ε H.T.⊨₀ bodyFo) (cong (b ∷_) vals-env)
```

このパスは二つの意味論的な整合則を合成します。`⊨-abs` はパラメータ抽象と拡張環境を結び、`⊨-map` は付け替えと写された環境を結びます。

```agda
        ∙ sym (⊨-abs ASt.AbsL.𝒮M A.inL ψ
                 (b ∷ map A.inL δ))
        ∙ sym (⊨-map ASt.AbsL.𝒮M A.inL id ψ
                 (b ∷ map A.inL δ))
```

存在の論理式の段階での充足が、体のパスに沿って裸の読みへ運ばれ、探索の閉包が必要とする充足可能性の証人が、ちょうど生み出されます。

```agda
      witness : H.T.Sat (n + countFo ψ) bodyFo (H.T.vals ds)
      witness = PT.map (λ { (b , hb) →
        b , subst ⟨_⟩ (sym (body-path b)) hb }) h
```

探索は、符号化された環境のもとで抽象された本体を満たす、包の中の最小の証人を返します。変換は、これをもとの論理式に対する Tarski-Vaught の対へ変える必要があります。

```agda
      finish : Σ[ a ∈ ASt.SL ]
                 ( ⟨ fst a ∈ˢ M ⟩
                 × ⟨ (a ∷ H.T.vals ds) H.T.⊨₀ bodyFo ⟩ )
             → Σ[ q ∈ A.SM ]
                 ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
```

証人は、部分構造の台へ読み戻されます。底の集合は包であり、所属は今産み出されたものです。

```agda
      finish (a , a∈H , ha) = q , sat
        where
        q : A.SM
        q = fst a , a∈H
```

証人の段階への包含は、証人そのものです。二つの台は、命題値の所属の証明だけが違い、それは反射性によって同一視されます。

```agda
        q≡a : A.inL q ≡ a
        q≡a = Σ≡Prop (λ z → (z ∈ˢ Lset α) .snd) refl
```

証人のもとの本体の充足は、体のパスに沿って段階の意味論へ、そして証人の同一視に沿って部分構造の台へ運ばれます。これが、もとの論理式と環境に対する Tarski-Vaught の結論にほかなりません。

```agda
        sat : ⟨ (A.inL q ∷ map A.inL δ) ASt.AbsL.⊨ᵐ (mapFo A.inL ψ) ⟩
        sat = subst (λ b → ⟨ (b ∷ map A.inL δ) ASt.AbsL.⊨ᵐ
                                (mapFo A.inL ψ) ⟩)
                (sym q≡a) (subst ⟨_⟩ (body-path a) ha)
```

したがって、Tarski-Vaught 条件から包の `Lset α` における初等性が得られます。

```agda
  elem : A.Elementary
  elem = A.TV→elem tv
```

## パラメータなし論理式を周囲の宇宙で読む

定数領域が空の論理式では、定数の非自明な付け替えなしに周囲の充足関係を比較できます。

```agda
module AtP = SemV.At (⊥* {ℓ-suc ℓ}) (λ b → Empty.rec* b) using ( _⊨_ )
```

パラメータなしの論理式の周囲の充足は、再利用のために名付けられます。重要な観察はこうです。パラメータなしの論理式は、改名しても変わらない。写し直す定数がないからです。

```agda
_⊨ₚ_ : {n : ℕ} → S ^ n → Formula (⊥* {ℓ-suc ℓ}) n → hProp (ℓ-suc ℓ)
_⊨ₚ_ = AtP._⊨_
embed-map : {ℓ₁ ℓ₂ : Level} {K : Type ℓ₁} {K' : Type ℓ₂} (f : K → K')
            {n : ℕ} (φ : Formula (⊥* {ℓ-suc ℓ}) n)
          → mapFo f (embed φ) ≡ embed φ
```

証明は、写しの法則と、空の領域の埋め込みが出現の上で恒等であるという事実を合成します。改名が動かすものは何も残っていません。

```agda
embed-map f φ =
    mapFo-comp Empty.rec* f φ
  ∙ cong (λ h → mapFo h φ) (funExt (λ b → Empty.rec* b))
opaque
  isOrdAt : Formula (⊥* {ℓ-suc ℓ}) 1
```

順序数性は、一つの枠をもつ有界論理式によって、引数自身が推移的であり、そのすべての要素も推移的であることとして表されます。

```agda
  isOrdAt =
    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
    ∧̇ (∀̇∈ (var zero) (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

`Δ₀` の証拠は外側の連言を通り、第一の節の二つと第二の節の三つの有界量化子をたどって、所属の原子式に至ります。

```agda
  Δ₀-isOrdAt : Δ₀ isOrdAt
  Δ₀-isOrdAt =
    δ-∧ (δ-∀∈ (δ-∀∈ δ-∈))
        (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
```

二つの読み取り補題は、`isOrdAt` の充足と順序数述語を双方向に正確に対応させます。

```agda
module Amb where
  opaque
    unfolding isOrdAt
```

論理式から順序数性を読み出すとは、二つの有界の節を、順序数の述語の二つの欄へ開くことです。引数の推移性と、すべての要素の推移性です。

```agda
    isOrdAt-out : (x : S) → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩ → IsOrd x
    isOrdAt-out x h =
        ( λ {x₁} {y} y∈x₁ x₁∈x → h .fst x₁ x₁∈x y y∈x₁ )
      , ( λ a a∈x {x₁} {y} y∈x₁ x₁∈a → h .snd a a∈x x₁ x₁∈a y y∈x₁ )
```

逆に、`IsOrd` の二つの成分から二つの有界な節が従います。三つの枠をもつ版は中央の自由な枠について同じ述語を表し、ほかの二つの自由な枠は論理式に現れません。

```agda
    isOrdAt-in : (x : S) → IsOrd x → ⟨ (x ∷ []) ⊨ₚ isOrdAt ⟩
    isOrdAt-in x o =
        ( λ a a∈x b hb → o .fst {a} {b} hb a∈x )
      , ( λ a a∈x b b∈a c hc → o .snd a a∈x {b} {c} hc b∈a )
isOrd-at-p : Formula (⊥* {ℓ-suc ℓ}) 3
```

三つの枠をもつ論理式の最初の連言支は、引数の要素の要素が引数の要素であること、すなわち第二の枠で読まれる推移性を言います。

```agda
isOrd-at-p =
    (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc (suc zero))))))
  ∧̇ (∀̇∈ (var (suc zero))
      (∀̇∈ (var zero)
```

第二の連言支は、引数の各要素 `a` が推移的であること、すなわち `c ∈ b ∈ a` ならば `c ∈ a` であることを述べます。

```agda
        (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))
```

その有界性の証拠は、同じ再帰に従います。続いて消去の補題が始まります。定数の出現をもたない論理式に対して、定数を消去しても Δ₀ の証拠は、場合ごとに保たれます。

```agda
Δ₀-isOrd-at-p : Δ₀ isOrd-at-p
Δ₀-isOrd-at-p = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
erase-Δ₀ : {m : ℕ} (φ : Formula CS.S m) (p : countFo φ ≡ 0)
         → Δ₀ φ → Δ₀ (Cnt.erase φ p)
erase-Δ₀ (t ∈̇ u) p δ-∈ = δ-∈
```

アトムはそのまま通り、命題の結合子は構造的に消去が施されるので再帰します。

```agda
erase-Δ₀ (t ≐ u) p δ-≐ = δ-≐
erase-Δ₀ (φ ∧̇ ψ) p (δ-∧ c d) = δ-∧ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ∨̇ ψ) p (δ-∨ c d) = δ-∨ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ (φ ⇒̇ ψ) p (δ-⇒ c d) = δ-⇒ (erase-Δ₀ φ _ c) (erase-Δ₀ ψ _ d)
erase-Δ₀ ⊥̇ p δ-⊥ = δ-⊥
```

有界量化子の場合は本体について再帰します。

```agda
erase-Δ₀ (∀̇∈ t φ) p (δ-∀∈ c) = δ-∀∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇∈ t φ) p (δ-∃∈ c) = δ-∃∈ (erase-Δ₀ φ _ c)
erase-Δ₀ (∃̇ φ) p ()
erase-Δ₀ (∀̇ φ) p ()
```

## 凝縮に必要な包のデータ

非有界量化子の場合は、それに対応する `Δ₀` の構成子が存在しないため不可能です。

```agda
module HullStage (lam : S) (ordλ : IsOrd lam)
```

枠組みは、指数が要素の後続を認める段階、その段階に含まれる始集合、そして空集合の指数への所属を受け取ります。

```agda
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩) (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

`Lset lam` の内部で、始集合は Skolem 包 `M` を生成します。`M` の各要素は段階内にとどまります。

```agda
  module ASt = AtStage lam ordλ
    using ( module AbsL; module AtM; module Hull; Ltr; SL; wL )
```

もとの集合と予備値である空集合は、いずれも包の構成の中に表示されます。

```agda
  module H = ASt.Hull X X⊆L ∅∈λ
    using ( module T; module XInM; Hull⊆L; X⊆M; hull-member
          ; val-in-Hull; ∅∈Lsetα; inStg )
```

この集合 `M` は凝縮の議論の台であり、その初等性と Mostowski 崩壊が議論のデータになります。

```agda
  M : S
  M = H.T.Hull
```

包 `M` に対し、その Mostowski 崩壊を `π`、崩壊像を `πX` とします。包の点を崩壊したものはすべて `πX` に属し、`πX` の各要素は包の点から得られ、`πX` は推移的です。さらに、包の推移的な点は崩壊によって固定されます。

```agda
  module C = Collapse M
    using ( module InjExt; π; πX; πX-intro; πX-member; πX-trans; fixes )
```

凝縮の議論では、崩壊像について二つの性質を仮定します。第一に、順序数 `δ` が像に属するなら、段階 `Lset δ` も像に属します。第二に、包の各要素の崩壊は、像に属する順序数を添字とするある段階に属します。この閉性と被覆の性質により、崩壊像を `L` の一つの段階と同定できます。

```agda
  module Condense
    (levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ C.πX ⟩ → ⟨ Lset δ ∈ˢ C.πX ⟩)
    (cover : (y : S) → ⟨ y ∈ˢ M ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ C.π y ∈ˢ Lset γ ⟩) ∥₁)
    where
```

分出によって、`πX` の要素のうち順序数であるものちょうどからなる集合を作ります。したがって `β` は崩壊像の順序数部分を表します。分出の述語は順序数性を述べる有界の論理式であり、Δ₀ の証拠によってどの環境でも小さいものです。

```agda
    β-sep : Σ[ s ∈ S ]
              (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt)))
    β-sep = separateFromSmall C.πX (λ y → (y ∷ []) ⊨ₚ isOrdAt)
              (λ y → D0.Δ₀-small Δ₀-isOrdAt (y ∷ []))
```

この順序数部分を `β` と書きます。以下では、`β` 自身が順序数であり、`β` が添字づける階層が崩壊像と一致することを示します。

```agda
    β : S
    β = β-sep .fst
```

`β` に属することは、`πX` に属し、さらにその要素を自由変数に割り当てたとき無定数の順序数公式を満たすことと同値です。

```agda
    β-spec : (y : S) → (y ∈ˢ β) ≡ ((y ∈ˢ C.πX) ⊓ ((y ∷ []) ⊨ₚ isOrdAt))
    β-spec = β-sep .snd
```

同値の第一の射影は、ベータのすべての要素が崩壊の像の要素であることを示します。

```agda
    β∈πX : (δ : S) → ⟨ δ ∈ˢ β ⟩ → ⟨ δ ∈ˢ C.πX ⟩
    β∈πX δ δ∈β = subst ⟨_⟩ (β-spec δ) δ∈β .fst
```

第二成分は、この無定数一自由変数公式の充足を、周囲の宇宙での順序数性へ変換します。

```agda
    β-ord : (δ : S) → ⟨ δ ∈ˢ β ⟩ → IsOrd δ
    β-ord δ δ∈β = Amb.isOrdAt-out δ (subst ⟨_⟩ (β-spec δ) δ∈β .snd)
```

逆に、崩壊の像の順序数はベータの中にあります。所属と順序数性という定義の二つの成分が供給され、定義の同値がそれをベータの内部へ運び戻します。

```agda
    ord∈β : (δ : S) → ⟨ δ ∈ˢ C.πX ⟩ → IsOrd δ → ⟨ δ ∈ˢ β ⟩
    ord∈β δ δ∈πX oδ = subst ⟨_⟩ (sym (β-spec δ)) (δ∈πX , Amb.isOrdAt-in δ oδ)
```

`β` が順序数であることを示すため、その二つの定義条件を確かめます。第一は推移性です。`z ∈ x ∈ β` ならば `z ∈ β` でなければなりません。

```agda
    β-isOrd : IsOrd β
    β-isOrd = β-trans , β-mem
      where
      β-trans : isTransV β
      β-trans {x = x} {y = z} z∈x x∈β =
```

推移性は、中間の所属のもとで崩壊の像の推移性を使い、中間の点の順序数性を周囲の論理式から読みます。第二の欄は、ベータのすべての要素が順序数、したがって推移的であることから従います。

```agda
        subst ⟨_⟩ (sym (β-spec z))
          ( C.πX-trans {x = x} {y = z} z∈x (β∈πX x x∈β)
          , Amb.isOrdAt-in z (mem-ord {A = x} (β-ord x x∈β) z z∈x) )
      β-mem : (x : S) → ⟨ x ∈ˢ β ⟩ → isTransV x
      β-mem x x∈β = β-ord x x∈β .fst
```

覆いの仮定は、包の要素から崩壊の要素へ一度持ち上がります。崩壊の要素は、単に、包のある要素の崩壊なので、その要素の覆いが同一視に沿って運ばれます。

```agda
    covered : (x : S) → ⟨ x ∈ˢ C.πX ⟩
            → ∥ Σ[ γ ∈ S ]
                 (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
    covered x x∈πX = PT.rec squash₁ go (C.πX-member x x∈πX)
      where
```

逆にたどるのは、崩壊自身の要素の記述です。像の要素は、単に、包のある要素の崩壊です。

```agda
      go : Σ[ y ∈ S ] (⟨ y ∈ˢ M ⟩ × (C.π y ≡ x))
         → ∥ Σ[ γ ∈ S ]
              (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩) ∥₁
      go (y , y∈M , e) = PT.map
        (λ { (γ , oγ , γ∈πX , h) →
```

覆いは、崩壊の値の等しさに沿って運ばれます。持ち上がった主張はすぐに使われます。ベータのすべての順序数は、ベータの中のより大きな順序数の中にあります。これが凝縮の議論の古典的な極限段階の一歩です。

```agda
          γ , oγ , γ∈πX , subst (λ w → ⟨ w ∈ˢ Lset γ ⟩) e h })
        (cover y y∈M)
    β-succ : (δ : S) → ⟨ δ ∈ˢ β ⟩
           → ∥ Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩) ∥₁
    β-succ δ δ∈β = PT.map go (covered δ (β∈πX δ δ∈β))
```

delta の順序数性はベータから読まれ、変換は覆いの結論を所属の形で言い直します。delta を含む層は、その指数をベータの中に選べるのです。

```agda
      where
      oδ : IsOrd δ
      oδ = β-ord δ δ∈β
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ δ ∈ˢ Lset γ ⟩)
         → Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
```

`δ` と `γ` はともに順序数なので、`δ ∈ Lset γ` から `δ ∈ γ` が従います。また `γ` は `πX` に属する順序数なので、`γ ∈ β` です。そして逆の包含が述べられます。崩壊のすべての要素は、ベータにおける層に属します。

```agda
      go (γ , oγ , γ∈πX , δ∈Lγ) =
        γ , oγ , ord∈Lset→∈ γ oγ δ oδ δ∈Lγ , ord∈β γ γ∈πX oγ
    πX⊆Lβ : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ x ∈ˢ Lset β ⟩
    πX⊆Lβ x x∈πX = PT.rec (snd (x ∈ˢ Lset β)) go (covered x x∈πX)
      where
```

逆の包含が成り立つのは、ベータにおける層がすべてのより小さい層を含むからです。段階の構成の単調性が、覆いの層をベータの中へ運びます。

```agda
      go : Σ[ γ ∈ S ] (IsOrd γ × ⟨ γ ∈ˢ C.πX ⟩ × ⟨ x ∈ˢ Lset γ ⟩)
         → ⟨ x ∈ˢ Lset β ⟩
      go (γ , oγ , γ∈πX , x∈Lγ) =
        Lset-mono {α = β} {β = γ} (ord∈β γ γ∈πX oγ) x∈Lγ
    Lβ⊆πX : (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ C.πX ⟩
```

順方向の包含は、ベータの層の要素を段階の構成で分解し、極限の一歩がベータの中のより大きな順序数を供給します。

```agda
    Lβ⊆πX x x∈Lβ = PT.rec (snd (x ∈ˢ C.πX)) go (Lset-out β x x∈Lβ)
      where
      go : Σ[ δ ∈ S ] (⟨ δ ∈ˢ β ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
         → ⟨ x ∈ˢ C.πX ⟩
      go (δ , δ∈β , x∈𝒟ₒδ) = PT.rec (snd (x ∈ˢ C.πX)) liftStage (β-succ δ δ∈β)
```

持ち上げの段階が述べられます。ベータの中で delta を含む順序数から、崩壊の中での `x` の所属を産み出します。

```agda
        where
        liftStage : Σ[ γ ∈ S ] (IsOrd γ × ⟨ δ ∈ˢ γ ⟩ × ⟨ γ ∈ˢ β ⟩)
             → ⟨ x ∈ˢ C.πX ⟩
        liftStage (γ , oγ , δ∈γ , γ∈β) =
          C.πX-trans {x = Lset γ} {y = x}
```

持ち上げは、二つの閉包を合成します。`x` は gamma より下の delta で定義されるので gamma の層に属し、さらに第一の仮定によって、崩壊の像は gamma における層を含みます。二つの包含は、宇宙の外延性のもとで出会います。

```agda
            (Lset-in γ δ x δ∈γ x∈𝒟ₒδ)
            (levelIn γ oγ (β∈πX γ γ∈β))
    ext : C.πX ≡ Lset β
    ext = extensionality C.πX (Lset β) (sub , sup)
      where
```

外延性の議論の前半は、各要素を橋を通して段階の読みへ運び、逆の包含を適用し、橋を通って戻します。

```agda
      sub : (x : S) → ⟨ x ∈ₛ C.πX ⟩ → ⟨ x ∈ₛ Lset β ⟩
      sub x x∈ₛπX = ∈∈ₛ {a = x} {b = Lset β} .fst
        (πX⊆Lβ x (∈∈ₛ {a = x} {b = C.πX} .snd x∈ₛπX))
      sup : (x : S) → ⟨ x ∈ₛ Lset β ⟩ → ⟨ x ∈ₛ C.πX ⟩
      sup x x∈ₛLβ = ∈∈ₛ {a = x} {b = C.πX} .fst
```

後半は順方向の包含について同じことを行い、二つの半分が、崩壊の像をベータにおける層と同一視します。

```agda
        (Lβ⊆πX x (∈∈ₛ {a = x} {b = Lset β} .snd x∈ₛLβ))
```

これで凝縮の主張が得られます。崩壊像は順序数 `β` を添字とする段階に等しくなります。応用では、段階 `Lset α` と一つの点 `x` の合併を始集合とし、`α ∈ lam`、`x ⊆ Lset α`、`x ∈ Lset lam` を仮定します。

```agda
    condenses : Σ[ γ ∈ S ] (IsOrd γ × (C.πX ≡ Lset γ))
    condenses = β , β-isOrd , ext
module UnionKit (α lam x : S) (ordα : IsOrd α) (ordλ : IsOrd lam)
  (α∈λ : ⟨ α ∈ˢ lam ⟩) (x⊆Lα : (z : S) → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ Lset α ⟩)
  (x∈Lλ : ⟨ x ∈ˢ Lset lam ⟩) (α∉ω : ⟨ α ∈ˢ ω ⟩ → Empty.⊥) where
```

始集合は `Lset α` と単集合 `{x}` の合併です。単集合の特徴づけから `x ∈ {x}` が得られます。

```agda
  X : S
  X = Lset α ∪ ⁅ x ⁆s
  x∈sgl : ⟨ x ∈ₛ ⁅ x ⁆s ⟩
  x∈sgl = SetPackage.classification (SingletonPackage x) x .snd refl
```

余分な点は、和の右側を通して始集合に属します。

```agda
  x∈X : ⟨ x ∈ˢ X ⟩
  x∈X = cup-inr (Lset α) ⁅ x ⁆s x (∈∈ₛ {a = x} {b = ⁅ x ⁆s} .snd x∈sgl)
```

段階のすべての要素は、左側を通して始集合に属します。

```agda
  Lα∈X : (z : S) → ⟨ z ∈ˢ Lset α ⟩ → ⟨ z ∈ˢ X ⟩
  Lα∈X = cup-inl (Lset α) ⁅ x ⁆s
```

単集合の特徴づけにより、`{x}` の各要素は `x` に等しくなります。

```agda
  sgl≡ : (z : S) → ⟨ z ∈ˢ ⁅ x ⁆s ⟩ → z ≡ x
  sgl≡ = sgl-out x
```

したがって、始集合への所属は二つの場合に分かれます。その点は `Lset α` に属するか、単集合 `{x}` に属します。

```agda
  X-mem : (z : S) → ⟨ z ∈ˢ X ⟩
        → ⟨ (z ∈ˢ Lset α) ⊔ (z ∈ˢ ⁅ x ⁆s) ⟩
  X-mem = cup-out (Lset α) ⁅ x ⁆s
```

生成集は周囲の段階に含まれます。段階の側の要素は、指数の包含に沿って、段階の構成の単調性によって運ばれます。

```agda
  X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z z∈X = PT.rec (snd (z ∈ˢ Lset lam)) go (X-mem z z∈X)
    where
    go : (⟨ z ∈ˢ Lset α ⟩ ⊎ ⟨ z ∈ˢ ⁅ x ⁆s ⟩) → ⟨ z ∈ˢ Lset lam ⟩
    go (inl z∈Lα) = Lset-mono {α = lam} {β = α} α∈λ z∈Lα
```

単元の側の要素は余分な点に帰着し、その段階への所属は仮定でした。

```agda
    go (inr z∈sgl) = subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym (sgl≡ z z∈sgl)) x∈Lλ
```

生成集は推移的です。段階の側の要素の要素は、層の推移性によって段階の中にあり、左の包含がそれを生成集の中に置きます。

```agda
  Xtr : isTransV X
  Xtr {x = a} {y = b} b∈a a∈X = PT.rec (snd (b ∈ˢ X)) go (X-mem a a∈X)
    where
    go : (⟨ a ∈ˢ Lset α ⟩ ⊎ ⟨ a ∈ˢ ⁅ x ⁆s ⟩) → ⟨ b ∈ˢ X ⟩
    go (inl a∈Lα) = Lα∈X b (layer-trans (Lset-layer α) b∈a a∈Lα)
```

単集合側では中間の集合は `x` です。仮定 `x ⊆ Lset α` により、その各要素は合併の左側に入ります。

```agda
    go (inr a∈sgl) = Lα∈X b (x⊆Lα b
      (subst (λ u → ⟨ b ∈ˢ u ⟩) (sgl≡ a a∈sgl) b∈a))
  one∈α : ⟨ sucV ∅ ∈ˢ α ⟩
  one∈α = Sum.rec
      (λ α∈ω → Empty.rec (α∉ω α∈ω))
```

無限とは `ω` に属さないことであり、順序数の三分法が場合を分けます。`ω` に属するなら仮定と矛盾し、`ω` と等しいなら数項一が所属の証人となり、`ω` が `α` より下なら `α` の推移性によって数項一がその中に入ります。

```agda
      (Sum.rec (λ α≡ω → subst (λ w → ⟨ sucV ∅ ∈ˢ w ⟩) (sym α≡ω) (#∈ω 1))
               (λ ω∈α → ordα .fst (#∈ω 1) ω∈α))
      (ord-tri α ordα ω ω-ord)
```

空集合は最初の後続の段階に現れます。基底の層の符号化が、後続の段階の記述に沿って運ばれるからです。

```agda
  ∅∈Lset1 : ⟨ ∅ ∈ˢ Lset (sucV ∅) ⟩
  ∅∈Lset1 = subst (λ w → ⟨ ∅ ∈ˢ w ⟩) (sym (Lset-suc ∅)) (∅∈𝒟ₒ ∅)
```

単調性が、空集合をまず `Lset α` へ、さらに `Lset lam` へ持ち上げます。

```agda
  ∅∈Lλ : ⟨ ∅ ∈ˢ Lset lam ⟩
  ∅∈Lλ = Lset-mono {α = lam} {β = α} α∈λ
    (Lset-mono {α = α} {β = sucV ∅} one∈α ∅∈Lset1)
```

ランクによる特徴づけにより、空集合が指数 `lam` 自身に属することが従います。残るのは包の外延性であり、これはその崩壊を単射にするために必要な最後の条件です。

```agda
  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = subst (λ w → ⟨ w ∈ˢ lam ⟩) (rank-fix ∅ ∅-ord)
    (rank-Lset lam ordλ ∅ ∅∈Lλ)
module HullExt (α : S) (ordα : IsOrd α)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset α ⟩)
```

空集合が指数に属するという仮定により、`Lset α` における Skolem 包は、その項代数に必要な既定値をもちます。

```agda
  (∅∈α : ⟨ ∅ ∈ˢ α ⟩) where
```

`M` を、`Lset α` の内部で `X` から生成される Skolem 包とします。段階への包含は初等的です。`M` に制限した所属関係の外延性を示すため、包の中の論理式と段階での解釈を比較します。

```agda
  module ASt = AtStage α ordα using ( module AbsL; module AtM; module Hull; SL )
  module H = ASt.Hull X X⊆L ∅∈α using ( module T; Hull⊆L )
  module A = ASt.AtM H.T.Hull H.Hull⊆L using ( SM; inL; module SemM )
  module E = HullElemDown α ordα X X⊆L ∅∈α using ( elem )
  module Mse = A.SemM.At A.SM id using ( _⊨_ )
```

包が名付けられ、二つの集合の対称差が所属の真値の水準で述べられます。ある点が一方に属し、他方には属さないと証明できる、という形です。

```agda
  M : S
  M = H.T.Hull
  Different : S → S → S → Type (ℓ-suc ℓ)
  Different x y z = (z ∈ᵗ x × (z ∈ᵗ y → Empty.⊥))
                  ⊎ (z ∈ᵗ y × (z ∈ᵗ x → Empty.⊥))
```

古典的に、等しくない集合は対称差の中に点をもちます。切り詰められた存在は、排中律によって判定されます。

```agda
  different : (x y : S) → (x ≡ y → Empty.⊥) → ∥ Σ[ z ∈ S ] Different x y z ∥₁
  different x y nxy = go (lem P)
    where
    P : hProp (ℓ-suc ℓ)
    P = ∥ Σ[ z ∈ S ] Different x y z ∥₁ , squash₁
```

もし二つの集合を区別する点がなければ、すべての所属命題が両方向で一致し、宇宙の外延性によって両者は等しくなり、仮定に矛盾します。

```agda
    go : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → ⟨ P ⟩
    go (inl p) = p
    go (inr np) = Empty.rec (nxy (extensionalV (λ z → ⇔toPath (fwd z) (bwd z))))
      where
      fwd : (z : S) → z ∈ᵗ x → z ∈ᵗ y
```

一致の両方向は排中律で判定され、失敗した方向はそれぞれの点を対称差に加えます。

```agda
      fwd z zx = Sum.rec (λ zy → zy)
        (λ nzy → Empty.rec (np ∣ z , inl (zx , nzy) ∣₁)) (lem (z ∈ˢ y))
      bwd : (z : S) → z ∈ᵗ y → z ∈ᵗ x
      bwd z zy = Sum.rec (λ zx → zx)
        (λ nzx → Empty.rec (np ∣ z , inr (zy , nzx) ∣₁)) (lem (z ∈ˢ x))
```

差の公式は選言 `(z ∈ x ∧ z ∉ y) ∨ (z ∈ y ∧ z ∉ x)` であり、二つの定数欄に二つの包の要素を入れます。

```agda
  φ : A.SM → A.SM → Formula A.SM 1
  φ x y = ((var zero ∈̇ con x) ∧̇ (¬̇ (var zero ∈̇ con y)))
        ∨̇ ((var zero ∈̇ con y) ∧̇ (¬̇ (var zero ∈̇ con x)))
  outer : (u v : S) (u∈M : u ∈ᵗ M) (v∈M : v ∈ᵗ M)
        → (z : S) → Different u v z
```

存在論理式の充足は切り詰められているので、区別する点も切り詰めの中で返します。対称差のどちらの分岐でも、同じ点が段階における論理式の対応する選言肢を証明します。

```agda
        → ∥ Σ[ a ∈ ASt.SL ]
            ⟨ (a ∷ []) ASt.AbsL.⊨ᵐ (mapFo A.inL (φ (u , u∈M) (v , v∈M))) ⟩ ∥₁
  outer u v u∈M v∈M z d = ∣ a , ∣ objectDifferent d ∣₁ ∣₁
    where
    objectDifferent = Sum.map
```

どちらの分岐でも、周囲での所属が肯定側の連言項を与え、不所属の証明を公式意味論が要求する否定へ持ち上げます。段階の推移性により、区別する点もその台に入ります。

```agda
      (λ (zu , nzv) → zu , λ zv → lift (nzv zv))
      (λ (zv , nzu) → zv , λ zu → lift (nzu zu))
    z∈L : ⟨ z ∈ˢ Lset α ⟩
    z∈L = Sum.rec
      (λ (zx , _) → layer-trans (Lset-layer α) zx (H.Hull⊆L u u∈M))
```

区別する点をその段階への所属と組にすると、段階の台における証人が得られます。包の外延性を示すため、まず包の各要素について、`x` に属するなら `y` にも属すると仮定します。

```agda
      (λ (zv , _) → layer-trans (Lset-layer α) zv (H.Hull⊆L v v∈M)) d
    a : ASt.SL
    a = z , z∈L
  refute : (x y : S) (x∈M : x ∈ᵗ M) (y∈M : y ∈ᵗ M)
         → (ag1 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩)
```

逆に、包の各要素について、`y` に属するなら `x` にも属すると仮定します。それでも `x` と `y` が等しくないなら、対称差の点から矛盾が導かれます。

```agda
         → (ag2 : (z : S) → z ∈ᵗ M → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
         → (x ≡ y → Empty.⊥) → Empty.⊥
  refute x y x∈M y∈M ag1 ag2 nxy = PT.rec Empty.isProp⊥ diff (different x y nxy)
    where
    xS : A.SM
```

二つの包の要素は、部分構造の台の要素として読まれ、差の論理式に代入する準備ができます。

```agda
    xS = x , x∈M
    yS : A.SM
    yS = y , y∈M
```

反証は、差の点を消去します。初等性が、差の点を証人とする存在の論理式の段階での充足を、包の中での同じ存在の充足へ変えます。

```agda
    diff : Σ[ z ∈ S ] Different x y z → Empty.⊥
    diff (z , d) = PT.rec Empty.isProp⊥ inside h
      where
      h : ⟨ [] Mse.⊨ (∃̇ (φ xS yS)) ⟩
      h = subst ⟨_⟩ (sym (E.elem 0 (∃̇ (φ xS yS)) []))
```

初等性により、差の論理式を満たす包の中の証人が得られます。その切り詰められた選言を消去すると、二つの非対称な所属命題のどちらが成り立つかが得られます。

```agda
        (outer x y x∈M y∈M z d)
      inside : Σ[ b ∈ A.SM ] ⟨ (b ∷ []) Mse.⊨ φ xS yS ⟩ → Empty.⊥
      inside (b , q) = PT.rec Empty.isProp⊥ cases q
        where
        cases : (⟨ fst b ∈ˢ x ⟩ × (⟨ fst b ∈ˢ y ⟩ → Lift Empty.⊥))
```

どちらの選言の枝でも、証人は一方の包の要素ではあって他方ではないとされ、対応する一致の仮定がその否定と矛盾します。この矛盾こそ、包の外延性が求めるものです。

```agda
              ⊎ (⟨ fst b ∈ˢ y ⟩ × (⟨ fst b ∈ˢ x ⟩ → Lift Empty.⊥))
              → Empty.⊥
        cases (inl (bx , nby)) = lower (nby (ag1 (fst b) (snd b) bx))
        cases (inr (by , nbx)) = lower (nbx (ag2 (fst b) (snd b) by))
```

包の外延性は古典的な背理法で証明する。集合の宇宙は h-集合なので `x ≡ y` は命題であり、排中律から等しい場合と等しくない場合に分かれる。`x ≢ y` なら、`refute` は包の中に `x` と `y` の一方だけに属する要素を与え、二つの所属一致の仮定に矛盾する。したがって `x ≡ y` である。

```agda
  hullExt : isExt M
  hullExt x y x∈M y∈M ag1 ag2 =
    Sum.rec (λ p → p) (λ np → Empty.rec (bad np))
      (lem ((x ≡ y) , isSetS x y))
    where
```

`bad` が矛盾する分岐を除き、包の外延性が完成する。

```agda
    bad : (x ≡ y → Empty.⊥) → Empty.⊥
    bad = refute x y x∈M y∈M ag1 ag2
```

## 崩壊を通して有界論理式を移す

崩壊と周囲の宇宙を比較するため、ここで推移的集合 `U` を固定する。定数を含まない Δ₀ 論理式を `U` の要素で評価すると、`U` 上の制限構造と周囲の構造で同じ真理値をもつ。

```agda
module Unpack (U : S) (Utr : isTrans U) where
```

制限された台 `SM` の要素は、集合とそれが `U` に属する証拠との組である。各組を第一成分へ射影すると対応する周囲の環境が得られ、有界絶対性 `abs₀` が射影の前後の充足を比較する。

```agda
  module Ab = FOL.Absoluteness.Single 𝒮ᵥ (λ x → x ∈ˢ U) Utr using (SM; abs₀; _⊨ᵐ_)
```

定数を含まない Δ₀ 論理式 `φ` について、`read` はまず `embed φ` を制限された台の上の論理式として扱う。有界絶対性が制限された読みと周囲の読みを比較し、`embed-⊨` が埋め込みに伴う改名を除き、空の定数領域からの関数の一意性が残る定数解釈を同定する。

```agda
  read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Ab.SM ^ n)
       → (δ Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
  read {n} {φ} dφ δ =
      Ab.abs₀ (mapΔ₀ Empty.rec* dφ) δ
    ∙ embed-⊨ 𝒮ᵥ {K = Ab.SM} fst φ (map fst δ)
```

最後のパスでは関数外延性を使う。定数領域が空なので、二つの定数解釈は各点で一致し、したがって等しい。次に `Lset lam` の内部で包を作るため、後続に閉じた順序数 `lam` と始集合 `X ⊆ Lset lam` を固定する。

```agda
    ∙ cong (λ ι → SemV.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
           (funExt (λ b → Empty.rec* b))
module Frame (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆Lλ : (z : S) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
```

さらに `∅ ∈ lam` を仮定する。これは包の構成が用いる基底段階の仮定である。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

`M` を `Lset lam` の内部で `X` から生成される包とする。以下では、段階への包含、それに対する初等性、そして上で証明した外延性を用いる。

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using (module ASt; module C; module Condense; module H; M)
  module ASt = HS.ASt using (module AbsL; module AtM; Ltr; SL)
  module A = ASt.AtM HS.M HS.H.Hull⊆L using (Elementary; SM; module SemM; inL)
  module HE = HullExt lam ordλ X X⊆Lλ ∅∈λ using (hullExt)
```

したがって `M` は外延的である。これは `M` をその推移的な Mostowski 崩壊と同一視するために必要な仮定である。

```agda
  Mext : isExt HS.M
  Mext = HE.hullExt
```

移送の議論は、包含 `M → Lset lam` の初等性を明示的に受け取る。これと `M` の外延性から、以下で使う二つの比較、すなわち包から段階への比較と、包からその崩壊への比較が得られる。

```agda
  module Carry (elem : A.Elementary) where
```

ここでは三つの構造、包 `M`、段階 `Lset lam`、推移的な崩壊像 `πX` を比較する。崩壊同型が第一と第三を結び、有界絶対性が二つの推移的集合をそれぞれ周囲の宇宙に結びつける。

```agda
    module CIso = CollapseIso HS.M Mext using (module I; iso-fwd; iso-bwd)
    module TL = Unpack (Lset lam) ASt.Ltr using (read)
    module Tπ = Unpack HS.C.πX HS.C.πX-trans using (module Ab; read)
```

所属は崩壊によって直接保存されます。所属の同型の順方向が、原子的な所属に必要な押し出しにちょうど当たります。

```agda
    member-push : (x y : S) → ⟨ x ∈ˢ HS.M ⟩ → ⟨ y ∈ˢ HS.M ⟩
                → ⟨ y ∈ˢ x ⟩ → ⟨ HS.C.π y ∈ˢ HS.C.π x ⟩
    member-push = CIso.iso-fwd
```

`Lset lam` は推移的なので、定数を含まない各 Δ₀ 論理式はそこで制限された読みと周囲の読みが一致する。`atL` はこの段階における `read` である。

```agda
    atL : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : ASt.SL ^ n)
        → (δ ASt.AbsL.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atL dφ δ = TL.read dφ δ
```

崩壊像 `πX` も推移的なので、定数を含まない Δ₀ 論理式について同じ内外の一致が成り立つ。

```agda
    atπ : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : Tπ.Ab.SM ^ n)
        → (δ Tπ.Ab.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atπ dφ δ = Tπ.read dφ δ
```

包自身の台のもとの読みは、初等性を通って分解されます。埋め込まれた論理式はまず内部で読まれ、その論理式が定数を運ばないため改名は固定され、結果は段階の読みへ運ばれます。

```agda
    atM : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
        → (δ CIso.I.⊨ᵐ embed φ) ≡ (map fst δ ⊨ₚ φ)
    atM {n} {φ} dφ δ =
        elem n (embed φ) δ
      ∙ cong (λ ψ → map A.inL δ ASt.AbsL.⊨ᵐ ψ) (embed-map A.inL φ)
```

段階での絶対性の後に残るのは環境の比較だけである。包の要素を `Lset lam` に含めても基礎にある集合は変わらないので、包含してから射影した周囲の集合のベクトルは、元の環境を直接射影したものに等しい。

```agda
      ∙ atL dφ (map A.inL δ)
      ∙ cong (λ γ → γ ⊨ₚ φ) (map-inL-fst δ)
      where
      map-inL-fst : {m : ℕ} (γ : A.SM ^ m)
                  → map fst (map A.inL γ) ≡ map fst γ
```

この等式は空の環境では直ちに成り立ち、環境の先頭に一つの成分を加えても保たれる。したがって、定数を含まない Δ₀ 論理式について、包の要素からなる環境での周囲の真理は、それらの崩壊値からなる環境での周囲の真理を導く。

```agda
      map-inL-fst [] = refl
      map-inL-fst (q ∷ γ) = cong (fst q ∷_) (map-inL-fst γ)
    push : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst δ ⊨ₚ φ ⟩
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
```

包の環境での周囲の真理から出発し、まず `atM` を逆向きに使って包の内部の真理を得る。`iso-inv` がそれを崩壊像へ移し、`embed-map` が空虚な定数の改名を除き、最後に `atπ` を順向きに使って崩壊値での周囲の真理へ戻す。

```agda
    push {n} {φ} dφ δ h =
      subst ⟨_⟩ (atπ dφ (map CIso.I.g δ))
        (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
               (embed-map CIso.I.g φ)
               (CIso.I.iso-inv n (embed φ) δ (subst ⟨_⟩ (sym (atM dφ δ)) h)))
```

`pull` では、崩壊値での周囲の真理を `atπ` に沿って逆向きに崩壊像の内部へ移す。`embed-map` で改名された形を戻し、`iso-inv-bwd` で包の内部の真理へ戻った後、`atM` を順向きに使って元の包の環境での周囲の真理を回復する。

```agda
    pull : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : A.SM ^ n)
         → ⟨ map fst (map CIso.I.g δ) ⊨ₚ φ ⟩
         → ⟨ map fst δ ⊨ₚ φ ⟩
    pull {n} {φ} dφ δ h =
      subst ⟨_⟩ (atM dφ δ)
```

`push` と `pull` を合わせると、定数を含まない任意の Δ₀ 論理式と、包の要素からなる任意の有限環境について、各成分をその崩壊値に置き換えても周囲での充足は変わらない。別の補題 `member-push` は、所属について対応する保存を直接与える。

```agda
        (CIso.I.iso-inv-bwd n (embed φ) δ
          (subst (λ ψ → ⟨ map CIso.I.g δ CIso.I.⊨ᵖᵐ ψ ⟩)
                 (sym (embed-map CIso.I.g φ))
                 (subst ⟨_⟩ (sym (atπ dφ (map CIso.I.g δ))) h)))
```