---
title: "有界な分出公理と置換公理"
module: L.Axioms.Separation
lang: ja
site: "Bedrock"
description: "有界な分出公理と置換公理"
stage: "構成可能段階と公理"
reading_order: 32
canonical: https://bedrock.institute/ja/L.Axioms.Separation.html
html: L.Axioms.Separation.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Separation.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantBounding, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Semantics, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, L.Definability, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Axioms.Separation.md, https://bedrock.institute/zh/L.Axioms.Separation.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 有界な分出公理と置換公理

有界な分出公理が求めるのは、構成可能集合 `a` のホスト側の部分型だけではありません。`a` に属し、与えられた Δ₀ 論理式を満たす `x` だけを要素とする、構成可能モデルの要素を求めます。有界な置換公理は、関数的な Δ₀ 関係の値からなる集合を求めます。どちらの証明でも、関係するデータを一つの順序数段階へ入れ、その段階で定義可能部分集合を作り、この段階内の計算を構成可能モデル全体での充足関係と比較します。

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

初めから二つの論理の層を区別する必要があります。論理式とその量化子は、モデルが解釈する対象言語に属します。真理値が決定可能であるという主張はホスト理論に属します。後続宇宙レベルの排中律を仮定します。この仮定は、構成可能集合を含む最小の層を割り当てる操作を通して証明に入ります。これは `L` の内部で主張される公理でも、選択原理でもありません。

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

そこで宇宙レベル `ℓ` とホスト側の仮定 `lem : LEM (ℓ-suc ℓ)` を固定します。ここから得られる各定理は、その型にこの仮定を明示的に保ちます。固定した段階での議論は、定義可能性、推移性、Δ₀ 絶対性だけを構成的に使います。古典的な依存が実際に現れるのは、任意の定数、始集合、または選ばれた像の値に、正準な最小段階の添字を割り当てるときです。

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

対象言語によって、第一の有界性が正確に定まります。論理式 `φ : Formula S n` はモデルの台 `S` の要素を定数として含むことができ、`n` 個の自由変数の位置をもちます。証明 `Δ₀ φ` は、`φ` に現れるすべての量化子が項によって有界であることを表します。所属の原子論理式は Δ₀ であり、連言と有界存在量化はこの性質を保ちます。この三つの閉性によって、分出の論理式と像の論理式も Δ₀ になります。

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

もう一つの有界性は定数を制約します。`BoundedTm P t` と `BoundedFo P φ` は、項または論理式に現れるすべての定数がホスト側の述語 `P` を満たすことを表します。論理式の量化子が有界かどうかについては何も述べないので、`mkBoundedFo` は Δ₀ でない論理式にも適用できます。この証明を使うと、改名によって各定数を選んだ段階の添字に置き換えられ、写像に関する補題によって、その構文上の変更の前後で充足関係を比較できます。

```agda
open import FOL.Manipulation.ConstantBounding
  using ( BoundedTm; BoundedFo; BoundedTm-mono; BoundedFo-mono; module Relabel )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Semantics
```

なぜ定数を一つの段階へ移すのでしょうか。段階 `Lset σ` には小さな提示があるため、その部分集合を定義する論理式は、この提示の添字を定数として使います。これに対して元の論理式は、`S` の任意の要素を定数として使います。改名した後では、`DefOf (Lset σ)` が、その論理式で選ばれる部分集合を周囲の累積階層の中で作り、構成可能性に関する結果がそれをモデルの要素として組み立てます。残る課題は、この段階で定義した部分集合の要素が、元の論理式が `L` で指定する要素と正確に一致することを証明することです。

```agda
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
```

階層に関する道具は、二つの規模の順序数上界を与えます。`bound2` は二つの段階の添字を一つの共通の順序数の中へ置き、`boundingOrd` は小さな型で添字づけられた族について同じことを行います。その後、段階の単調性によって所属を共通上界まで持ち上げます。操作 `stage` は、各構成可能集合に、それを含む最小の段階の添字を割り当てます。この構成では、この最小段階の操作だけが `lem` を使います。もう一方の端では、`uniqueL` がモデルの集合外延性を使い、各点での所属の仕様から一意性を証明します。

```agda
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans; Lset-mono
        ; 𝒟ₒ; 𝒟ₒ-intro; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; boundingOrd; bound2 )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS; 𝒟ₒ→isL; uniqueL )
```

ここで使ういくつかの等しさは、役割が異なります。`⇔toPath` は命題外延性を使い、二方向の含意を命題値の真理値の間のパスへ変えます。構成可能性の証明が命題をなすため、`Σ≡Prop` は基礎にある集合の等しさをモデル要素の等しさへ持ち上げます。集合外延性は、これとは別に `uniqueL` を通して使われます。最後に、命題的切り詰めは、選ばれた証人を保持せずに証人の存在だけを記録します。その除去子は、行き先が再び命題である場合にだけ使います。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
```

小さな提示は、モデルの所属を、順序数による上界と段階での定義可能性に必要な小さな添字型へ結びつけます。累積階層の集合 `A` に対して、型 `⟪ A ⟫` は提示された要素を添字づけ、`⟪ A ⟫↪` は添字が名指す集合を返します。逆に、`∈-asFiber` は所属の証明 `x ∈ A` を、添字と、その提示された集合から `x` へのパスへ変えます。この構成は、切り詰められていないファイバーのデータを局所的に使います。命題的切り詰めから代表を取り出すことはありません。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
```

`L` 上の命題値構造の台を `S` とします。要素 `x : S` は、周囲の集合 `fst x` と、その集合が構成可能であることの証明 `snd x` からなる依存対です。したがって `S` はモデルの台の型であり、`L` という名の集合ではありません。その等しさと所属は基礎にある集合から読み取られ、`hProp` に値を取ります。

```agda
open hPropStructure 𝒮ʟ
```

これらの公理が最終的に要求するのは、この台がホスト側のクラス `Q : S → hProp (ℓ-suc ℓ)` を実現することです。型 `SetOf Q` は、モデル要素 `b` と、各 `x : S` に対するパス `(x ∈ˢ b) ≡ Q x` を組にします。分出公理では、`Q x` は始集合への所属と対象言語の充足判断を連言で結びます。たとえば論理式が `x` は定数 `c` に属すと述べるなら、求める外延は `a` と `c` の共通部分です。証明はこのクラスを `L` の集合によって実現します。クラスそのものを対象言語の論理式と同一視することも、ホスト理論の部分型がすでに `L` に属すと仮定することもありません。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

