Lemma_3_2_5.md

論理式

ϕ, ψ := A | ⊥ | R₁ t | R₂ (t₁, t₂) | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ∀x.ϕ | ∃x.ϕ

A は命題記号
x は変数記号
t,t₁,t₂ は項
R₁は1変数述語記号
R₂は2変数述語記号

構造的帰納法

∀ P, (
　　(P(⊥)) ∧
　　(∀ A, P (A)) ∧
　　(∀ t R₁, P (R₁ t)) ∧
　　(∀ t₁ t₂ R₂, P (R₂ (t₁, t₂))) ∧
　　(∀ ϕ, P(ϕ) → P(¬ϕ)) ∧
　　(∀ ϕ ψ, P(ϕ) → P(ψ) → P(ϕ ∧ ψ)) ∧
　　(∀ ϕ ψ, P(ϕ) → P(ψ) → P(ϕ ∨ ψ)) ∧
　　(∀ ϕ ψ, P(ϕ) → P(ψ) → P(ϕ → ψ)) ∧
　　(∀ x ϕ, P(ϕ) → P(∀x.ϕ)) ∧
　　(∀ x ϕ, P(ϕ) → P(∃x.ϕ))
) → ∀ ϕ, P(ϕ)

注意: メタ論理の論理記号と対象言語の論理記号を区別なく使ってるから、いい感じに読み替えていただきたく🙏

参考 - 数学的帰納法
∀ P, P(0) ∧ (∀ n, P(n) → P(n+1)) → ∀ n, P(n)

定理3.2.5

M　: 対象領域がDのストラクチャー
s,t 　: D拡大閉項
x 　: 変数記号
ϕ　: x以外の自由変数が出現しないD拡大閉論理式

M(s) = M(t) ならば M(ϕ[s/x]) = M(ϕ[t/x])

証明

P(ϕ) := (ϕにx以外の自由変数が出現しないならば)M(ϕ[s/x]) = M(ϕ[t/x])
とした構造的帰納法を使う

(i) 命題記号や⊥の場合
簡単のため、P(⊥)のみ示す
つまり、 M(⊥[s/x]) = M(⊥[t/x]) を示せばよい。
ところが、⊥に自由変数xは出現しないので、⊥[s/x] = ⊥[t/x] = ⊥
よって、M(⊥[s/x]) = M(⊥) = M(⊥[t/x])
任意の命題記号Aについても、同様に示せる

(ii) 述語の場合
教科書では具体例を挙げて証明としてるが、厳密に証明するなら、一般に成り立つ事を言いたい。
詳細は「補足」に譲る

(iii) ¬ψ の場合
帰納法の仮定より M(ψ[s/x]) = M(ψ[t/x])
この時、M(¬ψ[s/x]) = M(¬ψ[t/x]) を示せばよい

M(¬ψ[s/x])
　= not M(ψ[s/x]) 　-- 便宜的に、真偽を反転させるメタ関数notを導入
　= not M(ψ[t/x]) 　-- 帰納法の仮定
　= M(¬ψ[t/x]) 　　-- 定義3.2.4

(iv) ψ ∧ ρ, ψ ∨ ρ, ψ → ρ の場合

簡単のため、P(ψ ∧ ρ)のみ示す

帰納法の仮定より
M(ψ[s/x]) = M(ψ[t/x]) かつ M(ρ[s/x]) = M(ρ[t/x])
この時、M((ψ∧ρ)[s/x]) = M((ψ∧ρ)[t/x]) を示せばよい

M(ϕ[s/x])
　= M((ψ∧ρ)[s/x])
　= M(ψ[s/x]∧ρ[s/x]) 　　　 　-- p.33 「代入の分配」を参照
　= M(ψ[s/x]) かつ M(ρ[s/x]) 　-- 定義3.2.4
　= M(ψ[t/x]) かつ M(ρ[t/x]) 　-- 帰納法の仮定
　= M(ψ[t/x]∧ρ[t/x]) 　　　 　-- 定義3.2.4
　= M((ψ∧ρ)[t/x])　　　　 　　-- 代入の分配
　= M(ϕ[t/x])

P(ψ ∨ ρ), P(ψ → ρ) についても同様に示せる　　

(v) ∀y.ψ, ∃y.ψ の場合

