コンピュータに数学研究ができないのはなぜ？

(1)

コンピュータに数学研究ができないのはなぜ？

ゲーデルの不完全性定理の紹介

北海道大学理学部数学教室辻下徹

1998.9.18

第 I 部

¹

2

1 不完全性定理前夜 3

1.1 形式システム. . . . 3

1.2 ヒルベルトの立場 . . . . 4

1.3 バッカス標準形 . . . . 5

1.4 ヒルベルト小伝 . . . . 5

1.5 カントールの楽園 . . . . 6

1.6 ラッセルのパラドックス(1903) . . . . 7

1.7 ラッセル小伝. . . . 7

2 形式システムの完全性と不完全性 8 2.1 形式主義の定式化 . . . . 8

2.2 自然数論PAに現れる記号. . . . 8

2.3 メタ数と形式的数 . . . . 9

2.4 自然数論PAの公理 . . . . 10

2.5 推論規則 . . . . 10

2.6 「定理」の定義 . . . . 12

2.7 証明の例 . . . . 12

2.8 論理式の真偽. . . . 12

2.9 形式システムの健全性 . . . . 13

2.10 形式システムの無矛盾性. . . . 13

2.11 ヒルベルトの夢：理論の完全性 . . . . 13

2.12 ゲーデルの完全性定理(1929) . . . . 14

2.13 ゲーデルの不完全性定理(1931) . . . . 15

2.14 ゲーデルのプラトニズム . . . . 15

2.15 形式システム：まとめ . . . . 16

2.16 演習問題 . . . . 16

第 II 部

²

17

3 ゲーデルの不完全性定理の証明 17 3.1 不完全性定理の証明：スケッチ . . . . 17

3.2 問題点：「論理式についての論理式」の意味付け. . . . 18

3.3 ゲーデル数 . . . . 19

3.4 計算可能関数の組み込み . . . . 19

3.5 代入操作と自己適用操作 . . . . 20

3.6 不動点定理. . . . 21

3.7 証明可能性判定プログラム. . . . 22

3.8 不完全性定理の証明の完結. . . . 24

3.9 形式主義がもたらしたもの. . . . 25

1「数学のたのしみ」(日本評論社)No.8 (1998.8)p104–114

2「数学のたのしみ」(日本評論社)No.9 (1998.10)掲載予定

(2)

4 ロベールの不動点定理 28

4.1 ロベールの不動点定理 . . . . 28

4.2 ロベールの不動点定理の応用リスト . . . . 28

4.3 カントールの対角線論法. . . . 29

4.4 ラッセルのパラドックス . . . . 29

4.5 タルスキーの真理定理 . . . . 30

4.6 プログラム停止問題の決定不能性 . . . . 30

4.7 生命システムでの不動点. . . . 31

4.8 心は脳の状態で表せない . . . . 31

4.9 自己印刷プログラム . . . . 33

5 まとめ 36 5.1 不完全性定理の含意 . . . . 36

5.2 数学の不定性. . . . 36

5.3 参考書 . . . . 37

第 I 部

２回にわけてクルト・ゲーデル（

1906-1978）が 1931

年に発見した不完全性定理について解説しようと思います。この有名な定理については数多くのよい解説書があるので、すでによく知っている高校生の方も多いと思います。しかし、数学という学問の鋭い切り口を与えるものとしては他に類を見ない定理ですので、数理論理学の専門家ではないですが、少なくともこれは知っておいてほしいと思う定理としてこれを取り上げることにしました。

今回は、不完全性定理を理解する鍵となる形式システムというものを明確にし、正しいことと証明できるということとの違いを明確にし、不完全性定理がどういうことを明らかにしたかを話します。

不完全性定理の証明は次回概略を話します。その後、証明に使われるゲーデル論理式の構成を普遍化したロベールの不動点定理を解説し、そのいろいろな応用を考えます。

タイトルの説明タイトルはいろいろな解釈が可能なので、何を話そうとしているのかをはっきりさせておこう。

タイトルの問いは「疑似問題」である。まず考えるべき本質的問題に気づかずに二次的問題を考える始めるとき、それは疑似問題であるという。もしも「コンピュータが数学を研究する」という文に意味がなければ、「コンピュータが数学研究ができるか否か」など考えることもできないし、ましてや「コンピュータが数学研究ができないのはなぜか」などと問うことは毛頭できない。

しかし、擬似問題は探索の出発点となる。それと取り組んでいるうちに、本当の問題が姿を表してくる。そういう点では、擬似問題は不可欠・不可避といってもよいかもしれない。どういう探索においても、本当の問題は何かということが最初の（そして場合によっては最後の）困難な問題だからだ。

最も楽な解答は、「コンピュータが数学研究をする」など無意味だ、従って、タイトルのような問いには全く何の意味もない、というものだ。

研究行為は、人間がすることであるからには論理的作業は氷山の一角に過ぎず、人間生物としての研究者のあらゆる面が研究行為に絡んでくる。この点を考慮すると、コンピュータが研究するなどと考えることは無理だ。しかし、この議論の論点はコンピュータは人間とは違うというだけで、一般的すぎて物足りない。