同じ対象言語の論理式を、二つの構造で読めるようになりました。記法 `γ ⊨v φ` は、生の集合からなる割り当てのもとで、周囲の累積階層における充足関係を表します。一方、`γ ⊨ φ` は台が `S` である構造における充足関係を表します。この二つの判断を区別しておくことが必要です。固定した段階での構成は、まず周囲で定義された部分集合についての主張を証明し、その後、絶対性によって構成可能モデルで意図した充足判断を回復します。

```agda
module SemV = FOL.Semantics 𝒮ᵥ
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )
```

構成可能クラスは推移的です。構成可能集合の要素は再び構成可能です。これは有界量化子を扱うのにちょうど十分です。構成可能な境界項の解釈に属する周囲の証人は `S` の要素として組み直せ、内側の証人は基礎にある集合へ射影できます。したがって Δ₀ 論理式についての帰納から、その周囲での真理値と内側での真理値の間のパス `abs₀` が得られます。これは Δ₀ 絶対性であり、`L` やいずれかの段階が任意の論理式について初等的であるという主張ではありません。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( abs₀ ) renaming ( _⊨ᵐ_ to _⊨_ )
```

## 置換による像

置換公理については、まず像をホスト側の述語として述べます。真理値 `ReplImage a φ z` は、ある `x : S` が存在して、`x ∈ˢ a` であり、対象言語の論理式 `φ` が割り当て `x ∷ z ∷ []` で充足されるという事実だけを表します。ここでは始域の要素が第零の位置、値の候補が第一の位置を占めます。このホスト側の添字付き存在は命題的切り詰めを使うため、どの始域の要素が `z` を生じたかを忘れます。これは、同じ像を一変数論理式によって定義するときに使う対象言語の有界存在 `∃̇∈` とは別のものです。この定義自体は、`φ` が Δ₀ であることも、関係が関数的であることも要求しません。

```agda
ReplImage : (a : S) (φ : Formula S 2) → S → hProp (ℓ-suc ℓ)
ReplImage a φ z = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((x ∷ z ∷ []) ⊨ φ)
```

## 関数的な像を抑える

置換公理で新たに生じる問題は、可能な値をすべて含む一つの段階を見つけることです。`FunctionalImage` は任意のホスト側の関係 `R` を扱い、各 `x ∈ˢ a` についてファイバー `Σ[ y ∈ S ] ⟨ R x y ⟩` が可縮であると仮定します。したがって、このファイバーには指定された中心があり、ほかのすべての関係する対はその中心に等しくなります。この仮定は、各始域の要素について存在と一意性をデータとして与えます。中心を射影することは通常の依存関数の適用であり、ホスト側の選択公理も対象理論の選択公理も使いません。

```agda
module FunctionalImage (a : S) (R : S → S → hProp (ℓ-suc ℓ))
                       (fc : (x : S) → ⟨ x ∈ˢ a ⟩
                           → isContr (Σ[ y ∈ S ] ⟨ R x y ⟩)) where
```

型 `Mem` は、始域の要素と、それが `a` に属するという証拠を組にします。可縮なファイバーについての仮定はこの証拠を入力として要求するので、単なる `x : S` だけでは足りません。`S` はすでに後続宇宙レベルにあるため、`Mem` は `boundingOrd` が要求する小さな添字型として直接使うには大きすぎます。基礎にある集合 `fst a` の正準な小さな提示は、上界の構成に必要な始域の要素を小さな型で列挙します。

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

`p : Mem` に対して、可縮なファイバー `fc (p .fst) (p .snd)` はすでにその中心を含んでいます。関数 `img` は中心の値の成分を射影し、証明付きの各始域の要素に対して一つの確定したモデル要素を与えます。これは各点で値を選んでいるように見えますが、切り詰められた存在を除去してはいません。中心は、与えられた依存関数 `fc` の明示的な成分だからです。

```agda
  img : Mem → S
  img p = fc (p .fst) (p .snd) .fst .fst
```

中心が含むのは選ばれた値だけではありません。その第二成分は `R (p .fst) (img p)` が成り立つことを証明し、`img-sat` はこの事実に名前を与えます。この区別には意味があります。`img` はその段階を抑えられる要素を与え、`img-sat` は、その選ばれた要素が与えられた始域の要素における関係の値であることを証明します。

```agda
  img-sat : (p : Mem) → ⟨ R (p .fst) (img p) ⟩
  img-sat p = fc (p .fst) (p .snd) .fst .snd
```

可縮性はまた、選ばれた中心を、ほかのすべての関係する対 `(y , h)` と同一視します。第一射影に合同性を適用すると `img p ≡ y` が得られます。これは構成可能性の証明も含む、モデル要素全体の等しさです。`img p` を共通の段階へ入れ、この等しさに沿って所属の証明を輸送すれば、`R (p .fst) y` を満たす任意の `y` を扱えます。関数性は始域の要素ごとに使われます。異なる始域の要素から生じる値が互いに異なるという主張ではありません。

```agda
  img-uniq : (p : Mem) (y : S) → ⟨ R (p .fst) y ⟩ → img p ≡ y
  img-uniq p y h = cong fst (fc (p .fst) (p .snd) .snd (y , h))
```

小さな添字の族を得るために、`memS` は添字 `m : ⟪ fst a ⟫` から始めます。この添字が提示する集合は `fst a` に属します。`a` は構成可能であり、構成可能クラスは推移的なので、この提示された集合も構成可能です。したがって、その集合と証明を組にして `S` の要素を作れます。さらに元の所属の証明を加えると `Mem` の要素となり、`img` とファイバーについての仮定を適用できます。

```agda
  private
    memS : ⟪ fst a ⟫ → Mem
    memS m = (⟪ fst a ⟫↪ m
             , isL-trans fm∈fa (a .snd)) , fm∈fa
      where
