数理論理学 初級

証明体系を組み立てる

この章について

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

前提知識

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

目次

自然演繹

証明体系の標準形。

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

健全性と完全性

証明できる ⟺ 真。

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

λ計算入門

計算の最小モデル。

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

直観主義論理 vs 古典論理

排中律をめぐって。

  • 排中律 $A \lor \neg A$
  • 構成的証明とは
  • sangi が構成的にこだわる理由

次のステップ

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

読み物

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

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

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

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

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

数学者の証明とプログラマのコードは、じつは同じものの二つの顔だった。「命題は型、証明は項、証明の整理は計算」――カリー＝ハワード対応の驚きを、二人の論理学者の物語とともに気軽に語る。