この章を読むか、対話型目次と依存グラフで別のルートを選べます。

有限な変数文脈の間の写像は、定数を固定したまま自由変数を改名して項と論理式へ作用する。環境の一致関係を用いる一つの意味論的定理が、弱化、交換、縮約をまとめて扱う。

構文の章が指摘した欠落、つまり代入も弱化もないことには理由がある。量詞の節が拡張された文脈の本体を直接受け取るため、変数を動かすための古典的な仕組みは不要であった。本書が実際に必要とする変数の移動は一つの装置で賄える。それが改名である。写像 ρ : Fin n → Fin m を論理式へ押し通し、弱化、交換、縮約を一つの正しさの定理で同時に扱う。

公式の自由変数が n 個のスロットで索引づけられているとき、それを m 個のスロットの文脈で捉えたい場面を考える。写像 ρ : Fin n → Fin m が各変数の行き先を決め、改名とはこの写像を公式のすべての自由変数に作用させることである。難所は量詞である。量詞の本体はスロットを一つ余分に持つ文脈で生きるので、ρ を束縛変数を乱さないように各束縛子の下で拡張する必要がある。

そして改名は一つの正しさの定理で測られる。旧環境と新環境の間の適切な関係のもとで、改名された公式は元の公式と同じ命題を表す。命題は任意の命題値をとる任意の集合論的構造の上で計算されるので、定理は充足関係そのものとまったく同じ一般性を持ち、シーケント計算で慣用される構造規則、すなわち弱化、交換、縮約は、すべて ρ の特定の選択として得られる。

構文の水準

renameTm と renameFo は写像 Fin n → Fin m を構文へ通す。束縛子の下では、liftρ が新しく束縛された変数を固定し、元の変数を与えられた写像で移す。

有界量詞の下に自由変数を持つ公式を取ろう。たとえば二つのスロットの文脈における ∀̇∈ x₀ (var 1 ∈̇ var 0) である。束縛変数は本体のスロット 0 であり、本体のスロット 1 は外側の自由変数 0 にあたる。改名 ρ : Fin n → Fin m は外側の変数を動かすが、束縛子の下では Fin (suc n) → Fin (suc m) 上の写像、つまり束縛されたスロット 0 をスロット 0 へ送り、各旧スロット suc i を suc (ρ i) へ送るものが必要になる。この拡張が liftρ ρ であり、束縛変数が決して乱されないことを保証する。

liftρ : ∀ {n m} → (Fin n → Fin m) → Fin (suc n) → Fin (suc m)
liftρ ρ zero    = zero
liftρ ρ (suc i) = suc (ρ i)

持ち上げが手に入れば、改名は項へ、さらに公式へと構造的再帰で拡張できる。renameTm の型が考えのすべてを述べている。n 個の自由変数スロットを持つ項が m 個のスロットを持つ項になるのである。定数 con k は自由変数をまったく名指さないのでそのまま通る。定数は文脈ではなくアルファベットに属し、その解釈は別の問題である。項のもう一つの形式である変数において、初めて ρ が実際に働く。

renameTm : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Term K n → Term K m
renameTm ρ (con k) = con k

公式でも同じ流れである。renameFo は同じ形をし、n 個のスロット上の公式を m 個のスロット上の公式へ変える。原子の節は項の引数を改名するので、例の公式では、外側のスロットにかぎれば var 1 ∈̇ var 0 は var (ρ 1) ∈̇ var (ρ 0) になる。命題結合子と偽はそれ自身は変数を持たず、改名された部分公式から再帰的に組み立て直される。

renameTm ρ (var i) = var (ρ i)

renameFo : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Formula K n → Formula K m
renameFo ρ (t ∈̇ u)  = renameTm ρ t ∈̇ renameTm ρ u
renameFo ρ (t ≐ u)  = renameTm ρ t ≐ renameTm ρ u
renameFo ρ (φ ∧̇ ψ)  = renameFo ρ φ ∧̇ renameFo ρ ψ

通常の量詞は、再帰呼び出しが初めて変わる場所である。本体は拡張された文脈に住むので、呼び出しには ρ ではなく liftρ ρ が渡される。これは例で述べた規則そのものである。束縛スロットはゼロに留まり、外側の改名は移された形でのみ本体に届く。