簡単のため、∀y.ψ の場合だけ示す

帰納法の仮定より M(ψ[s/x]) = M(ψ[t/x])
この時、M((∀y.ψ)[s/x]) = M((∀y.ψ)[t/x]) を示せばよい

x = y の場合、ψにxは自由出現しないので、(i)と同様に題意は満たされるので、
x ≠ y の場合のみ考える。

M((∀y.ψ)[t/x])
　= M(∀y.ψ[t/x]) 　　　　　　　　　　　　　　-- 代入の分配、x ≠ y より
　= 任意の変数記号aに対して、M(ψ[t/x][a/y]) 　-- 定義3.2.4
　= 任意の変数記号aに対して、M(ψ[s/x][a/y]) 　-- 帰納法の仮定
　= M(∀y.ψ[s/x])　　　　　　　　　　　　　　-- 定義3.2.4

補足1（項への代入についての補題）

項

t, t₁, t₂ := x | c | F₁ t | F₂ t₁ t₂

x は変数記号、c は定数記号、F₁, F₂ は関数記号

構造的帰納法

∀ P, (
　　(∀ x, P(x)) ∧
　　(∀ c, P(c)) ∧
　　(∀ F₁ t, P(t) → P(F₁ t)) ∧
　　(∀ F₂ t₁ t₂, P(t₁) → P(t₂) → P(F₂ t₁ t₂))
) → ∀ t, P(t)

定義3.2.5の補題

定義3.2.5と同様の前提において、任意のD拡張項t,t₁,t₂ に対して
M(t₁) = M(t₂) ならば、M(t[t₁/x]) = M(t[t₂/x])

証明

変数記号、定数記号の場合
代入操作で値が変わりうるのはtがxと一致する場合のみであり
M(x[t₁/x]) = M(t₁) = M(t₂) = M(t[t₂/x])
それ以外は自明

関数記号の場合
簡単のため、F₁ tの場合だけ示す
帰納法の仮定より、 M(t[t₁/x]) = M(t[t₂/x])
この時、M((F₁ t)[t₁/x]) = M((F₁ t)[t₂/x]) を示せばよい

M((F₁ t)[t₁/x])
　　= F₁ $^M$ (M(t[t₁/x]))
　　= F₁ $^M$ (M(t[t₂/x]))
　　= M((F₁ t)[t₂/x])

補足2(構造的帰納法の導出)

Knaster-Tarskiの最小不動点定理

完備束L上の単調関数fに対して、
　　μf = ⋀{X ⊆ $\mathcal{U}$ | f(X) ⊆ X}
が最小不動点となる

証明は割愛
完備束、単調関数の定義も割愛
fの最小不動点とは、f(X) = X となるXのうち最小のもの

帰納原理

μfの定義より直ちに以下が導ける 　　f(X) ⊆ X → μf ⊆ X

論理式についての帰納原理の導出

記号列の集合 $\mathcal{U}$ に対して、f : $\mathcal{P(U)}$ → $\mathcal{P(U)}$ を構築する

f(X) =
　　{⊥} ∪
　　{命題記号の集合} ∪
　　{R₁ t | R₁は1変数述語記号, tは項} ∪
　　{R₂ (t₁, t₂) | R₂は2変数述語記号, t₁, t₂は項} ∪
　　{¬ϕ | ϕ ∈ X} ∪
　　{ϕ ∧ ψ | ϕ, ψ ∈ X} ∪
　　{ϕ ∨ ψ | ϕ, ψ ∈ X} ∪
　　{ϕ → ψ | ϕ, ψ ∈ X} ∪
　　{∀x.ϕ | xは変数記号, ϕ ∈ X} ∪
　　{∃x.ϕ | xは変数記号, ϕ ∈ X}

$\mathcal{P(U)}$が完備即である事、fが単調関数である事の証明は割愛

次に、帰納法で証明したい述語をPとして、帰納原理でのXを{X | P(X)}とすると、以下が言える。
　　f({X | P(X)}) ⊆ {X | P(X)} → μf ⊆ {X | P(X)}
これが、構造的帰納法の帰納原理とほぼ同じ

参考文献

再帰的定義の数学的取り扱い
型システム入門 プログラミング言語と型の理論
論理プログラミングの基礎