健全性と完全性
「証明できる ⟺ 真」はなぜ言えるか
初級（大学1-2年レベル）
このページの目標
構文の $\vdash$ と意味の $\models$ を結ぶ二つの橋、健全性（導けたことは真）と完全性（真なら導ける）を理解する。両者がそろって初めて「証明できる ⟺ 真」が言えることを知る。
1. $\vdash$ と $\models$ をつなぐ二つの方向
入門で見たとおり、$\Gamma \vdash A$（規則で導ける）と $\Gamma \models A$（すべてのモデルで真）は別の定義である。両者の関係には、向きの違う二つの問いがある。
2. 健全性：導けたことは真
健全性 (soundness)
$\Gamma \vdash A \;\Rightarrow\; \Gamma \models A$。すなわち、証明体系で導けた式は、意味的にも（$\Gamma$ を真にするどのモデルでも）真である。
健全性は「証明体系が嘘を導かない」ことの保証である。これがなければ、規則で導けても実は偽、という事態が起こり、証明に意味がなくなる。証明したい中心はむしろこちらで、信頼の最低条件と言える。
証明は比較的やさしい。各推論規則について「前提がすべて真なら結論も真」（真理を保存する）ことを一つずつ確かめ、証明の構造（長さ・木の高さ）に関する帰納法でつなげればよい。自然演繹の各規則は、まさにこの真理保存を満たすように設計されている。
3. 完全性：真なら導ける
完全性 (completeness)
$\Gamma \models A \;\Rightarrow\; \Gamma \vdash A$。すなわち、意味的に正しい（$\Gamma$ から論理的に帰結する）式は、証明体系で必ず導ける。
完全性は「証明体系が真理を取りこぼさない」ことの保証である。健全性と逆向きで、こちらは一般にずっと示しにくい。一階述語論理に対しては Gödel の完全性定理（1929）として成り立ち、典型的には「導けない式には、それを偽にするモデルが作れる」という対偶を、極大無矛盾集合などを用いて構成する。
古典命題論理でも完全性は成り立ち、入門で触れた「規則で導ける ⟺ 恒真式」という同値がこれにあたる。
4. 完全性と不完全性は別物
名前が紛らわしいが、完全性定理と 不完全性定理 は対象が違う。完全性定理は「論理的に妥当な式はすべて導ける」という論理についての主張である。不完全性定理は「算術のような特定の理論には、真だがその理論内では証明できない命題がある」という主張である。前者は論理の妥当性、後者は特定理論の証明能力の限界を述べており、矛盾しない。
健全性と完全性は、構文（証明）と意味（真理）という二つの世界がきれいに対応することを保証する、論理学の土台となる結果である。この対応があるからこそ、「証明を作る」という構文的作業に「真理を確かめる」という意味的目標を安心して託せる。
まとめ
この章のポイント
- 健全性：$\Gamma \vdash A \Rightarrow \Gamma \models A$（導けたことは真。嘘を導かない）
- 完全性：$\Gamma \models A \Rightarrow \Gamma \vdash A$（真なら導ける。取りこぼさない）
- 両者がそろうと「証明できる ⟺ 真」が成り立つ
- 健全性は規則の真理保存＋帰納法、完全性（一階）は Gödel の完全性定理
- 完全性定理と不完全性定理は対象が異なり矛盾しない
よくある質問
健全性とは何か
「証明できることは真である」という性質、すなわち $\Gamma \vdash A$ ならば $\Gamma \models A$ が成り立つことである。証明体系が嘘を導かないこと（推論規則が真理を保存すること）を保証する。各規則が真理を保つことを確認し、証明の長さに関する帰納法で示す。
完全性とは何か
「真であることは証明できる」という性質、すなわち $\Gamma \models A$ ならば $\Gamma \vdash A$ が成り立つことである。意味的に正しい主張を証明体系が一つ残らず導けることを保証する。一階述語論理では Gödel の完全性定理として成り立つ。
完全性定理と不完全性定理は矛盾しないのか
矛盾しない。完全性定理は「論理的に妥当な式は導ける」という論理についての主張、不完全性定理は「算術のような特定の理論には真だが証明できない命題がある」という主張で、対象が異なる。前者は論理の妥当性、後者は特定理論の証明能力の限界を述べている。