著者：照井 一成［てるい・かずしげ］(1971-)
装幀：岡 孝治［おか・こうじ］
NDC：410.9 集合論．数学基礎論
件名：記号論理学
件名：情報科学
青土社 ||科学／数学／生物：コンピュータは数学者になれるのか？
【目次】
目次 [001-003]
はじめに 007
1 数学者を作ろう 011
1.1 数学者とは何か 012
数学者は証明する
言語と推論規則
初等数論から始めよう
1.2 人工言語を画定する 016
初等数論の言語
項と論理式
省略表現
束縛変数と自由変数
文の真偽
有界論理式
Σ_1論理式とΠ_1論理式
1.3 推論規則を画定する 030
公理と推論規則
等号の使い方を定める規則
数論規則の使い方を定める規則
論理記号の使い方を定める規則
1.4 形式系：ある架空の数学者 042
形式系と数学者
数学者Q氏
整数や有理数を表現する
Q氏＝小学生？
1.5 数学者を育成する 049
数学者IΣ_1氏
関数を定義する
数学者PA氏
実数は取り扱えないということ
2階の数学者たち
形式系の拡大と矛盾
1.6 ヒルベルト計画 064
歴史を振り返る
ヒルベルトの困惑
ヒルベルト計画発動
無矛盾性と健全性
2 対角線上に追い詰めろ 075
2.1 対角線論法とは何か 076
無限集合の比較
対角線論法
ラッセルのパラドックス
連続体仮説
2.2 言語の限界 086
ゲーデル符号化
連続関数の不動点
論理式の不動点
真理定義不能性
2.3 計算の限界 097
計算課題とプログラム
計算課題と決定可能性
無限大学の合格発表
コンピュータの限界
コンピュータの誕生
論理式の複雑さと計算の困難さ
2.4 証明の限界 111
形式系再び
第一不完全性定理
補足 1：ロッサ―化
補足 2：ヒルベルトの決定問題
2.5 第一不完全性から第二不完全性へ 126
第二不完全性定理
人間 vs. コンピュータ
ヒルベルト計画と不完全性定理
人工読者のための本
3 計算よ停まれ！ 137
3.1 数列の生成と停止 138
停まるか停まらぬか？
コラッツの予想
計算よ停まれ！
3.2 全員整列！ 144
整列集合
超限の国の買い物事情
多重集合が整列していること
木とケーニッヒの補題
定理3.3の証明
整列集合と計算の停止
原始再帰的でない関数
IΣ_1の計算能力
整列集合と選択公理
3.3 超限順序数の世界 164
数の拡大
無限の向こう側へ
順序数をω進法で表す
順序数と数列集合
もう一つの寓話
数学における整列性
3.4 ゲンツェンの無矛盾性証明 178
そして数学基礎論へ
ゲンツェンが成し遂げたこと
独立命題の研究へ
形式系の分離
証明は動き始める
ゲンツェンの死
4 NPの壁 195
4.1 しらみつぶしと数学知性 199
一筆書きできますか？
指数関数ヤバイ
定理は計算を速くする
高速化に限界はあるか？
ディオファントス方程式再び
マッチング
4.2 P・NPとは何か 213
Pの考え方
入力サイズについて
NPの考え方
P対NP問題
4.3 NP完全性：一蓮托生の難間たち 220
計算課題を別課題に還元する
NP完全問題
最初のNP完全問題
NP完全問題がいっぱい
NP完全問題に立ち向かう
4.4 計算・言語・証明の限界、再び 228
対角線論法の威力
対角線論法の限界
計算課題を論理式で表す
多項式時間階層のの崩壊
有界の数学者たち
4.5 P対NPの現在、未来、そして過去 247
計算複雑性理論の拡がり
P対NP問題の決着
ゲーデルの決定問題
NPの壁を回避せよ
5 活き活きした証明 257
5.1 ラムダ計算 258
関数を作ること、使うこと
ラムダ計算の基本
計算の具体例
ラッセルのパラドックス再び
5.2 証明はプログラムである 268
構成的証明
BHK解釈［Brouwer–Heyting–Kolmogorov interpretation］
カリー・ハワード対応［Curry–Howard correspondence］
“ゲーデル・ゲンツェン対応”
初等数論における証明とプログラム
構成的プログラミング
構成計算と証明支援系Coq
5.3 ２つの論理 292
構成的でない証明
真理条件と検証条件
古典数学者と構成的数学者の対話
クライゼル計画
制御演算子と古典論理
CPS変換
構成性の理解に向けて
5.4 証明の意味 310
証明とは連続写像である
証明とは線形写像である
記号に意味を与えよ
6 対角線方向にむかう未来 321
第1章 「数学者を作ろう」
第2章 「対角線上に追い詰めろ」
第3章 「計算よ停まれ！」
第4章 「NPの壁」
第5章 「活き活きした証明」
数学基礎論からコンピュータ科学へ
ヘイルズ［Thomas Callister Hales］の困惑
ロボットは東大に入れるか？
コンピュータは数学者になれるのか？
人間からの学習
証明支援系+自動定理証明+機械学習
対角線方向へ！
文献一覧 [345-352]
謝辞 [353]
索引 [355-357]