これからの話しでは、わざと数学研究の表層的な部分、数学を形式システムとして表現した部

(3)

分、だけに着目する。この部分であれば「コンピュータが数学を研究する」という文に「コンピュータが論理式を証明できるか否かを判定する」という具体的な意味を与えることができ、擬似問題であったタイトルの問いが真性問題となる。

なお、人工数学者

(Artificial Mathematician,

略して

AM)

という研究テーマがある。それは、数学研究における概念や定理の発見過程をコンピュータでシミュレートすることを目指すものであるが、これから話すことは

AM

研究の意義について何か否定的な主張するものであると誤解しないようにしてほしい。人工知能が思考理解への新しい切り口を与えたのと同様に、AM研究も数学研究プロセスの詳細理解への有効な新アプローチを与えることは明らかであるし、またそれ自身が奥の深い数学的研究テーマともなっている。

どういう立場でタイトルの問いを考えようとしているかを、少しわかっていただけたであろうか。

1 不完全性定理前夜

1.1 形式システム

序文で述べたように、研究成果の表現の仕方を通して数学を考えてみよう。これは、記号世界というスクリーンに数学を写して考えてみることともいえる。その映像には映っていないことがたくさんあり、数学そのものは本当は映像にはないのだが、その点には触れない。

数学は、いろいろな形（文字、数、図形など）をたくさん使う、しかも、効果的に本質的に使う。こういう「形」の一式とそれの取り扱い方を一緒にしたものを形式システムと呼ぶ。例えば、みなさんが一番よく馴染んでいるものの一つに、十進法と四則演算を込みにした、自然数の形式システムがある。

数の計算は、機械になったつもりで邪念なくやると間違いが少ない。2+3=? という計算を考えよう。数の形式システムを学び始める小学校１年の最初の頃は、2個の石の山と

3

個の石の山を合わせたらいくつの石の山になるかという問いとして、指を使って答えを出す。しかし、小学校２年になれば、一桁の数のたし算の結果は記憶しており即座に答えが出るし、桁数が多くなってもその記憶と繰上りの規則を組み合わせて、頭の片隅で機械的に計算ができるようになる。このような計算により

5312+4321=9633

という答えが出る場合、

` 5312 + 4321 = 9633

と書く。頭についた”`”という記号は、

5312 + 4321 = 9633

が計算により得られたことを表す。これを

5312 + 4321 = 9633

は証明できる、と読む。

これと対照的に、5312 個の小石の山と

4321

個の小石を合わせた石の山を数えてみて

9633

個となることを確認した場合には

| = 5312 + 4321 = 9633

と書く。頭についた”|

=”

という記号は、5312 + 4321 = 9633が、数や足し算の意味を考えてみると正しいということを表す。これを

5312 + 4321 = 9633

は正しい、と読む

(表 1

参照)。

この２つの記号

`, | =

の関係が数理論理学の中心テーマの一つとなる。この２つの違いがなんであるかはすぐにはわかりにくいと思うので、一応標語的に

ある主張が正しいということと証明できるということとは全く違うタイプのことだ

(4)

形の世界意味の世界

1 •

2 ••

3 • • •

· · ·

10 • • • • • • • • • •

23 • • • • • • • • • • • • • • • • • • • • • • • 2 + 4 = 6

•• • • •• ^は • • •

• • • ^と同じ計算により

5312 + 4321 = 9633

5312個の石の山と4321個の石の山を合わせると 9633個の石の山となる

`5312 + 4321 = 9633 |= 5312 + 4321 = 9633 表

1:

数の形式システムとその意味

ということ、つまり

` P

と

| = P

とは似て非なることを頭の片隅に今は入れておいて頂きたい。このことは、決して当たり前のことではなく、今世紀の前半の数理論理学研究の発展により明瞭になった区別だった。

1.2 ヒルベルトの立場

` 5312 + 4321 = 9633

の確認は計算機にプログラムしてやらせることができるのに対して、

| = 5312 + 4321 = 9633

の方は、数字の「意味」に関係することであり、数学的には扱いにくいことがらである。そこでヒルベルトは、意味の世界を切り捨てて記号の世界だけで数学の本質を表現してしまうことを企てた、これがヒルベルトのプログラム（有限の立場）と呼ばれるものである。

もう少し詳しく述べると、ヒルベルトの立場は次のようにいうことができる。

数の計算が数の意味など忘れても機械的にできるのと同じように、数学でも記号の意味を忘れて記号列の機械的な変形・操作だけに基づいて数学研究を表現しよう。

計算が正しければ計算結果が役に立つと同じように、記号の世界（形式システム）が現実世界のある一部を考慮して作られたものであるときは、記号の意味を考慮せずに行った形式システムの研究成果は、現実世界についての理解に有益であることが多いに違いない。

この立場を明確にすることが今回の主要な目標の一つ。まず、記号の世界を明確に表現する方法を説明しよう。

1.3 バッカス標準形

数式をあらわす記号列を説明する方法として次のようなものがある。

(5)

・数字とは

0, 12, 3, 4, 5, 6, 7, 8, 9

のどれか、

・演算記号とは

+, −, ×, ÷

のどれか、

