---
title: "構成可能モデル上の論理式の符号化"
module: L.Coding.Model
lang: ja
site: "Bedrock"
description: "構成可能モデル上の論理式の符号化"
stage: "内部の符号化：式と定義域"
reading_order: 42
canonical: https://bedrock.institute/ja/L.Coding.Model.html
html: L.Coding.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Model.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, FOL.Coding, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Absoluteness, L.Coding.PairFormulas, L.Axioms.Numerals]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Model.md, https://bedrock.institute/zh/L.Coding.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 構成可能モデル上の論理式の符号化

構成可能モデル `L` の要素は裸の集合ではありません。それは階層 `V ℓ` の集合に、「その集合が構成可能である」という証明を添えたものです。したがって `L` の中で一階の論理式を評価するとき、量化子はこのような対を渡ります。一方、本当に欲しい集合の符号化の事実、たとえばある Kuratowski 対があるグラフに属することは、底にある集合についての事実です。本章はこの二つの読みの間に橋を架けます。

橋には二つの方向があります。模型要素を外へ射影するときは構成可能性の証明を直接忘れられますが、有界な読み式の移送には `L` の推移性が保証する絶対性を使います。内向きには模型内部の証人が必要です。対が構成可能なグラフに属するという証明から、推移性がその対の構成可能性の証明を与え、`L` の要素にします。

対の読み式の上に、本章は「関数をグラフとして」という語彙を積み上げます。ここで、これらの条項が論理的に独立していることを見ておく価値があります。グラフの適用は、与えられた順序対がグラフに属すると主張するだけです。一価性は、一つの引数が多くとも一つの値を決めると言うだけで、どの引数が値を持つかには何も言いません。ちょうどの定義域と値域の制限は、それぞれさらなる側面を制約します。しかもこれら三つの条件はどれも、対の形をした要素についてしか語らないため、対でない余計な要素を候補のグラフが持つのを禁じません。第四の条項、すべての要素が添字と値の対であること、がその余計なものを排除します。合わせたものが `envOverAt` です。これは定義域 `d` と値域 `B` に対する、一つの候補グラフについての述語であり、ある集合がいつ `d` の上、`B` への環境であるかを言うものであって、環境の全体の集合を構成するものではありません。

後半は符号化に向かいます。順序対と数項は `L` の内部で作ることができ、それぞれ周囲の対応物へ射影されます。すべての符号はタグとペイロードの対なので、内部の符号はどれも、定数を射影した論理式の周囲の符号へ射影されます。この相容性こそ、階層側の読み式が、模型の内部で作られた符号を分析できる理由です。最後に二つの観察を添えます。環境の記述全体が割り当てに依存するのは三つの射影された集合を通してだけであり、同じグラフ、定義域、値域を提示するどんな割り当てにもそのまま移ります。また、ある符号が対であると分かれば、`L` の推移性がその二つの成分を一つの構成可能集合にまとめます。

二つの世界は同じ宇宙レベル `ℓ` の上にあります。内側の言語の割り当ては、台 `S` の要素からなるベクトルであり、各要素は周囲の集合に構成可能性の証明書を添えたものです。これに対して周囲の事実は、`fst` で各項目を射影して得られる底の集合について述べられます。本章の妥当性の主張はどれも、このような対の形の割り当てでの充足の判断と、射影された割り当てについての事実とを同一視する形を取ります。集合論の議論を始める前に、射影を一度、正しく処理しておかねばなりません。

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

open import Base.Prelude

module L.Coding.Model {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

妥当性の主張は真理値を比較するので、周囲の事実は命題としてまとめられます。特に階層の二集合の等しさは、階層が h-集合であるため命題です。パスと合同性がこの等しさを射影された参照とそろえ、絶対性、対、数項に関する集合論的内容はそれぞれの補題から入ります。

```agda
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∀̇_; ∀̇∈; ∃̇_; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
```

`L` の推移性は二つの関連した仕方で使われます。有界な読み式を移す Δ₀ 絶対性の基礎となり、また構成可能集合の要素から模型内の証人を作ります。直接の射影に新しい証人は要りませんが、論理式を外向きに読む移送定理はこの推移性に依存します。

```agda
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import V.Model {ℓ} using ( pair-singleton )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
```

有界論理式の外向きの方向は絶対性が担います。階層についての Δ₀ 論理式で、定数が構成可能な集合を名指すものは、`L` の中で読んでも意味が変わらず、二つの読みは一つの経路として一致します。対の読み式はまさにこの種の式なので、模型の中での充足は射影された集合の間の等式と同一視されます。内向きの方向に一般的な近道はなく、項目ごとに証明を明示的に構成するしかありません。本章が必要とするのは対の場合です。

```agda
open import L.Absoluteness {ℓ} using ( liftFo; transferFo )
open import L.Coding.PairFormulas {ℓ}
  using ( prAt; Δ₀-prAt; prAt-adequate; ∈pair-introL; ∈pair-introR )
open import L.Axioms.Numerals {ℓ}
  using ( numeralL; numeralL-fst; pairʟ; pairʟ-fst )
```

本章の存在主張の一部は、意図的に弱く作られています。グラフに項目が存在すると言うとき、主張するのはある項目が単に存在することであって、どれかを選び出すことではありません。このような主張は命題的截断の中に住み、命題値の対象へしか消去できません。截断された存在と明示的な証人を区別しておくことは、すべての妥当性の証明の両方向で重要です。存在の公式の充足は常に截断された形を持つからです。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( map )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
import Cubical.HITs.PropositionalTruncation as PT
```

真理値はレベル `ℓ-suc ℓ` の命題です。論理式はブール値ではなく `hProp` に評価され、それは底にある型と「それが命題である」ことの証明を包んだものです。これにより内側の構造の台 `S` も固定されます。その要素は、周囲の集合と構成可能性の証明書の対にほかなりません。以後、`γ ⊨ φ` は構成可能モデルにおける充足を意味し、`⟦ t ⟧ γ` は `S` の要素、すなわち証明書を伴う集合です。

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆ )

open hPropStructure 𝒮ʟ using ( S )
```

もう一つ、主張の形を定める構造的な事実があります。本章の読み式はどれも、検表の `fst` を通してのみ述べられ、それ以外の何ものも通りません。つまり、模型の中での充足は常に底の集合についての事実と比較され、証明書の内部の何かと比較されることはありません。同じ原則が最後の輸送の補題を可能にします。記述が参照する場所で同じ三つの底の集合を提示する割り当てどうしを、記述は区別できないのです。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ )
```

## 射影した環境での参照

本章の妥当性の主張はどれも、模型の要素からなる割り当てでの充足の判断を、**射影された**割り当てについての周囲の事実と比較します。射影された割り当てでは、各項目から `fst` によって構成可能性の証明書が剥ぎ取られています。二つの割り当ては同じ対象ではないので、比較を行う前に、射影された割り当てで変数を参照した結果が、元の割り当てで参照したものを射影したものに等しいことを知っておかねばなりません。以下の補題の内容はまさにそれだけです。この後、周囲の等式を `γ` 自身の項目で言い換えねばならないところでは、必ずこれが登場します。

証明は位置 `i` に対する再帰です。位置 `zero` では両辺ともリストの先頭に簡約されます。`lookup zero (x ∷ γ)` は `x` であり、cons の `map fst` は射影の cons であり、`x` の二度の第一射影は定義的に等しいので `refl` が得られます。後続の位置では、二つの参照がともに一項目進み、再帰呼び出しが議論を完成させます。ここで構成可能性はまったく使われず、この補題は対からなる任意の環境に対して成り立ちます。

```agda
lookup-fst : ∀ {n} (i : Fin n) (γ : S ^ n)
           → lookup i (map fst γ) ≡ fst (lookup i γ)
