---
title: "符号化再帰のための論理式表現"
module: L.Coding.Expressions
lang: ja
site: "Bedrock"
description: "符号化再帰のための論理式表現"
stage: "内部の符号化：式と定義域"
reading_order: 43
canonical: https://bedrock.institute/ja/L.Coding.Expressions.html
html: L.Coding.Expressions.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Expressions.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, FOL.Manipulation.ConstantBounding, L.Absoluteness, L.Coding.Environment, L.Axioms.Numerals, L.Coding.Model]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Expressions.md, https://bedrock.institute/zh/L.Coding.Expressions.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 符号化再帰のための論理式表現

符号化された充足関係の再帰は、`L` の内部で「環境 `γ` は符号 `c` の論理式を充足するか」という形の問いを判定しなければなりません。Kuratowski 対のような複合的な値を有界論理式で認識するには、証人自身が模型の要素でなければなりません。成分 `u` と `v` をもつ対 `q` に対しては、`s` が `q` に属し、`u` と `v` が `s` に属する構成可能集合 `s` が要ります。読みの論理式はこの三者を一度に束縛し、`v, u, s` に元の割り当てを続けた拡張割り当てのもとで二つの成分条件を評価します。元のスロットはずらしの下で保たれます。

本章はこれを一度だけ組み立てます。代入スロット、構成可能なリテラル、数項、Kuratowski 対からなる小さな式の言語上の構造的な読みを与え、その双方向の妥当性を証明します。外向きの方向は充足の判断から出発し、三つの命題的切り捨てを受けた存在を命題値のパスへ消去し、対の等式を帰納的な成分のパスと連結します。内向きの方向は二つの部分式の明示的な内部要素を選び、それらの共通の構成可能コンテナを取得します。截断から選択を取り出すことは一切ありません。

同じ読みはいくつもの方向に特殊化されます。式の値がある項の指示への所属は `L` の推移性を用います。周囲の値が項の構成可能な解釈に属するという事実がその値の構成可能性を証明し、それによって値は模型の要素として働けます。これは実際の構成であって、截断の消去を正当化する命題値の対象という制限とは別物です。外延的な集合の記述は普通の全称含意の対であり、外側に截断はなく、候補となる集合を構成するのではなく特徴づけます。アリティ付きタグの認識器は二層の入れ子の対、すなわちアリティと「タグとペイロードの対」を読みます。最後に、後者と環境拡張の論理式は有界絶対性によって持ち上げられます。その転送は確立された推移的モデルの設定と、射影の下での参照の相容性に依拠します。環境拡張の論理式が本章を閉じます。

複合的な集合の値を一階の有界論理式で記述するには、固定された部分を定数で名指し、各証人を集合で限界づけます。ここでのすべては、ひとつの固定されたレベル `ℓ` の上で行われます。周囲の階層は `V ℓ` であり、有界量化子がその要素を渡る模型は、その中に置かれた構成可能模型です。充足の判断は真理値を比較するものなので、これらの論理式が主張する事実は、`hProp (ℓ-suc ℓ)` の命題になります。

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

open import Base.Prelude

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

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

ひとつの区別の二つの側面が本章を貫きます。階層の外では、構造 `𝒮ᵥ` が `V ℓ` の上で一階の言語を解釈し、そこの Kuratowski 対が演算 `pr` です。模型の内側では、同じ言語が構成可能集合の上で改めて解釈されます。したがって複合的な値を認識する節は、両方の場所で同時に読めなければならず、以下の各妥当性の主張が述べるのはまさにそのことです。内部の論理式の模型での真理値が、経路として、`pr` と射影された割り当てについての対応する周囲の主張と同一視されるのです。

```agda
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∀̇_; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

構成可能模型の要素とは、周囲の集合に「それが構成可能である」という証明を添えたものです。`L` の推移性が、有界な証人が両側の間を移れるようにします。`isL-trans` により、構成可能集合の要素はそれ自身構成可能であり、したがってそれ自体が模型の要素になれます。有界絶対性は論理式について対応する仕事をします。階層についての、すべての定数が構成可能集合を名指す Δ₀ 論理式は、`L` の内部でも意味を変えません。`BoundedFo` データが記録する定数の有界性は、この転送が要る前提そのものです。後者と環境拡張の論理式はすでに階層の側で証明されており、模型への持ち上げはこの転送を適用することにほかなりません。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate
```

数項にはひとつの相容性の事実が必要です。内部の数項 `numeralL k` はフォン・ノイマンの自然数 `k` を模型の内部で実現し、`numeralL-fst` はその射影を周囲の `# k` と同一視します。数項の節の両方向はこれに依存します。いくつかの節は有限個のスロットについて同時に量化するので、環境はスロットの再索引付けに沿って移されます。ひとつの論理的な形式が全章を貫きます。妥当性の主張は命題の同値の二つの含意から得られる真理値の経路であり、対象言語の有界量化子は命題的切り捨てを受けた存在として読まれます。

```agda
        ; env; cons; shiftPairAt; sgl0At; pair0At; tag0At )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
```

周囲の階層 `V ℓ` は h-集合なので、その二つの集合の等しさは命題であり、真理値の中に置けます。これが後の梱包された等式を正当化するものです。自然数は集合として現れます。`# k` は階層におけるフォン・ノイマンの数項、`sucV` はその後者演算であり、宇宙レベルとも、符号が持つアリティの指標とも別の概念です。命題的切り捨ては単なる存在を与え、その消去が正当なのは命題値の対象に限られます。対の読みの外向きの証明はこの制限を明示的に守ります。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
```

ここで使う真理値はレベル `ℓ-suc ℓ` の `hProp` の命題であり、それぞれ「それが命題である証明」とともに梱包され、結合子と量化子はこれらの命題に直接作用します。模型の台 `S` は、周囲の集合と構成可能性の証明の対からなります。絶対性の仕組みはこの状況に対して一度だけ設けられます。相対化される構造は階層 `𝒮ᵥ`、部分模型を選ぶクラスは `isL`、Δ₀ 論理式を絶対的に保つのが推移性です。充足は `⊨`、項の解釈は `⟦_⟧` と書き、環境は模型の要素からなるベクトルです。

```agda
open hPropStructure 𝒮ʟ using ( S )

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

