健全性と完全性
「証明できる ⟺ 真」はなぜ言えるか
初級（大学1-2年レベル）
このページの目標
構文の $\vdash$ と意味の $\models$ を結ぶ二つの橋、健全性（導けたことは真）と完全性（真なら導ける）を理解する。両者がそろって初めて「証明できる ⟺ 真」が言えることを知る。
1. $\vdash$ と $\models$ をつなぐ二つの方向
入門で見たとおり、$\Gamma \vdash A$（規則で導ける）と $\Gamma \models A$（$\Gamma$ を真にするどのモデルでも $A$ が真）は別の定義である。両者の関係には、向きの違う二つの問いがある。
「真」の意味に注意 本ページで「真」と書くときは、つねに $\Gamma \models A$、すなわち$\Gamma$ を真にするどのモデルでも $A$ が真（論理的に真）という意味である。現実世界で正しい、という意味ではない。したがって「証明できる ⟺ 真」も、正確には「一階述語論理において、規則で導けること ⟺ すべてのモデルで真であること」という主張である。
2. 健全性：導けたことは真
健全性 (soundness)
$\Gamma \vdash A \;\Rightarrow\; \Gamma \models A$。すなわち、証明体系で導けた式は、意味的にも（$\Gamma$ を真にするどのモデルでも）真である。
健全性は「証明体系が嘘を導かない」ことの保証である。これがなければ、規則で導けても実は偽、という事態が起こり、証明に意味がなくなる。まず満たされていなければならないのはこちらで、証明体系を信用するための最低条件と言える。
証明は比較的やさしい。各推論規則について「前提がすべて真なら結論も真」（真理を保存する）ことを一つずつ確かめ、証明の構造（長さ・木の高さ）に関する帰納法でつなげればよい。自然演繹の各規則は、まさにこの真理保存を満たすように設計されている。
3. 完全性：真なら導ける
完全性 (completeness)
$\Gamma \models A \;\Rightarrow\; \Gamma \vdash A$。すなわち、意味的に正しい（$\Gamma$ から論理的に帰結する）式は、証明体系で必ず導ける。
完全性は「証明体系が真理を取りこぼさない」ことの保証である。健全性と逆向きで、こちらは一般にずっと示しにくい。一階述語論理に対しては Gödel の完全性定理（1930）として成り立ち、典型的には「導けない式には、それを偽にするモデルが作れる」という対偶を、極大無矛盾集合などを用いて構成する。
古典命題論理でも完全性は成り立ち、入門で触れた「規則で導ける ⟺ 恒真式」という同値がこれにあたる。
証明の筋道（雰囲気だけ） 完全性は次の対偶を示すことで得られる。(1) $\Gamma \vdash A$ でないとする。(2) すると $\Gamma \cup \{\neg A\}$ は無矛盾である。そこで言語に新しい定数（Henkin 定数）を追加し、存在文 $\exists x\, \varphi(x)$ のそれぞれに証人 $c$ を与える式 $\exists x\, \varphi(x) \to \varphi(c)$ を、無矛盾性を保ちながら足していく。(3) さらに極大無矛盾集合（それ以上どんな式を足しても矛盾してしまう、無矛盾な極大の集合）へ拡張し（Lindenbaum の補題）、その集合を設計図として、項そのものを個体とする項モデルを組み立てる。(4) できあがったモデルでは $\Gamma$ がすべて真で $A$ が偽になるから、$\Gamma \models A$ ではない。以上の対偶が完全性である。細部は本格的な論理学の教科書に譲る。
4. 完全性と不完全性は別物
名前が紛らわしいが、完全性定理と 不完全性定理 は対象が違う。完全性定理は「論理的に妥当な式はすべて導ける」という論理についての主張である。不完全性定理は「算術のような特定の理論には、真だがその理論内では証明できない命題がある」という主張である。前者は論理の妥当性、後者は特定理論の証明能力の限界を述べており、矛盾しない。
健全性と完全性は、構文（証明）と意味（真理）という二つの世界がきれいに対応することを保証する、論理学の土台となる結果である。この対応があるからこそ、「証明を作る」という構文的作業に「真理を確かめる」という意味的目標を安心して託せる。
5. 発展：完全性はどこまで成り立つか
この節は発展で、1〜4 節の目標は前節までで達成できている。ここまで単に「完全性」と述べてきたものは、正確には一階述語論理についての定理である。量化できるのは個体だけ、という制限を外して述語や集合そのものを量化できる高階論理へ進むと、この保証は失われる。
標準意味論の高階論理には、健全・完全・実効的な演繹体系がない
二階以上の論理を標準意味論（$n$ 項述語の変数は、台集合上のすべての $n$ 項関係を動くと読む解釈）で解釈するとき、健全かつ完全で、しかも公理と規則が機械的に検査できる（定理の集合が帰納的可算になる）演繹体系は存在しない。
理由は不完全性定理と表裏一体である。二階論理では帰納法を「すべての性質 $P$ について」という単一の公理として書けるため、二階ペアノ算術の公理を満たす構造は、同型を除いて $\mathbb{N}$ ただ一つになる（モデルが本質的に一つしかないこの性質を categorical、日本語では範疇的という。圏論とは無関係である）。だから算術の文 $\varphi$ について「公理から論理的に帰結する」ことと「$\mathbb{N}$ で真である」ことが一致する。もしここに健全・完全で、しかも証明を機械的に検査できる演繹体系があれば、証明を順に枚挙するだけで $\mathbb{N}$ で真な算術の文をすべて枚挙できてしまう。ところが標準モデル $\mathbb{N}$ で真な一階算術の文全体（真の算術）は帰納的可算ではない。したがってそのような体系はありえない。この事実は Gödel の不完全性定理や Tarski の真理定義不可能性と表裏一体である。
失われるのは完全性だけではない。コンパクト性定理も下向き Löwenheim–Skolem の定理も、標準意味論の二階論理では成り立たない。逆向きに見ると、抽象論理に対する自然な条件のもとで、この二つを保つ論理のうち最も表現力の高いものが一階述語論理であることが知られている（Lindström の定理）。表現力とメタ理論の良さは、あちらを立てればこちらが立たない関係にある。一階論理が数学の共通語として定着しているのは、この釣り合いの取れた位置にいるからである。
では HOL Light や Isabelle/HOL と完全性の関係は：これらの証明支援系が採用する高階論理は、標準意味論ではなく Henkin 意味論（一般モデル）で読む。関数型や述語型の領域を「考えうるすべての関数の集まり」に固定せず、内包公理を満たす適当な部分集合であればよい、とする解釈である。この読み替えのもとでは Henkin (1950) により完全性が回復し、体系は実質的に多ソートの一階論理として扱える。「高階論理は不完全である」という言い方は、あくまで標準意味論についての主張であって、実装された証明体系が壊れているという意味ではない。そもそも、与えられた証明を機械的に検査できることと意味論的な完全性は別の問題で、健全だが不完全な体系でも証明支援系としては十分に働く。
まとめ
この章のポイント
- 健全性：$\Gamma \vdash A \Rightarrow \Gamma \models A$（導けたことは真。嘘を導かない）
- 完全性：$\Gamma \models A \Rightarrow \Gamma \vdash A$（真なら導ける。取りこぼさない）
- 両者がそろうと「証明できる ⟺ 真」が成り立つ
- 健全性は規則の真理保存＋帰納法、完全性（一階）は Gödel の完全性定理
- 完全性定理と不完全性定理は対象が異なり矛盾しない
- 命題論理と一階述語論理は標準的な意味論に対して完全。一方、標準意味論の二階以上の論理には健全・完全・実効的な演繹体系がない（Henkin 意味論なら回復する）
参考文献
- Gödel, K. (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik und Physik, 37, 349–360.（一階述語論理の完全性定理）
- Henkin, L. (1949). "The completeness of the first-order functional calculus". Journal of Symbolic Logic, 14(3), 159–166.（極大無矛盾集合からモデルを作る現行の証明法）
- Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic, 15(2), 81–91.（一般モデルによる高階論理の完全性）
- Lindström, P. (1969). "On extensions of elementary logic". Theoria, 35(1), 1–11.（コンパクト性と Löwenheim–Skolem による一階論理の特徴づけ）
- Enderton, H. B. (2001). A Mathematical Introduction to Logic (2nd ed.). Academic Press.（健全性・完全性の標準的な教科書）
よくある質問
健全性とは何か
「証明できることは真である」という性質、すなわち $\Gamma \vdash A$ ならば $\Gamma \models A$ が成り立つことである。証明体系が嘘を導かないこと（推論規則が真理を保存すること）を保証する。各規則が真理を保つことを確認し、証明の長さに関する帰納法で示す。
完全性とは何か
「真であることは証明できる」という性質、すなわち $\Gamma \models A$ ならば $\Gamma \vdash A$ が成り立つことである。意味的に正しい主張を証明体系が一つ残らず導けることを保証する。一階述語論理では Gödel の完全性定理として成り立つ。
完全性定理と不完全性定理は矛盾しないのか
矛盾しない。完全性定理は「論理的に妥当な式は導ける」という論理についての主張、不完全性定理は「算術のような特定の理論には真だが証明できない命題がある」という主張で、対象が異なる。前者は論理の妥当性、後者は特定理論の証明能力の限界を述べている。
高階論理でも完全性定理は成り立つのか
標準意味論のもとでは成り立たない。二階以上の論理には、健全かつ完全で、しかも定理の集合が帰納的可算になる演繹体系が存在しない。これは二階ペアノ算術の範疇性と、真の算術（標準モデルで真な一階算術の文全体）が帰納的可算でないことから導かれる。ただし Henkin 意味論（一般モデル）で読み替えれば完全性は回復し、HOL Light や Isabelle/HOL はこの立場をとる。