数理論理学と型理論

数学修士無料 9 章有料 0 章

一階述語論理の完全性定理、ZFC、計算可能性、不完全性定理から、ラムダ計算、カリー＝ハワード対応、依存型理論、Lean の仕組みと数学の形式化までを一貫して扱う。

想定読者: 大学院生（修士課程）・数学や物理を深く学びたい人

前提テーマ:数学基礎、代数学（群・環・体）

このテーマの 100 本ノック（100 問）

目次

1. 第 1 章一階述語論理と完全性定理無料一階述語論理の構文と意味論を定義し、ヒルベルト流の証明体系の健全性とゲーデルの完全性定理をヘンキンの構成で証明する。コンパクト性定理、レーヴェンハイム–スコーレムの定理、非標準モデルを導く。
2. 第 2 章公理的集合論 ZFC無料ZFC の公理を一つずつ述べ、自然数・整数・有理数・実数を集合として構成して上限性質を証明する。順序数と超限帰納法、基数算術 κ·κ=κ、選択公理の同値形を示し、連続体仮説の独立性を述べる。
3. 第 3 章計算可能性無料チューリング機械と原始再帰・μ 再帰関数を定義して両者の等価性を示し、停止問題の決定不能性とライスの定理を、対角線論法と万能関数から証明する。「アルゴリズムで解ける」を数学の対象にする。
4. 第 4 章不完全性定理無料ペアノ算術のような形式体系を定義し、ゲーデル数化と対角化補題を組み立てて第一・第二不完全性定理の主張を正確に述べる。真理と証明可能性のずれ、非標準モデル、リーマン予想の独立性まで踏み込む。
5. 第 5 章型なしラムダ計算無料λ 項と β 簡約を定義し、並行簡約と完全展開によるチャーチ＝ロッサーの定理を証明する。不動点結合子で再帰を実現し、チャーチ数で再帰関数がちょうど λ 定義可能な関数であることを示す。
6. 第 6 章単純型付きラムダ計算とカリー=ハワード対応無料単純型付きラムダ計算の主部簡約定理と、テイトの還元可能性による強正規化定理を証明する。直観主義の自然演繹の証明と型付き λ 項が一対一に対応し、β 簡約が証明の回り道の除去になることを示し、BHK 解釈と Lean のコードで読み解く。
7. 第 7 章依存型理論無料マーティン＝レーフ型理論の Π 型・Σ 型・恒等型・宇宙・帰納型を規則として述べ、型理論版の選択公理、等号の対称性と輸送、0≠1 を規則から証明する。CIC の Prop と Type の区別、関数外延性と UIP の独立性まで、Lean 4 のコードと対応させて解説する。
8. 第 8 章証明支援系 Lean の仕組み無料Lean 4 が証明を確認する仕組みを、カーネルの型検査と定義的同値（β・δ・ι・ζ・η）、エラボレーションと単一化、tactic が項を作る過程に分けて説明する。公理 Quot.sound から関数外延性を、選択公理からディアコネスクの定理で排中律を証明し、de Bruijn 基準で信頼の境界を定める。
9. 第 9 章Lean による数学の形式化無料Lean 4 で群の公理系を型クラスの階層として定義して基本性質を証明し、商で整数を構成し、カントールの定理を形式化する。Mathlib の実数と測度論、バナッハの不動点定理と有限次元ハーン–バナッハの定理の形式化を Rikai の証明と対応させ、形式化が保証しないものを整理する。