open import L.Coding.Model {ℓ}
```

模型の辞書の中で、主な構成に決定的なのは対の形をした事実です。模型の対 `prʟ` は `prʟ-fst` によって周囲の対へ射影され、その有界な読みの論理式が `prAtL` です。レコード `Container` と `container` は、ある対に等しい値に対して、両方の成分を収める構成可能集合をひとつ作ります。有界な論理式で対を読むには、まさにそのような中間集合が必要であり、`lookup-fst` と `envOverAt` は、のちに使われる同じ辞書の射影と環境の事実です。

```agda
  using ( lookup-fst; prʟ; prʟ-fst; prAtL; prAtL-adequate; envOverAt
        ; Container; container )
```

模型における有界量化子は `S` の要素を渡ります。したがって論理式に認識させたい複合的な値は、それ自身が模型の要素である有界な証人によって一致させられねばなりません。本節はその一般的な道具を組み立てます。代入スロット、構成可能なリテラル、数項、Kuratowski 対から値を組み立てる帰納的な言語 `Expr` と、表現を論理式へ変えるひとつの構造的な読み、そして論理式の意味を表現の指す値と同一視する両方向の妥当性定理です。本章の残りはすべて、この読みの特殊化です。

本節は小さな二つの準備から始まります。`PairIs a p` は「周囲の値 `a` が `p` に等しい」という主張を真理値として梱包します。階層は h-集合なので、その等式の型は命題であり、`setIsSet` との対によって `hProp (ℓ-suc ℓ)` の要素になります。以後の妥当性の主張は、充足の判断とこれらの梱包された等式をパスに沿って比較することになります。式の言語そのものは自然数 `n` を指標とし、利用できる自由変数スロットの数を確定します。ひとつのスロットが使われないままであっても構いません。

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

module PairExpression where
  data Expr (n : ℕ) : Type (ℓ-suc ℓ) where
```

表現の言語は四つの構成子で確定し、それぞれが複合的な値が論理式に現れるひとつのしかたに対応します。`slot` `i` は周囲の割り当ての第 `i` 項を参照する、変数に相当するものです。`literal` `a` は模型の要素ひとつを、構成可能性の証明書ごとまとめて名指し、対象言語の定数のように振る舞います。`numeral` `k` はフォン・ノイマンの自然数 `k` を名指し、`pair` は二つの部分表現を Kuratowski 対へ合成します。表現は値の有限な記述であって、それ自身は集合ではないので、二つの独立した読み方が許され、目標はこの二つが一致することの証明です。

```agda
    slot : Fin n → Expr n
    literal : S → Expr n
    numeral : ℕ → Expr n
    pair : Expr n → Expr n → Expr n

  value : ∀ {n} → Expr n → (Fin n → V ℓ) → V ℓ
```

第一の読みは周囲のものです。階層の集合を各スロットに割り当てると、`value` は表現の指す集合を計算します。スロットは参照され、リテラルは `fst` で証明書を射影して捨てられ、数項は `# k` になり、対は指された二つの集合の Kuratowski 対 `pr` です。妥当性定理が右辺として取り戻すのはこの読みです。有界な論理式の意義は、外で自然に記述される値を模型の内部から識別することにあります。

```agda
  value (slot i) γ = γ i
  value (literal a) γ = fst a
  value (numeral k) γ = # k
  value (pair a b) γ = pr (value a γ) (value b γ)

  element : ∀ {n} → Expr n → (Fin n → S) → S
```

第二の読みは模型の内部にとどまります。`S` の要素を各スロットに割り当てると、`element` は `S` の要素をひとつ計算します。リテラルはもともと証明書を伴う模型の要素であり、数項は模型内部の数項 `numeralL` を使い、対は模型自身の対 `prʟ` で作られます。二つの読みは条項ごとに平行しており、この平行性こそ両者を結ぶ橋が証明できる理由です。比較はつねに対応する場合どうしの比較で済むからです。

```agda
  element (slot i) γ = γ i
  element (literal a) γ = a
  element (numeral k) γ = numeralL k
  element (pair a b) γ = prʟ (element a γ) (element b γ)

  element-fst : ∀ {n} (e : Expr n) (γ : Fin n → S)
```

橋となるのが `element-fst` です。内部の要素を射影すると、その道はちょうど、射影された割り当てにおける周囲の値になります。スロットとリテラルでは二つの読みが文字どおり一致するので、証明は `refl` です。数項が最初の本格的な場合で、その内部の形は `numeralL-fst` によって周囲の形へ射影されます。これは数項の章が供給する、内部の数項と周囲の数項の間の相容性の事実です。方向に注意してください。これは後章でも繰り返されます。道は内部の値の射影から周囲の値へ向かいます。

```agda
              → fst (element e γ) ≡ value e (λ i → fst (γ i))
  element-fst (slot i) γ = refl
  element-fst (literal a) γ = refl
  element-fst (numeral k) γ = numeralL-fst k
  element-fst (pair a b) γ = prʟ-fst (element a γ) (element b γ)
```

対の場合は独立した二つの相容性を連結します。模型の対は `prʟ-fst` によって周囲の対へ射影され、各成分の射影の法則は帰納的な事実です。`pr` の下での合同性が二つの成分の道をひとつにまとめ、入れ子になった表現の射影の法則は帰納法で従います。構文の側では、`lift3` が対の読み出しに要る再索引付けです。各スロットを三つ上げる、つまり `lift3 ρ i = suc (suc (suc (ρ i)))` とすることで、各スロットが指す旧来の項目を保ったまま、三つの新しい変数の分の空きができます。