```

局所的な証明 `fm∈fa` は、`memS` の所属の成分を与えます。正準な提示は、まず小さな所属関係によって所属を述べ、`∈∈ₛ` がその事実を累積階層の命題値の所属へ変換します。`fm∈fa` と証明 `a .snd` に推移性を適用すると、`memS` の構成可能性の成分が得られます。したがって同じ所属の事実が、提示された集合を始集合の中に位置づけると同時に、それを構成可能なモデル要素として組み立てることを可能にします。

```agda
      fm∈fa : ⟨ ⟪ fst a ⟫↪ m ∈ fst a ⟩
      fm∈fa = ∈∈ₛ {a = ⟪ fst a ⟫↪ m} {b = fst a} .snd (∈ₛ⟪ fst a ⟫↪ m)
```

これで、小さな型 `⟪ fst a ⟫` を通して始集合を走査できます。各添字 `m` について、選ばれた値 `img (memS m)` を含む最小の段階の添字を取り、その順序数性を `stage-ord` で与えます。構成的な操作 `boundingOrd` は、これらすべての添字より真に上にある一つの順序数を返します。共通上界の議論が使うのは `stage-ord` と `stage-mem` が与える事実であり、最小性は必要ありません。ただし、標準的な `stage` の割り当てから最小性も得られます。`a` が空なら添字の族も空ですが、`boundingOrd` はそれでも順序数上界を返し、像に要素があるとは主張しません。

```agda
    bImg = boundingOrd ⟪ fst a ⟫
      (λ m → stage (fst (img (memS m))) (img (memS m) .snd))
      (λ m → stage-ord (fst (img (memS m))) (img (memS m) .snd))
```

この上界の結果の第一射影を `βimg` と名づけます。これは順序数である段階の添字であり、段階そのものではありません。対応する段階は、累積階層の集合 `Lset βimg` です。`range∈βimg` は、関係するすべての値の基礎にある集合がこの段階に属すことを述べます。`Lset βimg` をモデル要素として組み立てるのは別の操作であり、順序数性の証明を必要とします。

```agda
  βimg : V ℓ
  βimg = bImg .fst
```

`bImg` の第二射影は、上界の二つの部分を証明します。その第一の部分をここで `βimg-ord` として取り出し、`βimg` が順序数であることを示します。この証明によって、`Lset βimg` をモデル要素として組み立てられます。残る部分は、小さな始域の添字 `m` ごとに、選ばれた値の段階の添字が `βimg` に属することを与えます。この比較を `stage-mem` と組み合わせると、選ばれた各像が `Lset βimg` に入ります。さらに、提示された始域の要素から任意の始域の要素へ輸送し、`img-uniq` を使うことで、その要素と関係するすべての値へ結論を広げます。したがって、順序数性と値域の包含は、同じ上界の構成から取り出される別々の主張です。

```agda
  βimg-ord : IsOrd βimg
  βimg-ord = bImg .snd .fst
```

関係のすべての値を抑えるため、`x ∈ˢ a`、候補 `y`、および `R x y` の証明を固定します。始集合への所属により、`x` は `a` の標準的な小さい表示から得られる要素と同一視されます。関数性はさらに、`y` をその表示された要素で選ばれた値と同一視します。その値は自身の標準的な段階に属し、その添字は `βimg` より真に小さいので、`Lset-mono` によって `Lset βimg` へ持ち上がります。最後に値の等式に沿って輸送すれば `y` の所属が得られます。したがって一つの段階 `Lset βimg` が、`a` の要素から関係によって得られるすべての値を含みます。先に標準的な段階を選ぶ部分は `lem` に依存しますが、ここでの最後の比較と上方への輸送は新たな古典原理を導入しません。

```agda
  range∈βimg : (x : S) → ⟨ x ∈ˢ a ⟩ → (y : S) → ⟨ R x y ⟩
              → ⟨ fst y ∈ Lset βimg ⟩
  range∈βimg x x∈a y h = subst (λ w → ⟨ fst w ∈ Lset βimg ⟩) image≡y
    (Lset-mono {α = βimg} {β = stage (fst (img (memS m))) (img (memS m) .snd)}
      (bImg .snd .snd m) (stage-mem (fst (img (memS m))) (img (memS m) .snd)))
```

所属のファイバーは、任意の始点と小さい表示を比較するための二つのデータを同時に与えます。第一射影は `fst a` の表示の添字 `m` です。これは単に要素が存在する集まりから選んだものではなく、所属の証明そのものに含まれるデータです。第二射影は、`m` が表示する集合と `fst x` との等式を与えます。モデル要素の第二成分 `isL` は命題値であり、同じ基礎集合をもつ二つの組を区別しないため、`Σ≡Prop`はこの基礎集合の等式を `memS m .fst ≡ x` へ持ち上げます。

```agda
    where
    m = ∈-asFiber {a = fst x} {b = fst a} x∈a .fst
    q : memS m .fst ≡ x
    q = Σ≡Prop (λ z → snd (isL z))
      (∈-asFiber {a = fst x} {b = fst a} x∈a .snd)
```

もとの関係の証明は `x` を始点とします。これを `q` の逆向きに沿って輸送すると、`R (memS m .fst) y` の証明になり、`memS m` において `fc` が選んだ中心と同じ値のファイバーに入ります。そのファイバーは可縮なので、`img-uniq` は中心`img (memS m)` と `y` を同一視します。関数性が使われるのは、固定した一つの始点に対する二つの値を比較するためです。異なる始点の値が異なるとは主張しません。

```agda
    image≡y : img (memS m) ≡ y
    image≡y = img-uniq (memS m) y (subst (λ z → ⟨ R z y ⟩) (sym q) h)
```

## 固定した段階での構成

固定した段階での議論は、順序数の添字 `σ` とその証明 `oσ` から始まります。構成 `DefC = DefOf (Lset σ)` は、`Lset σ` の要素をその標準的な小さい表示を通して扱います。そして、表示の添字を定数とする論理式と、各一変数論理式が切り出す部分集合 `defSet` を与えます。残る課題は、この段階に基づく定義を構成可能モデルでの充足と正確に比較することです。

```agda
module AtStage (σ : V ℓ) (oσ : IsOrd σ) where
  module DefC = DefOf (Lset σ)
```

有界論理式の絶対性には、対象となるクラスの推移性が必要です。ここで `DefC.M` は`Lset σ` の要素のクラスであり、`layer-trans (Lset-layer σ)` は、その要素の要素も再び段階内にあることをちょうど証明します。この証明は順序数性の証明 `oσ` を使いません。推移性は `Lset-layer σ` 自体から従います。この閉性によって、有界量化子の証人は制限された世界の内部に留まります。

```agda
  Atrans : Transitive 𝒮ᵥ DefC.M
  Atrans = layer-trans (Lset-layer σ)