renameFo ρ (φ ∨̇ ψ)  = renameFo ρ φ ∨̇ renameFo ρ ψ
renameFo ρ (φ ⇒̇ ψ)  = renameFo ρ φ ⇒̇ renameFo ρ ψ
renameFo ρ ⊥̇        = ⊥̇
renameFo ρ (∃̇ φ)    = ∃̇ renameFo (liftρ ρ) φ
renameFo ρ (∀̇ φ)    = ∀̇ renameFo (liftρ ρ) φ

有界量詞は二つの写像を同時に使う。例の公式はまさにここにある。∀̇∈ t φ では、限界 t は外側の文脈に住むので ρ で改名され、本体 φ は liftρ ρ で改名される。したがって ρ の下で ∀̇∈ x₀ (var 1 ∈̇ var 0) は ∀̇∈ (改名された限界) (var (suc (ρ 0)) ∈̇ var 0) になる。自由変数 0 への言及は移動に従って改名を追い、スロット 0 の束縛された出現はそのままである。これで構文の水準は完成である。次の節は、結果が最初の公式と同じ意味を持つかを問う。

renameFo ρ (∀̇∈ t φ) = ∀̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)
renameFo ρ (∃̇∈ t φ) = ∃̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)

意味論の水準

Agrees ρ γ δ は、ρ で対応する変数に二つの環境が等しい値を割り当てることを表す。この条件は束縛子の下で環境を拡張しても保たれ、構造帰納法によって改名後の項の表示と論理式の充足関係が等しいと分かる。

構文だけでは改名が意味を保つかを言えず、環境を比較する必要がある。環境は構造の台の要素からなるベクトルで、長さは文脈と一致する。大きい文脈には γ : Vec S m、小さい文脈には δ : Vec S n である。問いはこう変わる。ρ の視点から、γ と δ はいつ同じ割り当てとみなせるのか。

module Sat {ℓ} (𝒮 : ZFStructureₕ ℓ)
           {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) where

open ZFStructure 𝒮

private module Sem = FOL.Semantics 𝒮

答えが関係 Agrees ρ γ δ である。小さい文脈の各索引 i について、δ の i での値と γ の ρ i での値が台におけるパスとして等しくなければならない。参照の向きに注意してほしい。ρ は小さい文脈から大きい文脈へ向かうので、δ が i に割り当てるのは γ が ρ i に割り当てる値とちょうど同じである。n = 2 の例では、本体の変数 1 での一致は lookup (ρ 0) γ ≡ lookup 1 δ と読める。つまり大きい環境は像の位置で小さい環境と一致しなければならない。

open Sem.At K ι using ( _⊨_; ⟦_⟧ )

Agrees : ∀ {n m} → (Fin n → Fin m) → Vec S m → Vec S n → Type ℓ
Agrees ρ γ δ = ∀ i → lookup (ρ i) γ ≡ lookup i δ

正しさの定理：改名された論理式の大きい環境における意味は、元の論理式の小さい環境における意味と同じである。まず項から始め、いつもの帰納法に進む。各場合は同余性であり、束縛子の場合は agrees∷ を経由する。弱化 (使われない変数の挿入)、交換、縮約はすべて特殊例で、ρ を選ぶことによって得られる。

定理は公式の帰納法で進むので、一致関係は量詞の下の一歩を生き延びなければならない。実際に生き延ぶ。両方の環境に位置ゼロで同じ要素 x を加えると、x ∷ γ と x ∷ δ は liftρ ρ の下で一致する。索引ゼロでは計算から両辺とも x を読み、索引 suc i での要求は既存の ag i に帰着する。この補題 agrees∷ は、構文の持ち上げに対応する意味論上の対応物である。

agrees∷ : ∀ {n m} {ρ : Fin n → Fin m} {γ : Vec S m} {δ : Vec S n}
          (x : S) → Agrees ρ γ δ → Agrees (liftρ ρ) (x ∷ γ) (x ∷ δ)
agrees∷ x ag zero    = refl
agrees∷ x ag (suc i) = ag i

すべては二つの定理にかかっている。項については、γ と δ が ρ の下で一致するという仮定のもとで、大きい環境 γ で renameTm ρ t を評価したものは、小さい環境 δ で t を評価したものへのパスになる。公式では同様の主張が充足の命題を比較する。仮定 Agrees ρ γ δ が主張に実質を与える。環境の間に何の関係もなければ、表示の等しいことは成り立ちようがない。