```agda
    ∙ cong₂ pr (element-fst a γ) (element-fst b γ)

  lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin (3 + m)
  lift3 ρ i = suc (suc (suc (ρ i)))

  read : ∀ {n m} → Expr n → (Fin n → Fin m) → Fin m → Formula S m
  read (slot i) ρ q = var q ≐ var (ρ i)
```

読み出し `read` は、スロット `q` の表現を有界な論理式へ変えます。スロットは対応する再索引付けされた変数との等しさを、リテラルはその定数との等しさを、数項は内部の数項を名指す定数との等しさを要求します。数学的な内容を担うのは対の場合です。三つの有界存在によって、`q` の集合の中の集合 `s` と、`s` の中の要素 `u`、`v` を結び、`s` が `q` の項目の要素であり、`u` と `v` が `s` の要素になるようにします。そして模型の対の読みの論理式 `prAtL` を通して、`q` の項目が対 `pr u v` に等しいと主張します。成分の条件はその後、ずらしたスロットで帰納的に読まれ、これを `lift3` が担います。こうして複合的な値は、模型の内部から、Kuratowski の二成分をともに収める構成可能な中間集合を経由して認識されます。

```agda
  read (literal a) ρ q = var q ≐ con a
  read (numeral k) ρ q = var q ≐ con (numeralL k)
  read (pair a b) ρ q = ∃̇∈ (var q) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
    (prAtL (suc (suc (suc q))) (suc zero) zero
      ∧̇ (read a (lift3 ρ) (suc zero) ∧̇ read b (lift3 ρ) zero))))
```

妥当性には二つの方向があり、`out` は健全性の証明が消費する方向です。充足の判断の要素から、「スロット `q` の項目を射影すると指された値に等しい」という道を作ります。スロットとリテラルは定義どおりそのような道そのものであり、数項の場合は前提を `numeralL-fst` と合成します。方向は `element-fst` と同じです。本格的な仕事は対の場合にあり、次の二段がそれを扱います。

```agda
  out : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
       → ⟨ γ ⊨ read e ρ q ⟩ → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ))
  out (slot i) ρ q γ h = h
  out (literal a) ρ q γ h = h
  out (numeral k) ρ q γ h = h ∙ numeralL-fst k
```

対の場合の前提は三層に重なった截断された有界存在なので、証明はそれを一度にひとつずつ消去し、各消去には命題値の対象が必要です。ここで `setIsSet` が登場します。結論は階層 (h-集合) における道であり、したがって対象は命題なので、消去は正当です。截断が何を与え、何を与えないかは率直に述べるべきです。証人 `s`、`u`、`v` は要素として現れるので数学はそれを使えますが、前提が主張するのはそれらの単なる存在にすぎません。一意性も、選ばれた代表もありません。

```agda
  out (pair a b) ρ q γ = PT.rec (setIsSet _ _) (λ { (s , s∈ , hs) →
    PT.rec (setIsSet _ _) (λ { (u , u∈ , hu) →
      PT.rec (setIsSet _ _) (λ { (v , v∈ , p , ha , hb) →
        subst ⟨_⟩ (prAtL-adequate (suc (suc (suc q))) (suc zero) zero (v ∷ u ∷ s ∷ γ)) p
        ∙ cong₂ pr (out a (lift3 ρ) (suc zero) (v ∷ u ∷ s ∷ γ) ha)
```

三つの証人が手に入れば、最も内側の論理式は対の読み出し自身の妥当性によって展開されます。`p` を `prAtL-adequate` に沿って輸送すると、対の主張は等式 `fst (lookup q γ) ≡ pr (fst u) (fst v)` になります。続く二つの帰納的な前提が、スロット 0 と 1 での成分の射影、すなわち `fst u ≡ value a` と `fst v ≡ value b` を与え、`pr` の下での合同が右辺を `pr (value a) (value b)` へ書き換えます。これはまさにその対の表現の値です。内側の証明は、輸送ひとつと合同ひとつからなります。

```agda
                   (out b (lift3 ρ) zero (v ∷ u ∷ s ∷ γ) hb) }) hu }) hs })

  into : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
        → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ)) → ⟨ γ ⊨ read e ρ q ⟩
  into (slot i) ρ q γ h = h
  into (literal a) ρ q γ h = h
```

逆方向の `into` は、裸の等式から充足の判断の要素を構成します。スロットとリテラルは直接であり、数項の場合は `numeralL-fst` の対称と合成して、先の相容性の向きを逆にします。対の場合には三つの截断の層すべてを一度に供給しなければなりませんが、ここでは截断から何かを取り出すのではなく、証人をその場で構成します。内部の要素 `u` と `v` は再索引付けされた割り当てでの `element a` と `element b` として選ばれ、`Container` と `container` が調整済みの道 `e` を用いて、両方を収める構成可能な集合 `s` を、すべての所属の証明書とともに作ります。これは `L` の推移性の独立した使用であり、上で消去を正当化した命題値の確認とは別物です。あちらは截断を消費し、こちらは具体的な要素を作り出します。

```agda
  into (numeral k) ρ q γ h = h ∙ sym (numeralL-fst k)
  into {n} {m} (pair a b) ρ q γ h = ∣ s , c .snd .fst , ∣ u , c .snd .snd .fst ,
    ∣ v , c .snd .snd .snd ,
      subst ⟨_⟩ (sym (prAtL-adequate (suc (suc (suc q))) (suc zero) zero δ)) e
      , into a (lift3 ρ) (suc zero) δ (element-fst a η)
```

拡張された割り当て `δ` は `v ∷ u ∷ s ∷ γ` であり、その配置がこの構成のすべての簿記です。

