不完全性定理についてのゲーデルの証明の一部

G. J. Chaitin Godel's Proof of his Incompleteness Theorem の例をMathematicaとCommon Lispで書き直した。これは「証明」というよりも「ゲーデルの定理の主張」を説明するための文書である

準備運動
ゲーデルの定理

うそつきのパラドックス：「この文はうそである」

ゲーデルの定理：「この命題は証明できない」（真なのに証明できない命題がある）

準備運動

これは自分のコードを出力するプログラムの例でもある

Mathematicaの場合

Mathematicaで書くともっともわかりやすいだろう。まず x -> x[x] となるような関数fを作る

> f = Function[{x}, x[Hold[x]]];

次のように書いてもいい

f = Function[#[Hold[#]]];
f = #[Hold[#]] &;

そうすると、

> f[x]
x[Hold[x]]
> f[f]
Hold[Function[{x}, x[Hold[x]]]][Hold[Hold[Function[{x}, x[Hold[x]]]]]]
> ReleaseHold[f[f]]
Hold[Function[{x}, x[Hold[x]]]][Hold[Hold[Function[{x}, x[Hold[x]]]]]]

メーダーによれば、Mathematicaの記法では式

Function[x,body][arg]

は基本的に

ReleaseHold[Hold[body]/.HoldPattern[x]->arg]

と評価される。わかりやすくするために、f=#[h[#]]&からはじめると、

> Hold[x[h[x]]] /. x -> (#[h[#]] &)
Hold[(#1[h[#1]] &)[h[#1[h[#1]] &]]]
> ReleaseHold[%]
h[#1[h[#1]] &][h[h[#1[h[#1]] &]]]

Schemeの場合（MIT Scheme）

(define f (lambda (x) `(',x ',x)))
;Value: "f --> #[compound-procedure 2 f]"

これは (define (f x) `(',x ',x)) と書いてもよい（あとで見るように、Common Lispの場合は同じではない）

(f 'x)
;Value: ((quote x) (quote x))
(f f)
;Value: ((quote #[compound-procedure 2 f]) (quote #[compound-procedure 2 f]))
(eval (f f) nil)
;Value: ((quote #[compound-procedure 2 f]) (quote #[compound-procedure 2 f]))
(equal? (f f) (eval (f f) nil))
;Value: #t

#[compound-procedure 2 f] などは関数の実体を表している。f というシンボルは関数であるが、値を参照することもでき、その値は #[compound-procedure 2 f] だということである（ChaitinのSchemeならば値は (lambda (x) `(',x ',x)) となっていてわかりやすい）。MIT Schemeではこうなってしまうのだが、目的は果たせる

Common Lispの場合

Common LispではMathematicaやSchemeと違って、シンボルに値と関数が別々に格納される。関数 describe が実装されている場合、このことを簡単に確認できる（関数 describe がない場合は、symbol-value や symbol-function を調べればよい）。Schemeをまねて、

(setf f (lambda (x) `(',x ',x)))

とした場合、Allegro Common Lispでは

> (describe 'f)
F is a SYMBOL.
  Its value is #<Interpreted Function (unnamed) @ #x2100b532>
  It is INTERNAL in the COMMON-GRAPHICS-USER package.

となって、関数の実体が値として格納されていることがわかる。そのため、(f 'x) としてもエラーになり、(funcall (eval f) 'x) などとしなければならない。一方、

> (defun k (x) `(',x ',x))
K
> (describe 'k)
K is a SYMBOL.
  It is unbound.
  It is INTERNAL in the COMMON-GRAPHICS-USER package.
  Its function binding is #<Interpreted Function K>
    The function takes arguments (X)
> (k 'x)
('X 'X)

とすれば、関数の実体が関数として格納されるが、k は値を持たないため、(k k) などするとエラーになる。MathematicaとSchemeの場合と同様の記述をするためには、一つのシンボルに値と関数の両方を格納できるようにしなければならない。これは symbol-function に関数の実体を格納することで実現できる（MathematicaとSchemeと同様の記述ということにこだわらないのであれば、evalやsymbol-functionを使えばよい）。

ElispにあるfsetをCommon Lispでも定義しておく（その都度(setf (symbol-function 'a) b)と書いてもいい）

(defun fset (a b) (setf (symbol-function a) b))

これによって目的は果たせる

> (setq f '(lambda (x) `(,x ',x)))
(LAMBDA (X) `(,X ',X))
> (fset 'f f)
(LAMBDA (X) `(,X ',X))
> (describe 'f)
F is a SYMBOL.
  Its value is (LAMBDA (X) `(',X ',X))
  It is INTERNAL in the COMMON-GRAPHICS-USER package.
  Its function binding is #<Interpreted Function F>
    The function takes arguments ()

値と関数の両方が格納されていることがわかる

> (f 'x)
(X 'X)
> (f f)
((LAMBDA (X) `(,X ',X)) '(LAMBDA (X) `(,X ',X)))
> (eval (f f))
((LAMBDA (X) `(,X ',X)) '(LAMBDA (X) `(,X ',X)))
> (equal (f f) (eval (f f)))
T

`を使わないと少し面倒

> (setq f '(lambda (x) (list x (list 'quote x))))
(lambda (x) (list x (list (quote quote) x)))

ゲーデルの定理

「文に数を対応させるが、文の中で数を扱うことができるためにレベルが縮退する」というのがゲーデルの方法の本質である。「表現に名前を対応させるが、表現の中で名前を扱うことができるためにレベルが縮退する」というのが以下の方法の本質である。（これが簡単に実現できるのは、ここで扱う言語では表現がfirst-classだからである。First-classについてはSICPを参照）

表現に名前を対応させるのは簡単で、MathematicaならばHoldを、SchemeやLispならばquoteを使えばよい。名前が指す対象の表現 valueOf(x) を具体的に知りたいときは、MathematicaならばReleaseHoldを、SchemeやLispならばevalを使う

Mathematicaの場合

xが妥当な証明でないならFalseを返し、妥当な証明なら証明された定理を返すような関数 valid-proofQ があるとする（これは難しくないはず）。すべてのxについて valid-proofQ[x] がyと等しくないとき、yは証明不可能である。このことを主張する述語をis-unprovable とする

名前xに対して、表現is-unprovable[valueOf[x[Hold[x]]]] （この表現中のxは実際にはxが指す表現）を返すような関数gを考える

g = Function[isUnprovable[valueOf[#[Hold[#]]]]];

> g[x]
isUnprovable[valueOf[x[Hold[x]]]]

gに自分自身を作用させるた結果は、

> g[g]
isUnprovable[
  valueOf[isUnprovable[
      valueOf[Hold[isUnprovable[valueOf[#1[Hold[#1]]]] &][
          Hold[Hold[isUnprovable[valueOf[#1[Hold[#1]]]] &]]]]]]]

となり、ある名前で指される表現が証明不可能だと主張している。その表現を具体的に知るには名前をReleaseHoldすればよい

> ReleaseHold[First[First[g[g]]]]
isUnprovable[
  valueOf[isUnprovable[
      valueOf[Hold[isUnprovable[valueOf[#1[Hold[#1]]]] &][
          Hold[Hold[isUnprovable[valueOf[#1[Hold[#1]]]] &]]]]]]]

これはg[g]である。実際、

> g[g] === ReleaseHold[First[First[g[g]]]]
True

g[g]は証明可能であろうか。証明可能だという結論はg[g]の主張と矛盾する。よってg[g]は証明可能ではない。しかしこれはg[g]の主張である。よって、g[g]は証明不可能だが真である

Schemeの場合（MIT Scheme）

(define g (lambda (x) `(is-unprovable (value-of (',x ',x)))))
;Value: "g --> #[compound-procedure 3 g]"
(g 'x)
;Value: (is-unprovable (value-of ((quote x) (quote x))))
(g g)
;Value: (is-unprovable (value-of ((quote #[compound-procedure 3 g]) (quote #[compound-procedure 3 g]))))
(equal? (g g) (eval (cadr (cadr (g g))) nil))
;Value: #t

Lispの場合

省略なしで見るために(let ((*print-level* 6)) (princ (g g)))などとする

> (setq g '(lambda (x) `(is-unprovable (value-of (,x ',x)))))
(LAMBDA (X) `(IS-UNPROVABLE (VALUE-OF (,X ',X))))
> (fset 'g g)
(LAMBDA (X) `(IS-UNPROVABLE (VALUE-OF (,X ',X))))
> (g 'x)
(IS-UNPROVABLE (VALUE-OF (X 'X)))
> (g g)
(IS-UNPROVABLE
 (VALUE-OF
  ((LAMBDA (X) `(IS-UNPROVABLE (VALUE-OF (,X ',X))))
   '(LAMBDA (X) `(IS-UNPROVABLE (VALUE-OF (,X ',X)))))))
> (equal (g g) (eval (cadr (cadr (g g)))))
T