あどけない話

Internet technologies

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

Lisp

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

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

ゲーデルの不完全性定理

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

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

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

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

ゲーデルは「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年ぐらい意味不明だった。最近ようやく分かった気になったので、忘れないように記事にまとめてみた次第である。

知の限界

知の限界