lookup-fst zero    (x ∷ γ) = refl
lookup-fst (suc i) (x ∷ γ) = lookup-fst i γ
```

## 順序対

本章が築く橋には二つの方向があります。順方向には、模型の中での充足の判断、つまり各項目が模型の要素である割り当てのもとで評価された判断を、階層の集合についての事実へ変えなければなりません。各項目はまず `fst` で射影されるので、周囲の主張は常に射影された値について述べられます。辞書の最初の項目は順序対の認識です。周囲の読解式 `prAt q u v` は、位置 `q` の値が位置 `u` と `v` の値の Kuratowski 対であると言います。この読解式は有界 (Δ₀) なので意味は絶対的であり、`L` の言語で読んでも何の代償もありません。また定数をまったく名指さないので、持ち上げは定数にいかなる条件も課しません。定理はその帰結を正確に述べます。持ち上げられた読解式の模型の中での充足は、「位置 `q` の射影された値が `u` と `v` の射影された値の `pr` に等しい」という等式へのパスです。逆方向、すなわち裸の周囲の所属を模型の内部に住む証人へ戻す方向は、次の節で初めて現れ、そこでは `L` の推移性が働きます。

この主張は真理値を比較するので、右辺も真理値でなければなりません。階層の二つの集合の等式は、階層が h-集合であるため命題であり、`PairIs` はそのようなパスの型にちょうどその命題性の証明を包んで記録します。持ち上げられた読解式 `prAtL q u v` は、各定数を台 `S` へ改名した `prAt q u v` そのものです。ここには改名すべき定数がありませんが、有界性の証明書 `Δ₀-prAt` は依然として公式に伴われます。転送の補題がそれを要求するからです。

```agda
private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

prAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
prAtL q u v = liftFo (prAt q u v) _
```

妥当性の主張は、一本のパスによって、読解式の模型の中での充足と右辺のパッケージ化された等式を等しくします。射影がどこに立っているか注意してください。割り当て `γ` は `S` の要素からなり、等式は参照された項目の `fst` について述べられています。この辞書のどの項目もこの形を取ります。具体的な所属の事実が模型の台の内側ではなく階層に住んでいるからです。

```agda
prAtL-adequate : ∀ {n} (q u v : Fin n) (γ : S ^ n)
  → (γ ⊨ prAtL q u v)
  ≡ PairIs (fst (lookup q γ)) (pr (fst (lookup u γ)) (fst (lookup v γ)))
prAtL-adequate q u v γ =
    transferFo (prAt q u v) _ (Δ₀-prAt q u v) γ
```

証明は三つのパスを連結するだけで、新しいものは何も導入しません。まず転送の補題が有界性の証明書を使って、`L` の中での充足を、射影された割り当てでの `prAt q u v` の周囲の充足と等しいとします。次に読解式自身の妥当性定理が、その周囲の充足を解釈された値の間の等式へ書き換えます。最後に、射影された割り当てでの二度の参照を `γ` での参照の射影へ移し、合同によって等式を `PairIs` の下で組み立て直します。得られるのは約束された同一視そのものです。

```agda
  ∙ prAt-adequate q u v (map fst γ)
  ∙ cong₂ PairIs (lookup-fst q γ)
      (cong₂ pr (lookup-fst u γ) (lookup-fst v γ))
```

## グラフの適用

対象言語におけるグラフは順序対の集合であり、後の使用が問うのは常に、与えられた対がそれに属するかどうかです。以下の読解式はこれを有界な存在量化として表します。ある項が指す集合の要素の範囲で一つの要素が存在し、その本体が対の読解式であるというものです。その意味は、Kuratowski 対がグラフの底にある集合に属するという周囲の所属です。

順方向は充足を所属へ変えます。逆方向こそ模型が実際に働く場所です。存在量化を充足するには、底にある集合がその対であるような**模型の要素**を与えねばならず、仮定が供するのは集合にすぎません。この対が構成可能なのは、構成可能な集合に属し、構成可能なクラスが推移的だからです。この一段階が議論のすべてであり、証人が階層の中だけでなく模型の内部に作られねばならない場面では、同じ段階が繰り返されます。

定義は次のように読みます。項 `F` の値で限られた範囲の中に、グラフの要素が単にひとつ存在し、対の読解式を満たす、と。存在量化の束縛された項目が環境を伸ばし、対の読解式の三つの位置はその項目と、二つの引数のずらされた参照を指します。`F` 自身は、量化子が施したずらしの下で拡張環境の中で評価されます。

```agda
private
  appTerm : ∀ {n} → Term S n → Fin n → Fin n → Formula S n
  appTerm F x y = ∃̇∈ F (prAtL zero (suc x) (suc y))

  appTerm-adequate : ∀ {n} (F : Term S n) (x y : Fin n) (γ : S ^ n)
    → (γ ⊨ appTerm F x y)
```

妥当性の主張は材料に名前を付けます。`a` と `b` は二つの引数スロットの射影された値であり、`G` は項の解釈です。それは `S` の要素、つまり構成可能性の証明書を担う集合であり、その底にある集合がグラフです。主張されるのは、充足と周囲の所属、すなわち対 `pr a b` がグラフの底にある集合に属することとの間の、真理値のパスです。

```agda
    ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (⟦ F ⟧ γ))
  appTerm-adequate F x y γ = ⇔toPath fwd bwd
    where
    a = fst (lookup x γ)
    b = fst (lookup y γ)
```

補助の `read` は存在量化の一つのファイバーをほどきます。模型の要素 `z` と、拡張された割り当てが対の読解式を充足することの証明が与えられれば、前節の妥当性定理がその証明を、「`z` の底にある集合は `pr a b` に等しい」という命題へ輸送します。有界な存在量化の充足を展開すると、順方向は所属 `z∈G` とそのような読解式の証明の切り詰められた対を受け取ります。目標の所属が命題であるため截断の消去は正当であり、分岐の中では所属が `read` の供給するパスに沿って輸送されます。

```agda
    G = ⟦ F ⟧ γ

    read : (z : S) → ⟨ (z ∷ γ) ⊨ prAtL zero (suc x) (suc y) ⟩ → fst z ≡ pr a b
    read z h = subst ⟨_⟩ (prAtL-adequate zero (suc x) (suc y) (z ∷ γ)) h

    fwd : ⟨ γ ⊨ appTerm F x y ⟩ → ⟨ pr a b ∈ fst G ⟩
    fwd = PT.rec (snd (pr a b ∈ fst G))
