数理論理学と型理論 100 本ノック

修士100 問。全問無料です。

対象読者: 本テーマ第 1〜9 章（一階述語論理、ZFC、計算可能性、不完全性定理、ラムダ計算、カリー＝ハワード対応、依存型理論、Lean）の内容を一通り学んだ修士課程レベルの人。

テーマの目次へ（数理論理学と型理論）

執筆: Claude Code（Opus 5.5）、Claude Code（Sonnet 5.5）・監査 2 回（Claude Code）・最終 2026-10-12

読み込んでいます…

この冊について（出典・構成・使う定理）

主な参考文献

• H. B. Enderton, A Mathematical Introduction to Logic
• K. Kunen, Set Theory
• M. H. Sørensen, P. Urzyczyn, Lectures on the Curry–Howard Isomorphism
• R. Nederpelt, H. Geuvers, Type Theory and Formal Proof

問題はすべて Rikai の書き下ろしです。参考文献の演習や本文は転載していません。

構成

• 1〜13: 一階述語論理と完全性定理
• 14〜26: 公理的集合論 ZFC
• 27〜38: 計算可能性
• 39〜50: 不完全性定理
• 51〜61: 型なしラムダ計算
• 62〜73: 単純型付きラムダ計算とカリー＝ハワード対応
• 74〜83: 依存型理論
• 84〜92: 証明支援系 Lean の仕組み
• 93〜100: Lean による数学の形式化

形式: 単一選択 35・複数選択 16・○× 10・数値 15・並べ替え 8・誤り探し 8・記述 8。難易度 ★〜★★★★: 0 / 41 / 50 / 9。

この冊で使う定義・定理（144）

