```agda
open Alphabet W
private module DB = Semantic.DB W
private module Sem = Semantic.SemB W
```
小モデルの充足判断を `⊨ᴮ`、項の値づけを `⟦_⟧ᴮ` と改名する。これにより、橋渡しの議論では、この二つを章の前半で使った周囲の階層の充足 `⊨` と区別できる。
```agda
private
open Sem.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
```
論理式 `ψ` のメタレベルの環境 `δ` での意味論的な意味は、定数を付け替えた論理式が、`W` が担う小さなモデルの中で充足されることである。これが、橋が対象言語の表の項目を結びつける目標の意味論である。
```agda
Meaning : ∀ {n} → Formula Ab n → Vec DB.SM n → hProp (ℓ-suc ℓ)
Meaning ψ δ = δ ⊨ᴮ mapFo DB.ι ψ
```
基礎の集合 `Wv` は、小モデルの量化子が走る台である。これを表示 `W : S` と区別しておくことは、後の橋にとって重要である。対象言語の所属は集合 `Wv` を使い、構成可能性の証拠は `W` の第二成分に残る。したがって橋が量化するのは固定されたモデルの要素であり、すべての構成可能集合ではない。
```agda
private
Wv = W .fst
```
対応 `toS` は、アルファベット `Ab` の上の論理式のすべての定数を、構造 `S` の対応する定数へ付け替え、周囲の充足で判定できる `S` の上の論理式を作る。
```agda
toS : ∀ {n} → Formula Ab n → Formula S n
toS = mapFo (asConst W)
```
構成可能な充足集合 `SatW ψ` は、付け替えられた論理式を満たす符号化された環境を集める。それは充足を定義する内部の再帰の出力なので、`L` の要素である。
```agda
SatW : ∀ {n} → Formula Ab n → S
SatW ψ = Sat W (toS ψ)
```
`SatW ψ` への所属の外向きの読み出しは、内部の充足の所属の仕様から従う。`SatW ψ` の要素は、正しいアリティの環境の集合に属し、付け替えられた論理式の条件を満たす、符号化された環境である。
```agda
Sat-out : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ z .fst ∈ (SatW ψ) .fst ⟩
→ ⟨ z .fst ∈ (envSet W n) .fst ⟩ × ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩
Sat-out ψ z h = subst ⟨_⟩ (Sat-mem W (toS ψ) z) h
```
内向きの方向は、正しい環境集合への所属と再帰条件という二つの事実から出発し、その対を `Sat-mem` に沿って逆向きに輸送することで `SatW ψ` への所属を得る。したがって `Sat-out` と `Sat-in` は、所属の仕様が与えるパスに沿う二方向の輸送そのものであり、追加の意味論的仮定を必要としない。
```agda
Sat-in : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ z .fst ∈ (envSet W n) .fst ⟩
→ ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ → ⟨ z .fst ∈ (SatW ψ) .fst ⟩
Sat-in ψ z hz hc = subst ⟨_⟩ (sym (Sat-mem W (toS ψ) z)) (hz , hc)
```
補題 `extension-path` は、各点における真理値のパスを `SatW ψ` の正確な外延定理へ変える。符号化された各環境 `z` について、その前提は再帰条件 `cond W (toS ψ)` を目標命題 `P z` と同定する。`Sat-mem` の二方向を用いると、結論は `SatW ψ` の要素が、`P` を満たす `envSet W n` の要素にちょうど一致すると述べる。ここでは `z` を復号せず、環境ベクトルの代表も選ばない。
```agda
private
extension-path : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
→ ((z : S) → ((z ∷ []) ⊨ cond W (toS ψ)) ≡ P z)
→ ExtFact ((SatW ψ) .fst) ((envSet W n) .fst) (λ z → ⟨ P z ⟩)
extension-path ψ P e =
```
外向きの方向は、`Sat-out` を通して `SatW ψ` への所属の二つの成分を読み、各点の等式に沿って条件を運ぶ。内向きの方向は、性質を運び戻して `Sat-in` を適用する。どちらの方向も、代表を選ぶことなく、各点の等式だけを使う。
```agda
(λ z hz → Sat-out ψ z hz .fst , subst ⟨_⟩ (e z) (Sat-out ψ z hz .snd))
, (λ z hz hp → Sat-in ψ z hz (subst ⟨_⟩ (sym (e z)) hp))
```
偽の場合、目標の性質はどの `z` に対しても要素を持たない。もし `z` が `SatW ⊥̇` に属すれば、`Sat-out` は不可能な偽の充足を取り出す。逆に、その不可能な性質の証明を仮定すれば、候補は直ちに除去できる。残る成分は、仮に要素があれば正しいアリティを持つことを記録するだけなので、`botBridge` は `envSet W n` の内部で空の外延を与える。
```agda
botBridge : (n : ℕ) {k : ℕ} (env : Vec S k)
→ ExtFact ((SatW (⊥̇ {n = n})) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ env) ⊨ ⊥̇ ⟩)
botBridge n env = (λ z hz → Sat-out ⊥̇ z hz .fst , Sat-out ⊥̇ z hz .snd) , (λ z hz b → ⊥*-rec b)
```
`env` の枠 `ya` と `yb` が、それぞれ `a` と `b` の充足集合の基礎の集合を持つと仮定する。連言の橋は `SatW (a ∧̇ b)` を、二つの子の充足集合の両方に属する符号化環境 `z` として特徴付ける。本体を評価する前に `z` が環境の先頭へ加えられるため、元の枠は `suc ya` と `suc yb` で参照され、`i0` が `z` を指す。この移動が、表示された論理式に記録されたホスト側の `Fin` 境界である。
```agda
andBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : Vec S k) (ya yb : Fin k)
→ (lookup ya env) .fst ≡ (SatW a) .fst → (lookup yb env) .fst ≡ (SatW b) .fst
→ ExtFact ((SatW (a ∧̇ b)) .fst) ((envSet W n) .fst)
(λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)) ⟩)
andBridge a b env ya yb qa qb = extension-path (a ∧̇ b)
```
連言では、点ごとのパスが同じ候補環境 `z` の二つの記述を比較する。再帰条件は `z` が `SatW a` と `SatW b` の両方に属すことを述べ、二つの所属を `qa` と `qb` に沿って輸送すると、節の本体にある二つの対象言語の所属原子がちょうど得られる。この段階では子環境を復号しない。
```agda
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)))
(λ z i → (z .fst ∈ sym qa i) ⊓ (z .fst ∈ sym qb i))
```
選言の橋渡しは正確な外延記述を与える。ある環境が `SatW (a ∨̇ b)` に属すのは、それが `envSet W n` に属し、さらに節の環境の先頭に置いたとき、`a` の値または `b` の値に属すという対象言語の選言を満たすとき、そのときに限る。
```agda
orBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : Vec S k) (ya yb : Fin k)
→ (lookup ya env) .fst ≡ (SatW a) .fst → (lookup yb env) .fst ≡ (SatW b) .fst
→ ExtFact ((SatW (a ∨̇ b)) .fst) ((envSet W n) .fst)
(λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)) ⟩)
orBridge a b env ya yb qa qb = extension-path (a ∨̇ b)
```
選言の点ごとの比較は、同じ `z` の所属を二つのスロット等式に沿って輸送する。二つの選択肢は `z` の `SatW a` への所属と `SatW b` への所属であり、対象言語の選言はこの選択を正確に記録する。ここで別の環境の証人が作られることはない。
```agda
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)))
(λ z i → (z .fst ∈ sym qa i) ⊔ (z .fst ∈ sym qb i))
```
含意の橋渡しも、環境集合の内部で `SatW (a ⇒̇ b)` を特徴づける。候補環境 `z` における節の本体は、`z` が前件の値に属すならば、同じ `z` が後件の値に属すと述べる。
```agda
impBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : Vec S k) (ya yb : Fin k)
→ (lookup ya env) .fst ≡ (SatW a) .fst → (lookup yb env) .fst ≡ (SatW b) .fst
→ ExtFact ((SatW (a ⇒̇ b)) .fst) ((envSet W n) .fst)
(λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)) ⟩)
impBridge a b env ya yb qa qb = extension-path (a ⇒̇ b)
```
ここで必要なのは点ごとのパスである。`qa` と `qb` は前件と後件の値のスロットをそれぞれ `SatW a` と `SatW b` と同定する。これらの等式に沿って輸送すると、対象言語の含意は含意の再帰条件となり、環境そのものは変わらない。
```agda
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)))
(λ z i → (z .fst ∈ sym qa i) ⇒ (z .fst ∈ sym qb i))
```
二つの非有界量化子の本体は、まず `wi` が名指す台の上で量化する。存在の本体は台のある要素 `x` を求め、全称の本体はそのようなすべての `x` を扱う。どちらの場合も内側の有界存在が子論理式の値から項目を取り、それが `x` を古い環境の先頭に加えて得られるグラフであることを要求する。
```agda
quEx quAll : ∀ {k} → Fin k → Fin k → Formula S (1 + k)
quEx wi yai = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
quAll wi yai = ∀̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
```
補題 `direct-extension` は、量化子と原子の橋渡しに共通する議論を取り出す。`z` がベクトル `δ` のグラフと同定されたなら、`Meaning ψ δ` と節が表す性質 `P z` の間の両方向の写像を仮定し、`SatW ψ` が `envSet W n` のうち `P` を満たす部分にちょうど等しいことを示す。`δ` の復元は終始切り詰めの内側に保たれる。
```agda
private
direct-extension : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
→ ((δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ → ⟨ Meaning ψ δ ⟩ → ⟨ P z ⟩)
→ ((δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ → ⟨ P z ⟩ → ⟨ Meaning ψ δ ⟩)
→ ExtFact ((SatW ψ) .fst) ((envSet W n) .fst) (λ z → ⟨ P z ⟩)
```
外向きの半分では、まず `Sat-out` が `z` の環境集合への所属を与える。次に切り詰められた復元定理から、ベクトル `δ` と `z` をそのグラフに同定する等式を得る。命題 `P z` の内部で `Sat-small-spec` が元の `z ∈ SatW ψ` を `Meaning ψ δ` に移し、前向きの仮定が議論を終える。
```agda
direct-extension {n} ψ P f b = out , inn
where
out : (z : S) → ⟨ z .fst ∈ (SatW ψ) .fst ⟩ → ⟨ z .fst ∈ (envSet W n) .fst ⟩ × ⟨ P z ⟩
out z hz = Sat-out ψ z hz .fst , rec₁ ((P z) .snd)
(λ { (δ , q) → f δ z q (subst ⟨_⟩ (Semantic.Sat-small-spec W ψ δ z q) hz) })
```
内向きの半分でも、環境集合への所属から得られるのは切り詰められた組 `δ , q` だけである。逆向きの仮定が `P z` を `Meaning ψ δ` に送り、`Sat-small-spec` の逆向きが `z ∈ SatW ψ` を返す。目標の所属は命題なので、この切り詰めの消去は正当であり、復号ベクトルを大域的に選ぶことはない。
```agda
(Semantic.envSet-vectors W z (Sat-out ψ z hz .fst))
inn : (z : S) → ⟨ z .fst ∈ (envSet W n) .fst ⟩ → ⟨ P z ⟩ → ⟨ z .fst ∈ (SatW ψ) .fst ⟩
inn z hz hp = rec₁ ((z .fst ∈ (SatW ψ) .fst) .snd)
(λ { (δ , q) → subst ⟨_⟩ (sym (Semantic.Sat-small-spec W ψ δ z q)) (b δ z q hp) })
(Semantic.envSet-vectors W z hz)
```
補題 `child` は、一つの束縛変数について符号化された見方と意味論的な見方をそろえる。古い符号化環境が `δ` のグラフであり、名指された子論理式の値が `SatW a` なら、その値のある要素が `x` を古い環境の先頭に加えて得られるグラフであるという主張は、`Meaning a (x ∷ δ)` と命題として等しくなる。
```agda
child : ∀ {n k} (a : Formula Ab (suc n)) (δ : Vec DB.SM n) (x : DB.SM)
(γ : Vec S k) (zi yai : Fin k) → (lookup zi γ) .fst ≡ Semantic.graph W δ
→ (lookup yai γ) .fst ≡ (SatW a) .fst
→ ((Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)))
≡ Meaning a (x ∷ δ)
```
証明は `⇔toPath` で結ばれた一対の含意である。外向きの方向では、有界存在の切り詰められた証人を消去する。その証人は、子論理式の値に属する一つの項目と、その項目が `x` を古い環境の先頭に加えて得られるグラフであることを示す `consAtL` の証拠である。
```agda
child a δ x γ zi yai qz qa = ⇔toPath out inn
where
out : ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
→ ⟨ Meaning a (x ∷ δ) ⟩
out = rec₁ ((Meaning a (x ∷ δ)) .snd) (λ { (e , he , hc) →
```
外向きには、有界存在を命題 `Meaning a (x ∷ δ)` の中へ消去する。先頭追加の節と古いグラフの等式によって、証人 `e` は `x ∷ δ` のグラフと同定される。さらに `qa` が `e` の所属を `SatW a` への所属に書き換え、`Sat-small-spec` が求める意味論的充足を与える。
```agda
subst ⟨_⟩ (Semantic.Sat-small-spec W a (x ∷ δ) e
(Semantic.consAtL-out W δ x (e ∷ Semantic.intoL W x ∷ γ) i0 i1 (sh 2 zi) qz refl hc))
(subst (λ X → ⟨ e .fst ∈ X ⟩) qa he) })
inn : ⟨ Meaning a (x ∷ δ) ⟩
→ ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
```
内向きの方向では、正準な拡張環境 `envFor W (x ∷ δ)` を構成する。small-spec のパスを逆向きに読むと、意味論的充足はこの環境が `SatW a` に属することへ移る。続いて `consAtL-in` が、同じ環境と古い環境の間に必要なグラフ拡張の関係が成り立つことを示す。
```agda
inn h = ∣ Semantic.envFor W (x ∷ δ)
, subst (λ X → ⟨ (Semantic.envFor W (x ∷ δ)) .fst ∈ X ⟩) (sym qa)
(subst ⟨_⟩ (sym (Semantic.Sat-small-spec W a (x ∷ δ) (Semantic.envFor W (x ∷ δ))
(Semantic.envFor-graph W (x ∷ δ)))) h)
, Semantic.consAtL-in W δ x (Semantic.envFor W (x ∷ δ) ∷ Semantic.intoL W x ∷ γ)
```
`consAtL-in` の残りの引数は、古いグラフの等式 `qz`、新しい先頭要素 `x` の反射的な同定、そして拡張ベクトルに対する `envFor-graph` を与える。これらのデータが内向きの証人を閉じ、同値を完成させる。
```agda
i0 i1 (sh 2 zi) qz refl (Semantic.envFor-graph W (x ∷ δ)) ∣₁
```
存在の橋渡しは、量化子に関する最初の結果である。環境の集合の上での `∃̇ a` の内部の値への所属は、台の上で有界存在の形 `quEx` を充足することと同じであり、二つのスロットの等式が台と子の値を名指す。
```agda
exBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : Vec S k) (wi yai : Fin k)
→ (lookup wi γ) .fst ≡ Wv → (lookup yai γ) .fst ≡ (SatW a) .fst
→ ExtFact ((SatW (∃̇ a)) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ γ) ⊨ quEx wi yai ⟩)
exBridge a γ wi yai qw qa = direct-extension (∃̇ a) (λ z → (z ∷ γ) ⊨ quEx wi yai)
(λ δ z qz → map₁ (λ { (x , h) → Semantic.intoL W x
```
存在の橋渡しでは、`direct-extension` の後に残るのは `child` が与える二つの変換だけである。意味論的充足からは、切り詰めの中の模型要素 `x` を `L` に埋め込み、外側の有界な証人とする。逆に、対象言語で名指された台に属す証人を制限模型の要素として受け取り、`child` を通して読む。どちらの変換も命題的切り詰めの内側で行われる。
```agda
, subst (λ X → ⟨ x .fst ∈ X ⟩) (sym qw) (x .snd)
, subst ⟨_⟩ (sym (child a δ x (z ∷ γ) i0 (suc yai) qz qa)) h }))
(λ δ z qz → map₁ (λ { (x , hx , h) → (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
, subst ⟨_⟩ (child a δ (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
(z ∷ γ) i0 (suc yai) qz qa) h }))
```
全称の橋渡しは `∀̇ a` に対して同じ外延的事実を述べる。内部の値が環境を含むのは、台のすべての要素をその環境の先頭に加えたときに子論理式が充足される場合であり、またその場合に限られる。
```agda
allBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : Vec S k) (wi yai : Fin k)
→ (lookup wi γ) .fst ≡ Wv → (lookup yai γ) .fst ≡ (SatW a) .fst
→ ExtFact ((SatW (∀̇ a)) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ γ) ⊨ quAll wi yai ⟩)
allBridge a γ wi yai qw qa = direct-extension (∀̇ a) (λ z → (z ∷ γ) ⊨ quAll wi yai)
(λ δ z qz h x hx → subst ⟨_⟩
```
`direct-extension` が要求する前向きの写像では、名指された台の任意の対象レベルの要素を制限模型の要素に変え、意味論的な全称の仮定を適用し、`child` を意味論的充足から符号化された拡張の節へ逆向きに読む。逆向きの写像では、制限模型の要素を台へ埋め込み、符号化された全称を適用してから、`child` を外向きに読んで意味論的充足を復元する。
```agda
(sym (child a δ (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx) (z ∷ γ) i0 (suc yai) qz qa))
(h (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)))
(λ δ z qz h x → subst ⟨_⟩ (child a δ x (z ∷ γ) i0 (suc yai) qz qa)
(h (Semantic.intoL W x) (subst (λ X → ⟨ x .fst ∈ X ⟩) (sym qw) (x .snd))))
```
有界の量化子は、対象言語で三重に入れ子になった有界の層として述べられる。境界の項の値、その内側で台に属する要素、そして拡張の項目であり、順序は両方の量化子で同じである。
```agda
bqAll bqEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (1 + k)
bqAll wi ti yai N0i N1i =
∀̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
⇒̇ ∀̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ⇒̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
bqEx wi ti yai N0i N1i =
```
存在の形は三つの層を連言し、全称の形はそれらを含意として入れ子にする。境界項の値はその項の節によって読み取られ、最も内側の節は非有界の場合と同じグラフ拡張の等式を使う。
```agda
∃̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i))
∧̇ ∃̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ∧̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
```
項の意味論的な値は、`W` の要素からなるアルファベットの各定数を制限模型へ写し、得られた項を `δ` で評価することで定まる。定数は埋め込み `DB.ι` で解釈され、変数は `δ` の対応する位置から直接読まれる。集合として符号化された数項は後で変数の添字を表すためのものであり、この評価関数の一部ではない。
```agda
private
value : ∀ {n} → Term Ab n → Vec DB.SM n → DB.SM
value t δ = ⟦ mapTm DB.ι t ⟧ᴮ δ
```
定数項について、`term-out` は切り詰められた `TmIsV` の証拠を集合の等式へ消去する。定数の分枝では、対の符号化の単射性が第二成分を比較し、候補の値をその定数と同定する。変数の形をした分枝は異なるタグ `# 0` と `# 1` を等しくしてしまうため、不可能である。
```agda
term-out : ∀ {n} (t : Term Ab n) (δ : Vec DB.SM n) (z v : S)
→ z .fst ≡ Semantic.graph W δ → TmIsV (ct t) (z .fst) (v .fst)
→ v .fst ≡ (value t δ) .fst
term-out (con q) δ z v qz = rec₁ (setIsSet _ _)
(λ { (inl e) → sym (pr-inj e .snd)
```
変数項では、定数の形をした分枝が同じタグの相違によって排除される。変数の形をした分枝では、対の符号化の単射性が格納された添字を `i` の数項と同定し、等式 `qz` がその所属を正準なグラフへ移す。そこで `lookup-spec` により、候補の値が `δ` の第 `i` 成分にちょうど等しいと分かる。切り詰めはこの命題的な等式の中へのみ消去される。
```agda
; (inr (i , e , _)) → ⊥₀-rec (znots (#-inj′ {0} {1} (pr-inj e .fst))) })
term-out (var i) δ z v qz = rec₁ (setIsSet _ _)
(λ { (inl e) → ⊥₀-rec (snotz (#-inj′ {1} {0} (pr-inj e .fst)))
; (inr (j , e , hp)) → subst ⟨_⟩ (lookup-spec (Semantic.values W δ) i (v .fst))
(subst2 (λ a E → ⟨ pr a (v .fst) ∈ E ⟩) (sym (pr-inj e .snd)) qz hp) })
```
逆向きの補題は、実際の意味論的な値から `TmIsV` を組み立て直す。定数の場合、与えられた等式を逆向きにし、タグ `# 0` を持つ対の構成子を通して輸送すると、命題的切り詰めの中に定数の形をした選択肢が得られる。
```agda
term-in : ∀ {n} (t : Term Ab n) (δ : Vec DB.SM n) (z v : S)
→ z .fst ≡ Semantic.graph W δ → v .fst ≡ (value t δ) .fst
→ TmIsV (ct t) (z .fst) (v .fst)
term-in (con q) δ z v qz e = ∣ inl (cong (pr (# 0)) (sym e)) ∣₁
term-in (var i) δ z v qz e = ∣ inr (# (toℕ i) , refl
```
変数の場合、証人は数項 `# (toℕ i)` を格納された添字として使う。与えられた等式は候補値を第 `i` 番目の意味論的成分と同定し、`lookup-spec` はその等式を、対応する対が正準なグラフに属することへ変える。最後に `qz` に沿って逆向きに輸送し、その対を与えられた符号化環境へ戻す。
```agda
, subst (λ E → ⟨ pr (# (toℕ i)) (v .fst) ∈ E ⟩) (sym qz)
(subst ⟨_⟩ (sym (lookup-spec (Semantic.values W δ) i (v .fst))) e)) ∣₁
```
有界量化子のモジュールは、境界の項、部分式、五つのスロット、そして五つの等式を固定する。台、項の符号化、部分式の値、そして二つの数項のスロットで、すべて共有された文脈の上で読まれる。
```agda
module BqBridge {n : ℕ} (t : Term Ab n) (a : Formula Ab (suc n)) {k : ℕ} (Γ : Vec S k)
(wi ti yai N0i N1i : Fin k)
(qw : (lookup wi Γ) .fst ≡ Wv) (qt : (lookup ti Γ) .fst ≡ ct t) (qa : (lookup yai Γ) .fst ≡ (SatW a) .fst)
(q0 : (lookup N0i Γ) .fst ≡ # 0) (q1 : (lookup N1i Γ) .fst ≡ # 1) where
```
残る証明では、有界量化子が使う対象言語の項の節を、直前に確立した意味論的な項の値へ結び付ける必要がある。以下の局所補題はこの対応を `BqBridge` の固定されたスロットと等式の上に保ち、後続の量化子の議論が同じ台、項の符号、子論理式の値、数項のタグを使うようにする。
```agda
private
```
対象言語の項の節が `v ∷ z ∷ Γ` で成り立つなら、`tmIs-out` はまずそれを項のスロットにある符号についての `TmIsV` として読む。次に `qt` に沿って輸送し、そのスロットの値を実際の符号 `ct t` に置き換えると、`term-out` が必要とする表現レベルの主張が得られる。
```agda
tmOut : (z v : S) → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
→ TmIsV (ct t) (z .fst) (v .fst)
tmOut z v h = subst (λ u → TmIsV u (z .fst) (v .fst)) qt
(tmIs-out (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1 h)
```
逆に、`ct t` についての `TmIsV` の主張を `qt` に沿って逆向きに輸送し、`tmIs-in` に渡す。結果は `v ∷ z ∷ Γ` における対象言語の項の節そのものであり、橋渡しは符号化された節と意味論的な項の評価との間を両方向に移動できる。
```agda
tmIn' : (z v : S) → TmIsV (ct t) (z .fst) (v .fst)
→ ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩
tmIn' z v h = tmIs-in (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1
(subst (λ u → TmIsV u (z .fst) (v .fst)) (sym qt) h)
```
意味論的環境 `δ` に対し、`bound δ` は境界項の値を `L` へ埋め戻した集合である。これは符号化された有界量化子の最外側の値スロットに対する正準な証人となり、有界論理式はその要素の上を動く。
```agda
bound : Vec DB.SM n → S
bound δ = Semantic.intoL W (value t δ)
```
境界は台に属する。値の第二成分が台への所属であり、台の名指しの等式に沿って輸送される。
```agda
bound∈W : (δ : Vec DB.SM n) → ⟨ (bound δ) .fst ∈ (lookup wi Γ) .fst ⟩
bound∈W δ = subst (λ X → ⟨ (value t δ) .fst ∈ X ⟩)
(sym qw) ((value t δ) .snd)
```
`z` が `δ` のグラフであるとき、`bound δ` の基礎の集合は定義上 `t` の意味論的な値の基礎の集合そのものなので、反射律が `term-in` に必要な等式を与える。得られる `TmIsV (ct t) (z .fst) ((bound δ) .fst)` は、選んだ境界が符号化環境における符号化項の値を表すことを証明する。
```agda
bound-term : (δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ
→ TmIsV (ct t) (z .fst) ((bound δ) .fst)
bound-term δ z qz = term-in t δ z (bound δ) qz refl
```
次に、`bound-term` が与えた表現レベルの証明を `tmIn'` によって対象言語の `tmIs` へ変換し、有界量化子の本体が使う正確にずらされたスロットへ置く。これにより、正準な意味論的境界を本体の最外側の量化層へ挿入できる。
```agda
bound-read : (δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ
→ ⟨ (bound δ ∷ z ∷ Γ)
⊨ tmIs (suc (suc ti)) i1 i0
(suc (suc N0i)) (suc (suc N1i)) ⟩
bound-read δ z qz = tmIn' z (bound δ) (bound-term δ z qz)
```
有界な全称の橋渡しの前向きの半分では、項の節を満たす任意の候補値 `v` と、台に属しかつ `v` に属す任意の要素 `x` を考える。補題 `term-out` は `v` の基礎の集合を `t` の実際の意味論的な値の基礎の集合と同定するので、`x` の所属を意味論的な境界への所属へ輸送できる。全称の意味論的仮定が子論理式の真理を与え、`child` がそれを符号化された拡張の節へ戻す。
```agda
allInBridge : ExtFact ((SatW (∀̇∈ t a)) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i ⟩)
allInBridge = direct-extension (∀̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i)
(λ δ z qz h v hv ht x hx hxv → subst ⟨_⟩
(sym (child a δ (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
(v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa))
```
逆向きの半分では、意味論的境界に属す任意の制限模型の要素 `x` が子論理式を満たすことを示す。符号化された全称を正準な値 `bound δ` に適用し、必要な条件を `bound∈W` と `bound-read` から得る。さらに埋め込まれた要素 `intoL W x` に適用し、その台への所属と仮定された境界への所属を使う。最後に `child` を外向きに読むと `Meaning a (x ∷ δ)` が得られる。
```agda
(h (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
(subst (λ V → ⟨ x .fst ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv)))
(λ δ z qz h x hx → subst ⟨_⟩
(child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)
(h (bound δ) (bound∈W δ) (bound-read δ z qz)
```
最後の引数は、`x` が境界項の意味論的な値に属すという仮定そのものである。この所属を与えると、そのようなすべての `x` に対する全称の検証者が完成し、`direct-extension` が要求する逆向きの含意も完成する。
```agda
(Semantic.intoL W x) (subst (λ X → ⟨ x .fst ∈ X ⟩) (sym qw) (x .snd)) hx))
```
有界な存在量化の橋渡しは、`∃̇∈ t a` に対して同じ外延的事実を述べる。環境集合の内部では、内部の値への所属は、台の上の三層の有界存在論理式を充足することと同値である。
```agda
exInBridge : ExtFact ((SatW (∃̇∈ t a)) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i ⟩)
exInBridge = direct-extension (∃̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i)
(λ δ z qz → map₁ (λ { (x , hx , h) → bound δ
, bound∈W δ
, bound-read δ z qz
```
有界な存在の意味論的証人 `x` から、前向きの写像は正準な外側の値 `bound δ` を選び、その台への所属と項の証明を与え、`x` を内側の台の証人として埋め込む。`x` の意味論的境界への所属は保たれ、`child` を逆向きに読むことで必要な符号化された拡張の証人が得られる。存在の証人はすべて命題的切り詰めの内側に保たれる。
```agda
, ∣ Semantic.intoL W x , subst (λ X → ⟨ x .fst ∈ X ⟩) (sym qw) (x .snd) , hx
, subst ⟨_⟩ (sym (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)) h ∣₁ }))
(λ δ z qz → rec₁ squash₁ (λ { (v , hv , ht , h) → map₁
(λ { (x , hx , hxv , hc) → (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
, subst (λ V → ⟨ x .fst ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv
```
逆向きの写像では、外側の切り詰められた証人が項の候補値 `v` を与え、内側の証人が台に属しかつ `v` に属す要素 `x` と、符号化された子論理式の拡張を与える。項の節を外向きに読むと、`v` の基礎の集合が実際の意味論的な境界の基礎の集合と同定される。その等式に沿って `x` の所属を真の境界へ輸送し、さらに `child` が符号化された子の証拠を意味論的充足へ移す。
```agda
, subst ⟨_⟩ (child a δ (x .fst , subst (λ X → ⟨ x .fst ∈ X ⟩) qw hx)
(v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa) hc }) h }))
```
原子の本体が束縛する値は三つではなく二つである。台の要素 `v` を `t` の候補値とし、台の要素 `x` を `u` の候補値とする。その後、二つの `tmIs` の節と与えられた関係式 `rel` を連言し、文脈 `x ∷ v ∷ z ∷ Γ` で評価する。符号化環境 `z` はもとから自由な引数であり、`rel` は束縛される項目ではなく論理式である。
```agda
atomEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (3 + k) → Formula S (1 + k)
atomEx wi ti ui N0i N1i rel =
∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc wi)))
(tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i)
∧̇ (tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ∧̇ rel)))
```
`AtomBridge` は所属原子と等号原子に共通する証明を抽象化する。項 `t`、`u` と五つのスロット等式が、それらの符号とタグ `# 0`、`# 1` の読み方を定める。さらに引数 `op`、`R`、`rel` がそれぞれメタレベルの原子、対応する周囲の二項関係、その関係を表す対象言語の論理式を指定する。
```agda
module AtomBridge {n : ℕ} (t u : Term Ab n) {k : ℕ} (Γ : Vec S k)
(wi ti ui N0i N1i : Fin k)
(qw : (lookup wi Γ) .fst ≡ Wv) (qt : (lookup ti Γ) .fst ≡ ct t) (qu : (lookup ui Γ) .fst ≡ ct u)
(q0 : (lookup N0i Γ) .fst ≡ # 0) (q1 : (lookup N1i Γ) .fst ≡ # 1)
(op : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j)
(R : V ℓ → V ℓ → Type (ℓ-suc ℓ))
(rel : Formula S (3 + k))
(agree : (z v x : S) → (⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩ → R (v .fst) (x .fst))
× (R (v .fst) (x .fst) → ⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩))
(cnd-out : (δ : Vec DB.SM n) → ⟨ Meaning (op t u) δ ⟩ → R ((value t δ) .fst) ((value u δ) .fst))
(cnd-in : (δ : Vec DB.SM n) → R ((value t δ) .fst) ((value u δ) .fst) → ⟨ Meaning (op t u) δ ⟩) where
```
一致の仮定は、新たに先頭へ加えられた三つの項目における `rel` と `R` の正確な接続を述べる。`x ∷ v ∷ z ∷ Γ` での `rel` の充足から `R (v .fst) (x .fst)` が得られ、その関係の証明から `rel` の充足を組み立て直せる。したがって、橋渡しが任意の表現式を使えるのは、両方向が与えられている場合に限られる。
さらに二つの仮定が、選んだ関係を意図した原子の意味論へ結び付ける。第一の仮定は `Meaning (op t u) δ` を二つの項の評価値の間の `R` へ送り、第二の仮定は同じ関係からその意味を組み立て直す。このため、一般的な橋渡しは所属と等号のどちらにも同じ形で使える。
文脈 `δ3 z v x = x ∷ v ∷ z ∷ Γ` は、`u` の候補値をスロット `i0`、`t` の候補値を `i1`、符号化環境を `i2` に置く。これらは二つの項の節と関係の接続が使う、新たに現れた三つの項目である。一方、一般の論理式 `rel` は、引き継いだ `Γ` の項目も利用できる。`atomEx` が新たに束縛するのは `x` と `v` だけで、`z` はもとから自由な環境引数である。
```agda
private
δ3 : (z v x : S) → Vec S (3 + k)
δ3 z v x = x ∷ v ∷ z ∷ Γ
```
二つの外向きの読みは、`δ3 z v x` における対象言語の項の節を `TmIsV` の主張へ変える。`qt` に沿った輸送により、第一の主張は実際の符号 `ct t` と候補値 `v` に関するものとなり、`qu` に沿った輸送により、第二の主張は `ct u` と候補値 `x` に関するものとなる。符号化環境 `z` は両者に共通である。
```agda
tOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct t) (z .fst) (v .fst)
tOut z v x h = subst (λ w → TmIsV w (z .fst) (v .fst)) qt
(tmIs-out (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
uOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct u) (z .fst) (x .fst)
uOut z v x h = subst (λ w → TmIsV w (z .fst) (x .fst)) qu
```
逆向きの読みは、`TmIsV` から二つの対象言語の項の節を組み立て直す。`t` については、まず符号を `qt` に沿って逆向きに輸送し、その結果を `tmIs-in` に渡す。`uIn` の宣言は、`u` の値のスロットにおける同じ構成を用意する。
```agda
(tmIs-out (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h)
tIn : (z v x : S) → TmIsV (ct t) (z .fst) (v .fst) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩
tIn z v x h = tmIs-in (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
(subst (λ w → TmIsV w (z .fst) (v .fst)) (sym qt) h)
uIn : (z v x : S) → TmIsV (ct u) (z .fst) (x .fst) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩
```
`u` については、`qu` に沿った逆向きの輸送が `TmIsV (ct u) (z .fst) (x .fst)` を呼出し側のスロットが名指す符号についての主張に変え、`tmIs-in` が第二の対象言語の項の節を組み立て直す。これで橋渡しは、二つの候補値のそれぞれについて読み書きの両方向を備える。
```agda
uIn z v x h = tmIs-in (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1
(subst (λ w → TmIsV w (z .fst) (x .fst)) (sym qu) h)
```
定理 `atomBridge` はここで、各符号化環境について原子の意味論的な値と `atomEx` を比較するよう `direct-extension` に求める。その前向きの写像は `Meaning (op t u) δ` から出発し、二つの有界な値の証人、それぞれの項の節、そして `x ∷ v ∷ z ∷ Γ` における関係式を構成しなければならない。逆向きの写像は同じデータを逆にたどる。
```agda
atomBridge : ExtFact ((SatW (op t u)) .fst) ((envSet W n) .fst) (λ z → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩)
atomBridge = direct-extension (op t u) (λ z → (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel) out inn
where
out : (δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ → ⟨ Meaning (op t u) δ ⟩
→ ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩
```
外向きの構成では、`t` と `u` の実際の意味論的な値を `L` へ埋め込んだものを、二つの有界な証人として選ぶ。制限模型での値の第二成分が、それらの台への所属を示す。`term-in` に続く `tIn` と `uIn` が二つの項の節を与え、さらに `cnd-out` に続いて `agree` の逆向きの半分を使うと、対象言語の関係が得られる。二つの証人は、入れ子になった二つの命題的切り詰めの中へ導入される。
```agda
out δ z qz h = ∣ v , subst (λ X → ⟨ v .fst ∈ X ⟩) (sym qw) ((value t δ) .snd)
, ∣ x , subst (λ X → ⟨ x .fst ∈ X ⟩) (sym qw) ((value u δ) .snd)
, tIn z v x (term-in t δ z v qz refl)
, uIn z v x (term-in u δ z x qz refl)
, agree z v x .snd (cnd-out δ h) ∣₁ ∣₁
```
局所名 `v` と `x` は、評価された項 `t` と `u` をそれぞれ `L` へ埋め込んだ要素である。これらは `atomEx` の二つの値量化に対する正準な証人である。原子の符号そのものが名指すのは二つの項の符号であり、ここでの証人は特定の環境 `δ` におけるそれらの値を与える。
```agda
where
v x : S
v = Semantic.intoL W (value t δ)
x = Semantic.intoL W (value u δ)
```
`atomBridge` の逆向きの含意は、メタレベルの環境 `δ`、符号化された環境 `z`、および `z` を `δ` の正準なグラフと同一視する等式から始まる。残る仮定は、`atomEx` が `z` で成り立つことである。外側の命題的に切り詰められた有界存在は、候補 `v`、それが `W` に属することの証明 `hv`、および内側の存在の証明 `h` を与える。`Meaning (op t u) δ` は命題なので、`rec₁` によってこの切り詰めをその目標へ消去し、続いて内側の切り詰めも同様に消去できる。この時点の `v` はまだ `t` の値の候補にすぎない。内側の証人から得る項の値の記録によって、初めて実際の意味論的な値と同一視される。
```agda
inn : (δ : Vec DB.SM n) (z : S) → z .fst ≡ Semantic.graph W δ
→ ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩ → ⟨ Meaning (op t u) δ ⟩
inn δ z qz = rec₁ ((Meaning (op t u) δ) .snd) (λ { (v , hv , h) →
rec₁ ((Meaning (op t u) δ) .snd) (λ { (x , hx , ht , hu , hr) →
cnd-in δ (subst2 R (term-out t δ z v qz (tOut z v x ht))
```
内側の証人は、第二の候補 `x`、その所属証明 `hx : x ∈ W`、二つの項の節の証明 `ht` と `hu`、および対象言語の関係の証明 `hr` を与える。`hv` と `hx` は二つの存在量化子の境界を記録するが、ここではそれ以上使う必要はない。まず `agree z v x .fst` が `hr` を `R (v .fst) (x .fst)` として読み取る。`z` は `δ` の正準なグラフなので、`tOut` と `uOut` は二つの項の節の証明を `term-out` に渡す。得られる等式は、`v` と `x` の基礎の集合を、それぞれ `t` と `u` の意味論的な値の基礎の集合と同定する。次に `subst2` がその二つの同定に沿って `R` を運び、最後に `cnd-in` が運ばれた関係を `Meaning (op t u) δ` に変える。これで原子の橋が完成する。下流では所属と等号の場合にそれぞれ具体化される。`SatSoundC` では、部分符号に関する閉性と論理式の構造再帰により、外延事実を比較して表要素を `SatW` に固定する。`SatHoldsC` では、コードの復号、あらかじめ与えられた表の値、全域性、および指定された領域を使い、同じ橋によって十個の節をすべて満たす。`SatisfactionDescription` はコード領域と環境の塔に関する事実を与え、正準なグラフ `SatGraph.pairs W` が `tableAt` を満たすことを証明し、`towerAt`、`codesAt`、`tableAt` を `satAt` としてまとめる。その `SatRead` モジュールは、得られた充足関係グラフ、コード集合、環境の塔について、所属を両方向に読む補題を公開する。
```agda
(term-out u δ z x qz (uOut z v x hu)) (agree z v x .fst hr)) }) h })
```