Schemeによる第一不完全性定理の実装

『知の限界』という本を買ったら第一不完全性定理をLispで実装する方法が載っていた。しかし、そのコードはSchemeでは動かないように思えたので、Schemeで実装をしてみた。不完全性定理では、コード中の引数に自身のコード渡して、自己言及的なゲーデル文Gを構成して証明するのだが、S式はコードもただのデータなので、こういうことが出来るのかと感心した。本書では、第一不完全性定理以外にも、不動点や停止問題のLisp実装も示されており、それらはここで示すコードと本書を読めばSchemeで実装可能に思う。

ただし、本書は面白いが、第一不完全性定理の説明などはほとんどないため、そもそも第一不完全性定理を知らない場合は、理解するのは難しそうではある。

知の限界[復刻改装版] (00)

Schemeによる再実装

Schemeで再実装したものは以下の通りとなる。

まず、「「xはxである」という文は証明できない」というgを考える。文なのでS式で返す。

(define (L x y) (cons x (cons y '())))

;; 「xはxである」は証明できない
(define g
  '(lambda (x) (L 'is-unprovable (L x x))))

つぎに、S式を評価するための補助関数を以下のように定義する。

;; (eval l)
(define (eval0 l)
  (eval l '()))

;; 1ステップだけ評価
;; (eval ((car l) (cdr l)))
(define (eval1 l)
  (apply (eval0 (car l)) (cdr l)))

とすると、ゲーデル文G = (g g)はSchemeでは以下のようになる。

((eval0 g) g)

第一不完全性定理はGもnot Gも証明できないようなGが存在するというものなので、証明してみる。
まず、G = (is-unprovable G)となることを確認する。

;; ゲーデル文G
;; g(x) = 「xはxである」は証明できない
;; G = g(g) = 「「xはxである」は証明できない」に自身を代入した文は証明できない
(let (
      (G ((eval0 g) g))
      )
  (print "\n以下のようなGを考える（Gはゲーデル文）。")
  (print "G = (g g)")
  (print "  = " G)
  (print "  ;; 上式の引数を簡約")
  (print "  ;; (L (car G) (eval1 (cadr G)))")
  (print "  = " (L (car G) (eval1 (cadr G))))
  (print "  ;; Gと上式の引数が同じ")
  (print "  ;; (equal? G (eval1 (cadr G))) = " (equal? G (eval1 (cadr G))))
  (print "  = " (L 'is-unprovable 'G) " ; Gは証明できない")
  )

以下のようなGを考える（Gはゲーデル文）。
G = (g g)
  = (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x)))))
  ;; 上式の引数を簡約
  ;; (L (car G) (eval1 (cadr G)))
  = (is-unprovable
      (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x))))))
  ;; Gと上式の引数が同じ
  ;; (equal? G (eval1 (cadr G))) = #t
  = (is-unprovable G) ; Gは証明できない

あとは、一般的な第一不完全性定理通り、以下のように証明できる。この部分は本書には載っていない。

Gを証明可能と仮定する。すると、(is-unprovable G)が正しいと証明可能となる。つまり、Gは証明できないと証明できることになる。背理法よりGは証明不可能。

not Gを証明可能と仮定する。ここで、
not G = not (is-provable G) = (provable G)
となる。これより、not Gが証明可能となると、Gも証明可能でなければならなので矛盾。背理法よりnot Gが証明不可能。

Gもnot Gも証明できない。Q.E.D.

ソースコード

ソースコードは以下にある。
github.com

これは、Gaucheで実行することができ、実行すると以下のように出力される。

$ gosh incomplete_theorem.scm
第一不完全性定理：Gもnot Gも証明できないようなGが存在する

g = (lambda (x) (L 'is-unprovable (L x x)))
とする。

以下のようなGを考える（Gはゲーデル文）。
G = (g g)
  = (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x)))))
  ;; 上式の引数を簡約
  ;; (L (car G) (eval1 (cadr G)))
  = (is-unprovable (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x))))))
  ;; Gと上式の引数が同じ
  ;; (equal? G (eval1 (cadr G))) = #t
  = (is-unprovable G) ; Gは証明できない

Gを証明可能と仮定する。
すると、(is-unprovable G)が正しいと証明可能となる。
つまり、Gは証明できないと証明できることになる。
背理法よりGは証明不可能。

not Gを証明可能と仮定する。
ここで、
not G = not (is-provable G)
      = (provable G)
となる。
これより、not Gが証明可能となると、Gも証明可能でなければならなので矛盾。
背理法よりnot Gが証明不可能。

Gもnot Gも証明できない。Q.E.D.