• 定義 3.1 群・アーベル群 群論入門：群の公理と、対称性を計算するための言葉 → 95 番
• 定理 7.1 カントールの定理 濃度と無限：全単射で測る「無限の大小」 → 98 番
• 定理 5.1 商集合の普遍性 関係と同値関係：「同じ」とは何か（同値類・商集合・well-defined） → 96 番
• 公理 2.1 ZFC の公理 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 14, 17, 25 番
• 系 5.4 順序数の集まりについて 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 23 番
• 定義 6.1 基数 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 18, 21 番
• 定義 8.1 連続体仮説 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 24 番
• 定義 4.2 デデキントの切断 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 19, 26 番
• 定義 4.4 切断の演算 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 19 番
• 定義 3.1 後者と自然数 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 16, 20 番
• 定義 5.1 順序数 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 16, 23 番
• 演習 9.2 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 18 番
• 演習 9.1 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 25 番
• 補題 6.2 無限基数は極限順序数 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 18, 21 番
• 補題 5.2 順序数の基本性質 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 16 番
• 命題 7.1 選択公理と順序数 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 22 番
• 命題 2.2 すべての集合の集合は存在しない 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 14 番
• 注意 5.7 置換公理がなぜ要るか 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 17 番
• 定理 8.2 連続体仮説の独立性（ゲーデル、コーエン） 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 24 番
• 定理 4.3 切断の全順序性と上限性質 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 26, 99 番
• 定理 6.3 ヘッセンベルクの定理 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 15 番
• 定理 5.3 順序数の比較可能性 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 15, 22 番
• 定理 3.2 ペアノの公理 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 20 番
• 定理 3.3 再帰的定義の原理 公理的集合論 ZFC：数学のすべてを「集合」から組み立てる → 17 番
• 系 7.3 停止問題の補集合は半決定可能でない 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 31, 33, 37 番
• 定義 7.1 停止問題 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 30, 35 番
• 定義 5.1 機械の番号 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 27 番
• 定義 4.1 部分再帰関数 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 29, 32, 38 番
• 定義 3.1 原始再帰関数 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 29 番
• 定義 2.2 機械が計算する関数 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 28 番
• 例 2.3 後者関数を計算する機械 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 27 番
• 補題 8.1 パラメータの固定（s-m-n） 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 34, 37 番
• 補題 5.2 1 ステップの算術化 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 28 番
• 命題 3.2 原始再帰関数の道具箱 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 29 番
• 注意 6.4 チャーチ＝チューリングの提唱 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 36 番
• 注意 7.4 決定問題とのつながり 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 31 番
• 定理 6.3 チューリング計算可能性と部分再帰性の一致 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 36 番
• 定理 7.2 停止問題の決定不能性 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 31, 32, 33, 35 番
• 定理 5.3 クリーネの標準形定理 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 33, 37 番
• 定理 6.2 部分再帰関数はチューリング計算可能 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 32, 37 番
• 定理 8.2 ライスの定理 計算可能性：チューリング機械・再帰関数・停止問題とライスの定理 → 30, 34, 35 番
• 定義 8.1 Prop と Type 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 75, 81, 83, 84 番
• 定義 5.1 恒等型 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 76, 77, 80, 82 番
• 定義 2.1 判断 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 77 番
• 定義 3.1 Π 型（依存関数型） 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 74, 78 番
• 定義 4.1 Σ 型（依存対型） 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 74, 78, 82 番
• 定義 7.1 宇宙 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 81 番
• 例 6.2 加法と 0 + n = n 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 77, 79, 90 番
• 演習 9.3 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 80 番
• 演習 9.2 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 79 番
• 命題 5.2 等号の基本性質 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 76, 92 番
• 命題 8.2 ∃ から証人を取り出せない理由 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 75, 81, 83 番
• 定理 4.2 型理論版の選択公理 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 75 番
• 定理 5.3 UIP と関数外延性の独立性 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 80 番
• 定理 7.2 ペアノの第 4 公理 依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く → 79 番
• 定義 3.2 意味論的帰結 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 2 番
• 定義 4.1 論理公理と導出 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 5 番
• 定義 2.2 項と論理式 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 1, 4, 11 番
• 定義 3.1 構造と充足 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 2, 10 番
• 定義 5.5 項モデル 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 3, 6 番
• 例 6.3 「有限」は一階では表せない 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 8, 12 番
• 例 3.3 群の公理からの帰結 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 2 番
• 例 6.2 非標準モデル 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 11 番
• 演習 7.4 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 9 番
• 演習 7.1 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 10 番
• 補題 4.6 新しい定数の変数化 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 13 番
• 補題 5.2 ヘンキン公理を足しても無矛盾 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 6 番
• 補題 5.3 ヘンキン理論 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 7 番
• 補題 5.4 リンデンバウムの補題 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 3, 6, 7 番
• 補題 3.4 代入補題 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 1 番
• 補題 5.6 真理補題 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 3, 6, 7 番
• 注意 6.5 スコーレムのパラドックス 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 9 番
• 定理 6.1 コンパクト性定理 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 8, 11, 12 番
• 定理 5.7 ゲーデルの完全性定理（可算言語） 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 7, 44 番
• 定理 6.4 レーヴェンハイム–スコーレムの定理 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 9 番
• 定理 4.3 健全性 一階述語論理と完全性定理：「証明できる」と「真である」が一致する理由 → 5, 13 番
• 演習 6.3 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 93, 94, 97, 100 番
• 演習 6.4 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 97 番
• 演習 6.1 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 95 番
• 補題 4.1 1 次元の拡張 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 99 番
• 命題 3.1 符号反転の well-defined 性 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 96 番
• 注意 2.1 Mathlib の代数階層 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 95 番
• 定理 4.2 有限次元のハーン–バナッハの定理 Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 → 99 番
• 系 5.2 G は真である ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 44 番
• 定義 4.1 ゲーデル数 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 41 番
• 定義 3.1 無矛盾性・完全性・健全性・帰納的公理化可能性 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 39, 42 番
• 定義 2.2 ペアノ算術 PA とロビンソン算術 Q ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 41 番
• 定義 4.2 証明可能性述語と無矛盾性の文 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 43, 48, 50 番
• 例 8.3 グッドスタインの定理 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 45, 47 番
• 例 5.4 G が偽になるモデル ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 44 番
• 例 3.4 掛け算を捨てると完全になる ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 39 番
• 例 3.5 真の算術は完全だが公理化できない ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 39, 40 番
• 演習 9.3 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 45 番
• 演習 9.1 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 39 番
• 演習 9.2 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 42 番
• 補題 4.3 対角化補題（不動点補題） ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 43, 48 番
• 命題 3.3 完全性から決定可能性へ ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 40 番
• 命題 8.1 Π₁ 文が反証できないなら、それは真である ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 45 番
• 注意 8.4 連続体仮説は事情が違う ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 24 番
• 注意 6.3 ゲンツェンの無矛盾性証明とヒルベルトの計画 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 46 番
• 注意 6.2 レープの定理と、証明可能性の作法 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 46 番
• 注意 5.3 ロッサーによる改良 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 49 番
• 定理 5.1 第一不完全性定理（ゲーデル、1931 年） ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 40, 43, 49, 50 番
• 定理 6.1 第二不完全性定理（ゲーデル、1931 年） ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 42, 46, 50 番
• 定理 4.4 タルスキの真理定義不可能性 ゲーデルの不完全性定理：「真だが証明できない」とは何のことか → 48 番
• 系 4.6 チャーチ＝ロッサーの帰結 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 54, 57, 58, 59, 61 番
• 定義 3.1 β 簡約 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 53, 54, 58, 60 番
• 定義 6.1 チャーチ数と λ 定義可能性 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 53, 59, 60 番
• 定義 2.1 λ 項 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 51, 52 番
• 定義 2.2 置換 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 52 番
• 例 6.3 チャーチ数の演算 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 59 番
• 例 3.2 簡約のいろいろな振る舞い 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 54, 61 番
• 演習 7.2 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 55 番
• 演習 7.1 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 60 番
• 補題 4.3 並行簡約の基本性質 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 56 番
• 補題 4.4 並行簡約と置換 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 56 番
• 補題 4.5 三角補題 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 55, 56 番
• 定理 4.1 チャーチ＝ロッサーの定理 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 55, 56, 61 番
• 定理 5.1 不動点定理 型なしラムダ計算：関数の適用と置換だけで計算を書き尽くす → 57 番
• 公理 6.1 Lean の公理 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 88, 89 番
• 定義 7.1 de Bruijn 基準 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 87, 93, 97, 100 番
• 定義 3.1 定義的同値 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 85, 86, 90, 91, 96, 98 番
• 定義 2.1 カーネルの型付け規則（概略） 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 84, 87 番
• 演習 8.1 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 85 番
• 注意 3.2 定義的同値の判定アルゴリズム 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 86 番
• 定理 6.3 ディアコネスクの定理 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 88, 89, 92 番
• 定理 6.2 関数外延性 証明支援系 Lean の仕組み：カーネル・定義的同値・tactic・三つの公理 → 88, 89, 91 番
• 定義 5.1 BHK 解釈 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 73 番
• 定義 4.1 含意の自然演繹 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 68 番
• 定義 3.2 還元可能な項 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 66 番
• 定義 2.1 単純型付きラムダ計算 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 62, 63, 71 番
• 例 2.3 自己適用には型が付かない 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 65 番
• 演習 6.4 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 69, 73 番
• 演習 6.3 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 69 番
• 演習 6.2 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 64 番
• 補題 3.5 基本補題 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 67 番
• 補題 3.3 還元可能性の 3 条件 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 66, 67 番
• 補題 2.2 生成補題と型の一意性 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 62, 64, 70, 71 番
• 補題 4.3 正規形の形 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 70, 71, 72 番
• 補題 3.4 抽象の還元可能性 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 66, 67 番
• 注意 3.6 テイトの方法の要点 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 65 番
• 定理 4.2 カリー＝ハワード対応（含意の断片） 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 68, 69, 72 番
• 定理 3.1 強正規化定理 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 63, 65, 67, 72 番
• 定理 2.5 主部簡約定理 単純型付きラムダ計算とカリー＝ハワード対応：証明はプログラムである → 64, 72 番