| スロット | 項目 | 役割 |
| --- | --- | --- |
| 0 | `v` | `b` の内部要素 |
| 1 | `u` | `a` の内部要素 |
| 2 | `s` | 中間集合、`q` の項目の要素 |
| `i + 3` | 古いスロット `i` | 元の割り当て、そのまま |

対の論理式は `s ∈ q`、`u ∈ s`、`v ∈ s`、そして `q ≡ pr u v` を主張します。`u` がスロット 1 に、`v` がスロット 0 にあるので、`lift3` によって、スロット 1 での `read a` とスロット 0 での `read b` はちょうど古いスロットを参照します。各部分証明は `into` 自身がずらしたスロットで組み立て、読まれる成分の射影の経路 `element-fst` を与えられ、最後に三つの入れ子の截断された存在は、層ごとにひとつの明示的な `∣_∣₁` で閉じられます。

```agda
      , into b (lift3 ρ) zero δ (element-fst b η) ∣₁ ∣₁ ∣₁
    where
    η : Fin n → S
    η i = lookup (ρ i) γ
    u v : S
```

残りの局所的な定義は、この構成の算術を記録します。`η` は古い割り当てを再索引付けされたスロットに制限したものであり、`u` と `v` はそのもとでの二つの部分表現の明示的な内部的な要素です。これらは直接選ばれるのであって、截断から取り出されるのではありません。経路 `e` は、スロット `q` の項目が周囲の対 `pr (fst u) (fst v)` に等しいと述べます。その方向が重要です。前提 `h` は項目が対全体の指す値に等しいと言い、成分の射影の合同 `element-fst` の対称と合成することで、コンテナの構成が期待する対象がちょうど得られます。

```agda
    u = element a η
    v = element b η
    e : fst (lookup q γ) ≡ pr (fst u) (fst v)
    e = h ∙ sym (cong₂ pr (element-fst a η) (element-fst b η))
    c : Container (lookup q γ) u v
```

コンテナは経路 `e` から作られ、その最初の成分がまさに求める構成可能な集合 `s` です。これは二つの Kuratowski 成分のどちらにも到達する共通の中間体であり、`s` はスロット `q` の項目の要素であり、`u` と `v` は `s` の要素です。`v`、`u`、`s` の順に `γ` の先頭へ付け加えると、元よりアリティが三だけ大きい拡張された割り当て `δ` が得られます。以後、内向きの構成に要る材料はどれも、遊離した要素ではなく `δ` の項目になります。

```agda
    c = container (lookup q γ) u v e
    s : S
    s = c .fst
    δ : S ^ (suc (suc (suc m)))
    δ = v ∷ u ∷ s ∷ γ
```

二つの方向が、述べられた形に組み上がります。`adequate` は、`γ` での充足の判断が、真理値として、「スロット `q` の項目の射影」と「周囲の指示値」との、梱包された等式に等しいと述べます。`⇔toPath` が `out` と `into` の組の含意をこの経路に変えます。最初の応用として、`member e C` は表現 `e` の値が項 `C` の指示に属すると述べます。`C` の解釈の要素について有界に量化し、その要素で拡張した割り当てのもとで、表現を先頭スロットへずらした読み出しを要求します。

```agda
  adequate : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
            → (γ ⊨ read e ρ q) ≡ PairIs (fst (lookup q γ)) (value e (λ i → fst (lookup (ρ i) γ)))
  adequate e ρ q γ = ⇔toPath (out e ρ q γ) (into e ρ q γ)

  member : ∀ {n} → Expr n → Term S n → Formula S n
  member e C = ∃̇∈ C (read e suc zero)
```

`member` の外向きの読みは、截断された有界存在を消去し、要素 `x`、その所属の証明 `h`、そして `x` で拡張した割り当てが表現の読みを満たす証明 `p` を受け取ります。妥当性を外向きに `p` に適用すると等式 `fst x ≡ value e ...` が得られ、その等式に沿って `h` を輸送すれば、`fst x` の所属が表現の値の所属へ移ります。対象は所属命題 `value e ... ∈ fst (⟦ C ⟧ γ)` であり、その第二成分が `PT.rec` に必要な命題性の証明を与えます。

```agda
  member-out : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
              → ⟨ γ ⊨ member e C ⟩ → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩
  member-out e C γ = PT.rec (snd (value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ)))
    (λ { (x , h , p) → subst (λ v → ⟨ v ∈ fst (⟦ C ⟧ γ) ⟩) (out e suc zero (x ∷ γ) p) h })

  member-in : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
```

内向きの読みはその要素を示さねばなりませんが、表現 `e` の値そのものを模型の要素にすれば証人になります。前提によりそれは `fst (⟦ C ⟧ γ)` の要素であり、項の解釈は構成可能なので、`L` の推移性がその値の構成可能性の証明書を与えます。ここで `isL-trans` がしているのはまさにそれです。截断の消去は行われません。証明書と周囲の値を組にした明示的な模型要素 `x` が、有界存在の証人になります。拡張された割り当ての先頭は定義によりその値へ射影されるので、帰納的な `into` は経路 `refl` を受け取ります。

```agda
             → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩ → ⟨ γ ⊨ member e C ⟩
  member-in e C γ h = ∣ x , h , into e suc zero (x ∷ γ) refl ∣₁
    where
    x : S
    x = value e (λ i → fst (lookup i γ)) , isL-trans h (snd (⟦ C ⟧ γ))
```

最初の特殊化は、一般的な読み出しをタグの認識器に変えます。`tagAtL s k x` は、スロット `s` で「数項 `k` とスロット `x` の対」という表現を読むもので、したがって、スロット `s` の項目が `# k` とスロット `x` の項目の順序対であると主張する有界論理式です。再帰に現れる符号は、ペイロードと対になった数値のタグを帯びており、まさにこの形をしています。

```agda
tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = PairExpression.read
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)
```

