数理論理学 初級

証明体系を組み立てる

この章について

初級では、証明体系そのものを実際に組み立てる。自然演繹は各論理結合子に「導入規則」と「除去規則」を与える体系で、証明検査カーネルの論理層を理解するための基本的なモデルになる。さらに、組み立てた証明体系が意味論とどう噛み合うか（健全性と完全性）、計算のモデルである λ計算、そして 直観主義論理 vs 古典論理（排中律を認めるか）という、構成的数学にとって決定的な分岐点を学ぶ。

前提知識

  • 入門編（構文と意味の区別、推論規則の発想）
  • 関数と写像の基本

目次

自然演繹

導入規則と除去規則による代表的な証明体系。

  • 導入規則と除去規則
  • 仮定の放電
  • 証明木

健全性と完全性

証明可能性と、意味論的な妥当性を結ぶ二つの定理。一階述語論理では両者が一致する（Gödel の完全性定理）。

  • 健全性 $\vdash \Rightarrow \models$
  • 完全性 $\models \Rightarrow \vdash$
  • 構文と意味を結ぶ橋

λ計算入門

計算をとらえる基本的な形式モデル。

  • 型なし λ計算と β簡約
  • 単純型付き λ計算
  • 項と型

直観主義論理 vs 古典論理

排中律をめぐって。

  • 排中律 $A \lor \neg A$
  • 構成的証明とは
  • 構成的証明を重視する理由

次のステップ

初級で自然演繹と λ計算をつかんだら、中級編へ進み、単純型理論と高階論理 (HOL)、シーケント計算とカット除去、強正規化、そして証明アシスタントの基盤と LCF アーキテクチャを学ぼう。直観主義論理は既存記事 構成的証明 とも接続する。

読み物

「計算しよう」― 推論を計算にする夢 ［読み物］

ライプニッツが夢みた推論の機械化を、ブールの代数からフレーゲの記号法、そして自然演繹の規則へとつながる一本の物語として気軽にたどる。

命題から述語へ ［読み物］

「すべての人間は死ぬ」をなぜ命題論理で書けないのか。述語と量化子 ∀∃ がどう世界の解像度を上げ、ソクラテスの三段論法を通したのかを肩の力を抜いて語る。

証明はプログラムだった ［読み物］

数学者の証明とプログラマのコードのあいだには、驚くほど深い対応がある。カリー＝ハワード対応では「命題は型、証明は項、証明の整理は計算」――その驚きを、カリーとハワードの物語とともに気軽に語る。