・数とは数字と数を並べたもの、

・数式とは、数であるか、または、数式と演算記号と数式を並べて括弧にいれたもの。

３番目と４番目は誤植ではないかと感じたかもしれない。説明するべきものを用いて説明しているので意味がないようであるが、

数式

→ (数式演算記号数式)

→ (数 + (数式演算記号数式))

→ (5 + (数 −

数))

→ (5 + (2 − 4))

という変形規則であると考えれば意味がある。

記号列の集まり（これを形式言語という）を指定するには、チョムスキーが

1950

年代に導入した生成文法（以下単に文法という）が便利である。文法の中でも文脈自由文法と呼ばれる特殊な文法は、数学やプログラミング言語に登場する記号列を記述するのに適している。バッカス標準形

（以下

BN

形式と略記）を用いると文脈自由文法を簡潔に表現できる。たとえば上の数式の定義は次のようになる：Lを数字、Oを演算子、N を数、Eを数式をあらわすとすると

L ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 O ::= + | − | × | ÷

N ::= L | LN E ::= N | (EOE)

1.4 ヒルベルト小伝

ここで、形式主義を打ち出したヒルベルト

(1862-1943)

の足跡をいくつかを紹介しておこう。

１９世紀後半、不変式（読者にも身近な対称式や交代式がその例である）の研究は数学の中心的テーマの一つであった。その研究は、膨大な計算により具体的な群作用で不変な多項式を具体的構成することに重点があった。そういう中で２８才のヒルベルトは、具体的構成なしに不変式全体の代数的構造を明確にする論文を発表した。不変式を構成せずに精密に研究できるなどということは全く予想外のことであったに違いなく、不変式論の大家であった５３才のゴルダンは「それは数学ではない、神学だ」と叫んだという。しかしゴルダン自身は直ちにヒルベルトの不変式論の革命的な重要性を知りその結果の改良もしたという。

実物を苦労して構成する研究に比べると、背理法による存在証明を途中で使うヒルベルトの議論は「言葉の綾」的な側面があり数学的内容に乏しいようにみえるが、実物の個性によらないことを調べることが目的であるならば、「丁度よいレベル」の議論と考えることもができる。いずれにせよ、ヒルベルトのこの業績により、数学研究という概念自身が変容したことは確かといえる。

「幾何学基礎論」(1899)は、公理系における無定義用語の意味は何でもよい、点を机、線を椅子と思っても良い、と述べたことで、公理的方法の適用範囲に限りがないことを宣言したものとし

(6)

て画期的なものである。

１９００年の国際数学者会議では、数学の全領域から

23

の問題を選びだしたが、それは今世紀の多くの数学者にとって道標のような役割を果たすほど射程の長い洞察に満ちた選定であった。

ヒルベルトの数学研究の全体を貫いているのは数学が自由であることへの信念であり、それは有名な言葉に表現されている：

何者もカントールの楽園から我々を追放することはできない

1910

年以降は形式主義を提唱し、有限の立場で数学を基礎付けることに専念した。なぜ、基礎付けに専念したか。それは、かれの非構成的議論に意味があることを保証するのに必要があった

こと

(§2.1

参照)、そして、彼がカントールの楽園と呼んだ集合論に矛盾があることをラッセルが

1908

年に発表し

(§1.6

参照)、カントールの楽園を守る必要が生じたためである。

1.5 カントールの楽園

集合についてはすでに習っていることと思うが、少しだけ補足しておこう。カントール

(1845- 1918)

³は集合を次のように規定した。

「集合」というのは、われわれの直観や思考の対象で、しかも、区別のできる確定した対象

m

を集めて、

M

という全体にまとめたものだ、と考えることにする（mは

M

の「元」と呼ぶことにする）。

「対象の確定した集め方」には２通りある。外延的な方法（要素を列挙する方法）と内包的な方法（要素の特徴付けを与える方法）とである。例えば、奇数の集合は、外延的に

{ 1, 3, 5, · · · }

と与えることもできるし、内包的に

n

x x

は

2

で割り切れない自然数

o

のようにも与えることができる。

内包的に与えた集合の外延を求めることもその逆も一般にはむずかしい。

たとえば方程式

f (x) = 0

を解くことは、内包的に与えた集合

n

x f (x) = 0 o

の外延を求めることである。逆が難しい例としては、データ

s

がプログラム

P

よって背理法により

V

は正統な集合ではないことになる。

ところが、V は正統な集合ではないということは、V は自分自身を含むことを意味する。すなわち

V

は

V

の要素である。このことは、V が正統な集合であることを意味する。

以上により、V は正統な集合ではなく、しかも正統な集合であることが示された。まとめると

V ∈ V ⇐⇒ V

は正統的でない

⇐⇒ V / ∈ V.

となり、V

∈ V

かつ

V ∈ V

でない、ということになり、矛盾。

“正統性”

のような明確な性質について内包性原理を適用すると矛盾が生じることは、集合論の

有効性がすでに広く浸透していただけに、多くの数学者に大きな衝撃を与えた．カントールの友人であったデデキントは切断による実数の定義を与えた「数とは何か、何であるべきか」(1872)という画期的な著書の再版を許可することをしばらくためらった、という。

