数理論理学 中級

型理論と証明論

この章について

中級では、現代の証明アシスタントを支える理論に踏み込む。単純型理論 = 高階論理 (HOL) は HOL Light や Isabelle/HOL の土台であり、シーケント計算とカット除去、強正規化・停止性は「なぜ型検査が必ず終わるか」「なぜ証明を機械的に正規化できるか」という証明論の核心を与える。最後に LCF アーキテクチャ（小さな信頼カーネル＋非信頼タクティク）を軸に、HOL Light / Isabelle / Coq / Lean の基盤の違いを概観する。

前提知識

  • 初級編（自然演繹、λ計算、健全性・完全性）
  • 計算可能性は 計算理論 と接続する

目次

単純型理論 = HOL

高階論理の土台。

  • 単純型と Church の型
  • 高階の量化
  • HOL Light / Isabelle の基盤

シーケント計算・カット除去

証明論の主定理。

  • シーケント $\Gamma \vdash \Delta$
  • カット規則と除去
  • 部分論理式性

強正規化・停止性

計算が必ず終わる。

  • 正規形と簡約
  • 強正規化定理
  • 型検査の決定性

計算可能性・決定可能性

何が機械で判定できるか。

  • 決定可能・半決定可能
  • 停止性問題
  • 型検査と証明検査の違い

証明アシスタント概観・LCF

小さなカーネルを信頼する。

  • LCF アーキテクチャ
  • HOL Light / Isabelle / Coq / Lean
  • タクティクは信頼しない

次のステップ

中級で HOL とカット除去、LCF アーキテクチャをつかんだら、上級編へ進み、依存型理論 (MLTT / CIC)、Gödel の不完全性定理、de Bruijn 基準と TCB、ZFC・HOL・型理論の比較を学ぼう。証明アシスタントの実例は Lean による証明 も参照。

読み物

ヒルベルトの夢と、その先 ［読み物］

数学をまるごと機械的に確かめたい ―― ヒルベルトの壮大な計画とその限界、そして夢の跡地からカット除去・正規化・証明アシスタントが育った逆転劇を物語として読む。

「正しい」と「証明できる」のあいだ ［読み物］

真であることと証明できることは同じなのか。意味の世界（モデル）と記号の世界（形式体系）を、健全性と完全性定理がどう橋渡しするのか、その「気持ち」を気軽に語る。