⟦⟧-rename : ∀ {n m} (ρ : Fin n → Fin m) (t : Term K n)

項の証明は短い。項の中身が少ないからである。定数は環境に依存せず ι k を表すので、二つの評価は refl で同じである。変数 var i は小さい側では lookup i δ、大きい側では lookup (ρ i) γ を表し、索引 i での一致がまさに両者をつなぐパスなので、ag i がこの場合を閉じる。本質は一つ上の公式の定理にある。

            (γ : Vec S m) (δ : Vec S n) → Agrees ρ γ δ
          → ⟦ renameTm ρ t ⟧ γ ≡ ⟦ t ⟧ δ
⟦⟧-rename ρ (con k) γ δ ag = refl
⟦⟧-rename ρ (var i) γ δ ag = ag i

⊨-rename : ∀ {n m} (ρ : Fin n → Fin m) (φ : Formula K n)

公式の定理は二つの命題の間のパスを述べる。大きい側の γ ⊨ renameFo ρ φ と、小さい側の δ ⊨ φ である。まず例の有界量詞を考える。その本体にはさらに束縛子がない。残りの場合はここで述べる同余と再帰という二つの型のどちらかに従う。原子公式では、項の定理が改名された項と元の項の表示の間のパスを与え、cong₂ がそのパスを集合の所属関係や等号を通して運ぶ。結合子の場合も対応する論理演算に cong₂ を使い、偽は refl で足りる。

           (γ : Vec S m) (δ : Vec S n) → Agrees ρ γ δ
         → (γ ⊨ renameFo ρ φ) ≡ (δ ⊨ φ)
⊨-rename ρ (t ∈̇ u)  γ δ ag = cong₂ _∈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
⊨-rename ρ (t ≐ u)  γ δ ag = cong₂ _≈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
⊨-rename ρ (φ ∧̇ ψ)  γ δ ag = cong₂ _⊓_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)

無制限の存在量詞 ∃̇ φ の下では、充足は台のすべての候補要素 x を渡るので、証明は両側の x の関数が各点で等しいことを示さねばならず、ここで funExt が登場する。各 x で両側の環境は拡張 x ∷ γ と x ∷ δ であり、agrees∷ x ag により liftρ ρ の下で一致する。これは小さい公式での帰納法の仮定にほかならない。ここが設計全体の要点である。一致関係は拡張の下で保たれるように作られているので、再帰呼び出しがそのまま通る。

⊨-rename ρ (φ ∨̇ ψ)  γ δ ag = cong₂ _⊔_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
⊨-rename ρ (φ ⇒̇ ψ)  γ δ ag = cong₂ _⇒_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
⊨-rename ρ ⊥̇        γ δ ag = refl
⊨-rename ρ (∃̇ φ)    γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
  ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))

非有界な全称量化子 ∀̇ φ は双対で、∃[ x ] P x の代わりに ∀[ x ] P x を使い、funExt と agrees∷ の手順は同じである。有界全称量詞 ∀̇∈ t φ は二つの材料を組み合わせる。その充足は、x ∈ˢ ⟦ t ⟧ γ から本体の充足への含意についての x に対する ∀[ x ] P x である。限界は項の定理が供給する x ∈ˢ_ を通る cong を寄与し、本体は liftρ ρ での再帰呼び出しを寄与し、cong₂ _⇒_ が両者を含意の間の求めるパスへ接合する。

⊨-rename ρ (∀̇ φ)    γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
  ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))
⊨-rename ρ (∀̇∈ t φ) γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
  cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
            (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

有界存在量詞 ∃̇∈ t φ が鏡像の形で帰納を閉じる。x に対する ∃[ x ] P x、改名された限界 x ∈ˢ ⟦ t ⟧ γ を ⊓ で本体の充足に結び、agrees∷ を経る同じ再帰呼び出しである。決して使われなかったものに注目してほしい。ρ の単射性である。定理は任意の写像 Fin n → Fin m に対して述べられているので、二つの変数を一つへ畳み込むこと (縮約) も、変数を間隔を空けて並べること (弱化) も、順序を入れ替えること (交換) も、同じく許される。

⊨-rename ρ (∃̇∈ t φ) γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
  cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
            (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

まとめ

変数の改名は、構文写像、環境の一致、定理 ⊨-rename からなる。文脈の写像を選ぶことで、この一つのインターフェースを弱化、交換、縮約へ特殊化できる。