1.7 ラッセル小伝

ユーモアと健全な常識を持った数学者・哲学者バートランド・ラッセル

(1872-1970)

は、ホワイトヘッドとともにプリンキピア・マテマティカ

(1910-3)

という大著を残している。この本に取り組んでいる最中に、百年後の図書館で「この本はもういらないから処分しよう」という司書の会話を夢で見たという逸話があるが、北大数学科の図書室では現在この本は第２書庫に移されていてふだんは利用者の目に触れない。完成までに１０年を費やしたものであるが、「『プリンキピア・マテマティカ』を書く楽しみはことごとく１９００年後半の数カ月に局限されていた」という自伝の一節には心が痛む。しかし、数理論理学という学問を樹立したものとして人類史上に残る著作の一つであることは言うまでもない。

ウィトゲンシュタインが哲学者になるか飛行士になるか迷って相談に来たとき、小文を書かせ見た。それを読んで直ちに迷う必要はないことを告げた。ウィトゲンシュタインは後に主著の一つ

「論理哲学論考」でプリンキピア・マテマティカを批判するのであるが、ラッセルはとても愛情とユーモアに満ちた序文を書いている。

1954

年

84

才のラッセルは水爆反対の声明を出し全世界の科学者に署名を呼び掛けた。

(8)

2 形式システムの完全性と不完全性

形式システムというものをもう少し詳しく説明し、ゲーデルの発見を明確にしよう。

2.1 形式主義の定式化

まず、形式主義をもう少し正確に表現しておこう。数学理論の形式化は、次のステップからなる。

記号化命題を論理式と呼ばれる特殊な記号列で表現し、その意味は議論しない。

推論推論を記号列の機械的変形と考える。変形の規則は推論規則と呼ばれる。

公理いくつかの論理式を選びだし公理と呼ぶ。どうしてそれを公理として選んだかという問いは無視すると決意する。いくつかの公理は、理論に依存しない普遍的なもので、論理公理と呼ばれる。⁴

定理公理から推論して得られる論理式を定理と呼ぶ．論理式

P

が定理であるとき

