健全性と完全性：証明と意味論の対応関係 - 記号論理学

健全性（soundness）と完全性（completeness）は、証明体系と意味論の関係を表す重要な概念です。この2つが成り立つとき、「証明できること」と「論理的に正しいこと」が一致します。

意味論と構文論

論理学には2つの側面があります。意味論（semantics）は真理値や論理的帰結を扱い、構文論（syntax）は証明や導出を扱います。

意味論では、Γ ⊨ φ は「前提 Γ がすべて真のとき結論 φ も真」を意味します。構文論では、Γ ⊢ φ は「前提 Γ から証明規則を使って φ が導出できる」を意味します。

健全性と完全性は、この2つの世界をつなぐ橋渡しの役割を果たします。

健全性とは

健全性（soundness）とは、証明可能な式はすべて論理的に正しい、という性質です。

もし Γ ⊢ φ ならば Γ ⊨ φ

これは「証明体系が嘘をつかない」ことを意味します。証明規則に従って導いた結論は、必ず意味論的にも正しいのです。

完全性とは

完全性（completeness）とは、論理的に正しい式はすべて証明可能である、という性質です。

もし Γ ⊨ φ ならば Γ ⊢ φ

これは「証明体系に漏れがない」ことを意味します。意味論的に正しいことは、証明規則を使ってすべて導けるのです。

完全性は健全性の逆方向です。両方が成り立つとき、⊨ と ⊢ は一致します。

命題論理の健全性と完全性

命題論理において、自然演繹も公理系も健全かつ完全です。つまり、命題論理では「証明できる」ことと「トートロジーである」ことが完全に一致します。

健全性の証明は比較的容易です。各推論規則が妥当な推論であることを確認すればよいのです。たとえばモーダスポネンスは、真理値表で確認すると確かに妥当です。

完全性の証明はより技巧的です。任意のトートロジーに対して証明が構築できることを示す必要があります。

完全性定理の意義

命題論理の完全性定理は、1920年代にポストとベルナイスによって示されました。

この定理の意義は、真理値表という「機械的な」方法と、証明という「人間的な」方法が同じ結果を与えることを保証する点にあります。どちらの方法を使っても、正しい命題を漏れなく特定できます。

強完全性と弱完全性

完全性には2つのバージョンがあります。

弱完全性は、トートロジーがすべて証明可能、つまり ⊨ φ なら ⊢ φ です。前提のない場合です。

強完全性は、任意の前提からの帰結が証明可能、つまり Γ ⊨ φ なら Γ ⊢ φ です。これはより一般的な主張です。

命題論理では、弱完全性から強完全性が導けます。演繹定理と呼ばれる補助定理を使います。

次回からは、命題論理を超えた述語論理の世界に入っていきます。