```

逆方向こそ、構成可能モデルが登場する場面です。裸の所属の証明 `⟨ pr a b ∈ fst G ⟩` から、切り詰められた存在量化の住人を与えなければなりませんが、その第一成分は集合 `pr a b` そのものではいけません。それは階層の集合であって `S` の要素ではないからです。証人は次の行で作られます。ここに示された分岐は、所属と読解式の証明を一つに包みます。後者の証明は `refl` を妥当性のパスを逆向きに輸送して得られるもので、証人の底にある集合が定義的に `pr a b` であるため、これで構いません。

```agda
      (λ { (z , (z∈G , h)) → subst (λ w → ⟨ w ∈ fst G ⟩) (read z h) z∈G })

    bwd : ⟨ pr a b ∈ fst G ⟩ → ⟨ γ ⊨ appTerm F x y ⟩
    bwd h = ∣ zS , (h , subst ⟨_⟩
        (sym (prAtL-adequate zero (suc x) (suc y) (zS ∷ γ))) refl) ∣₁
      where
```

証人は、この節で唯一、真に模型に固有の構成です。`pr a b` を `S` の要素として提示するには、その構成可能性の証明書が必要です。仮定はこの対が `G` の底にある集合に属すると述べ、`G` は自身の証明書を担っています。構成可能なクラスの推移性がこの二つの事実を `isL (pr a b)` へ変えます。構成可能な集合の要素は構成可能なのです。証人が揃ったところで、公開形式 `appAt` はグラフを変数のスロットに固定し、項 `var f` を読みます。その妥当性は、特定の項における一般定理の実例、すなわち射影された対がスロット `f` の値の底にある集合に属することにほかなりません。

```agda
      zS : S
      zS = pr a b , isL-trans {x = fst G} {y = pr a b} h (G .snd)

appAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
appAt f = appTerm (var f)

appAt-adequate : ∀ {n} (f x y : Fin n) (γ : S ^ n)
```

この特殊化により、後のグラフ述語は割り当てのスロットを通してグラフを参照できます。射影後の各出現は一様に `pr (fst x) (fst y) ∈ fst (lookup f γ)` となるので、一価性と定義域の議論では同じ所属の形を一貫して使えます。

```agda
  → (γ ⊨ appAt f x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (lookup f γ))
appAt-adequate f = appTerm-adequate (var f)
```

読む対象となるグラフは、変数のスロットにある必要はなく、模型の固定された要素として直接名指されても構いません。定数の項 `con F` はまさにそれであり、妥当性の主張はそれに応じて簡単になります。定数は要素 `F` そのものとして解釈されるので、右辺は `fst F` への所属となり、グラフのための環境の項目にはまったく触れません。

定義は共通の読解式を `con F` で実例化します。定数はそれ自身として解釈されるため、有界な存在量化は `fst F` の要素を直接渡ります。妥当性の主張はまさにそれを記録します。充足は、二つの引数の値の射影された対が `fst F` に属することへのパスです。右辺の所属は射影後の周囲の所属であり、左辺の存在量化子は依然として模型の要素の上を渡ります。

```agda
appC : ∀ {n} → S → Fin n → Fin n → Formula S n
appC F = appTerm (con F)

appC-adequate : ∀ {n} (F : S) (x y : Fin n) (γ : S ^ n)
  → (γ ⊨ appC F x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F)
```

証明は定数の項における共通の妥当性定理であり、自前の議論を何も必要としません。`appAt` と合わせて、辞書はこれで、スロットによって与えられたグラフの中の対の所属と、固定された要素として与えられたグラフの中の対の所属の両方を認識し、それぞれの意味が正確に周囲の所属となっています。

```agda
appC-adequate F = appTerm-adequate (con F)
```

## 一価性

グラフが一価であるとは、その中の第一成分の等しい任意の二つの対が、第二成分も等しいということです。これは対の所属についてだけの主張であり、グラフが要素を持つことも、与えられた引数が現れることも言わないので、後で現れる定義域の条件とは論理的に独立です。

この主張は一本のパスではなく二つの方向として述べられます。実際に使われる形、すなわち対象言語の主張から、同じ引数に対して記録された二つの値の底にある集合の等式へと外向きに読み出す形です。

外側から読みます。すべての `x`、`y`、`y'` に対し、`x` と `y` の対がグラフに属し、かつ `x` と `y'` の対も属するなら、値 `y` と `y'` は等しい、ということです。要求される等式は、二つの値の底にある集合の間の等式です。`y` と `y'` はそれ自体模型の要素だからです。ここにはグラフが空でないことも、すべての引数が値を持つことも述べられていません。それは独立した定義域の条件です。

```agda
svAt : ∀ {n} → Fin n → Formula S n
svAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
  ⇒̇ (appAt (suc (suc (suc f))) (suc (suc zero)) zero
  ⇒̇ (var (suc zero) ≐ var zero)))))