Σ ` P

と書く。

自然数を扱う具体的形式システム

PA（ペアノの公理系）を通して形式システムを説明しよう。

2.2 自然数論 PA に現れる記号

BN

形式を用いて、自然数論

PA

を表現する記号列を導入しよう。数式

(E)

と論理式

(P )

という２種類の記号列があり次で定められる。ただし

V ::= x | y | z · · ·

は変数。

E ::= o | V | sE; | E + E | E × E P ::= > | ⊥ | E = E | ¬P | P ∧ P

| P ∨ P | P ⇒ P | ∀x.P | ∃x.P |

各記号の「意味するところは」次の通りである。しかし、形式主義の立場では、こういった意味はプライベートなインフォーマルなものとして、それには一切頼らずに話しを進めると決意する。

記号の意味

2.3 メタ数と形式的数

10¹⁰⁰

z }| {

s · · · s o

は、その存在はもはや現実のものではなく理論上のものであり明瞭さの度合いについては大きな数と違いはない。

記号列の世界は意味を捨象しても決して明瞭な世界ではないのである。

メタ言語については、もう一つ注意しておきたいことがある。これは気付けば当たり前のことなのであるが、うまく説明することが困難なことである。それは、日常言語を用いて議論する部分が形式システムの理論の中核であるという点だ。形式システム自身には何の”命”もないのである。この自明な点は、余りに自明すぎてかえって見過ごされてしまう恐れがある。数学の理論をうまく形式化すると、それによって産み出された形式システムは「我々がいようがいまいがそれ自身としてすべてを語る」ということがありそうな気がするかもしれないが、これはわれわれがその形式システムを使って議論しているという肝要なことを忘れた錯覚である。このことは忘れないでおいて欲しい。

なお意味を捨象した形式システムは、それ自身自明でない数学的対象であり、その理解にはゲーデルのような稀な人物をまって初めて深まるような見通せない数学的対象なのであある。

(10)

2.4 自然数論 PA の公理

少し脱線してしまったが、話しを元に戻そう。

形式システムの定式化（すなわち空回りのない議論ができるように言葉使いなどを明確に設定すること）の仕方にはいろいろな流儀がある。公理と推論規則とはセットとなって論理システムをなすので、どちらに重きを置くかはいわば趣味の問題といえるかもしれない。自然演繹やシーケント計算の形式のものは、論理公理を最小にして推論規則を主にするもののであるが、ふつうの証明行為に近い形式化でわかりやすいので、これを採用する。

まず、公理は次のような論理式とする。

s

の公理

∀x.(¬(o = sx)),

∀x.(¬(x = o) ⇒ ∃y.(x = sy)),

∀x.∀y.(sx = sy ⇒ x = y).

（ゼロでないこととある数の次の数であることとは同値で、次の数が同じ２数は同じである。）

演算の公理

∀x.(x + o = x),

∀ x. ∀ y.(x + sy = s(x + y)),

∀ x.(x × o = o),

∀x.∀y.(x × sy = x × y + x),

（これらが「正しい」ことは

sx

が

x + 1

P

を満たす。）

2.5 推論規則

以下の推論規則は自然演繹とよばれるタイプのものである。一般に、横線の上にならんだ論理式が定理ならば、下の論理式が定理であるという規則をあらわす⁵。

これらの推論規則は、自然数論

PA

だけでなく、多くの数学理論の形式化に共通に使われる普遍的なものである。なお、これらの規則は、括弧内に書いたような当たり前の推論を記号列の機械的変形規則として表現したものであるが、形式システムの下では、これらの機械的変形規則による変形自身を推論と考え、意味を考えた”推論”は一切認めない。

5一部は証明過程についての「大域的情報」が必要なので、この説明では不正確である。詳しくは次の節§3.1を参照。

(11)

命題論理の推論規則

P ∧ Q P

P ∧ Q Q

P, Q P ∧ Q

（

P ∧ Q

が定理ならば

P

は定理等々、Pと

Q

が定理ならば

P ∧ Q

が定理）

P P ∨ Q

Q

P ∨ Q P ∨ Q

[P] ·· · R

[Q] ·· ·

R R

⇒

の推論規則を適用するが、それ以外に排中律がある。

P ∨ ¬P

∀

の規則

∀x.P P [x/t]

P(x)

∀x.P (x)

（前半の

t

は数式．

P (x)

がすべての

x

について成立てば、変数

x

を具体的なもの

t

に置き換えたも

·· · Q Q

（前半の

t

は任意の数式、後半の変数

y

は

Q

と他の仮定には現れてはいけない。）

等号の推論規則

x = x

x = y P (z/x)

P (z/y )

(12)

（最後は、P(z)の

z

に

x

を代入して定理であれば、

z

に

x

と等しいものを代入しても定理である、

という推論。）次の推論規則は派生的に得られる。

x = y

y = x (対称律) x = y y = z

x = z (推移律)

たとえば、対称律は、P

(z) ≡ z = x

について上の推論規則を適用すれば

x = y x = x y = x

.

推移律は、P(w)

≡ w = z

に等式の推論規則を使うと

x = y

y = x

対称律

y = z x = z

.

2.6 「定理」の定義

図１のように推論規則を続けた適用したものを証明図という。論理式

P

が、

•

ある推論の下段とはなっていない

• [P ]

∀y.(so+sy) =s(so+y) so+so=s(so+o)

∀x.(x+o=x) so+o=so

対称律 so=so+o

x=x

∀x.x=x sso=sso

(P(z)≡sz=sso) s(so+o) =sso

推移律 so+so=sso

2.8 論理式の真偽

形式システムの記号を解釈すると論理式は具体的な主張となり、正しいか否かということが意味を持つようになる。数理論理学では、解釈は集合の世界で行われるが、それについての解説は省

(13)

く。素朴に、記号に意味を与える、と考えてもらいたい。自然数論

PA

の場合でいえば、§2.2で与えたインフォーマルな説明が解釈であると考えていただければよい。

解釈

I

の下で、論理式

P

が正しい主張となるとき，

I | = P

と書く．ある解釈の下でどの公理も正しいとき、その解釈は形式システムのモデルであるという。

論理式

P

がどのモデルでも正しいとき

| = P

と書き，P はトートロジー（恒真論理式）であるという．

2.9 形式システムの健全性

` P

ならば

| = P

であるとき，つまり定理はどのモデルでも正しいとき，形式システムは健全であるという．

形式システムを、特定の解釈のもとで使うことを意図して導入するときは、健全性が成立つように注意しながら公理や推論規則を定めなければ役にたたない。つまり、

•

正しい論理式の中から公理を選び，

•

正しい論理式から正しい論理式が推論されるように推論規則を選ぶ．

そうすれば健全なことが保証される．

§2

の第

2,4,5

節で導入した形式システム

PA

が、自然数による表２のような解釈に関して健全

であることはほとんど「明らか」であろう。

2.10 形式システムの無矛盾性

形式システムがモデルを持つとする。そのとき、ある論理式とその否定とが共に証明できる、

ということはありえない、その論理式の解釈は正しくしかも正しくないということになってしまうからである。

ある形式システムが無矛盾であるとは、どの論理式についても、それとその否定とが同時に証明できることはありえないことをいう。あとで述べるゲーデルの完全性定理により無矛盾な形式システムはモデルを持つこと、別言すれば、単なる記号のシステムであるだけではなく数学的に意味のある言説の表現となっているということ、がわかる。

2.11 ヒルベルトの夢：理論の完全性

ヒルベルトの夢は、簡単に表現すれば次のようになる。

すべての真理を定理として把握したい．

(14)

次に説明する意味で完全な形式システムを作ることができればこの夢は成就する。

どの論理式も具体的な解釈の下では、それが正しいかその否定が正しいかのいずれかである。

この主張の中の「正しい」を「証明可能」に置き直したものが完全性である。すなわち、ある形式システムが完全であるということは、どの論理式についても、それが証明できるかその否定が証明できるかのいずれかであることをいう（図

1

参照）。

証明可能な論理式

反駁可能な論理式

図

1:

完全な理論

