『コンピュータは数学者になれるのか？――数学基礎論から証明とプログラムの理論へ』(照井一成青土社 2015)

著者：照井一成［てるい・かずしげ］(1971-)
装幀：岡孝治［おか・こうじ］
NDC：410.9　集合論．数学基礎論
件名：記号論理学
件名：情報科学

青土社 ||科学／数学／生物：コンピュータは数学者になれるのか？

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-

作者:照井一成
青土社

Amazon

【目次】
目次　[001-003]

はじめに　007

1 数学者を作ろう　011
1.1　数学者とは何か　012
　　数学者は証明する
　　言語と推論規則
　　初等数論から始めよう

1.2　人工言語を画定する　016
　　初等数論の言語
　　項と論理式
　　省略表現
　　束縛変数と自由変数
　　文の真偽
　　有界論理式
　　 $\Sigma_{1}$ 論理式と $\Pi_{1}$ 論理式

1.3　推論規則を画定する　030
　　公理と推論規則
　　等号の使い方を定める規則
　　数論規則の使い方を定める規則
　　論理記号の使い方を定める規則

1.4　形式系：ある架空の数学者　042
　　形式系と数学者
　　数学者 $Q$ 氏
　　整数や有理数を表現する
　　 $Q$ 氏＝小学生？

1.5　数学者を育成する　049
　　数学者 $I \Sigma_{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 \Sigma_{1}$ の計算能力
　　整列集合と選択公理

3.3　超限順序数の世界　164
　　数の拡大
　　無限の向こう側へ
　　順序数を $\omega$ 進法で表す
　　順序数と数列集合
　　もう一つの寓話
　　数学における整列性

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　2つの論理　292
　　構成的でない証明
　　真理条件と検証条件
　　古典数学者と構成的数学者の対話
　　クライゼル計画
　　制御演算子と古典論理
　　 CPS変換
　　構成性の理解に向けて

5.4　証明の意味 310
　　証明とは連続写像である
　　証明とは線形写像である
　　記号に意味を与えよ

6　対角線方向にむかう未来　321
　　第1章「数学者を作ろう」　
　　第2章「対角線上に追い詰めろ」　
　　第3章「計算よ停まれ！」　
　　第4章「NPの壁」　
　　第5章「活き活きした証明」　
　　数学基礎論からコンピュータ科学へ
　　ヘイルズ［Thomas Callister Hales］の困惑
　　ロボットは東大に入れるか？
　　コンピュータは数学者になれるのか？
　　人間からの学習
　　証明支援系+自動定理証明+機械学習
　　対角線方向へ！

文献一覧　[345-352]
謝辞　[353]
索引　[355-357]