書評: 結城浩『数学ガール ゲーデルの不完全性定理』

数学ガール ゲーデルの不完全性定理の書評



結城浩による数学の小説『数学ガール』シリーズの第三巻だ。

コンピュータ科学、計算科学、計算可能性といった分野でゲーデルの不完全性定理が登場することがあり、それがどういったものか、どのようにして計算化学と関わっているのかを知りたく、本書を紐解いた。形式的体系、完全性、無矛盾性といった言葉はわかった。しかし、ゲーデルの不完全性定理の証明および計算科学との関係はわからなかった。

(追記 5月29日) ちなみに、この記事が著者にツイートされていた。




書評

不完全性定理までの導入はわかりやすいが、不完全性定理の説明は難しい

本書を読むと、


  • 形式的論理がどういったものか
  • 無矛盾性
  • 完全性

についてはよく学べる。他にも証明に入るまでの準備段階の「ペアノの公理」や、「形式的体系」、「カントールの対角線論法」、「ε-δ論法」の理解は捗るだろう。

大学の教養程度の数学なら得意だった自分は、本書のゲーデルの不完全性定理の証明は追えなかった。まるで著者が力尽きて投げやりになったかのように説明が舌足らずだった。厳密さに欠けるからかもしれないし。単に説明が足りないのかもしれない。的確な質問をしてくれるはずの登場人物も、忽然と聡明になり、僕はついていけず困ってしまった。具体的には、対角化や自己言及などは理解できなかった。

それでも、ゲーデルの不完全性定理に関する書物の中では、本書は特に容易に読み進めやすいものの一つだと思われる。他の本では、より一層面食らう人も多いのではないか。

ただ、著者はプログラマーなのだが、ゲーデルの不完全性定理と計算科学の関わり方についての記述はほとんどなかった。Wikipediaの再帰理論によれば、
チャーチ(1936a、1936b)とチューリング(1936)はゲーデルの不完全性定理の証明(1931)で用いられた技法に触発され、それぞれ独立に、ダフィット・ヒルベルトが1928年に提示した Entscheidungsproblem(決定問題)(en)が有効に決定できないことを示した。この結果は、任意の数学的命題が真か偽かを正しく判定するアルゴリズムが存在しないことを明らかにした。
といった記述がある(May 26, 2015 ,18:15)。不完全性定理がアルゴリズムの判定に関わっているらしく、興味深い。

ここまでは、私の主観的な考えに基づいた文章だ。


以下に、本書から学べることを客観的に述べた。

ゲーデルの不完全性定理に至るまで - 数学の基礎付けとヒルベルト計画 -

Kurt Friedrich Gödel

順を追って流れを書いた。

形式的体系、論理式、公理、証明、定理


形式的体系とは何か、論理式を定義し、その論理式の中から公理を定める。公理から出発して推論規則によって得られた論理式は全て定理と呼ばれる。公理というのは、証明を作るときに無条件で使える論理式のことだ。公理に真偽ない。論理式が証明されていることと、真であることは別だ。

形式的というのは、公理や論理式を文字列の操作だとみなす考え方のことを言う。例えば、