その妥当性の補題は新しい証明を要りません。この表現について恒等リラベルで一般的な妥当性を実体化すると、その計算結果はすでに、充足の判断が、射影された項目と `pr (# k)` されたペイロードの `PairIs` と同一視されるというものです。これが本節全体の型です。表現を選び、`PairExpression.adequate` を引用すれば、節の意味が読み取れます。

```agda
  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s γ

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b = PairExpression.read
```

第二の特殊化は、それ自身が対であるようなペイロードを扱い、二層の対は表現の中に入れ子になっています。`tagPairAtL s k a b` は「数項 `k` と、スロット `a` と `b` の対との対」という表現を読むので、`pr (# k) (pr (entry a) (entry b))` の形の項目を認識します。タグが二成分のペイロードの上に載ったものです。

```agda
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))
```

妥当性の補題はここでも一般的なものから直接計算され、三つの成分すべてを、タグの数項と、射影後の二つのペイロードの項目とを取り戻します。入れ子は完全に表現の読み出しの内部で処理されます。この層の節から見えるのは、表現の形だけです。

```agda
      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s γ
```

## 外延によって集合を定める

前節の構造的な読みは Kuratowski 対の層を通して値を認識しましたが、多くの再帰の節が語りたいのは、ある集合の要素が何であるかということです。両者は同じ種類の主張、すなわち模型の中の一階の論理式が、周囲の階層へ読み戻されたときにスロットの値をちょうど指し示す、という形をしています。本節ではその外延的な形を作ります。

`extAt` y φ は、スロット `y` の集合について、その要素が一変数の条件 `φ` を満たす対象とちょうど一致することを述べます。外側の構造は、普通の連言で結ばれた二つの非有界な全称量化です。一方は集合への所属から `φ` への含意、もう一方は逆向きの含意です。`extAt` 自体は新たな命題の切り捨てを導入しませんが、パラメータ `φ` は任意の論理式であり、その内部に量化子や切り捨てられた存在を含むことはあります。外側の証拠が素の連言であるため、二つの読みは連言の射影そのもの、導入もそれらの順序対そのものになります。これは記述としてちょうどよい強さです。この論理式は候補となる集合を特徴づけるだけで、そのような集合が存在するかどうかには何も言いません。存在は、後で値を供給する構成の仕事です。

この定義は候補のための新しい変数を一つ束縛し、全体として二つの非有界な全称量化の連言です。すなわち、スロット `y` の集合のすべての要素が `φ` を満たすこと、そして `φ` を満たすすべてのものが要素であること。外側の結合子は普通の連言であり、`extAt` はどちらの含意も切り捨てで包みませんが、条件 `φ` はそのまま渡され、量化子や切り捨てられた存在を内部に含む任意の論理式であって構いません。`extAt` 自体が確定するのは外側の形だけです。量化子の下にある二つの含意の対であり、各側は模型の要素とその充足の証明の上の関数です。これこそ、この論理式が記述として機能する理由です。値を束縛するだけで、値の存在を主張することはないのです。

```agda
extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
```

二つの読みは、外側の連言の二つの射影です。`extAt y φ` の要素から出発して、`extAt-out` は第一の成分を取ります。これはすべての模型の要素 `z` に対して、`fst z` がスロット `y` の集合に属することから、拡張された環境での `φ` の充足への含意を割り当てます。`extAt-in` は第二の成分を取り、同じ含意を逆向きに与えます。どちらの読みも切り捨ての除去も証人の選択も経路に沿う輸送も行いません。`φ` の内部に何があっても、この外側の層では証拠は順序対であり、各読みは文字どおりその射影です。

```agda
            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd
```

導入は射影を逆向きに走らせるもので、二つの含意をそれぞれ関数として与えたときの順序対です。そこで `extAt-in-both` が成り立ちます。条件の両方向をともに確立できる節は、二つの関数を対にするだけでこの論理式を充足し、外側の層ではそれ以上の仕事は要りません。量化子や切り捨てに伴う仕事はすべて `φ` の内部で起き、そこで片づけられます。この主張はそのまま読む価値があります。二つの関数から充足の判断の要素を作るのであって、`φ` を満たす要素をもつ集合の存在については何も主張しません。そのような集合が実際に供給されるかどうかは、値が構成される側で決まる事柄であり、ここではありません。

```agda
  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g
```

## 二層の鍵を読む

充足関係の再帰における鍵は、二層の入れ子になった対から組み上げられた集合です。アリティと符号との対であり、符号そのものはタグの数項とペイロードとの対です。したがって有界な論理式で鍵を認識するとは、この二層の対を検査することですが、構造的な読みは任意の入れ子の式をすでに扱えるので、その任に十分に応えます。そこで以下の各論理式は適切な式に読みを適用したものであり、各妥当性補題は `PairExpression.adequate` の対応する特殊化です。アリティが数項に固定されず変数スロットとして残されているのは意図的なことです。異なるアリティの部分論理式を生む構成子の節は、アリティの値そのものについて語る必要があるからです。

`arityTagPairAtL c ar k a b` は、スロット `c` の集合が順序対であることを述べます。第一成分はスロット `ar` の集合であり、第二成分はさらに、`# k` という数項とスロット `a`、`b` の集合の対との対です。定義式は `pair (slot ar) (pair (numeral k) (pair (slot a) (slot b)))` という形で、恒等リラベルの下で `c` において読まれます。これはペイロードが二スロットの符号である鍵の形状です。

```agda
arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c
```

妥当性の主張は、この論理式の真理値を命題 `PairIs (fst (lookup c γ)) (...)`、すなわち周囲の階層におけるパスと同一視します。これは `c` の集合が各スロットの射影から組み上げられた入れ子の Kuratowski 対に等しいと述べるものです。各成分は右辺から読み取れます。タグの数項 `# k` は固定されており、`ar`、`a`、`b` はそれぞれ参照された値を寄与します。この主張は一方向の含意ではなく真理値の間のパスなので、後の証明ではどちらの方向にも書き換えに使えます。

