書記が数学やるだけ#954 健全性の証明-2，代入補題

健全性の証明において代入補題が必要なものをここで整理する。

問題

説明

代入補題とは、一階述語論理の意味論において、「論理式の中の変数を別の『項』に置き換えてから意味を評価すること」と、「変数の割り当てをあらかじめ書き換えてから元の論理式の意味を評価すること」が完全に一致することを示した定理である。

解答

項に対する代入補題の証明について，「項の物理的な書き換え」と「割り当ての事前更新」がもたらす値の一致を、項の構造に関する帰納法で示す。

この結果をベースに、論理式 α の真偽（充足関係）においても代入補題が成立することを，(i) 原子論理式・(ii) 含意（β→γ）(iii) 全称記号（∀wβ）のそれぞれについて，論理式の構造に関する帰納法で示す。

代入補題の具体例について。

左辺の検証：α[1,2,3] の記号代入を行い、α[τ/v]=P(f(f(w))) を導出する。初期状態 s の下でこれを評価し、真理値（T または F）を確定させる。

右辺の検証：項 τ=f(w) の解釈値 s(τ) を計算し、更新された割り当て s′=s[v↦s(τ)] を具体的に求める。この s′ の下で元の論理式 P(f(v)) を評価する。

代入補題を用いた推論規則・妥当式の健全性の証明を以下に示す。

本記事のもくじはこちら：