```

`Atrans` を `DefC.Refine` に与えると、有界論理式を比較する結果が使えるようになります。改名された記法 `_⊨σ_` は、精緻化モジュールが与える周囲の `V` 値の読みを表します。段階の添字を、それが表示する要素として解釈し、得られた論理式を周囲の階層で評価します。特に `Δ₀` 論理式について、`RefC.abs-defSet` は定義可能部分集合への所属をこの周囲の読みと同一視します。これが後の意味論的な橋の前半です。

```agda
  module RefC = DefC.Refine Atrans
  open RefC.Abs using () renaming ( _⊨ᵛ_ to _⊨σ_ )
```

述語 `Below c` は、基礎集合 `fst c` が `Lset σ` に属することだけを表します。その役割は項や論理式に現れる定数を証明することであり、`BoundedFo Below φ` は`φ` の各定数についてこの証明を保持します。自由変数への付値や量化された証人を制約するものではありません。充足する値が段階内にあることは、後で `carveAt` の別の仮定 `cover` が保証します。

```agda
  Below : S → Type (ℓ-suc ℓ)
  Below c = ⟨ fst c ∈ Lset σ ⟩
```

付け替え `RL` は、`Below` を満たす各モデル定数を、小さい表示 `⟪ Lset σ ⟫` の添字へ変えます。意味論側の二つの写像は、モデル要素から基礎集合を取る `fst` と、表示の添字からそれが指す集合を取る `⟪ Lset σ ⟫↪` です。`fst c ∈ Lset σ` の証明に対して、`∈-asFiber` は必要な添字と、その添字が実際に `fst c` を指すという等式を同時に返します。この二つの射影が、正しい付け替えに必要な可換三角形を与えます。

```agda
  module RL = Relabel {K = S} {K' = ⟪ Lset σ ⟫} {W = V ℓ}
                fst ⟪ Lset σ ⟫↪ Below
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .fst)
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .snd)
```

この橋は、同じ数学的な付値に対する二つの充足命題を比較します。左辺では、まず`RL.liftFo` が `φ` の各定数を表示の添字へ付け替え、`mapFo DefC.ι` がその添字を表示される要素として解釈し、`_⊨σ_` が周囲の階層で `⟪ Lset σ ⟫↪ m` において評価します。右辺では、もとの論理式を構成可能モデルの内部で、組にした要素`(⟪ Lset σ ⟫↪ m , xL)` において評価します。定数の境界 `h`、`Δ₀` の証明 `dφ`、構成可能性の証明 `xL` が、これらの視点の移動を正当化します。

```agda
  satBridge : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ((⟪ Lset σ ⟫↪ m ∷ []) ⊨σ (mapFo DefC.ι (RL.liftFo φ h)))
              ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  satBridge φ h dφ m xL =
