LanguageEL - 41semicolon/41semicolon.github.io GitHub Wiki

代入/衝突判定/帰結関係

代入・衝突判定・帰結関係でワンセット。教科書によって少しずつ定義が異なるがその目的は同じ。代入に関する失敗例を避けるため。例えば∃y(x≠y)にy/xをすると∃y(y≠y)となり意味が異なる。回避するためにどれかの定義をいじる:

Rautenberg流: 少しきつめ
- 衝突判定(φとt/x): var(t)-{x} のすべての変数が bnd(φ) に含まれない
- 代入: (∀xφ)[t/x] = ∀xφ もしくは (∀yφ)[t/x] = ∀y(φ[t/x])。
- 帰結関係: 非衝突の場合 ∀xφ ⊢ φ[t/x](全称例化) φ[t/x] ⊢ ∃xφ(存在汎化)
戸次流: 標準的？
- 衝突判定(∀yφとt/x): x∉free(φ) または y∉free(t)
- 代入: (∀xφ)[t/x] = ∀xφ, 非衝突なら (∀yφ)[t/x] = ∀y(φ[t/x]), 衝突時はリネーム
- 帰結関係: ∀xφ ⊢ φ[t/x](全称例化) φ[t/x] ⊢ ∃xφ(存在汎化)

あと Kleene流があるかも。

意味論的なあれこれ

∀の意味論が難しいワケ : ∀の意味論は「M ⊨ ∀xα ⇔ M[a/x] ⊨ α ただし a は a ∈ A なる全ての値」となる。これを理解したい。左辺は∀を含む論理式の充足性に関する言明だ。右辺は x に対する値付けがちょっとづつ違う |A| 個のモデルに関する言明だ。つまり、「∀を含む論理式の充足性をしらべる時は、∀を外した論理式に対して |A| 個の場合分けをしたうえで充足性を議論しなくてはならない」となり、これなら直観的にも納得がいく。また別の意味で特徴的なのは、M における充足性を調べるために M じゃないモデルの充足性の結論を必要とする点。

代入・大域代入

変数を項に移す操作を代入という。(例: x↦1 や x↦x+4 や x↦z+4)。

さて、Var → Term なる写像(term function)を定め、Constant → Constant には恒等写像を定めると、帰納的に Term → Term が定まり、最終的にFormula → Formula な写像も定まる。この写像を大域代入 σ という。ここで、帰納的に定める部分はほぼ自明だが量化子が絡む部分だけ注意が必要。つまり σ(∀xα) = ∀x τ(α)。ここでτは τ(x) = x, τ(y) = σ(y) なる代入 τ。

一度大域代入の概念がわかると、同時代入や１変数の代入は大域代入の一種とみなせる。

代入の制約

∃y.x=y において代入 y/x を施すと ∃y.y=y となるが(意味論を考えると)まずそうだ。統語的な操作としての代入の定義はそのままに、意味論的に代入を無制限に許さない仕組みが必要。そのための条件が collision free 判定となる。つまり「collision free なら、代入操作を行ってよい」というような規則をつくる。なお、以下の定義を大域代入に拡張するのは自然にできる:

定義: collision free
CL(φ, t/x) :=  ∀(y∈var t). y ∉ bndφ - {x}

CLが成立する例1 (定数代入):
 - φ: ∃x(x≠y), σ: [a/x]
 - φ: ∃x(x≠y), σ: [a/y]
 - φ: ∃x(x≠y), σ: [a/z]
CLが成立する例2 (恒等代入):
 - φ: ∃x(x≠y), σ: [x/x]
CLが成立する例3 (新規変数の代入)
 - φ: ∃x(x≠y), σ: [z/x]
 - φ: ∃x(x≠y), σ: [w+z/x]
CLが成立する例4 (代入元 x 関連)
 - φ: ∃x(x≠y), σ: [x+1/x]
 - φ: ∃x(x≠y), σ: [x+z/x]
CLが成立する例5 (代入先で未束縛)
 - φ: ∃x(x≠y), σ: [y/x]
 - φ: x≠y, σ: [y/x]

CLが成立しない例1 (代入先で束縛)
 - φ: ∃y(x≠y), σ: [y/x]

CL を確認するための手順

Step1: 代入項 t を見て (代入元である) x 以外の変数を列挙して、そいつらが
Step2: 代入先 φ にいなければOK。あるならその変数について
Step3: 束縛されてなければOK。なければNG。

代入と変異

意味論では構造＋割り当てを与えて式の充足性を見る。特に量化子のついた論理式の意味は、モデルの変異という概念によって応えられる。そして、モデルの変異は、代入と密接に結びついている。

例えば、∀x.x=x という論理式の充足性を考える際、我々はx↦0やx↦1や・・・・といった割り当てを複数考えてそれぞれの充足性を見る。これは複数の変異を考えるということだが、一方で、論理式に対して 0/x, 1/x, ... などの代入操作をして得られた論理式と結びついていることがわかる（注: 0,1,...は定数として定義されているとした）。

これらを数理的に整備すると以下の定理が得られる:

以下が成立する。ただし登場する代入は全て collision free である

M ⊨ φσ ⇔ Mσ ⊨ φ (代入の定理)
∀Xφ ⊨ φ[T/X] (全称例化)
φ[T/X] ⊨ ∃Xφ (存在汎化)
s=t, φ[s/x] ⊨ φ[t/x]

注：教科書によっては全称例化や存在汎化は無制限に許されるように定義されていることがある（というかそっちの方が多い）。