もしもその理論が健全で完全ならば，どの文

P

とどのモデル

I

についても

` P ⇐⇒ I | = P

ゲーデルはヒルベルトに夢は部分的には正しいことを示した（完全性定理）が、夢自体は叶わぬことを示してしまった（不完全性定理）.

2.12 ゲーデルの完全性定理 (1929)

１階の述語論理と呼ばれる形式システム

(自然数論 PA

の中の論理公理と推論規則とを持つ形式システム)は、数学の多くの理論を表現できるもので重要なものである（しばしば形式システムという言葉でこれを指す）。

トートロジーは証明できる.

すなわち

| = P ⇒ ` P .

対偶をとれば、証明できない論理式はトートロジーではない、つまり、あるモデルでは正しく無い。これを次のようにいうことができる。

証明できない論理式には反例がある

特別な場合として、形式システムが無矛盾ならば証明できない論理式

⊥

があるので、その反例としてモデルが少なくとも一つ存在する。従って

(15)

無矛盾な形式システムはモデルを持つ.

実際にはこの特別な場合を使って、一般の完全性定理が示されるのである。

これにより、記号列だけの世界に過ぎない形式システムも、無矛盾でさえあれば数学的内容を持つことになる。これはヒルベルトが主張した数学の「自由さ」の根拠を与えるものと考えることもできる。

2.13 ゲーデルの不完全性定理 (1931)

しかし、一つの形式システムにはたいてい複数のモデルがあり、一つのモデルでは正しいが別のモデルでは正しくない論理式が存在してしまうことが、ゲーデルによって示された。

ゲーデルは自然数論

PA

が無矛盾ならば完全ではありえないことを、

` G

でも

` ¬G

でもないような論理式

G

を構成することにより証明した。

これにより、論理式の全体は図

2

のようになっていることがわかる。

証明可能な論理式

反駁可能な論理式 G

図

2:

形式システムの一般の姿

こうして、無矛盾な形式システムに数学的内容がつくにはつくが、その内容は形式システムだけではコントロールできないということが明確になったのである。ゲーデルはどのようにしてこのような結果を得たののであろうか？

2.14 ゲーデルのプラトニズム

ゲーデルは、自然数論の無矛盾性を仮定して実数の公理系の無矛盾性を証明しようとしていて、

自然数論では真理概念がその内部で定義できないことに気付き、それを整理して不完全性定理に到ったことが知られている。しかし、完全性定理の論文の序文にはすでに不完全性の可能性を予感していたことを示す文がある（以上は林晋氏に教示頂いた）。なお、後年、ゲーデルは強烈なプラトニズムを表明し、数学の

incompletability(完全に形式化できないこと), inexhaustibility

（汲み尽くせないこと）を「根本的事実」として述べている。

プラトニズムは、数学的対象は「イデアの世界」に実在すると考える、しかし、我々はその影しか認識できないという立場である。この立場からすれば、形式システムも当然イデアの影を捕ら

(16)

えることしかできないのであるから、形式システムにより数学が完全に捕捉できるという形式主義は最初から意味を持たない。ゲーデルがいつのころから強烈なプラトニストとなったかはわからないが、不完全性定理は当然と思っていたことは十分あり得る。なお、ゲーデルに限らず、多くの人たちは形式主義に懐疑的であったようである。ヒルベルトの共同研究者であるベルナイスもそういう主張をしてヒルベルトを怒らせたことがあるそうである。

2.15 形式システム：まとめ

今回お話ししたことをまとめておこう。

•

数学的対象・その操作・それらの間の関係を記号化し、新たな操作や主張（論理式）を合成する方式を与え、正しい主張を選び、さらに正しい主張から正しい主張を導く方法（推論）

自分自身を印刷するプログラムを書け。プログラミング言語は任意である。ただし印刷命令は具体的な文字列に限るものとする。

(17)

第 II 部

以上、数学を形式化する、ということがどういうことかを説明しました。それはユークリッドに始まる公理的形式をさらに抽象化したものでした。少し復習しておきましょう。

まず、数学的対象を記号化するだけでなく、その性質やそれらの間の関係なども文字列で表現し、それを論理式と呼びます。次にいくつかの論理式を選び公理と呼びます。公理に特定な機械的操作を施して得られる論理式を定理と呼び、定理に到る機械的操作の全体を証明と呼びます。このように表現された文字列・操作の全体が一つの形式システムをなします。

形式システムを導入することにより、ヒルベルトは今世紀初めに数学を襲ったラッセルのパラドクスという激震から、数学を救い出そうと試みたわけです。

その試みの成否を決める鍵は、完全で無矛盾な形式システムが作れるかどうかです。すなわち

「正しいことはすべて証明でき、間違ったことはすべて反駁できるか否か

(前回の記号を使えば、

| = P

ならば

` P , | = P

でなければ

` ¬P

とできるか否か)」が争点になります。「正しい」という非形式的な言葉を消去すると、(証明と反駁が同時にできる論理式はないという)無矛盾性と、(証明も反駁もできない論理式はないという)完全性とを合わせ持つものが、まさにヒルベルトが夢見た形式システムです。