```

最初の三つのパスは、連続する二つの定数解釈を整理します。最初の `⊨-map` は段階の定数解釈 `DefC.ι` を展開します。二番目の適用を逆向きに使うと、同じ読みが表示写像 `⟪ Lset σ ⟫↪` を通す形になります。次に `RL.liftFo-correct` を `cong` によって充足の下へ移し、「添字へ付け替えてから再び指す」解釈を、`fst` による直接の解釈へ置き換えます。この最後の段階は `RL` の可換三角形から得られる構文上の論理式の等式です。

```agda
      ⊨-map 𝒮ᵥ DefC.ι fst (RL.liftFo φ h)
        (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (⊨-map 𝒮ᵥ ⟪ Lset σ ⟫↪ id (RL.liftFo φ h)
             (⟪ Lset σ ⟫↪ m ∷ []))
    ∙ cong (λ ψ → (⟪ Lset σ ⟫↪ m ∷ []) ⊨v ψ) (RL.liftFo-correct φ h)
```

第四のパスは再び `⊨-map` を使い、定数と環境をともに `fst` を通して読む周囲での充足を、モデル要素上の対応する論理式へ移します。この時点で、もとの論理式と、組にされた一要素環境がそろいます。最後のパスは `abs₀` を逆向きに使います。`Δ₀` 絶対性により、基礎集合における周囲での真理が構成可能モデル内部での真理へ戻ります。結果は hProp 間の等式なので、後の議論は証明をどちら向きにも輸送できます。

```agda
    ∙ ⊨-map 𝒮ᵥ fst id φ (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (abs₀ dφ ((⟪ Lset σ ⟫↪ m , xL) ∷ []))
```

必要な所属の仕様をここで直接述べられます。段階の表示の添字 `m` と、それが表す集合が構成可能であるという証明 `xL` に対し、持ち上げた論理式が切り出す定義可能部分集合への所属は、もとの論理式が `L` で充足されることに等しくなります。左辺は`Lset σ` の小さい表示を使い、右辺は同じ表示された集合をモデル要素として組にします。この等式が、段階内の構成を分出が実現すべき述語へ結びます。

```agda
  carveSat : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
           → (⟪ Lset σ ⟫↪ m ∈ DefC.defSet (RL.liftFo φ h))
             ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  carveSat φ h dφ m xL =
```

証明は二つの意味論的な等式の合成です。まず `RefC.abs-defSet` が、推移性と持ち上げられた `Δ₀` の証明を用いて、`DefC.defSet (RL.liftFo φ h)` への所属を、表示された要素における `mapFo DefC.ι (RL.liftFo φ h)` の周囲での充足と同一視します。次に `satBridge` が、その周囲の命題を、もとの論理式の構成可能モデル内部での充足と同一視します。定義可能性によってまず周囲の階層へ到達し、モデルの絶対性が最後のつながりを与える、という順序が要点です。

```agda
    RefC.abs-defSet (RL.liftFo φ h) (RL.Δ₀-liftFo h dφ) m ∙ satBridge φ h dφ m xL
```

演算 `carve` は `DefC.defSet` そのものであり、残りの構成で使うために安定した名前を与えたものです。不透明に指定しても集合は変わらず、新しい存在原理も加わりません。自動的な展開を止めるだけです。数学的には `carve ψ` は引き続き、段階の表示上の一変数論理式 `ψ` が `Lset σ` から選び出す部分集合です。続く補題が、この部分集合を使うために必要な所属と構成可能性の事実を与えます。

```agda
  opaque
    carve : Formula ⟪ Lset σ ⟫ 1 → V ℓ
    carve ψ = DefC.defSet ψ
```

論理式 `ψ` 自身が、`carve ψ` が `Lset σ` の定義可能部分集合であることを証言します。構成子 `𝒟ₒ-intro` が要求するのは、そのような論理式と、その `defSet` と対象集合との外延的な等式が単に存在することです。そこで明示的な組 `(ψ , refl)` を`∣ ψ , refl ∣₁` として命題的切り詰めに入れます。その結果、所属命題`carve ψ ∈ 𝒟ₒ (Lset σ)` は、どの論理式が定義したかを保持しません。この補題は、後で `𝒟ₒ→isL` が構成可能性を導くための前提を与えます。この行は命題的切り詰めを導入するだけで、そこから論理式を除去して取り出すことはしません。

```agda
  opaque
    unfolding carve
    carve∈𝒟ₒ : (ψ : Formula ⟪ Lset σ ⟫ 1) → ⟨ carve ψ ∈ 𝒟ₒ (Lset σ) ⟩
    carve∈𝒟ₒ ψ = 𝒟ₒ-intro (Lset σ) (DefC.defSet ψ) ∣ ψ , refl ∣₁
```

`DefC.defSet` が作る定義可能部分集合は、すべて周囲の集合 `Lset σ` に含まれます。補題 `carve⊆` は、この包含を不透明な名前について記録します。`DefC.defSet⊆A` によって `y ∈ carve ψ` から `y ∈ Lset σ` を得ます。この包含は、`y` が構成可能モデルで何らかの論理式を満たすかどうかには依存しません。`defSet` が段階の表示された要素だけを走るという定義から従います。

```agda
    carve⊆ : (ψ : Formula ⟪ Lset σ ⟫ 1) (y : V ℓ) → ⟨ y ∈ carve ψ ⟩
           → ⟨ y ∈ Lset σ ⟩
    carve⊆ ψ y mem = DefC.defSet⊆A ψ y mem
```

`carveSat` の順向きの読みは、切り出された集合への所属をモデルでの充足へ変えます。表示された要素が `carve (RL.liftFo φ h)` に属するなら、hProp の等式 `carveSat` に沿う置換によって、対応するモデル要素が `φ` を満たす証明が得られます。ここで新しい論理的含意を証明しているのではありません。`subst` は、すでに得た等式の左端の要素を右端へ輸送するだけです。

```agda
    imageOut : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
               (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
             → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
             → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
    imageOut φ h dφ m xL mem = subst ⟨_⟩ (carveSat φ h dφ m xL) mem
```

逆向きの読みは、同じ等式を反対向きにたどります。組にされた表示要素による `φ` の充足を `sym (carveSat ...)` に沿って輸送すると、切り出された集合への所属が得られます。`imageOut` と `imageIn` は合わせて点ごとの対応の両方向を与えますが、この時点では固定した段階に表示される要素だけが対象です。任意の充足するモデル要素をそこで表示できることは、後の `cover` の議論が保証します。

```agda
    imageIn : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
            → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
    imageIn φ h dφ m xL sat = subst ⟨_⟩ (sym (carveSat φ h dφ m xL)) sat
```

充足は、モデル要素が携える証明成分には依存しません。各 `isL x` は命題なので、基礎集合の等式 `fst u ≡ fst v` は `Σ≡Prop` により `u ≡ v` へ持ち上がり、充足の証明は得られた一要素環境の等式に沿って輸送されます。証明本体は `dφ` を参照しないため、この輸送は数学的には任意の論理式について成り立ちます。`Δ₀` の引数は証明で使われないまま文に残っており、証明は排中律も使いません。

```agda
  opaque
    ⊨-transport : (φ : Formula S 1) (dφ : Δ₀ φ) (u v : S) → fst u ≡ fst v
                → ⟨ (u ∷ []) ⊨ φ ⟩ → ⟨ (v ∷ []) ⊨ φ ⟩
    ⊨-transport φ dφ u v p =
      subst (λ z → ⟨ (z ∷ []) ⊨ φ ⟩) (Σ≡Prop (λ x → snd (isL x)) p)
```

## 一つの段階で分出する

各添字 `m : ⟪ Lset σ ⟫` は、段階の実際の要素を表示します。標準的な小さい所属の証明 `∈ₛ⟪ Lset σ ⟫↪ m` は、`∈∈ₛ` の第二の向きによって周囲の命題`⟪ Lset σ ⟫↪ m ∈ Lset σ` へ変換されます。`σ` は順序数なので、`Lset→isL σ oσ` はこの段階への所属を構成可能性の証明へ変え、表示された集合を `S` の要素として組にできるようにします。固定した段階の構成で `oσ` が使われるのはこの箇所です。

```agda
  private
    memberIsL : (m : ⟪ Lset σ ⟫) → ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩
    memberIsL m = Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
      (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))
```

固定した段階での一般構成は、一変数論理式 `χ`、そのすべての定数が `Below` を満たす証明、`Δ₀` の証明、および `χ` を満たす各モデル要素の基礎集合が `Lset σ` に属するという被覆条件を受け取ります。目標は、充足述語を実現するものの可縮な型を与えることです。`uniqueL` はこの目標を、点ごとの所属仕様をもつ一つの明示的なモデル要素へ帰着します。命題外延性が各 `z` での二方向の含意を真理値のパスにし、集合外延性が実現する集合の一意性を与えます。

```agda
  carveAt : (χ : Formula S 1) (hχ : BoundedFo Below χ) (dχ : Δ₀ χ)
            (cover : (z : S) → ⟨ (z ∷ []) ⊨ χ ⟩ → ⟨ fst z ∈ Lset σ ⟩)
          → isContr (SetOf (λ z → (z ∷ []) ⊨ χ))
  carveAt χ hχ dχ cover = uniqueL (λ z → (z ∷ []) ⊨ χ) (replElt , spec)
    where
```

選ばれた実現要素の基礎集合は `carve (RL.liftFo χ hχ)` です。定数の境界 `hχ` により、各定数を段階へ付け替えることが正当化されます。`carve∈𝒟ₒ` は、得られた `defSet` が`Lset σ` の定義可能冪集合に属することを証明します。この所属に `𝒟ₒ→isL σ oσ` を適用すると、モデル要素の第二成分が得られます。したがって定義可能性が構成可能な実現要素の存在を与え、その正確な外延は別に `spec` が証明します。

```agda
    replElt : S
    replElt = carve (RL.liftFo χ hχ)
            , 𝒟ₒ→isL σ oσ (carve (RL.liftFo χ hχ)) (carve∈𝒟ₒ (RL.liftFo χ hχ))
```

仕様は各モデル要素 `z` について、`z` が `replElt` に属することと、`z` が `χ` を満たすこととの間のパスを与えます。順向きの含意は `z ∈ˢ replElt` から始まります。`replElt` の基礎集合は切り出された集合なので、`carve⊆` が `fst z` を `Lset σ` に入れ、標準的な表示がその集合を指す添字 `m` を与えます。切り出された集合への所属を表示された代表へ輸送すると、`imageOut` がそこでの充足を与え、`⊨-transport` が基礎集合の等式に沿ってそれを `z` へ戻します。この向きでは所属自体から必要な段階の境界が得られるため、被覆仮定は使いません。

```agda
    spec : (z : S) → (z ∈ˢ replElt) ≡ ((z ∷ []) ⊨ χ)
    spec z = ⇔toPath fwd bwd
      where
      fwd : ⟨ z ∈ˢ replElt ⟩ → ⟨ ((z ∷ []) ⊨ χ) ⟩
      fwd z∈ = ⊨-transport χ dχ (⟪ Lset σ ⟫↪ m , xL) z q (imageOut χ hχ dχ m xL m∈)
```

これらの局所データは、標準的な表示へ移る過程を明示します。まず `fz∈Lσ` は、切り出された集合が段階に含まれることから従います。この所属に `∈-asFiber` を適用すると、添字 `m : ⟪ Lset σ ⟫` とパス `q : ⟪ Lset σ ⟫↪ m ≡ fst z` が得られます。両者は一つの所属ファイバーの二つの射影なので、選択原理は使われません。パス `q`は互いに逆の向きに使われます。まず切り出された集合への所属を表示された集合へ移し、次に組にした代表での充足を `z` へ戻します。

```agda
        where
        fz∈Lσ = carve⊆ (RL.liftFo χ hχ) (fst z) z∈
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst
        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd
```

仕様の順方向は、二つの段階で締めくくられます。層の中で表されたメンバーが、モデルの元として梱包され、その構成可能性は段階そのものから来ます。そして、その表されたメンバーに対して証明された、刻まれた集合への所属が、名指しの等式に沿って、もとの元へ運ばれます。これで順方向は完成です。刻まれた集合の元は、モデルの中で、自分自身のもとで論理式を満たすのです。

```agda
        xL = memberIsL m
        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) (sym q) z∈
```

逆方向は、覆いの仮定から始まります。ここで覆いの仮定を使います。論理式を満たす各要素はこの段階に属すと仮定されているので、与えられた充足の証明を適用すると。すると、段階への所属の繊維が、標準的な代表の添字を取り戻します。

```agda
      bwd : ⟨ ((z ∷ []) ⊨ χ) ⟩ → ⟨ z ∈ˢ replElt ⟩
      bwd qz = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) q m∈
        where
        fz∈Lσ = cover z qz
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst
```

代表は一つの等式によって名指され、充足はその代表のところへ移されます。充足が底の集合のみに依存するのですから、底の集合のあいだの等式で十分です。代表は、それ自身の構成可能性を添えて、モデルの元として梱包され、論理式は、もとの元の代わりに、代表について成り立ちます。

```agda
        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd
        xL = memberIsL m
        satz : ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ χ ⟩
        satz = ⊨-transport χ dχ z (⟪ Lset σ ⟫↪ m , xL) (sym q) qz