```agda
arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))
```

証明は `PairExpression.adequate` を同じ式、同じリラベル、同じスロットに適用する一行の特殊化です。有界な証人、截断された存在の除去と導入、`prAtL` の妥当性に沿う輸送はすべて構造定理で一度に片づけられているため、ここに新しい意味論的議論は現れません。対ペイロードの場合が整うと、一つのペイロードを持つ変種 `arityTagAtL c ar k a` が同じ仕方で定義されます。違いは最も内側の式が二つのスロットの対ではなく単一のスロット `a` である点だけです。

```agda
arityTagPairAtL-adequate c ar k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c γ

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n
```

本体は恒等リラベルの下で `c` において構造的な読みを適用するものであり、妥当性の主張もやはり `PairIs` のパスの形をとります。すなわち `c` の集合は、アリティの値と「`# k` と `a` の値の対」との対に等しいということです。符号のペイロードが二つではなく単一のスロットである場合、たとえば変数の番号一つや部分論理式のスロット一つである場合に、必要なのはまさにこの形です。

```agda
arityTagAtL c ar k a = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)
```

妥当性の証明はここでも、同じ式とスロットに対して `PairExpression.adequate` を引用するもので、対の場合と同じ作法です。したがって二つのアリティ付きタグ論理式と二つの妥当性補題は、唯一の構造定理の上に立ちます。読みを汎用的に作ったことの見返りがこれです。復元されたアリティの値をその後どう扱うかは、充足関係の再帰の節に属する事柄であり、それらの節は `L.Coding.SatisfactionClauses` で述べられます。本章が供給するのは、それらの節が読む形状です。

```agda
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c γ
```

## 表から部分符号を引く

充足関係表のエントリは、アリティと符号からなる鍵に対して、その論理式を充足する環境の集合を記録します。したがって部分論理式の値を読むとは、その鍵を対象言語の内部で作ること、すなわちアリティと部分符号の対を作り、候補となる集合との等しさを主張することを意味します。部分論理式自身のアリティでは表の項目を全称量化し、鍵の等式を含意の前件として一致する項目を選びます。部分論理式が変数を束縛するときには、同じ参照が次のアリティで行われ、そのアリティは次節の後者の論理式が内部で証人となります。

## 節の共通形

再帰の一つの節は、符号、そのアリティ、ペイロードの成分、そして符号の位置に記録された値を束縛し、符号のタグ付きの形を述べ、記録された値の間で構成子ごとの条件を一つ述べます。節を読み戻すことは、本章で確立した妥当性の補題に沿った書き換えの連鎖であり、節を組み立てることは、その書き換えを逆向きに走らせることです。

## 正の結合子

論理積と論理和にとって、構成子ごとの条件は小さなものです。符号の位置の値は二つの部分値の逐点連言、それぞれ逐点選言であり、いずれも同じアリティの表から読み出されます。この条件のほかに節が要るものは、上の参照の仕組みだけです。

## 周囲の環境集合

`envSetAt` は、外延による特徴づけによって、あるスロットにあるアリティの、別のスロットの台の上での環境の集合を記述します。これは集合を特徴づけるのであって、構成するのではありません。

この定義は、外延による特徴づけをスロット `E` に適用し、条件として環境の述語 `envOverAt` をとります。この述語は定義域と値域に対して一つの候補環境を分類するものなので、`extAt` が新たに束縛する変数 (拡張された環境の位置 0) が候補の役割を果たします。定義域と値域の引数が `suc ar` と `suc B` と現れるのは、条件が拡張された環境で評価されるからであり、論理式自身が束縛するスロットより一つアリティが上です。射影 `extAt-out` と `extAt-in` により、`envSetAt E ar B` の証明はちょうど二つの含意を与えるもの、すなわち `E` の集合が、`ar` に記録されたアリティの上で `B` の台が受け入れる候補環境をちょうど含む、と言うものになります。この論理式は集合を記述するだけで、その構成は充足関係表が作られる場所で行われます。

```agda
envSetAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envSetAt E ar B = extAt E (envOverAt zero (suc ar) (suc B))
```

## 含意と偽

論理の節のうち、含意と偽は、その値の形において正の結合子と一線を画します。偽には部分符号がなく、共通の外延の枠組みの中で条件が偽なので、その値は空です。ただし枠組みが束縛する周囲の環境集合は使います。含意は、符号のアリティにおけるすべての環境の集合の上で解釈されるため、その節はその周囲の集合を名指し、外延的に制約しなければなりません。前節の環境の集合が存在するのはまさにこのためです。含意は「補集合と後件の結び」ではなく含意として述べられるとき、`hProp` 上の関数空間の含意と一致します。含意を直接用いれば、排中律を呼び出さずに構成的な意味論と一致します。

## 次のアリティ

`sucAtL` は、スロット `j` の集合がスロット `i` の集合の `sucV` であることを述べる内部論理式です。その妥当性補題は任意の集合に適用でき、数項や順序数であることを仮定しません。

部分論理式が一つ高いアリティにある節は、現在のアリティの後続であると制約されたアリティで表を参照します。階層側の論理式 `sucAt` はこの集合の等式を表し、定数を含みません。持ち上げには `liftFo` が要求する `BoundedFo InL` の引数が必要です。これとは別の定理 `Δ₀-sucAt` は、後で `transferFo` に渡され、有界絶対性を正当化します。

定義は `sucAtL i j = liftFo (sucAt i j) _` です。`sucAt` は定数を含まないため、その `BoundedFo InL` の引数には非自明な定数の構成可能性の証人はありません。妥当性の証明では、`transferFo` はこの引数と、階層側の Δ₀ 証明書である `Δ₀-sucAt i j` とを別々に受け取ります。得られるパスは充足を `PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))`、すなわちスロット `j` の集合がスロット `i` の集合の後続集合であるという命題と同一視します。

