書記が数学やるだけ#951 証明の形式化-1

構文論における証明の形式化を整備する。

問題

本問において，公理は嘉田『数理論理学』に基づいたものを用いる。

説明

演繹とは、あらかじめ与えられた「前提（仮定）の集合 Γ」と、その論理体系で正しいと認められている「公理」から出発し、定められた「推論規則」のみを有限回適用して、新たな論理式をステップ・バイ・ステップで導き出す一連の記号列のことである。この成否は純粋に構文論的（シンタックス、すなわち記号の形とルールのみ）に決定され、個々の論理式が持つ具体的な「意味（真偽）」には依存しない。

特に，前提となる仮定の集合 Γ が空集合である（＝何の前提も置かない）場合の演繹を、特に証明と呼ぶ。

解答

演繹定理（Γ,A⊢B⇒Γ⊢A→B） ：「A であると仮定して議論を進め、首尾よく B が導出できたなら、仮定を外して『A ならば B である』と結論づけてよい」という、日常的な数学的推論を正当化する。

演繹定理の逆（Γ⊢A→B⇒Γ,A⊢B） ：「A→B」という関係が成立している体系に、新たな事実として前提「A」を追加すれば、前件肯定（Modus Ponens）によって機械的に「B」を導出できることを保証する。

この一対の定理により、「含意（→）の証明」と「仮定（前提）の追加・削除」の自由な往来が可能となる。

全称記号（∀）の導入を構文論的に制御するための、変数の出現制約に関わるメタ定理である。

一般化定理（Γ⊢ψ⇒Γ⊢∀vψ）： 導出された論理式 ψ 内の変数 v が、前提集合 Γ のどの論理式にも自由出現していなければ、その v は完全に任意であるとみなして、安全に ∀v を付与できることを示す。

定数の一般化（Γ⊢φ[c/v]⇒Γ⊢∀vφ） ：数学の証明における「任意の定数 c について議論し、最後に全称化する」という手続きの形式化である。前提 Γ に一切出現しない任意の定数記号 c について主張が成立すれば、それはすべての v について成り立つことと同義となる。

存在例化（Γ,α[c/v]⊢β⇒Γ,∃vα⊢β） ：存在命題「∃vα」から結論 β を導く際、直接 ∃ を扱う代わりに、既存の論理式や前提と重複しない仮の定数記号 c を導入し、「α[c/v]」を仮定して演繹を進める手法である。結論 β が定数 c の固有の性質に依存せず導出できれば、元の存在前提のみから β を導いたとみなすことができる。

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