数理論理学
Mathematical Logic — 証明・型・計算の数学
このシリーズについて
数理論理学は、数学的な「推論」や「証明」そのものを数学の対象として厳密に扱う分野である。「証明とは何か」「何を信頼の土台にするか」「どの論理基盤を選ぶか」という問いに、形式体系の理論で答えを与える。
本シリーズは、形式体系の構文と意味の区別という入口から始め、自然演繹、健全性と完全性、λ計算と型理論、Curry–Howard 対応、依存型理論、Gödel の不完全性定理、そして de Bruijn 基準・信頼計算基盤 (TCB)・証明アシスタントの設計へと進む。最終的には、構成的実数を土台にした証明検査カーネルの設計まで、入口から現代の定理証明系の現在地までを筋道立てて辿ることを目標とする。
レベル別学習
学習の流れ
主な学習内容
構文と意味
記号の操作（構文）と、それが何を意味するか（意味）の区別。形式体系を理解する出発点。
証明 ＝ プログラム
Curry–Howard 対応。命題は型、証明は項、簡約は計算。型理論ベースの証明系の背骨。
健全性と完全性
「証明できる」と、ある意味論のもとで「妥当である」がいつ一致するか。構文と意味を結ぶ二つの橋。一階述語論理についての Gödel の完全性定理と、特定の形式体系についての不完全性定理は別の主張である。
体系の限界
Gödel の不完全性定理。算術を十分に表現できる無矛盾な形式体系は、一定の条件のもとで、自分自身の無矛盾性をその体系の内部では証明できない。
信頼計算基盤 (TCB)
de Bruijn 基準・小さな検査カーネル・「生成器 → 検査器」。何を信頼すれば証明を信頼できるか。
代表的な 3 つの基礎づけ
ZFC（集合論）・HOL（高階論理）・型理論。数学を建てる土台の代表的な選択肢とその違い（ほかに圏論的な基礎づけや HoTT/UF もある）。
なぜ数理論理学を学ぶのか
数理論理学を学ぶ理由は複数ある：
- 証明の本質：「証明とは何か」を直感ではなく形式的に理解する
- 信頼の土台：何を公理・規則として認めれば数学が建つかを知る
- 計算との対応：Curry–Howard 対応により、論理の証明と型付き計算の間に深い対応があることが分かる
- 証明アシスタント：Coq・Lean・Isabelle・HOL Light の理論的基礎を理解する
- 形式検証：seL4・CompCert・Flyspeck のような大規模検証を支える原理を学ぶ
関連・応用分野
- 証明アシスタント：Coq・Lean・Agda・Isabelle・HOL Light
- 形式検証：OS カーネル (seL4)、コンパイラ (CompCert)、数学定理 (Flyspeck)
- プログラミング言語理論：型システム、型安全性、依存型
- 数学基礎論：集合論・モデル理論・再帰理論との接点
- 計算機による数学：構成的数学、証明検査カーネルの設計
よくある質問
数理論理学とは何か
数理論理学は、数学的な推論・証明・計算そのものを数学の対象として厳密に研究する分野である。形式体系の構文と意味、証明の構造（証明論）、論理と型・プログラムの対応（型理論・Curry–Howard 対応）、体系の限界（不完全性定理）などを扱い、証明アシスタントや形式検証の理論的基礎を与える。
証明とプログラムが同じものだというのはどういう意味か
Curry–Howard 対応とは、命題が型に、証明がその型を持つプログラム（項）に、証明の簡約が計算に対応するという発見である。「$A$ ならば $B$」の証明は「$A$ 型の入力から $B$ 型の出力を作る関数」に対応する。この対応が Coq・Lean・Agda などの型理論ベースの証明アシスタントの背骨になっている。
健全性と完全性の違いは何か
健全性 (soundness) は「証明できることは真である」（証明体系が嘘を導かない）こと、完全性 (completeness) は「真であることは証明できる」（真理を取りこぼさない）ことを指す。ここでいう「真」は、ある意味論のもとで妥当であることを指す。両者が成り立てば「証明できる ⟺ 妥当」となり、構文（証明）と意味（真理）が一致する。たとえば一階述語論理には、標準的な意味論に対する Gödel の健全性・完全性定理がある。
なぜ証明アシスタントは小さなカーネルを信頼の土台にするのか
LCF アーキテクチャの考え方で、すべての証明を検査する小さなコア（信頼計算基盤・TCB）だけを信頼し、証明を生成するタクティクは信頼しない設計を指す。タクティクにバグがあっても、生成された証明はカーネルが必ず再検査するため、不健全な結論は通らない（fail-closed）。信頼すべきコードを最小化することで、体系全体の信頼性を一点に集約できる。
完全性定理と不完全性定理は矛盾しないのか
対象が違うので矛盾しない。Gödel の完全性定理は一階述語論理という論理そのものについての主張で、「標準的な意味論で妥当な式は証明体系で導ける」という。一方、不完全性定理は算術のような特定の形式体系についての主張で、「その体系の内部では証明も反証もできない文がある」という。前者は論理の妥当性、後者は個々の理論の証明能力の限界を述べている。