完全な形式システムを作ることができる数学的理論もありますが、それは一般にはないものねだりであることをゲーデルの不完全性定理が示してしましました。

以上が前回の要約ですが、今回はこの定理の証明の概略を説明し、形式化という操作の本性を見つめたいと思います。また、証明の核心にある「不動点定理」を普遍化したロベールの定理を概説し、それを用いて、生命的過程のある特徴や心身問題への一つのヒントが与えられることを見たいと思います。

3 ゲーデルの不完全性定理の証明

ϕ

自身を取ると、

ϕ(ϕ) = ϕ(ϕ)

は証明できないとなるので、ϕ(ϕ)がまさにゲーデル文となる。

3.2 問題点：「論理式についての論理式」の意味付け

スケッチで使った「論理式についての論理式」という概念はまだ定義されていない。

集合論では、論理式

P(x)

は集合

n

x P (x) o

をきめる、ということにより、性質

P

が性質

Q

を持つという文に、集合

n

x P (x) o

が性質

Q

を満たす、という意味を与えることができた。

私達は今「論理式が証明不可能である」というようなメタ概念を問題としている。この概念はメタではなく形式系に属する概念ではないか、と思い込んでいないだろうか？もう一度証明概念を導入した前回の

§2.4–6

のところを読み直してもらいたい。そこでは、どういう図形が証明図であるか説明し、その図が、その最下部に書いてある論理式の証明である、というように述べた。しかし、証明図という幾何学的対象についての理論はまだ何も形式化してはおらず、それについてどのような土俵で議論すべきかは何もまだ決めていないのである。それを決めないでは、証明不可能であることが証明可能かというような問は、まだ問いとして確定していないのである。

ゲーデルの不完全性定理の証明では、ゲーデル数という概念装置を利用して、証明可能性というメタ概念を形式化する。すなわち、

•

論理式

P

を数

dP e

で表わし,

•

論理式

についての

PA

論理式

A

により形式的に表現されるものもあることになる⁷。PAは強い記述能力を持つので、多くの数学的なメタ概念は

PA

論理式で表現できることがわかるのであるが、後で述べるタルスキーの定理が示すように例外もある。

以上の準備が終わったとすると、前節にスケッチしたゲーデル論理式の構成法は次のように実現できる。PA論理式

ϕ(n)

が

n

は１自由変数を持つ論理式

R

のゲーデル数であり、dR(n)eは証明可能数ではないという意味を持つとする。このとき

ϕ( d ϕ e )

は、まさに、ϕ(

d ϕ e )

が証明できないことを意味するゲーデル論理式となる。

この筋書きに基づいて証明するために以下

6自由変数を一つだけ持つ論理式のこと。

7「メタ的性質PはあるPA論理式で表現できる」は、「正当化」という事が意味のないタイプの主張である。

(19)

•

ゲーデル数の導入．

•

自己代入（

dQ(x)e

の

x

に

ⁿ

表

3:

= 720326954760913500.

3.4 計算可能関数の組み込み

PA

の内部には

+, ×

の組み合わせで得られるような「関数」しか用意されてはいない。しかし、計算可能関数は最初から

PA

の内部にあるものとしてよいことがわかる。今言ったことの内容を完全に説明することは多くの紙数を要するが、考え方自身は以下のようにわかりやすいことなのである。

まず、計算可能性の意味を了解することはコンピュータが身近な現代では簡単だ。身近な

Basic

や

C

などのプログラミング言語を使ってプログラムできるものが計算可能な関数である。ただし、メモリーの大きさには制限がなく、どんな大きな数でも処理できる、という夢の計算機を考えるのであるが。

ある入力に対していつまでも計算が終了しない可能性のあるプログラムもある。意図しない無限ループが潜在する（いわゆるバグのある）プログラムがその例である。しかし、「まともな」プログラムでもそういうことがある。例えば、円周率を

10

進展開して

7

が

100

個連続することがあるかどうかを判定するプログラムを考えよう。もしも、そういうことがないとすると、そのプログ

(20)

ラムを走らせると止まらないことになる。こういう止まらないかもしれないプログラムによる「計算」も計算論では取り扱う。

f がある。ただし、xは

s

の後に

o

を

x

個並べた

PA

) × x

3

で表現される。

しかし、関数

f

が計算可能であっても

PA

の数式として

+, ×

だけで書き下せるとは限らない。

例えば、f

(n)

を

n

番目の素数とすると、関数

f

は計算可能であるが、PAの数式では書けない。

しかし、mが

n

番目の素数であるということを意味する

PA

論理式

P RIM E(m, n)

は存在する、

ということが上の主張からわかるのである。

これを使うと、計算可能関数は形式システム内部にあるものとして使ってよいことがわかる。

もう少し正確にいうと、その関数に対し、上の定理により存在が保証された論理式を

P

とし、今まで使っていない記号（たとえば

g）を用意し、公理