((A) → (B)) → (((¬(A))∨(A)) → ((¬(A)∨(B)))

が公理と言われても困るし、この論理構造を把握することは難しいが、意味を考えず、形だけを見て、ただの文字列だと思うことはできる。まるで、公理と推論規則を機械的に適用することで得られたものだと考えるということだ。

そもそも数学とは何か


そもそも、私たちが数学として扱うものは、どういったものなのか。
証明や公理と呼ばれるものは何なのか。
加算の+や、自然数の3といった算術は何なのか。

数学者は、数学を形式的体系とみなし、公理と推論規則を繰り返し適用した論理式の列を証明と呼び、その列の末項の論理式を定理と呼ぶことにした。形式的体系には様々なものが考えられるが、その中に私たちが日常的な意味で数学と呼ぶものがあるのではないか。

ヒルベルトによる数学の基礎付け計画はゲーデルの提出した論文によって失敗した

ダフィット・ヒルベルトという19-20世紀初頭に生きた数学者は、数学に剣虎な基礎を与えるためのヒルベルト計画を提唱した。それにより、数学は無矛盾で完全であるという基礎づけを行おうとした。しかし、それはゲーデルが不完全性定理を提出したことで、打ち破られた。

ゲーデルは25歳のとき『プリンキピア・マテマティカおよび関連した体系の形式的に決定不能な命題についてI』という論文を提出した。そこでは、要約すると次のような論文冒頭で始まる。


二つの包括的な形式的体系、つまりプリンキピア・マテマティカおよびツェルメロ・フランケルの集合論の公理系では、数学で使すべての証明が形式化できる。そのため、この体系では全ての数学的問題がこの体系の公理と推論で決定できると考えたくなるが。しかし、それは以下に示すように正しくない。


ゲーデルはその論文で、「無矛盾な形式的体系Pの中では、決定不能な文G (Gも¬Gも証明できない)」  (第一不完全性定理) を提示し、更に、「無矛盾な形式的体系Pの中では「形式的体系Pは無矛盾である」ことを示す形式的証明が形式的体系Pには存在しない」 (第二不完全性定理) を示した。

不完全性定理の持たれがちなイメージは見当違いだ

「打ち破られた」とか「理性の限界」と聞くと、ネガティブなイメージがつきまとうが、恐らくそれは見当違いだ。そもそも、「理性の限界」という表現は、ゲーデルが60歳になったときのお祝いの言葉としてオッペンハイマーが述べたもので、数学的な表明ではない(P.311)。ゲーデルの第二不完全性定理は
ある条件を満たす形式的体系には、自己の無矛盾性を表現する文の形式的証明は存在しない。(P.310)
というもので、数学の限界や欠陥を示したものではない。「ある条件を満たす形式的体系」についての定理だ。また、「不完全」と聞くと、ネガティブなイメージを持つかもしれないが、これも数学における意味であり、辞書の意味とは異なる。


原論文: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I


本書に出てきたことを整理

次に、以下に、主に本書P.311までの範囲に登場した項目をメモしておく。P.312以降から不完全性定理の証明が始まるが、それはまとめられなかった。

形式的体系Hのまとめ

論理式 F1 xが変数ならば、xは論理式である。
論理式 F2 xが論理式ならば、¬(x) も論理式である。
論理式 F3 xとyが論理式ならば、(x)∨(y)も論理式である。
論理式 F4 F1 - F3 で定められるものだけが論理式である。
(P.130)

記号 IMPLY →
記号 (x) → (y) を (¬(x))∨(y) と定義する。(P.133)

公理 P1 ((x)∨(x)) → (x)
公理 P2 (x) → ((x)∨(y))
公理 P3 ((x)∨(y)) → ((y)∨(x))
公理 P4 ((x) → (y)) → (((z)∨(x)) → ((z) ∨(y)))

推論規則 Modus Ponens xと、(x) → (y) から、yが推論できる。
(P.143)

ただし、ゲーデルの不完全性定理の証明では、形式的体系Pを構築する。プリンキピアマテマティカの体系PMにペアノの公理やいくつかの公理 (論理式の定義や、ペアノの公理、命題論理の公理、述語論理の公理)を加えたものだ。

意味の世界と形式の世界の対応

数学というものに意味を見出す世界と、機械的に文字列の処理を行う形式的世界の関係だ

意味の世界, 形式の世界
算術, 算術の形式的体系
述語や命題, 論理式
述語, 自由変数を含む論理式
命題, 自由変数を含まない論理式(文)
自然数, 数項
1, 1のゲーデル数
2, 1のゲーデル数' (ただし、「'」は後続数を表す)

(P.223)

述語と命題

二つの自由変数を持つ述語Rの自由変数に数m, nを代入してできる命題をR(m, n)とする
述語<<xはyで割り切れる>>は自由変数を持つので、それ自体では真偽が決まらないが、命題<<12は3で割り切れる>>は成り立つし、命題<<12は7で割り切れる>>は成り立たない>>
(P.329)

論理式と文

二つの自由変数を持つ論理式rの自由変数を数項で置換してできる文をr<m, n>
述語や命題は意味の世界、論理式や文は形式の世界の概念。rは論理式のゲーデル数で、r<mn>は文のゲーデル数
(P.329)

矛盾している形式的体系

数式的体系の、ある論理式Aに対して、Aと¬Aの両方とも、その形式的体系で証明できるとき、その形式的体系を矛盾しているという。
(P.212)

無矛盾な形式的体系

形式的体系の、どんな論理式Aに対しても、Aと¬Aの両方がその形式的体系で証明されることはないとき、その形式的体系は無矛盾であるという。
(P.213)

不完全な形式的体系

形式的体系の、ある文Aに対して、Aと¬Aの両方とも、その形式的体系で証明できないとき、その形式的体系は不完全であるという。
(P.214)

完全な形式的体系

形式的体系の、どんな文Aに対しても、Aと¬Aの少なくとも一方は、その形式的体系で証明できるとき、その形式的体系は完全であるという。
(P.215)

ヒルベルト計画


  • 形式的体系の導入: 数学を形式的体系として表現する。
  • 無矛盾性の証明: 数学を表現した形式的体系に<<矛盾がない>>ことを証明する。
  • 完全性の証明: 数学を表現した形式的体系が<<完全である>>ことを証明する。
(P.302)

対角化

f 一変数論理式
f<f> 一変数論理式fの自由変数をすべて、fのゲーデル数を数項にしたもので置き換えた文
(P.350)

ゲーデルの第一不完全性定理

ある条件を満たす形式的体系には、以下の両方が成り立つ文Aが存在する。
  • その形式的体系には、Aの形式的証明は存在しない。
  • その形式的体系には、¬Aの形式的証明は存在しない。
(P.309)

ゲーデルの第二不完全性定理

ある条件を満たす形式的体系には、自己の無矛盾性を表現する文の形式的証明は存在しない。
(P.309)




結城浩(2009). 『数学ガール ゲーデルの不完全性定理』. ソフトバンククリエイティブ (1800円+税)




コメント

人気の投稿