```

ここで定義可能性の順方向を使います。代表は論理式を満たすので、代表は刻まれた集合に属します。そして名指しの等式が、この所属をもとの元へ運び戻します。両方向がそろい、仕様は、すべての元において、二つの命題の相等となります。刻まれた実現への所属と、モデルの中で論理式を満たすこととの相等です。

```agda
        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = imageIn χ hχ dχ m xL satz
```

段階での分出は、先の構成を部分集合に特化したものです。仮定は、始集合がすでに段階の中にあるということ。その論理式は、「始集合への所属」と与えられた論理式との連言であり、所属の原子が有界であり、連言が有界性を保つので、有界な論理式です。定数も有界です。始集合が段階の下に供給され、論理式の定数には証明書が付いていたからです。こうして固定段階の定理は、モデルの欄の分出が求める、ちょうどあの可縮な実現を返します。

```agda
  separateAt : (a : S) (fa∈σ : ⟨ fst a ∈ Lset σ ⟩)
               (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
  separateAt a fa∈σ φ h dφ =
    carveAt ((var zero ∈̇ con a) ∧̇ φ) ((tt* , fa∈σ) , h) (δ-∧ δ-∈ dφ)
```

固定段階の定理の覆いの仮定は、最初の連言だけによって解除されます。連言を満たす元は「始集合への所属」を満たし、始集合は段階の中にあり、段階は推移的です。ゆえにその元も段階の中にあります。分出の述語における所属の連言が飾りではない数学的理由は、これです。切り出そうとしている層の内側へ、すべての候補を運び込むのが、この連言なのです。

```agda
      (λ z q → layer-trans (Lset-layer σ) {x = fst a} {y = fst z} (q .fst) fa∈σ)
```

## 論理式を収める段階を求める

独立に選ばれた上界を比較するため、層の条件を順序数の添字でパラメータ化します。その数学的内容は先ほどと同じで、元の底の集合が添字の指す層に属するということです。こうして、先に選んだ一つの層を変数として扱い、後の探索で層について量化できるようになります。

```agda
Below′ : V ℓ → S → Type (ℓ-suc ℓ)
Below′ σ c = ⟨ fst c ∈ Lset σ ⟩
```

最初の持ち上げの補題は、項の有界性を指標に沿って運びます。ある段階の指標が別の指標に先行すれば、第一の層の下にある定数はすべて、第二の層の下にもあります。塔の狭い増大によるものです。そして項の有界性の証明書は、各定数ごとにこの点ごとの単調性を施すことで、より大きな指標へ運ばれます。項そのものは変わらず、有界性の証明だけが輸送されます。

```agda
liftTmTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (t : Term S n)
         → BoundedTm (Below′ σ) t → BoundedTm (Below′ β) t
liftTmTo {σ} {β} σ∈β t h =
  BoundedTm-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') t h
```

第二の持ち上げの補題は、論理式について同じことをします。すべての定数がある段階の指標の下にある論理式は、それより後のどんな指標の下でも、その性質を保ちます。証明は、論理式のすべての定数の位置で、項の補題を施すものです。この二つの持ち上げの補題があれば、ある段階で得た有界性の証明を、残りのデータのために選んだ任意の後の段階へ輸送できます。

```agda
liftFoTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (φ : Formula S n)
         → BoundedFo (Below′ σ) φ → BoundedFo (Below′ β) φ
liftFoTo {σ} {β} σ∈β φ h =
  BoundedFo-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') φ h
```

定数の上界の探索は項から始まり、二つの場合は明確に異なります。定数には、それ自身が初めて属する層を上界として、その添字の順序数性と定数の所属証明を添えます。変数は定数を含まないため、空の層と自明な証明を返します。ここには上界を求めるべき定数がなく、変数の値が空集合に属すとは主張しません。

```agda
mkBoundedTm : ∀ {n} (t : Term S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedTm (Below′ σ) t)
mkBoundedTm (con c) = stage (fst c) (c .snd)
                    , (stage-ord (fst c) (c .snd) , stage-mem (fst c) (c .snd))
mkBoundedTm (var i) = ∅ , (∅-ord , _)
```

二つの探索結果をまとめる操作は、一度だけ、一般的に述べられます。指標に沿って持ち上げられるどんな二種類の証明書にも対応します。入力は、結果の対です。おのおの、順序数の指標とその順序数性と、証明書。出力は、共通の指標における一つの結果で、二つの証明書がともにそこへ運ばれます。持ち上げの二つの操作がパラメータなので、同じ構成を、二つの項、二つの論理式、または項と論理式に適用できます。

```agda
private
  mkBounded : ∀ {ℓc ℓd} {C : V ℓ → Type ℓc} {D : V ℓ → Type ℓd}
            → (liftC : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → C σ → C β)
            → (liftD : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → D σ → D β)
            → (r₁ : Σ[ σ ∈ V ℓ ] (IsOrd σ × C σ))
```

共通上界の構成は三段階からなります。二つの指標の限界を取ります。それは両方の上にある順序数です。第一の指標がその限界に先行し、第二もそうであることを記録します。そして、この二つの包含関係に沿って、持ち上げの操作を施し、二つの証明書がともに共通の指標を述べるようにします。証明書について使われるのは、持ち上げられるという形だけであり、それ以外の性質は何も使いません。

```agda
            → (r₂ : Σ[ σ ∈ V ℓ ] (IsOrd σ × D σ))
            → Σ[ σ ∈ V ℓ ] (IsOrd σ × (C σ × D σ))
  mkBounded liftC liftD r₁ r₂ = b .fst , (b .snd .fst ,
      ( liftC (b .snd .snd .fst) (r₁ .snd .snd)
      , liftD (b .snd .snd .snd) (r₂ .snd .snd) ))
```

限界そのものは、順序数の章による、二つの順序数の合併です。どちらの順序数もそれに先行するような順序数です。これが、この再帰に必要な唯一の順序数論的事実であり、構成的なものです。古典的なパラメータが入り込むのはここではなく、もっと早く、各定数の最も早い段階が名指されたところなのです。

```agda
    where
    b  = bound2 (r₁ .fst) (r₂ .fst) (r₁ .snd .fst) (r₂ .snd .fst)
```

論理式の上の探索は、構文を再帰します。二つの原子的な形は、それぞれの二つの項の限界をまとめます。命題の結合子は、その二つの部分論理式の限界をまとめます。いずれの場合も、仕事をするのは、先ほどのまとめ役であり、有界性の証明は共通の添字へ輸送されます。

```agda
mkBoundedFo : ∀ {n} (φ : Formula S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ)
mkBoundedFo (t ∈̇ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (t ≐ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (φ ∧̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo (φ ∨̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
```

残りの場合は、その非対称が教訓的です。偽の論理式は定数を含まないので、空の段階が上界になります。非有界量化子の定数の上界は、本体の上界と同じです。量化子そのものは定数をひとつも導入しないので、再帰は、その下を何も触れずに通過します。有界量化子は、さらにその限定項を含みます。その範囲を定める項が一つの定数を名指すので、項の限界と本体の限界とをまとめるのです。

```agda
mkBoundedFo (φ ⇒̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo ⊥̇        = ∅ , (∅-ord , _)
mkBoundedFo (∃̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)
```

有界存在は、有界全称量化子と同じふるまいをします。範囲を定める項の限界と、本体の限界とがまとめられます。この探索全体の性質のうち、二つの独立した概念を分けるものを強調しておきます。この再帰が調べるのは定数だけです。だから、非有界な量化子を含む論理式に対しても、うまく行きます。したがって、ここで産み出される証明書は、論理式が有界かどうかについて何も語りません。定数がある段階の下にあることと、量化子が有界であることは、終始、別々の概念なのです。

```agda
mkBoundedFo (∃̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)
```

## Δ₀ 分出公理

有界な分出が、いま、完全な形で述べられます。始集合と、量化子がすべて有界であるような一変数論理式に対して、「始集合の要素であり論理式を満たす」という述語は、モデルの元による可縮な実現をもちます。段階を定めた後、固定段階での分出定理を一度適用します。

```agda
separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ
           → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
separateΔ₀ a φ dφ = AtStage.separateAt σ oσ a fa∈σ φ h dφ
  where
  rφ = mkBoundedFo φ
```

この層は二つの上界から定まります。先に構成した探索が論理式の定数を抑える上界を与え、既に得られている層の割り当てが始集合を含む最初の層を与えます。二つの添字を併合し、論理式の証明書をその層まで持ち上げます。これにより、論理式の定数と始集合は同じ上界の下に置かれます。

```agda
  sa = stage (fst a) (a .snd)
  bb = bound2 (rφ .fst) sa (rφ .snd .fst) (stage-ord (fst a) (a .snd))
  σ  = bb .fst
  oσ = bb .snd .fst
  h  = liftFoTo {σ = rφ .fst} {β = σ} (bb .snd .snd .fst) φ (rφ .snd .snd)
```

始集合自身の位置は別に扱います。始集合はそれが初めて現れる層に属し、併合から得られる包含関係によって、この所属を共通の層まで持ち上げます。これが固定層の定理に必要な被覆の仮定であり、塔の単調性と層の割り当てに伴う証明書から直接得られます。

```agda
  fa∈σ : ⟨ fst a ∈ Lset σ ⟩
  fa∈σ = Lset-mono {α = σ} {β = sa} (bb .snd .snd .snd) (stage-mem (fst a) (a .snd))
```

## Δ₀ 置換公理

有界な置換は、その関数性の仮定とともに述べられます。始集合と、量化子がすべて有界な二変数論理式を取り、各要素に対応する値の繊維が可縮であると仮定します。このとき、像の述語はモデルの元による可縮な実現をもちます。証明は述語の相等に沿って実現可能性を輸送します。関数性によって関連する値に共通の上界を与え、その上界を得た後は通常の分出によって像を集めます。

```agda
replaceΔ₀ : (a : S) (φ : Formula S 2) → Δ₀ φ
          → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (x ∷ y ∷ []) ⊨ φ ⟩))
          → isContr (SetOf (ReplImage a φ))
replaceΔ₀ a φ dφ fc =
  subst (λ Q → isContr (SetOf Q)) (sym Q≡)
```

関数像の上界に関する定理を、関係の第一の位置を始域とする順序で適用すると、共通の像の段階、その順序数性、覆いの事実が得られます。そして、その段階をモデルの元として梱包したところで、一変数の像の論理式に対して、完全な有界分出が施されます。この論理式の有界性の証拠は、有界存在の場合のものです。加わった量化子は一つだけで、それが源によって有界にされているからです。

```agda
    (separateΔ₀ (LsetS βimg βimg-ord) imageFo (δ-∃∈ dφ))
  where
  module I = FunctionalImage a (λ x y → (x ∷ y ∷ []) ⊨ φ) fc
  open I using ( βimg; βimg-ord; range∈βimg )
```

一変数の像の論理式の意味は次のとおりです。それは、対象言語でこう言います。始集合のどこかのメンバーが、外側の候補と関係づけられる、と。そして有界存在が、そのメンバーを環境の最初の枠へ押し込みます。ここでの有界存在は、対象言語自身の量化子です。一方、像の述語の外側の存在は、ホストレベルの切り詰められた存在です。二者は意味においては意味論を通して一致しますが、同じ統語的な対象ではありません。両者を区別することで、次の等式を正確に述べられます。

```agda
  imageFo : Formula S 1
  imageFo = ∃̇∈ (con a) φ
```

守衛つきの述語は、構成が検証できるものを集めます。候補が、梱包された共通の像の段階の中にあり、一変数の像の論理式を満たす、ということ。段階への所属を表す連言は分出の上界を与え、もう一方の連言は実際の像を記述します。したがって、後で覆いの定理を用いて段階の条件を取り除けます。

```agda
  BoundedImage : S → hProp (ℓ-suc ℓ)
  BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)
```

二つの述語の相等は点ごとに成り立ち、その二方向は手間が違います。順方向。切り詰められた源の証人から、守衛つきの述語へ。消去が正当なのは、守衛つきの述語が命題だからです。覆いの事実が段階への所属を供給し、同じ始域の要素と充足の証明を、論理式が要求する位置の順序で切り詰めの中へ戻します。逆方向には、何も要りません。候補における像の論理式の充足は、その意味論により、ちょうどその候補における像の述語だからです。段階の連言は捨てられ、第二の連言がそのまま主張となります。始域が第一の位置を占めるため。変数の入れ替えは、どこにも要らないのです。

```agda
  Q≡ : ReplImage a φ ≡ BoundedImage
  Q≡ = funExt (λ y → ⇔toPath (into y) (λ p → p .snd))
    where
    into : (y : S) → ⟨ ReplImage a φ y ⟩ → ⟨ BoundedImage y ⟩
    into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) →
```

`ReplImage a φ` に属する候補 `y` について、始域の要素 `x`、所属の証明 `x∈a`、充足の証明 `h` は、命題的切り詰めのもとでのみ与えられます。`BoundedImage y` は命題なので、`PT.rec` は、その二つの連言を構成する間にこれらのデータを使えます。第一の成分は `range∈βimg` から得られます。関数性により、`a` の要素と関係するすべての値は `Lset βimg` に属します。第二の成分では、同じ `x`、`x∈a`、`h` を命題的切り詰めの中へ戻します。`imageFo = ∃̇∈ (con a) φ` の意味論により、これはちょうど `y` が `imageFo` を満たすことの証明です。したがって、始域の要素が切り詰められていないデータとして返されることはありません。

これで `ReplImage a φ y` から `BoundedImage y` への含意が完成します。段階への所属の成分を捨てる逆向きの含意と合わせて `Q≡` が得られ、`sym Q≡` に沿う輸送によって `replaceΔ₀` が証明されます。正確には、仮定 `lem : LEM (ℓ-suc ℓ)`、`φ` の Δ₀ 証人、および各 `x ∈ˢ a` における値のファイバーの可縮性のもとで、結論は `isContr (SetOf (ReplImage a φ))` です。これはここで述べた Δ₀ 置換定理です。この枝は新たな古典的原理を導入しませんが、`range∈βimg` が用いる共通の段階の構成は `lem` に依存します。

```agda
      range∈βimg x x∈a y h , ∣ x , (x∈a , h) ∣₁ }
```

## まとめ

有界な分出と有界な置換は、同じ方針に従います。まず始集合と論理式の定数を一つの順序数層の下に置き、置換ではさらに関係するすべての値も同じ層の下に収めます。次に定義可能性によってその層の内部で必要な部分集合を作り、変名と Δ₀ 絶対性によって、その所属関係を構成可能モデルにおける充足と同一視します。こうして、唯一のホスト側の仮定 `lem : LEM (ℓ-suc ℓ)` のもとで `separateΔ₀` と `replaceΔ₀` が得られます。