あどけない話

インターネットに関する技術的な話など

Lisper のためのゲーデルの不完全性定理

注:この記事の内容には、問題があるようなので、勉強して書き直す予定です。

ゲーデルの不完全性定理を読んでも理解できない Lisper のために、Lisp のコードで不完全性定理を説明してみる。昨日と同様に Emacs Lisp を使うが、Common LispScheme でもコードはあまり変らない。

ゲーデル不完全性定理

ゲーデル不完全性定理とは、おおざっぱに言うと「(自然数論を含む帰納的に記述できる)公理系が無矛盾であれば、証明も反証もできない命題が存在する」と言うことだ。これは嘘つきのパラドックスと似ていると言われている。

嘘つきのパラドックスとは、「この文は嘘である」という文は、正しいとも間違っていると言えないということ。この文が正しいと仮定すると、この文は嘘となり、仮定と一致しない。一方、この文が間違っていると仮定すると、この文は嘘ではなくなり、文の内容と一致しない。矛盾の根源は、この文がこの文自体について述べている自己言及にある。

ゲーデルは少し内容を変えて、「この文は証明できない」という命題を考えた。可能性としては二つある。証明可能な定理であるか、証明不可能な定理でないものであるか。この文が証明可能であると仮定すると、この文は証明できないことになり、仮定と一致しない。つまり、公理系が矛盾していることになる。そこでこの可能性を捨てて、この文は証明不可能であると仮定する。すると、仮定と文の内容が一致するので、この公理系には証明できない命題が存在することになる。つまり、この公理系は不完全だ。

後述の「知の限界」の著者チャイティンは以下のように述べている。

ゲーデルは「xがyを証明する」ということを算術的に表現するのです。これは非常に巧妙な方法ですが、数学的叙述が正の整数とも考えられるという基本的な考えは、今日では、さほど驚くことには思えません。結局、すべての記号列が、現代のコンピュータでは数値で表されているからです。... ゲーデル数は、1930年代よりも今の方がずっと理解しやすいのです。

Lisp による不完全性定理の証明

不完全性定理Lisp で証明するには、「このS式は証明できない」と主張するS式が構成できればよい。

まず最初にS式が妥当な証明か判断する valid-proof-p という関数を考える。この関数は、引数が妥当な証明なら証明された定理を返し、そうでないなら nil を返す。この関数は実際には実装しないけれど、S式を走査して妥当かを判定するアルゴリズムはあるとする。

つぎに、unprovable-p という関数を考える。この関数は、与えられたS式が証明できないことを主張する。実装としては、与えられたS式 a が、すべてのS式 b に対して (valid-proof-p b) と等しくないこと言えばよい。

次に以下のような関数 g を考える。

(set 'g '(lambda (x) `(unprovable-p (eval (,x ',x)))))
(fset 'g g)

関数 g は、`(,x ',x) を eval しているので、`(,x ',x) という名前から値を取り出し、その値が証明不可能だと主張していることになる。

では、g に g を与えた場合、何が証明不可能だと主張していることになるだろう?

(pp (g g))(unprovable-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
	(,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
	(eval
	 (,x ',x)))))))

eval より後ゴチャゴチャしている部分が名前である。この名前は値はなんだろう?それを知るには、(g g) から名前を取り出して、eval すればよい。

(pp (eval (cadr (cadr (g g)))))(unprovable-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
	(,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
	(eval
	 (,x ',x)))))))

さっきと同じものが出てきた。Lisp に同じだと確認させてみよう。

(equal (g g) (eval (cadr (cadr (g g)))))t

結局どういうことだろう?

(g g) は、ある名前が指すS式が証明不可能だと主張しているS式である。ある名前が指すものを取り出してみると (g g) であった。すなわち (g g)は、「自分自身が証明不可能だ」と主張するS式である。

くどいようだが、この意味を考えてみる。(g g) が証明可能なら、証明不可能を肯定したことになるので、公理系が矛盾していることになる。(g g) が証明不可能なら、(g g) の主張と一致する。証明不可能な問題があることになり、公理系は不完全である。

なにか騙されたような気も拭いきれないが、これがLispによるゲーデル不完全性定理の証明である。

参考文献

昨日の記事と今日の記事の元ネタは、「知の限界」という本である。この本は、内容は素晴らしいが、言葉が足りないため読破するのは難しい。私は、不完全性定理のLisp, Mathematicaによる記述を参考にこの本を読んだが、2年ぐらい意味不明だった。最近ようやく分かった気になったので、忘れないように記事にまとめてみた次第である。

知の限界

知の限界