```agda
sucAtL : ∀ {n} → Fin n → Fin n → Formula S n
sucAtL i j = liftFo (sucAt i j) _

sucAtL-adequate : ∀ {n} (i j : Fin n) (γ : S ^ n)
  → (γ ⊨ sucAtL i j) ≡ PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))
sucAtL-adequate i j γ =
```

証明は三つのパスを連結します。まず転送の補題が有界性の証明書を使い、持ち上げられた論理式の `L` での充足を、射影された割り当て `map fst γ` での `sucAt i j` の周囲の充足と等しいとします。転送は確立された推移的モデルの設定に依拠します。次に階層側の妥当性定理 `sucAt-adequate` が、その充足を解釈された値の間の等式へ書き換えます。最後に `lookup-fst` が射影された割り当てでの二度の参照を `γ` での参照の射影へ移し、合同が `sucV` を内側へ移し、`cong₂` が等式を `PairIs` の下で組み立て直します。得られるのは述べられた同一視です。

```agda
    transferFo (sucAt i j) _ (Δ₀-sucAt i j) γ
  ∙ sucAt-adequate i j (map fst γ)
  ∙ cong₂ PairIs (lookup-fst j γ) (cong sucV (lookup-fst i γ))
```

## 環境を拡張する

`consAtL` は新しい先頭値による環境の拡張を記述し、その妥当性補題が得られる符号化環境を正確に同一視します。

量化された本体は、現在の環境の先頭に値を一つ加えた環境で評価されます。階層側の論理式 `consAt` はこの操作をすでに特徴づけており、`consAtL` は同じ特徴づけを構成可能模型の内部で表します。持ち上げには、符号化された拡張を組み立てる単集合、対、タグ、鍵の移動の各関係について有界性の証明が必要です。これらの関係は定数の数項を導入しません。指定されたタグは空集合であり、新しい先頭値はスロット `m` から読まれます。直後にここで定義される独立の補題 `numL` は、数項を実際に名指す別の有界論理式のために、周囲の数項の構成可能性を記録します。

`numL k` はここで定義され、周囲の数項 `# k` が構成可能であることを示します。内部数項 `numeralL k` はその射影の構成可能性をすでに備え、`numeralL-fst k` がその射影を `# k` と同一視します。このパスに沿って証明を輸送すると `⟨ isL (# k) ⟩` が得られます。続く非公開の定義は、空のタグを認識する論理式について `BoundedFo InL` のデータを与えます。これは有界な形と、現れる定数の構成可能性の証人を組み合わせたものです。特に `sgl0At k` はスロット `k` の集合を `{∅}` と特徴づけます。空の要素をもち、すべての要素が空であるという条件です。`bddSgl0` はこの組み合わせたデータを与えるもので、独立な Δ₀ 定理ではありません。

```agda
numL : (k : ℕ) → InL (# k)
numL k = subst (λ w → ⟨ isL w ⟩) (numeralL-fst k) (numeralL k .snd)

private
  bddSgl0 : ∀ {n} (k : Fin n) → BoundedFo InL (sgl0At k)
  bddSgl0 k = (_ , (_ , _)) , (_ , (_ , _))
```

`pair0At k j` は、スロット `k` の集合を非順序対 `{∅, W}` と特徴づけます。ここで `W` は元の割り当てのスロット `j` の値であり、内側の量化子に入ると同じ値を `suc j` が指します。二つのスロットの値からなる Kuratowski 対ではありません。`tag0At s x` は `sgl0At` と `pair0At` を組み合わせます。指定された二要素が `{∅}` と `{∅, W}` なので、スロット `s` の集合は Kuratowski 対 `pr ∅ W` です。`bddPair0` と `bddTag0` は、これらの記述の `BoundedFo InL` データを与え、必要な定数の構成可能性の証人も含みます。

```agda
  bddPair0 : ∀ {n} (k j : Fin n) → BoundedFo InL (pair0At k j)
  bddPair0 k j = (_ , (_ , _)) , ((_ , _) , (_ , ((_ , _) , (_ , _))))

  bddTag0 : ∀ {n} (s x : Fin n) → BoundedFo InL (tag0At s x)
  bddTag0 {n} s x =
      (_ , bddSgl0 {suc n} zero)
```

`bddTag0` の残りの部分は、空集合タグ自体に使う単集合の証明書と、外側と内側の対の層のための証明書とを対にします。その後の `bddShift` は `shiftPairAt p' p` を証明します。すなわち `p'` の項目は、`p` の項目の数項の鍵をその後者に置き換え、対になった値はそのままにして得られるものとして認識されます。ここで証明書を単一のプレースホルダとして書けるのは、論理式の有界な部分論理式が、すでに扱った葉と有界量化子と同じだからです。

```agda
    , ( (_ , bddPair0 {suc n} zero (suc x))
      , (_ , (bddSgl0 {suc n} zero , bddPair0 {suc n} zero (suc x))) )

  bddShift : ∀ {n} (p' p : Fin n) → BoundedFo InL (shiftPairAt p' p)
  bddShift p' p = _

  bddCons : ∀ {n} (e' m e : Fin n) → BoundedFo InL (consAt e' m e)
```

`bddCons` は拡張の論理式が必要とするすべてを組み立てます。三つの連言を読むと、拡張されたグラフは `m` の値の上に載った空集合タグである項目、すなわち新しい先頭の項目を保持し、ずらしたスロットでの `bddTag0` が証明します。旧グラフの各項目は鍵を後者へずらして現れ、二つアリティが上の `bddShift` が証明します。残りの連言は、拡張の外へ読み出す所属の方向について同じ二つの証明書を繰り返します。各連言の証明書はその量化子が作る深さに置かれるため、注釈のアリティが `suc (suc n)` まで増えるのです。

