Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ定数を含む論理式は、定数の各出現を新しい変数で置き換え、その定数をベクトルに記録することで、パラメータを持たない論理式へ変換できる。そのベクトルを環境から与えても充足関係は保存されるため、パラメータ付き論理式を後の符号化に利用できる。
本章ではこの置換そのものを構成する。FOL.Manipulation.ConstantOccurrences の出現数え上げが新しく必要な変数の個数を決め、配置が各出現にどの変数の枠を与えるかを決める。置換は構造的な一回の走査で済み、章末の妥当性定理が置換前後の充足関係を同一視する。これが後で論理式を符号化するときに用いる事実である。
論理式を使う議論では定数が要る。集合 $a$ がパラメータ付きで定義可能だと言うには、$a$ を名前で言及する論理式を書くからである。しかし符号化の議論では、パラメータを持たない論理式だけを扱えると便利である。パラメータ抽象はそれを可能にする翻訳である。定数の各出現を新しい変数に置き換え、定数をベクトルに記録して環境から供給できるようにする。
この置き換えは定数ごとではなく、出現ごとに行われる。定数 $c$ が二度現れれば、二度記録され、二つの変数を受け取る。出現単位で記録するため、翻訳は二つの名前が等しいかを判定する必要がなく、アルファベット K に可判定な等式は要らない。定数の出現を数える章の位置的な数え上げが簿記のすべてを担う。
open import Cubical.Data.Vec using ( _++_ )
具体的には、この翻訳は前の章で用意された二つのデータを使う。定数の出現の個数は新しく必要な変数の数を決め、記録された定数のベクトルは、解釈の後でそれらの変数が何を表すかを決める。置き換えそのものは配置と呼ばれる関数で記述され、各出現がどの変数の枠を受け取るかを決める。
構成全体は論理式の上の一度の構造的な走査である。章の末尾で証明される妥当性の定理は、定数解釈の下での元の論理式の充足と、拡張された環境の下での抽象化の充足を同一視する。後の符号化の議論が依拠するのはまさにこの同一視である。
定数の出現はすべて変数になるため、翻訳後の論理式には定数がまったく含まれない。つまり、元をひとつも持たないアルファベットの上にある。コードでは空の型 ⊥* がこのアルファベットの役を担う。解釈すべきものがないので、この解釈が実際に要求されることはなく、型が存在して翻訳後の構文に well-formed な台を与えるだけで十分である。
抽象化
配置は定数の各出現に、より大きな文脈の変数を割り当てる。placeFo はこの置換を構造的に行い、absFo は元の自由変数の直後にある、出現回数と同じ長さの連続した領域を選ぶ。
走査は任意の配置 θ に対して述べられる。この一般性は再帰から強制される。部分論理式で用いられる配置は走査の内部で作られるため、帰納法の仮定はすべての配置について成り立つ必要がある。θ を抽象的なまま保つことで、妥当性の証明もモジュール的に保たれる。本節では項について、次に論理式について、この二つの走査を構成する。
置き換えの一般形は走査で、論理式のほかに配置 θ : Fin (countTm t) → Fin (n + k) を受け取る。θ は数え上げの章で列挙された順に t の出現の枠を読み、それぞれに対して利用可能な n + k 個の枠の一つを指名する。このうち n 個は元の自由変数、k 個は新しいパラメータの枠である。出力は空のアルファベット ⊥* の上の項である。生き残る定数はないからである。
placeTm : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (t : Term K n)
→ (Fin (countTm t) → Fin (n + k)) → Term (⊥* {ℓz}) (n + k)
placeTm (con c) θ = var (θ zero)
placeTm {k = k} (var i) θ = var (padRight k i)
placeFo : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (φ : Formula K n)
項の二つの場合が、二つの基本的な動きを示す。定数 con c は出現をちょうど一つ、すなわち第 0 枠に持ち、配置がどの変数で置き換えるかを決める。それが var (θ zero) である。変数 var i は出現を持たないので配置は使われないが、文脈は n から n + k へ伸びたため、古い添字を埋め込み直す必要がある。padRight k は i を先頭 n 枠の中の同じ位置へ送り、参照法則により連結された環境でも値は保たれる。
→ (Fin (countFo φ) → Fin (n + k)) → Formula (⊥* {ℓz}) (n + k)
placeFo (t ∈̇ u) θ = placeTm t (λ i → θ (padRight (countTm u) i))
∈̇ placeTm u (λ j → θ (padLeft (countTm t) j))
placeFo (t ≐ u) θ = placeTm t (λ i → θ (padRight (countTm u) i))
≐ placeTm u (λ j → θ (padLeft (countTm t) j))
二項ノードでは出現リストが分裂し、ここで配置の算術が現れる。原子 t ∈̇ u を、t = con c、u = con d とすると、出現リストは c ∷ d ∷ [] で、c は添字 0、d は添字 1 にある。そこで左の項は padRight を通して配置を読み、u に属する countTm u 個の枠を飛び越える。右の項は padLeft を通して読み、t に属する countTm t 個の枠をまたぐ。こうして各部分項は自分の出現の枠だけに働く配置を受け取り、翻訳された二つの部分項が元の接続詞で再結合される。
placeFo (φ ∧̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
∧̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ∨̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
∨̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ⇒̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
論理式の走査は、この例を構造的再帰で一般化したものである。二つの部分からなる構成子は、原子であれ命題的な接続詞であれ、出現リストをまさにこの方法で分割する。第一因子の出現が第二因子の出現に先立ち、左の走査は θ に右側の個数を越える padRight を、右の走査は左側の個数を越える padLeft を合成する。偽 ⊥̇ は出現をまったく持たず、自分自身に翻訳される。どの節も二度目の走査や改名の補題を要しない。再帰の前に配置を合成しておくことで、翻訳全体が一度の構造的走査に保たれる。
⇒̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo ⊥̇ θ = ⊥̇
placeFo (∃̇ φ) θ = ∃̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇ φ) θ = ∀̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇∈ t φ) θ = ∀̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
束縛子の下では文脈が一つ伸ぶ。これが二つ目の繰り返し現れる動きである。∃̇∈ t φ では、意味論が本体を評価するときに束縛変数を環境の左に追加するため、パラメータの枠はすべて一つずれる。本体は配置 suc ∘ θ の下で走査され、さらに項の出現を越える padLeft で調整される。項そのものは本体の出現を越える padRight で前の方に配置される。非有界の量化子 ∃̇ と ∀̇ はずらしだけを持つ。これらの節で十個の論理式の構成子がすべてカバーされる。
(placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
placeFo (∃̇∈ t φ) θ = ∃̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
(placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
本の残りの部分で使うのは次のインスタンスである。予算を出現回数ちょうどにとり、配置は変数の直後に続く領域とする。これが求める抽象化であり、その型が本章の主結果を述べる。K 上の自由変数 n 個の論理式が、自由変数 n + countFo φ 個の無パラメータ論理式になる。
padLeft n は出現 j を枠 n + j へ送る配置そのものなので、記録された各定数は、constantsFo φ が並べる順に、元の変数の後ろの最初の空き枠を受け取る。他に選ぶべきものはない。
定義は一度の呼び出しだけである。absFo φ = placeFo φ (padLeft n)。添字の算術はすべて走査の内側に繰り込まれているため、抽象化自身は場合分けを持たない。予算が数え上げと一致するため、配置は事実上、出現の枠とパラメータの枠の間の全単射になるが、コードがそのことを述べる必要はない。
absFo : ∀ {ℓz ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Formula (⊥* {ℓz}) (n + countFo φ)
absFo {n = n} φ = placeFo φ (padLeft n)
妥当性
妥当性は、定数解釈の下にある元の論理式と、拡張した変数環境の下にある抽象化後の論理式を比較する。配置された各変数が記録済みの定数の解釈を持つなら、項の表示と論理式の充足関係は構造帰納法で一致する。
この比較は、台が S である構造 𝒮 の中で、元の定数の一つの解釈 ι : K → S の下に述べられる。二つの意味論の読み方が並べて用意される。_⊨_ と ⟦_⟧ は K 上、ι の下の論理式と項に対応し、その改名されたコピー _⊨₀_・⟦_⟧₀ は抽象化の定数域 ⊥* に対応する。⊥* は空なので無パラメータの側に本物の解釈は要らないが、意味論のモジュールはこのデータを要求するため、⊥*-rec が空虚にそれを供給する。
妥当性とは、抽象化が意味を変えないという主張である。同じ論理式の二つの評価を比較する。一方は K 上の元の構文で、定数は写像 ι : K → S によって解釈される。他方は空のアルファベット上の翻訳後の構文で、連結された環境 γ ++ σ の中で評価される。γ は元の自由変数の値を、σ は記録された定数の解釈を保持する。ここで S は命題値の構造 𝒮 の台であり、Vec S n は長さ n の環境の型である。
module _ {ℓ} (𝒮 : ZFStructureₕ ℓ) where
open ZFStructure 𝒮
private module Sem = FOL.Semantics 𝒮
この比較は、両側をつなぐただ一つの仮定に依存する。各出現について、配置の指名した変数がそこに記録された定数の解釈を保持する、すなわち lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)) というものである。この後のすべては、この仮定を保ちながら構文に対する構造的帰納法である。翻訳後の構文は空のアルファベットの上にあるため、その読み方 _⊨₀_ と ⟦_⟧₀ には本物の定数解釈は要らない。ただし意味論のモジュールはこのデータを要求するため、空の型の消去が空虚にそれを供給する。
module _ {ℓz ℓc} {K : Type ℓc} (ι : K → S) where
open Sem.At K ι using ( _⊨_; ⟦_⟧ )
open Sem.At (⊥* {ℓz}) ⊥*-rec using ()
renaming ( _⊨_ to _⊨₀_ ; ⟦_⟧ to ⟦_⟧₀ )
この主張は配置 θ に関して汎用的である。しかも汎用的でなければならない。再帰における配置は再帰呼び出しの箇所で作られるからである。主張は変数に依存しない形で与えた環境 γ とパラメータ環境 σ の上で述べられ、ただ一つの仮定で制約される。すなわち、出現のたびに、配置の指す位置にはその位置に記録された定数の解釈が入っている、というものである。この仮定こそ「定数が環境から供給される」の全内容であり、具体的な環境を代入するのではなく仮定として述べることで、どの節もベクトルを正規化する必要がなくなる。
二つの部分からなる構成子に必要な準備は、この仮定を二つに分けることだけである。分かれた各半分は、それぞれ補埋の法則との一度の合成になる。
帰納法の不変条件は、出現ベクトル全体に関する仮定 h である。新しく必要な仕事は、二項の構成子がこのベクトルを左の部分 p と右の部分 q に分けるときに、それを分割することだけである。h が、γ ++ σ の中の枠 θ j に p ++ q の第 j 項の解釈が入っていると述べているとする。左の被演算子に必要なのは p の長さより小さい添字 j だけで、そのような添字を q を越える padRight を通して読めば、p の対応する項がちょうど回復する。それが法則 lookup-padRight である。これを h と合成し、続けて ι を施せば、再帰呼び出しの左の前提が得られる。
private
leftHalf : ∀ {n k a b} (θ : Fin (a + b) → Fin (n + k))
(γ : Vec S n) (σ : Vec S k) (p : Vec K a) (q : Vec K b)
→ (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
→ (∀ i → lookup (θ (padRight b i)) (γ ++ σ) ≡ ι (lookup i p))
右半分はその鏡像である。q の添字は padLeft を通して読まれ、これは p の a 個の枠をちょうどまたぐ。そして lookup-padLeft が、連結の中で読み取った項を q の対応する項と同一視する。a が rightHalf では明示的な引数で leftHalf では暗黙だったことに注意してほしい。配置の定義域 Fin (a + b) だけでは a は定まらないが、padLeft はいくつの枠をまたぐかを正確に知らされる必要があるからである。
leftHalf θ γ σ p q h i = h (padRight _ i) ∙ cong ι (lookup-padRight p q i)
rightHalf : ∀ {n k} a {b} (θ : Fin (a + b) → Fin (n + k))
(γ : Vec S n) (σ : Vec S k) (p : Vec K a) (q : Vec K b)
→ (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
→ (∀ j → lookup (θ (padLeft a j)) (γ ++ σ) ≡ ι (lookup j q))
leftHalf と rightHalf が揃えば、分割の不変条件は一度限り確立される。以下の帰納法の二項の節はすべて、この二つの補題のどちらかを通して結合仮定を制限するだけで、どの節も再び連結された環境の内部を見ることはない。
rightHalf a θ γ σ p q h j = h (padLeft a j) ∙ cong ι (lookup-padLeft a p q j)
まず項から始める。二つの場合はいずれもすぐに示せる。定数の値は、仮定がその位置に述べている解釈そのものである。変数の値は変化せず、補埋の法則が拡張された環境の中でそれを再び見つけ出す。
帰納法は項から始まる。ここでは不変条件がすでにすべての仕事をしている。主張はこうである。h が配置された枠を正しく埋めているなら、解釈 ι の下で t の γ における値は、空のアルファベットの上で翻訳後の項の γ ++ σ における値に等しい。定数 con c の翻訳は var (θ zero) で、その γ ++ σ での値は lookup (θ zero) (γ ++ σ) である。仮定 h zero がこれを ι c と同一視する。これはまさに主張であり、等式の向きが逆なだけである。
⟦⟧-place : ∀ {n k} (t : Term K n) (θ : Fin (countTm t) → Fin (n + k))
(γ : Vec S n) (σ : Vec S k)
→ (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsTm t)))
→ ⟦ t ⟧ γ ≡ ⟦ placeTm t θ ⟧₀ (γ ++ σ)
⟦⟧-place (con c) θ γ σ h = sym (h zero)
変数 var i では何も置き換えられず、付け替えられただけである。翻訳はそれを padRight k i、すなわち広い文脈の中の同じ枠へ移し、補埋の法則により γ ++ σ で調べれば元の値が回復する。定数と変数の場合が済むと、残りの構成子は分割の不変条件で扱われる二項ノードか束縛子のどちらかで、論理式レベルの帰納法も同じ型に従う。
⟦⟧-place (var i) θ γ σ h = sym (lookup-padRight γ σ i)
続いて帰納法の十二の場合である。ここで十個の論理式の場合を扱い、二つの項の場合は先ほど証明済みである。命題の各原始節はすべて合同である。意味論が各構成子に割り当てるのは対応する論理演算そのものであり、間に変換の層がないからである。四つの束縛節は環境に値を一つ追加し、拡張後の環境で帰納法の仮定を用いるが、パラメータ位置に関する仮定はそのまま通用する。左側への要素の追加と配置の suc による移し替えは計算によって打ち消し合うので、束縛子は固有の補題を必要としない。二つの有界節は、その構成子と同じく左に項、右に本体という形で二分割される。
論理式レベルの主張 ⊨-place は項の補題と同じ形をしている。表示の代わりに充足が現れる。配置された枠に関する仮定 h の下で、(γ ⊨ φ) は ((γ ++ σ) ⊨₀ placeFo φ θ) に等しい。代表的な原子は所属 t ∈̇ u である。原子の充足は二つの項の値の、構造の所属関係に沿った合同なので、この節は走査が実際に用いた配置で各被演算子に項の補題を適用する。
⊨-place : ∀ {n k} (φ : Formula K n) (θ : Fin (countFo φ) → Fin (n + k))
(γ : Vec S n) (σ : Vec S k)
→ (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)))
→ (γ ⊨ φ) ≡ ((γ ++ σ) ⊨₀ placeFo φ θ)
⊨-place (t ∈̇ u) θ γ σ h = cong₂ _∈ˢ_
各被演算子の仮定は、分割の不変条件が供給するものそのものである。constantsTm t ++ constantsTm u に対する結合仮定 h を、左では padRight で、右では padLeft で制限したものである。等号の原子 t ≐ u もまったく同様に扱われ、所属の代わりに構造の等号 ≈ˢ が現れる。続く命題的な接続詞では、項の補題を論理式レベルの帰納に置き換えるだけである。
(⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
(leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
(⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
(rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
⊨-place (t ≐ u) θ γ σ h = cong₂ _≈ˢ_
連言が最初の純粋に命題的な節である。意味論は φ ∧̇ ψ の充足を、二つの充足値に命題の連言 _⊓_ を施したものとして定義するので、この節は二つの帰納法の仮定の下での cong₂ _⊓_ になり、h は constantsFo φ と constantsFo ψ の間で分割される。証明は (γ ⊨ φ) ⊓ (γ ⊨ ψ) を単に hProp ℓ の命題として扱い、合同だけを用いる。対による表現を仮定することも、それを分解することもない。
(⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
(leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
(⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
(rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
⊨-place (φ ∧̇ ψ) θ γ σ h = cong₂ _⊓_
選言は命題の選言 ⊔ で、含意はその含意の演算 ⇒ で同じパターンを繰り返す。三つの命題的な節が違うのは、cong₂ が施される論理演算だけである。分割された仮定を含め、その他の部分はまったく同じである。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
(leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
(⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
(rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
⊨-place (φ ∨̇ ψ) θ γ σ h = cong₂ _⊔_
ここでパターンを一度まとめておく。残りの各節は、その構成子に意味論が割り当てた論理演算で合同を取るか、環境に値を一つ追加して再帰するかのどちらかであり、新しい発想を必要とする節はない。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
(leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
(⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
(rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
⊨-place (φ ⇒̇ ψ) θ γ σ h = cong₂ _⇒_
偽がこれを裏付ける。環境や配置がどうであれ、等式の両辺は偽命題 ⊥なので、この節は refl で済む。翻訳がパラメータ領域にまったく言及しない唯一の構成子でもある。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
(leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
(⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
(rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
⊨-place ⊥̇ θ γ σ h = refl
非有界の量化子 ∃̇ φ が束縛子の場合で、その内容はずらしが打ち消し合うことである。走査は本体を suc ∘ θ の下に置いた。束縛値を左に追加するとすべてのパラメータ枠が一つずれるからである。一方、意味論は x ∷ γ の上で量化する。そこで再帰的主張は x ∷ γ で用いられ、そこでは lookup (suc (θ j)) (x ∷ γ ++ σ) が計算によって lookup (θ j) (γ ++ σ) に化け、これはちょうど h である。この打ち消しは定義的なので、証明のどこにもずらしのための補題は現れない。
⊨-place (∃̇ φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
⊨-place (∀̇ φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
⊨-place (∀̇∈ t φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong₂ _⇒_
全称量化子 ∀̇ の議論も同じで、代数の存在量化の演算 ∃[ x ] P x の代わりに全称量化の演算 ∀[ x ] P x が現れるだけである。演算が名指しされるのは外側の cong の一点だけで、その下の帰納は同一である。
(cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
(leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
(⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
(rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
⊨-place (∃̇∈ t φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → cong₂ _⊓_
有界量化子は二つの動きを組み合わせる。∀̇∈ t φ では、走査は項 t を文脈の前の方で、本体の出現を越える padRight によって抽象化し、本体の配置は項の出現を越える padLeft との合成によって suc だけずらした。したがってこの節は cong₂ _⇒_ である。一方は項の補題によって x が抽象化された界に属することを、他方はずらした帰納によって x ∷ γ での再帰的主張を結ぶ。leftHalf と rightHalf が h を constantsTm t と constantsFo φ の間で分割する。存在形の有界量化子 ∃̇∈ は ⇒ の代わりに ⊓ を用いる鏡像である。これで言語のすべての構成子が同じ不変条件で扱われた。
(cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
(leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
(⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
(rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
妥当性そのものは、抽象化が選んだ配置と、収集が指定するパラメータ環境、すなわち解釈済みの定数そのものを選べば直ちに従う。仮定は二つの補埋め法則を順につなげたものになり、定理はまさにこの主張を述べる。元の論理式の γ での充足は、収集された定数で γ を拡張した後の抽象化の充足と一致する。
主定理は帰納法を一度だけ具体化する。absFo φ は配置 padLeft n での走査によって作られたので、⊨-place はまさにその配置で用い、パラメータ環境は map ι (constantsFo φ)、すなわち記録された定数を順に解釈したものと取る。得られる定理は次を述べている。元の論理式の γ での充足は、これらの解釈済み定数で γ を拡張した後の抽象化の充足と一致する。
⊨-abs : ∀ {n} (φ : Formula K n) (γ : Vec S n)
→ (γ ⊨ φ) ≡ ((γ ++ map ι (constantsFo φ)) ⊨₀ absFo φ)
⊨-abs {n} φ γ = ⊨-place φ (padLeft n) γ (map ι (constantsFo φ)) hyp
where
hyp : ∀ j → lookup (padLeft n j) (γ ++ map ι (constantsFo φ))
残るのは、この σ の選択が仮定を果たすことを見ることである。配置 padLeft n は出現 j を項 n + j へ送るが、これは連結の後半に落ちる。lookup-padLeft がその項を lookup j (map ι (constantsFo φ)) と同一視し、lookup-map が解釈を引き抜いて、ちょうど ι (lookup j (constantsFo φ)) を与える。二つの法則を合成したものが仮定であり、それを満たせば ⊨-place が定理を与える。数学的に言えば、パラメータを持たない論理式と有限で順序づけられたパラメータのベクトルの組は、定数付きの元の論理式と同じ外延を持つ。
≡ ι (lookup j (constantsFo φ))
hyp j = lookup-padLeft n γ (map ι (constantsFo φ)) j
∙ lookup-map ι (constantsFo φ) j
定義可能な部分集合とは何か
パラメータ抽象は、定義可能な部分集合を与えるデータを分離する。すなわち、パラメータを持たない論理式、有限なパラメータベクトル、そして所属を判定する変数である。妥当性により、この提示は元の定数付き論理式とまったく同じ外延を持つ。
ここには形状上の要点が一つあり、それがアリティ 1 の場合をわざわざ書き下す理由である。アリティ 1 では拡張後の環境は x ∷ map ι p、つまり一つの要素の後にパラメータが続く形になり、これは本書の他のどこでも一項環境が持つのと同じ形である。
一変数の定義可能な部分集合のために、この系は環境を x ∷ [] と固定する。アリティ 1 の論理式はただ一つの要素 x で判定され、定理は x に解釈済みのパラメータを続けた環境での抽象化の判定を与える。この主張は命題の間の道の等式なので、所属の二つの読み方は取り替えて使える。定義可能な部分集合を符号化する後の章は、定数の改名も論理式の変更もせず、パラメータを持たない論理式とパラメータベクトル map ι (constantsFo φ) を直接扱って構わない。
⊨-abs₁ : (φ : Formula K 1) (x : S)
→ ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι (constantsFo φ)) ⊨₀ absFo φ)
⊨-abs₁ φ x = ⊨-abs φ (x ∷ [])
まとめ
absFo は定数の出現ごとに変数を一つ加えて定数を除き、⊨-abs は記録した定数を環境へ付け加えた後の充足関係を同定する。これは論理式そのものを符号化するときに使う有限パラメータの提示である。