```

二つの方向は、固定されたグラフのスロット `f` と固定された環境 `γ` に対して述べられるので、局所的な述語が外部の意味を一度記録します。`Holds x y` は、`x` と `y` の射影された対がグラフの底にある集合に属することを言い、これは `appAt-adequate` を一度適用して得られる形そのものです。続く二つの妥当性の実例は、どちらの含意を読んでいるのかを固定します。`at` は値 `y` を持つ対のためのもので、`at'` は `y'` を持つ対のためのものです。

```agda
module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds : S → S → Type (ℓ-suc ℓ)
    Holds x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at : (x y y' : S)
```

各補助命題は、三つの量化された要素で拡張した環境での妥当性の実例であり、公式の添字はそれに応じてずれます。`at` と `at'` は命題の間のパスなので、証明はどちらの側からでも輸送で移せます。以下の二つの方向の補題がするのはまさにそれで、向きが逆なだけです。

```agda
       → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero))
       ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero)
                  (y' ∷ y ∷ x ∷ γ)

    at' : (x y y' : S)
```

対象言語の主張を外へ読み出すと、使える結論が得られます。`svAt f` の充足が与えられれば、量化子は模型の任意の要素 `x`、`y`、`y'` に対してその含意を供給します。二つの所属 `Holds x y` と `Holds x y'` を、それぞれ外部の形から量化子が期待する充足の形へ輸送して渡せば、二つの底にある値の等式 `fst y ≡ fst y'` が得られます。結論が射影後の集合の等式であり、模型の要素としての `y` と `y'` の等式は主張されていないことに注意してください。

```agda
        → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) zero)
        ≡ (pr (fst x) (fst y') ∈ fst (lookup f γ))
    at' x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) zero
                   (y' ∷ y ∷ x ∷ γ)

  svAt-out : ⟨ γ ⊨ svAt f ⟩
```

逆向きは充足を取り出すのではなく組み立てます。二つの所属が一致する任意の三つの要素を、それらの値の等しさへ送る関数は、三つの量化子と二つの含意が要求するものにちょうど等しく、必要な所属の証明はそれぞれ、外部のものを `at` か `at'` に沿って順方向へ輸送して作られます。二つの補題を合わせると、`svAt f` の充足と外部の一価性の条件は互いに従いますが、述べ方はそれらを二つの関数として保ち、一本のパスへはまとめていません。

```agda
           → (x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y'
  svAt-out h x y y' p q = h x y y'
    (subst ⟨_⟩ (sym (at x y y')) p) (subst ⟨_⟩ (sym (at' x y y')) q)

  svAt-in : ((x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y')
          → ⟨ γ ⊨ svAt f ⟩
```

導入の方向 `svAt-in` は除去の鏡像で、輸送の向きが逆です。外部の所属をそれぞれ妥当性の経路に沿って順方向へ、含意が期待する充足の形へ運び、三つの全称量化子が関数 `h` を適用します。どちらの方向でも、主張全体が底にある集合の水準に保たれます。結論は射影された値 `fst y` と `fst y'` の等しさであり、供給される所属も射影された対についてのものです。ここでは、すべての引数が値を持つことも、グラフが空でないことも主張しません。それは次節の定義域の条件に委ねられています。

```agda
  svAt-in h x y y' p q = h x y y'
    (subst ⟨_⟩ (at x y y') p) (subst ⟨_⟩ (at' x y y') q)
```

## 定義域

前節の適用の読み式が答えるのは一つの問いです。この二つの値の対はグラフに属するか。グラフはある引数では命中し、別の引数では外れることがあるので、次の構造的性質は、どの引数が項目を持つのかを問います。定義域に属するとは値を持つことであり、その読み式は模型に対する無界の存在量化がひとつあれば足ります。定義域の条件は続いて、候補の集合 `d` とグラフを比べ、「`d` に属する」ことと「値を持つ」ことが互いに含意し合うと言います。対象言語には双条件が備わっていないため、これは二つの含意として述べられます。

ここまでに展開した三つの論理的成分、適用、一価性、ちょうどの定義域は互いに独立であり、後ではそれぞれが別々に使われます。グラフは一価でありながら引数を漏らすことも、`d` の上でちょうど定義されながら多値であることもできます。この条件が何かを構成するのではない点にも注意してください。これは述語であり、ある候補の集合がそれを満たすかどうかを判定するだけです。二つの除去の補題はそれぞれ一方向で使われます。`domAt-out` は実際の項目を消費して定義域への所属を与え、`domAt-in` は定義域への所属を消費して項目の切り詰められた存在だけを与えます。定義域への所属だけからは、ある項目が存在することしか分からないからです。ある集合が外部の証拠からこの記述を**充足**することを示すときに必要な導入の方向には、三つ目の名前が与えられます。

定義は模型に対する無界の存在量化がひとつです。引数と `y` の対がグラフに属するような値 `y` が、単に存在する、というものです。量化子が渡るのは階層のある段階ではなく模型の台 `S` なので、読み式は言うべきことをちょうど言います。妥当性の主張は存在量化の充足を対応する依存和へ展開します。`∃[ y ∶ S ] _` は `y` の存在を命題的に包装するため、右辺もそれ自体切り詰められており、そのような `y` の存在しか主張しません。

```agda
inDomAt : ∀ {n} → Fin n → Fin n → Formula S n
inDomAt f x = ∃̇ (appAt (suc f) (suc x) zero)

inDomAt-adequate : ∀ {n} (f x : Fin n) (γ : S ^ n)
  → (γ ⊨ inDomAt f x)
  ≡ (∃[ y ∶ S ] (pr (fst (lookup x γ)) (fst y) ∈ fst (lookup f γ)))
```

証明に新しい議論は要りません。無界な存在量化の充足はそのファイバーの選言なので、両辺は各 `y` で点的に一致し、その点的な一致こそ、拡張環境での適用の妥当性の実例です。値を持つことが確まったところで、定義域の条件 `domAt f d` は候補の集合 `d` をグラフと両方向に比べます。すべての要素 `x` に対し、射影された `x` の `d` への所属は値を持つことを含意し、値を持つことは `d` への所属を含意する、というものです。二つの含意が連言で結ばれるのは、言語がその共同の主張を表す記号を持たないからです。

```agda
inDomAt-adequate f x γ =
  cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ y → appAt-adequate (suc f) (suc x) zero (y ∷ γ)))

domAt : ∀ {n} → Fin n → Fin n → Formula S n
domAt f d = ∀̇ ( (inDomAt (suc f) zero ⇒̇ (var zero ∈̇ var (suc d)))
             ∧̇ ((var zero ∈̇ var (suc d)) ⇒̇ inDomAt (suc f) zero) )
```

方向の補題は、固定されたグラフのスロット `f`、候補 `d`、環境 `γ` に対して述べられます。補助の `step` は、量化された本体の妥当性のパスを一度固定します。模型の要素 `x` において、「値を持つ」公式の充足は、射影された `x` と `y` の対がグラフに属するような `y` の切り詰められた存在へのパスです。以下の輸送はすべてこの一本のパスを通ります。

```agda
module _ {n : ℕ} (f d : Fin n) (γ : S ^ n) where
  private
    step : (x : S)
         → ((x ∷ γ) ⊨ inDomAt (suc f) zero)
         ≡ (∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)))
```

除去の `domAt-out` は項目を消費して定義域への所属を与えます。実際の証人の対 `x`、`y` と所属 `p` が与えられれば、切り詰められた形は `∣ y , p ∣₁` として組み立てられ、`step` を逆向きに輸送されて量化子が期待する充足の形になり、`x` で最初の含意に渡されます。出力は、射影された `x` が射影された `d` に属するという、切り詰めのない素の所属の証明です。

```agda
    step x = inDomAt-adequate (suc f) zero (x ∷ γ)

  domAt-out : ⟨ γ ⊨ domAt f d ⟩ → (x y : S)
            → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup d γ) ⟩
  domAt-out h x y p = h x .fst (subst ⟨_⟩ (sym (step x)) ∣ y , p ∣₁)
```

除去の `domAt-in` は逆方向に進み、切り詰めを保ちます。定義域への所属 `m` は二つ目の含意に渡され、その結論は「値を持つ」公式の充足です。`step` に沿って順方向に輸送すると、切り詰められた依存和に変わります。この切り詰められた形こそ正しい主張です。定義域への所属だけからは、ある項目が存在することしか、どれであるかは分かりません。

```agda
  domAt-in : ⟨ γ ⊨ domAt f d ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩
           → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁
  domAt-in h x m = subst ⟨_⟩ (step x) (h x .snd m)

  domAt-intro : ((x : S)
                 → (⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩
```

導入の方向は、二つの含意を点的に包装します。仮定は、各 `x` に対して関数の対を要求します。一方は項目の切り詰められた存在から `d` への所属へ、もう一方はその逆へ進むものです。対象がどちらも命題であるため、ここで切り詰められた和を消去するのは正当であり、各成分での `step` に沿う輸送は、二つの除去の補題と互いに鏡像です。

```agda
                    → ⟨ fst x ∈ fst (lookup d γ) ⟩)
                 × (⟨ fst x ∈ fst (lookup d γ) ⟩
                    → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩))
              → ⟨ γ ⊨ domAt f d ⟩
  domAt-intro g x = (λ h → g x .fst (subst ⟨_⟩ (step x) h))
```

組み立ては、全称量化子の下での含意の連言の形そのものです。各 `x` に対して対が与えられ、第一成分は最初の含意に、第二成分は二つ目の含意に答え、各成分はその側が要求する向きの輸送で調整されます。これにより、定義域だと主張される集合を、外部の証拠だけから `domAt f d` を充足すると証明できます。

```agda
                  , (λ m → subst ⟨_⟩ (sym (step x)) (g x .snd m))
```

## モデル内部の対

これまでの妥当性の主張は、模型の論理式を外へ読み出して周囲の事実へ変えるものでした。残りの課題はその逆です。読み式が語る周囲の集合が射影として現れるように、模型の内部で何かを作ること。すべては一つの構成、すなわち模型の二つの要素の順序対にかかっています。それが存在するのは、模型が自身の対の構成を持つからです。Kuratowski の方式に従ってこれを三度施せば、任意の二つの要素の内部対が得られ、証明書を補う必要はありません。対の構成は構成によって台に着地するからです。証明すべきは、この内部対が周囲の対へ射影されることです。底にある集合を通して読めば、射影された二つの成分の階層の対がちょうど得られ、二度現れる成分は単集合の等式が処理します。

モデル内部での Kuratowski 対の符号化は、周囲の定義を項ごとに写します。`pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆` は、`pairʟ a a` と `pairʟ a b` に `pairʟ` を施したものになります。`pairʟ` は構成によって台 `S` に着地するため、結果は証明書を補うことのないモデルの要素です。内側の `pairʟ` の各出現がすでに自身の構成可能性を担っているので、それらを重ね合わせるのに追加の証明は要りません。

```agda
prʟ : S → S → S
prʟ a b = pairʟ (pairʟ a a) (pairʟ a b)

prʟ-fst : (a b : S) → fst (prʟ a b) ≡ pr (fst a) (fst b)
prʟ-fst a b =
    pairʟ-fst (pairʟ a a) (pairʟ a b)
```

射影の等式は、同じ再帰を `V` の中で展開します。外側の射影は二つの射影の対を与え、第一成分は `fst a` とそれ自身の非順序対へ射影され、階層の等式 `pair-singleton` がそれを `fst a` の単集合へ畳みます。得られるのは約束された同一視です。モデルの対を底にある集合を通して読めば、ちょうど `pr (fst a) (fst b)` が得られます。この等式が次節の要になります。タグと対から成るすべての符号がこれを通して射影されるからです。

```agda
  ∙ cong₂ ⁅_,_⁆ (pairʟ-fst a a ∙ pair-singleton (fst a)) (pairʟ-fst a b)
```

## モデルにおける符号化

対 `prʟ` と数項は単射であり、これは一般的な符号化の仕組みが構造に求める条件のすべてなので、項と論理式は `L` 自身の中へ符号化できます。ここから二つの事実が従います。第一に、符号は**構成によって**モデルの要素であり、構成可能性の証明書を補う必要がありません。第二に、異なる式は異なる符号を持つことで、これは符号を鍵とする表に必要な性質です。異なる部分式の出現が同じ鍵を共有してはならないからです。

続いて、橋渡しが二つの符号化を比較します。内部の対と数項は周囲の対応物へ射影され、すべての符号はタグが数項と本体を対にする形で組み立てられているので、各符号は定数を `fst` で射影した論理式の周囲の符号へと射影されます。階層の側で証明された妥当性の定理を、モデルの内部で作られた符号に適用できるのはこのためです。

`prʟ` の単射性は、その射影と同じ道をたどります。モデルの要素の対が等しければ、両辺を `prʟ-fst` に沿って射影することで周囲の対の等しさが得られ、周囲の単射性 `pr-inj` が射影された成分の等しさを取り戻します。各成分の等しさは、第二成分が命題、すなわち証明書 `isL` である依存和の中に住むので、`Σ≡Prop` によって、第一成分の等しさからモデルの要素全体の等しさを結論できます。

```agda
prʟ-inj : {a b c d : S} → prʟ a b ≡ prʟ c d → (a ≡ c) × (b ≡ d)
prʟ-inj {a} {b} {c} {d} e =
    Σ≡Prop (λ v → snd (isL v)) (pr-inj q .fst)
  , Σ≡Prop (λ v → snd (isL v)) (pr-inj q .snd)
  where
```

周囲の対の等しさのパスは、手もとの三つの等式から組み立てます。左の対の射影を逆向きにたどり、仮定の等しさを `fst` の下で施し、右の対を射影します。同じ型が数項の単射性も与えます。ここでは `numeralL-fst` が射影の役を務め、`#-inj′` が射影された有限順序数の等しさから自然数の添字の等しさを取り戻します。

```agda
  q : pr (fst a) (fst b) ≡ pr (fst c) (fst d)
  q = sym (prʟ-fst a b) ∙ cong fst e ∙ prʟ-fst c d

numeralL-inj : {j k : ℕ} → numeralL j ≡ numeralL k → j ≡ k
numeralL-inj {j} {k} e =
  #-inj′ (sym (numeralL-fst j) ∙ cong fst e ∙ numeralL-fst k)
```

二つの単射性が揃うと、一般的な符号化の仕組みが構造 `𝒮ʟ` で実例化されます。`prʟ` を対に、`numeralL` を数項に取ると、得られるモジュール `LCode` が項と論理式を台 `S` の中へ符号化します。橋渡しの補題は続いて二つの符号化を結びます。基本の場合はすでに `tagBridge` に見えます。タグは数項と本体を対にするので、その射影は `prʟ-fst` と数項の射影等式により、射影された本体の周囲のタグになります。

```agda
module LCode = FOL.Coding {ℓ-suc ℓ} 𝒮ʟ prʟ prʟ-inj numeralL numeralL-inj

tagBridge : (k : ℕ) (x : S) → fst (LCode.mkTag k x) ≡ VCode.mkTag k (fst x)
tagBridge k x = prʟ-fst (numeralL k) x ∙ cong₂ pr (numeralL-fst k) refl

codeBridgeTm : ∀ {n} (t : Term S n) → fst LCode.⌜ t ⌝ᵗ ≡ VCode.⌜ mapTm fst t ⌝ᵗ
codeBridgeTm (con c) = tagBridge 0 c
```

項の再帰には二つの場合しかありません。定数はタグ 0 をそれ自身に施したものとして符号化されるので、橋はその定数での `tagBridge 0` です。変数はタグ 1 をその添字の数項に施したものとして符号化され、追加の合同の段階が、数項の射影等式をタグの下へ移します。`mapTm fst` が変数の定数をその射影に置き換えたからです。論理式の再帰も同じように始まります。所属は二つの項を対にし、ここでのタグ 0 は周囲の符号化における所属の構成子を示し、本体のパスは `prʟ-fst` に二つの項の橋に対する合同が続きます。

```agda
codeBridgeTm (var i) =
  tagBridge 1 (numeralL (toℕ i)) ∙ cong (VCode.mkTag 1) (numeralL-fst (toℕ i))

codeBridge : ∀ {n} (φ : Formula S n) → fst LCode.⌜ φ ⌝ ≡ VCode.⌜ mapFo fst φ ⌝
codeBridge (t ∈̇ u) = tagBridge 0 _ ∙ cong (VCode.mkTag 0)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
```

残りの二項の構成子は一つの型を繰り返します。各構成子は固有のタグで示され、本体は二つの直接の部分式の符号の順序対であり、射影のパスはタグの等式に、二つの再帰的な橋の対に対する合同を複合したものです。等号、連言、選言、含意が異なるのは、タグの番号と、二つの橋をどちらに施すかだけです。

```agda
codeBridge (t ≐ u) = tagBridge 1 _ ∙ cong (VCode.mkTag 1)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (a ∧̇ b) = tagBridge 2 _ ∙ cong (VCode.mkTag 2)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ∨̇ b) = tagBridge 3 _ ∙ cong (VCode.mkTag 3)
```

零項と一項の構成子も、退化した本体で同じ枠組みに収まります。恒偽はタグ 5 をゼロの数項に施したものとして符号化されるので、その橋は数項の射影を内に含むタグの等式一本です。非有界の量化子は部分式を一つしか担わないため、対は現れず、本体のパスはその部分式の再帰的な橋をタグの下で輸送したものです。

```agda
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ⇒̇ b) = tagBridge 4 _ ∙ cong (VCode.mkTag 4)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge ⊥̇       = tagBridge 5 _ ∙ cong (VCode.mkTag 5) (numeralL-fst 0)
codeBridge (∃̇ a)   = tagBridge 6 _ ∙ cong (VCode.mkTag 6) (codeBridge a)
```

有界量化子は、両方の水準に関わる唯一の構成子です。有界量化子は項と論理式を対にするので、本体のパスは外側の対を射影した後、項の橋と論理式の橋をそれぞれの成分に施します。これで再帰は項と論理式のすべての構成子を扱い尽くし、すべての内部の符号が、射影された論理式の周囲の符号へ射影されることが分かりました。

```agda
codeBridge (∀̇ a)   = tagBridge 7 _ ∙ cong (VCode.mkTag 7) (codeBridge a)
codeBridge (∀̇∈ t a) = tagBridge 8 _ ∙ cong (VCode.mkTag 8)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
codeBridge (∃̇∈ t a) = tagBridge 9 _ ∙ cong (VCode.mkTag 9)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
```

## 環境

集合 B の上の環境とは、その値がすべて B に入る関数のことです。したがって候補集合 e が環境であるのは、次の四つが同時に成り立つとき、そのときに限ります。e が一価であること、定義域が与えられた d であること、値が B に入ること、そして e が**順序対からできている**ことです。四つの条項は論理的に独立しており、それぞれに役割があります。一価性は二度現れる引数だけを制約し、定義域の条項は項目を持つ引数が d の要素にちょうど一致することを言い、値の制限はすべての値が B に入ることを言います。最初の三つは順序対であるような e の要素についてしか語らないので、対でない要素を余分に持つ集合でも通ってしまいます。第四の連言がこれを塞ぎます。e のすべての要素が「d の要素と B の要素の対」であることを要求し、各環境を d × B の部分集合にします。対でない要素の排除は、最初の三つからは得られないものです。

本節が与えるのは、一つの候補についての述語と、各連言を読み出す消去補題です。特定の集合がある長さの環境の全体の集合である**かどうか**は、別の、しかもより難しい問題であり、ここでは扱いません。

第三の連言は値の範囲を制限します。二つの変数 x と y について全称量化し、x と y の対がグラフ e に属するなら、値 y は B に属さねばならないと述べます。何が述べられて**いない**かにも注意してください。特定の x が値を持つことは要求せず、それは別の定義域の条項の仕事です。この条項はすでにある項目だけを制約するので、グラフを関数にするわけでも、その定義域を固定するわけでもありません。

```agda
valuesInAt : ∀ {n} → Fin n → Fin n → Formula S n
valuesInAt f B = ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
                     ⇒̇ (var zero ∈̇ var (suc (suc B))) ))

valuesInAt-out : ∀ {n} (f B : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ valuesInAt f B ⟩ → (x y : S)
```

この条項を読み出すのは一方向だけで、しかも直接です。第一成分 x、値 y となる対がグラフにあれば、全称量化子を x と y に適用し、残る課題は内側の含意です。まず所属の事実 p を前件の充足へ変換します。`appAt-adequate` はその充足を、射影した環境 (y ∷ x ∷ γ) での所属と同一視するので、その対称な等式に沿って輸送すれば、量化された本体が要求する論拠がちょうど得られます。結論は射影した値の射影した B への所属であり、至る所で截断は現れません。

```agda
               → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
               → ⟨ fst y ∈ fst (lookup B γ) ⟩
valuesInAt-out f B γ h x y p = h x y
  (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ))) p)

pairsInAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
```

第四の連言、すなわち対の条項は、有界量化子だけで書かれています。e のすべての要素 s に対し、d の要素 u と B の要素 v で、s が u と v の対に等しいものが存在する、と述べるのです。量化子が実際の要素を動くので、この条項は e、d、B にすでにあるものだけを制約し、その意味は射影後にこれらの集合から読み出されます。本体は本章の前で与えた対の読み式 `prAtL` で、添字は三つの束縛子ぶんだけ後ろへずれます。

```agda
pairsInAt e d B =
  ∀̇∈ (var e) (∃̇∈ (var (suc d)) (∃̇∈ (var (suc (suc B)))
    (prAtL (suc (suc zero)) (suc zero) zero)))

pairsIn-out : ∀ {n} (e d B : Fin n) (γ : S ^ n) → ⟨ γ ⊨ pairsInAt e d B ⟩
            → (s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
```

対の条項からの抽出は充足の形を保ちます。結論は命題的截断であり、そのような u と v が単に存在することしか主張しません。前提 h は「公式が成り立つ」ことの截断された証明であり、s∈ は射影した s の射影した e への普通の所属です。この型は、何が取り出せるかを正確に述べます。u が d に属し、v が B に属し、s の底集合がそれらの底集合の対に等しいこと、すべて単に存在するとしてです。

```agda
            → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                  (⟨ fst u ∈ fst (lookup d γ) ⟩
                   × (⟨ fst v ∈ fst (lookup B γ) ⟩
                      × (fst s ≡ pr (fst u) (fst v)))))) ∥₁
pairsIn-out e d B γ h s s∈ = PT.rec squash₁
```

証明は、截断の内側で二つの有界存在を剥がします。命題的截断の消去がここで正当なのは、目標が再び命題、すなわち Σ 型の截断だからです。したがって何かを大域的に選ぶのではなく、各分岐が自分の証拠を変換するだけです。内側の一歩は本章で繰り返し現れたのと同じ輸送です。`prAtL-adequate` が本体の充足を経路 `fst s ≡ pr (fst u) (fst v)` に変え、環境は束縛子の順に v、u、s を加えて伸ばします。

```agda
  (λ { (u , (u∈ , hv)) → PT.map
    (λ { (v , (v∈ , hp)) → u , (v , (u∈ , (v∈ , subst ⟨_⟩
      (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ)) hp))) })
    hv })
  (h s s∈)
```

逆向きは、要素ごとの主張を前提として取ります。射影した s が射影した e に属するすべての s に対し、前提が与えるのは截断された四つ組、すなわち u と v とそれぞれの所属および対の等式の単なる存在であり、課題はそれを有界公式の充足へ変えることです。両方向は一つの経路に併合されず、別々の補題として保たれます。後の議論は毎回どちらか一方向しか使わないからです。

```agda
pairsIn-in : ∀ {n} (e d B : Fin n) (γ : S ^ n)
           → ((s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
              → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                    (⟨ fst u ∈ fst (lookup d γ) ⟩
                     × (⟨ fst v ∈ fst (lookup B γ) ⟩
```

構成は、前提の截断されたデータを公式の充足へ直接変換します。証拠 u と v はそれぞれの所属とともにそのまま通り、対の等式 eq は妥当性の経路の対称な等式に沿って輸送され、本体の充足になります。ここでは集合レベルの対の等式から読み式の充足へ戻るからです。截断は `PT.map` を通してのみ現れ、並べ直したデータの周りに截断された和を組み立て直します。公式自身の意味が、その量化子の担う截断を供給します。

```agda
                        × (fst s ≡ pr (fst u) (fst v)))))) ∥₁)
           → ⟨ γ ⊨ pairsInAt e d B ⟩
pairsIn-in e d B γ k s s∈ = PT.map
  (λ { (u , (v , (u∈ , (v∈ , eq)))) → u , (u∈ , ∣ v , (v∈ , subst ⟨_⟩
    (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ))) eq) ∣₁) })
```

四つの条項を組み合わせると、定義域 d、値の範囲 B の環境であることの定義が得られます。一価性、ちょうどの定義域、値の制限、そして対の条項を `∧̇` で連言したものです。続く無名モジュールはアリティ、三つの添字、環境 γ、および「γ がこの連言を充足する」ことの截断された証明を固定し、四つの射影を一度だけ述べて再利用できるようにします。

```agda
  (k s s∈)

envOverAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envOverAt e d B =
  svAt e ∧̇ (domAt e d ∧̇ (valuesInAt e B ∧̇ pairsInAt e d B))

module _ {n : ℕ} (e d B : Fin n) (γ : S ^ n) (h : ⟨ γ ⊨ envOverAt e d B ⟩) where
```

各射影は、四重連言の充足が作る入れ子の対の、対応する成分にほかなりません。第一は e の一価性、第二は e と d を結ぶ定義域の条項、第三は B への値の制限、第四は対の条項そのものです。四つがそろえば、環境であることの一面だけを必要とする議論は、連言を組み立て直さずにそれを取り出せます。環境を構成する議論も、連言を一項ずつ検査できます。

```agda
  envOver-sv     : ⟨ γ ⊨ svAt e ⟩
  envOver-sv     = h .fst
  envOver-dom    : ⟨ γ ⊨ domAt e d ⟩
  envOver-dom    = h .snd .fst
  envOver-values : ⟨ γ ⊨ valuesInAt e B ⟩
```

四つの射影は定義の分解可能性も示します。一意性、定義域、値域、対の形は別々に移したり利用したりでき、その連言は候補が `d` 上で `B` に値をとる環境だという一つの主張を保ちます。

```agda
  envOver-values = h .snd .snd .fst
  envOver-pairs  : ⟨ γ ⊨ pairsInAt e d B ⟩
  envOver-pairs  = h .snd .snd .snd
```

これまでに組み立てた読み式はどれも、割り当てがその添字に置いた底にある集合だけを見ます。グラフ、定義域、値の集合についての充足の主張は、常に検表した項目を `fst` で射影してから述べられます。したがって環境の記述は、射影されたグラフ、射影された定義域、射影された値の集合という三つの集合に外延的に依存するだけで、割り当てのそれ以外の側面には依存しません。アリティの異なりうる二つの割り当てが、記述が参照する添字に同じ三つの集合を置くなら、記述は一方で成り立つときちょうど他方でも成り立ちます。

これが後に「ある割り当てについての主張」を「構成が実際に作った集合についての主張」へ変える仕組みです。構成は好きな添字づけで環境を提示してよく、三つの底集合が一致する限り、記述はそのまま通用します。

移転の定理には、値の制限の導入方向、つまり前に取り出されなかった方向、「グラフのすべての対についての主張」から充足そのものへ戻る方向が必要です。グラフの中の任意の対を B の値へ送る関数が与えられれば、二つの全称量化子を適用し、適用の読み式の妥当性の等式によって所属の事実を前件の充足へ変えます。これで `valuesInAt` の両方向が、方向ごとに一つの補題として使えるようになりました。

```agda
valuesInAt-in : ∀ {n} (f B : Fin n) (γ : S ^ n)
              → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
                 → ⟨ fst y ∈ fst (lookup B γ) ⟩)
              → ⟨ γ ⊨ valuesInAt f B ⟩
valuesInAt-in f B γ k x y hp = k x y
```

定理は、アリティの異なりうる二つの割り当て γ と `γ'` を比較し、各側で三つの添字を選びます。前提は射影された集合の間の経路、すなわちグラフ、定義域、値の集合が階層の集合として要素ごとに等しいことです。両側の添字同士の関係については何も仮定せず、射影後の検表の結果だけを仮定します。これはまさに、環境を別の添字づけで提示する構成の置かれた状況です。

```agda
  (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ)) hp)

envOverAt-transport : ∀ {n n'} (γ : S ^ n) (γ' : S ^ n')
                      (e d B : Fin n) (e' d' B' : Fin n')
                    → fst (lookup e γ) ≡ fst (lookup e' γ')
                    → fst (lookup d γ) ≡ fst (lookup d' γ')
```

一価性の移転は、γ での消去補題と `γ'` での導入補題の合成です。`γ'` で同じ入力 x に対する二つの値 y と `y'` が記録されていれば、まず両側の射影されたグラフにおける対の所属を同一視する経路に沿って、前提を γ 側の充足へ戻します。消去補題が二つの射影された値の相等を与え、導入補題がそれを `γ'` での充足として包み直します。相等そのものには輸送が要りません。両側の値とも S の要素だからです。

```agda
                    → fst (lookup B γ) ≡ fst (lookup B' γ')
                    → ⟨ γ ⊨ envOverAt e d B ⟩ → ⟨ γ' ⊨ envOverAt e' d' B' ⟩
envOverAt-transport γ γ' e d B e' d' B' qe qd qb h =
    svAt-in e' γ' (λ x y y' p q →
      svAt-out e γ (envOver-sv e d B γ h) x y y'
```

定義域の条項は `domAt` の導入補題を通って移り、`γ'` で二つの含意をそろえて与えます。第一の含意は、値を持てば定義域に属する、というものです。値の切り詰められた存在だけから、γ での消去補題が射影された定義域 d への所属を生みます。所属という命題への消去には証人を選ぶ必要がなく、経路 qd がその所属を `d'` 側へ運びます。

```agda
        (subst ⟨_⟩ (sym (at x y)) p) (subst ⟨_⟩ (sym (at x y')) q))
  , ( domAt-intro e' d' γ'
      (λ x → (λ m → subst (λ w → ⟨ fst x ∈ w ⟩) qd
                (PT.rec (snd (fst x ∈ fst (lookup d γ)))
                  (λ { (y , p) → domAt-out e d γ (envOver-dom e d B γ h) x y
```

第二の含意は逆向きで、定義域に属すれば値を持つ、というものです。まず `d'` での所属を対称な経路で戻し、γ での消去補題が「項目がある」ことの切り詰められた存在を与えます。そして切り詰めの内側で、本体の充足を `γ'` 側の形へ置き換えます。値の y 自身はそのまま通ります。これが正しいのは、二つのグラフが一致するのは射影後だけで、項目は S の要素だからです。

```agda
                         (subst ⟨_⟩ (sym (at x y)) p) })
                  m))
            , (λ hx → PT.map (λ { (y , p) → y , subst ⟨_⟩ (at x y) p })
                (domAt-in e d γ (envOver-dom e d B γ h) x
                  (subst (λ w → ⟨ fst x ∈ w ⟩) (sym qd) hx))))
```

値の制限では、新しい射影グラフへの対の所属から始めます。グラフ所属のパスを逆向きに使って旧グラフへ移し、そこで `valuesInAt-out` により値が旧集合 `B` に属することを得ます。最後に `qb : B ≡ B′` に沿って一度だけ順方向へ輸送し、`B′` への所属を得ます。したがって `qb` を使うのは旧値集合から新値集合への一回だけです。

```agda
    , ( valuesInAt-in e' B' γ'
        (λ x y p → subst (λ w → ⟨ fst y ∈ w ⟩) qb
          (valuesInAt-out e B γ (envOver-values e d B γ h) x y
            (subst ⟨_⟩ (sym (at x y)) p)))
      , pairsIn-in e' d' B' γ'
```

対の条項が最後に移り、輸送はすべて切り詰めの内側にとどまります。γ で条項を読み出すと、証拠 u と v、射影された d と B へのそれぞれの所属、そして対の等式が単に存在するとして得られます。二つの所属は qd と qb によってそれぞれ `d'` と `B'` へ運ばれます。一方、等式 `fst s ≡ pr (fst u) (fst v)` には輸送がまったく要りません。これは底にある集合についての主張であり、前提はまさにそれらが一致することを言っているので、等式は両側で同一です。

```agda
        (λ s s∈ → PT.map
          (λ { (u , (v , (u∈ , (v∈ , eq)))) →
            u , (v , ( subst (λ w → ⟨ fst u ∈ w ⟩) qd u∈
                     , ( subst (λ w → ⟨ fst v ∈ w ⟩) qb v∈ , eq ) )) })
          (pairsIn-out e d B γ (envOver-pairs e d B γ h) s
```

残りの材料は経路 `at` です。各 x と y に対し、両側で「その対が射影されたグラフに属する」ことを同一視する経路です。これは合同であり、二つのグラフの間の等式 qe を、対の成分を固定した所属述語に適用したものです。定理の内部でグラフに関わる輸送はすべてこの一つの経路を通るので、議論全体は与えられた三つの等式のみに依存し、隠れたものはありません。

```agda
            (subst (λ w → ⟨ fst s ∈ w ⟩) (sym qe) s∈))) ) )
  where
  at : (x y : S) → (pr (fst x) (fst y) ∈ fst (lookup e γ))
                 ≡ (pr (fst x) (fst y) ∈ fst (lookup e' γ'))
  at x y = cong (λ w → pr (fst x) (fst y) ∈ w) qe
```

## 対の成分を収める集合

対の形をした符号を読むと二つの成分が現れますが、両方を**ひとつの**構成可能集合の要素として持ち出せると便利です。候補は数学そのものが決めます。`fst x` が `fst u` と `fst v` の順序対なら、非順序対 `⁅ fst u , fst v ⁆` は `fst x` に属するので、`L` の推移性によりそれ自身構成可能であり、しかも二つの成分はどちらもその要素です。この節が記録するのは、まさにこの証拠と三つの所属の事実、すなわち型 `Container x u v` と、経路 `fst x ≡ pr (fst u) (fst v)` からそれを造る構成 `container` です。

この型は、モデルの要素 `s` に三つの周囲の所属の事実を、すべて射影後に述べる形でまとめます。`s` の底集合が `fst x` に属し、`u` と `v` の底集合がともに `fst s` に属するというものです。それ以外の主張はなく、とりわけ `s` がこの性質を持つ極小の集合であるとは言いません。構成 `container` は「`fst x` が `pr (fst u) (fst v)` に等しい」という仮定を受け取り、証拠と三つの証明書をひとまとめにして返します。

```agda
Container : (x u v : S) → Type (ℓ-suc ℓ)
Container x u v = Σ[ s ∈ S ] (⟨ fst s ∈ fst x ⟩ × (⟨ fst u ∈ fst s ⟩ × ⟨ fst v ∈ fst s ⟩))

opaque
  container : (x u v : S) → fst x ≡ pr (fst u) (fst v) → Container x u v
  container x u v e = s , (s∈ , (∈pair-introL refl , ∈pair-introR refl))
```

証拠は、二つの底集合の非順序対です。Kuratowski 符号の外側の非順序対の一要素として、反射経路での導入規則により `pr (fst u) (fst v)` に属し、仮定 `e` に沿って輸送すれば `fst x` への所属になります。これこそ `L` の推移性が受け取る入力です。非順序対が構成可能な集合に属する以上、`isL-trans` はそれを証明書込みで `S` の要素として与えます。残る二つの所属、すなわち `fst u` と `fst v` がそれに属することは、反射経路での二つの導入規則によります。

```agda
    where
    s∈ : ⟨ ⁅ fst u , fst v ⁆ ∈ fst x ⟩
    s∈ = subst (λ w → ⟨ ⁅ fst u , fst v ⁆ ∈ w ⟩) (sym e) (∈pair-introR refl)
    s : S
    s = ⁅ fst u , fst v ⁆ , isL-trans s∈ (snd x)
```

## まとめ

本章は、意味論の両側の間を埋めました。論理式は `L` の中で、構成可能な要素からなる環境のもとで充足されますが、表現すべき具体的な事実は底集合についての周囲の事実です。辞書の各項目は、正確な妥当性の経路によってこの二つを結びます。順序対の認識は絶対的であり、グラフの所属は推移性によって構成可能な証拠を獲得し、環境の記述は一価性、ちょうどの定義域、値の制限、対の条項を集めて、射影された三つの集合だけに依存します。構文の符号化は続いて `L` 自身の中で実例化され、橋渡しの定理は、内部の符号が射影された論理式の周囲の符号へ射影されることを示すので、階層の側で書かれた読み式が内部で造られた符号に適用できます。容器は、対の形をした符号に対して、二つの成分をともに収める構成可能な集合をひとつ供給します。