```agda
  bddCons {n} e' m e =
      (_ , bddTag0 {suc n} zero (suc m))
    , ( (_ , (_ , bddShift {suc (suc n)} zero (suc zero)))
      , (_ , ( bddTag0 {suc n} zero (suc m)
             , (_ , bddShift {suc (suc n)} (suc zero) zero) )) )
```

有界性の証明書がそろうと、`consAtL e' m e` は階層側の論理式 `consAt e' m e` を `liftFo` で持ち上げたものであり、その証明書として `bddCons` が与えられます。この妥当性の主張には、後者の場合にはなかった条件が付きます。族 `g : Fin k → V ℓ` と、スロット `e` に置かれた集合が符号化環境 `env g` であるという証明 `hE` を仮定するのです。その仮定の下で、`consAtL e' m e` の充足は、真理値として `PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))` と同一視されます。すなわち `e'` の集合は、`m` の値を `g` の先頭に付け加えて得られる符号化環境にほかなりません。この論理式は、すでに符号化された環境に対して候補を分類するものであって、環境を構成するものではありません。旧環境についての仮定こそ、この分類を意味の定まったものにする前提です。

```agda
consAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
consAtL e' m e = liftFo (consAt e' m e) (bddCons e' m e)

consAtL-adequate : ∀ {n} (e' m e : Fin n) (γ : S ^ n)
  {k : ℕ} (g : Fin k → V ℓ)
  → fst (lookup e γ) ≡ env g
```

証明は転送の補題から始まり、その入力は一度にすべて与えられます。論理式 `consAt e' m e`、その有界性の証明書 `bddCons`、そして階層側で記録された Δ₀ の証明書 `Δ₀-consAt` です。このステップは有界絶対性の実際の働きであり、確立された推移的モデルの設定に依存します。`L` が推移的であり、論理式が名指す定数がすべて構成可能であることから、持ち上げられた論理式の台での充足は、射影された割り当て `map fst γ` での元の論理式の充足へと移ります。そこでは周囲の事実を直接述べることができます。

```agda
  → (γ ⊨ consAtL e' m e)
  ≡ PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))
consAtL-adequate e' m e γ g hE =
    transferFo (consAt e' m e) (bddCons e' m e) (Δ₀-consAt e' m e) γ
  ∙ consAt-adequate e' m e (map fst γ) g
```

階層側の妥当性定理 `consAt-adequate` は次に、周囲の充足を、新しいスロットと拡張された符号化環境との同一視へ書き換えます。仮定は射影された形で必要なので、入り口で `lookup-fst e γ` が `hE` と連結されます。すなわち `e` の項目の射影は `env g` に等しいのです。続いて合同が残る二度の参照を移します。`e'` の値は `lookup-fst` で、`m` の値は関数 `λ w → env (cons w g)` の下で `cong` で処理されます。経路の連鎖は約束された `PairIs` の同一視でちょうど終わります。これで本章固有の数学は閉じます。構文の形、アリティ、環境、そしてその拡張を認識するのに必要な内部論理式は、すべてここに揃いました。

```agda
      (lookup-fst e γ ∙ hE)
  ∙ cong₂ PairIs (lookup-fst e' γ)
      (cong (λ w → env (cons w g)) (lookup-fst m γ))
```

## 非有界量化子

二つの非有界量化子の節は、共通の有界な枠 `extB` を使います。この枠は周囲の環境集合 `F` と拡張のデータを束縛してから、量化子固有の本体を適用します。`quBody q` では、引数 `q` は台の集合 `w` を走る外側の量化子であり、存在の場合は有界存在、全称の場合は有界全称です。拡張された環境が本体に記録された値に現れることを述べる内側の論理式 `∃̇∈ ya (consAtL ...)` は、どちらの場合にも変わりません。したがって全称の場合に変わるのは外側の量化子だけで、最も内側の連言を含意へ置き換えるのではありません。

## 項の評価と二つの原子論理式

項は変数か定数です。したがって符号化された項を評価する節には二つの場合があります。変数の値は環境がその鍵に記録するものであり、定数の値はその定数そのものであり、どの環境でも同じです。二つの原子論理式はその後、両方の項の符号を評価して、得られた値を模型の中で比較します。一方は所属を、他方は等式を主張します。そのペイロードは項の符号の対であり、充足関係表にはそこにエントリがないため、この節は枠組みに任せずに自分で参照を作るのです。

## 有界量化子

有界量化子のペイロードは、項の符号と論理式の符号の対です。境界は二つの場合をもつ評価の読みによって環境の中で評価され、本体の値はひとつアリティ上で読まれ、付け加えられる値は台と評価された境界の両方の要素に限られます。台と境界の両方を渡ることは冗長ではありません。参照意味論は台の上で量化し、境界への所属で防ぎます。境界は台の外に要素をもつことも十分にあり得るので、境界だけを渡る量化は、表がもたないエントリを要求することになります。

## まとめ

本章は、符号化された充足関係の節が `L` の内部で複合的な値を認識するための一階論理式を組み立てました。それを支えるのは三種類の主張です。表現の読みの構造的な妥当性は、スロット、リテラル、数項、Kuratowski 対についての論理式の充足を、両方向で、射影された項目と指示された周囲の値の等しさと同一視します。対の場合は構成可能な中間集合を通って行われます。外延的な特徴づけ `extAt` は二つの全称含意の普通の連言であり、その読みと導入は射影と対です。そして内部の後者の論理式と環境拡張の論理式は、推移的モデルの上の有界絶対性によって持ち上げられ、その妥当性の経路は転送された充足、階層側の定理、射影の下での参照の相容性から連結されます。符号化充足関係の再帰を成す節の形状は、この上に立ちます。