` ∀y∀x[y = g(x)⇔P (x, y)]

を添加した形式システムを考えても、証明できる

PA

論理式は増えないことが比較的容易にわかる。

以上により、停止することが保証されているプログラムにより計算できる関数は、PA 内の正式な関数と同様に使ってよいことがわかる。

たとえば、Q(g(x), y)も正式な論理式であると考えてよい。もしも

g

を使わないでこれを表わせば、

∃z[Q(z, x) ∧ P (x, z)],

すなわち、P

(x, z)

と

Q(z, x)

とを満たす

z

があるという間接的な言い方になる。このとき、zは

g(x)

でなければならないので、結局「Q(g(x), x)」を主張したことになる、というわけである。これに比べると、

Q(g(x), y)

という論理式をじかに使える場合には、概念的見通しは遥かによくなる。

概念的な見通しの良さの効力は少々の技術的煩雑さを償って余りあるものがあることは言うまでもない。

3.5 代入操作と自己適用操作

以下、ゲーデルの定理の証明に必要な関数を用意しよう。まず最初に「代入」を行うプログラム

(21)

のに数を代入

を用意する。これは数

m

と論理式

P(x)

のゲーデル数

dP(x)e

を入力すると

P (x)

の自由変数

x

に

m

を代入した論理式

P (m)

のゲーデル数を出力するものである。

このプログラムを書くには特別なアイディアは要らない。まず数

dP (x)e

を因数分解して文字列に戻す。文字

x

を数

m

を置き換える。最後に文字列をゲーデル数に変換する。終わり。

２番目の入力が、論理式のゲーデル数ではなかったり、変数が２個以上または変数がない論理式のゲーデル数であったりする場合のことが気になるかもしれない。しかし、いずれも計算の途中でチェックできることなので、そうであることが判明した時点で

0

を出力して止まるようにしておけばよい。

は変数を持たない論理式の全体の変換をひき起す：T

7→ RdT e .

上の定理はこの変換が不動点を持つことに他ならない。

この一見手品風の証明がよく飲み込めない場合は見取り図

3

を見ていただきたい。

論理式数

∆ ∆

にを代入

∆

図

3:

不動点定理の証明の見取り図: 左側に閉論理式の世界を書き、右側に数の世界を書く。

Rx

は数

m

ごとに閉論理式

Rm

を定めるので、右から左への写像を与えている。いま、∆は右の世界の変換であるから、これを

R

と合成して、右から左への写像

Q

を得る。

3.7 証明可能性判定プログラム

次に証明概念を形式化する。証明図は平面的図形であるがこれも数で表現できる。証明図の構造自身は木グラフと呼ばれる幾何的構造を持っている。例えば、前回の図１の証明図は、図

4

のように木の各辺に論理式を書き各頂点に推論規則の名前を書いたもので表現できる。木の幾何的構造を一次元的な文字列で表示できるのであろうかと心配になるかもしれないが、それは簡単なことである。例えば、上の図は次のような括弧式で表現すればよい。

((((•))) ( (((•))) (((•))) ) ).

(23)

推移律

代入特殊化対称律

特殊化

特殊化一般化

公理

公理公理

へを代入したものが右上の仮定なので、左上の仮定からを代入した結論も正しい

∀ ∀

∀

図

4:

証明木

(24)

すなわち、一番上の葉ごとに

•

を用意し、推論をするごとに括弧を加えればよいのである。証明木のすべての情報を書くには、括弧を加えるときに、

(仮定

1

, · · · ,

仮定n

,

推論規則,結論) というように付加情報を添えればよいだけだる。たとえば、

の場合であれば、

((A, c), (a, b, B, d), C, e)

となる。証明図を文字列に表現した後は、論理式の場合と同じようにそのゲーデル数を定めることができる。ただし、推論規則に割り当てた新しい記号に対する数を決めておく必要があるが、表

3

ではまだ使っていない、15以上の数で

14

のべきではないものを割り当てればよい。

以上のようなやりかたで証明図

Ξ

もゲーデル数

dΞe

で表現されたことになる。

そこで、２つの数

p, m

を入力し、pが証明図のゲーデル数であり、その結論のゲーデル数が

m

である場合に

1,

そうでないとき（

m

が論理式のゲーデル数でないか、pが証明図のゲーデル数ではない場合も含めて）0を出力する関数

P RV (p, m)

を考える。この関数は数学的には今言ったような言い方で決まっているが、果たして計算可能であろうか？

プログラムが得意な読者は、この関数

PRV

のプログラムの構想をすぐに思いつくであろう。入力の

p

を因数分解し文字列を復元しそれが木構造を表現しているかどうか確かめ、さらに、その木に書かれているすべての情報を調べて、証明図になっているかどうかを確認することは容易である。証明図であることがわかったら、あとは、その結論の論理式のゲーデル数を計算して、それがもう一方の入力と一致するかどうかを調べればよいだけである。

以上により、次のようなプログラムが書ける：

m p

p は証明図のゲーデル数でその結論のゲーデル数はmか？

1 if YES 0 if No

{

こうして、数

m

が、定理のゲーデル数であることを表現する論理式

P r

が

Pr(m) := ∃x.[P RV (x, m) = 1]

と定義され、証明概念の形式化が完了する。

3.8 不完全性定理の証明の完結

以上により、ゲーデルの不完全性定理の証明ができたことになる。すなわち、論理式

コンピュータに数学研究ができないのはなぜ？