数理論理学 中級

型理論と証明論

この章について

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

前提知識

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

目次

単純型理論 = HOL

高階論理の土台。

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

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

Gentzen 流証明論の中心定理。

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

強正規化・停止性

簡約はいつ、なぜ止まるのか。

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

計算可能性・決定可能性

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

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

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

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

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

次のステップ

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

読み物

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

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

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

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

数学が自分の限界を語るとき ［読み物］

自然数の算術を含むほど豊かで、かつ無矛盾な体系には、その体系では証明も反証もできない命題が残る。「自分はこの体系では証明できない」と述べる文をどう組み立てたのか、ゲーデルの不完全性定理を気軽に語る。

うそつきのパラドックス ［読み物］

「この文は偽である」は、真としても偽としても反対の結論が跳ね返る。自分自身を否定的に指す文が生む矛盾の正体と、ゲーデルが自己言及を形式体系の中へ持ち込んだ道を気軽に語る。

同じ公理、ちがう世界 ［読み物］

自然数の一階の公理を満たす世界は一つとは限らない。ふつうの自然数も、余分な要素を持つ非標準の世界も等しく従う。モデルという考え方と言葉と世界のずれを気軽に語る。