数理論理学
Mathematical Logic — 証明・型・計算の数学
このシリーズについて
数理論理学は、数学的な「推論」や「証明」そのものを数学の対象として厳密に扱う分野である。「証明とは何か」「何を信頼の土台にするか」「どの論理基盤を選ぶか」という問いに、形式体系の理論で答えを与える。
本シリーズは、形式体系の構文と意味の区別という入口から始め、自然演繹・健全性と完全性（証明論）、λ計算と型理論、Curry–Howard 対応、依存型理論、Gödel の不完全性定理、そして de Bruijn 基準・信頼計算基盤 (TCB)・証明アシスタントの設計へと進む。最終的には、構成的実数を土台にした証明検査カーネルの設計まで、入口から現代の定理証明系の現在地までを筋道立てて辿ることを目標とする。
レベル別学習
学習の流れ
主な学習内容
構文と意味
記号の操作（構文）と、それが何を意味するか（意味）の区別。形式体系を理解する出発点。
証明 ＝ プログラム
Curry–Howard 対応。命題は型、証明は項、簡約は計算。型理論ベースの証明系の背骨。
健全性と完全性
「証明できる」と「真である」がいつ一致するか。構文と意味を結ぶ二つの橋。
体系の限界
Gödel の不完全性定理。十分強い体系は自分自身の無矛盾性を証明できない。
信頼計算基盤 (TCB)
de Bruijn 基準・小さな検査カーネル・「生成器 → 検査器」。何を信頼すれば証明を信頼できるか。
3 つの基礎
ZFC（集合論）・HOL（高階論理）・型理論。数学を建てる土台の選択肢とその違い。
なぜ数理論理学を学ぶのか
数理論理学を学ぶ理由は複数ある：
- 証明の本質：「証明とは何か」を直感ではなく形式的に理解する
- 信頼の土台：何を公理・規則として認めれば数学が建つかを知る
- 計算との統一：Curry–Howard 対応により、論理と計算が同じものだと分かる
- 証明アシスタント：Coq・Lean・Isabelle・HOL Light の理論的基礎を理解する
- 形式検証：seL4・CompCert・Flyspeck のような大規模検証を支える原理を学ぶ
関連・応用分野
- 証明アシスタント：Coq・Lean・Agda・Isabelle・HOL Light
- 形式検証：OS カーネル (seL4)、コンパイラ (CompCert)、数学定理 (Flyspeck)
- プログラミング言語理論：型システム、型安全性、依存型
- 数学基礎論：集合論・モデル理論・再帰理論との接点
- 計算機による数学：構成的数学、証明検査カーネルの設計