08/01/16 23:14:00
;;チャイティン Lispによるゲーデルの証明
;;(valid-proof? x) の定義があると仮定する。ｘが妥当な証明なら'()
;;xが妥当な証明なら実証された定理を返す。
;;ｓ式ｙが証明できない⇔すべてのｓ式ｘについて (valid-proof? x)が
;;ｙと等価とは限らない。
;;これを肯定する述語が (is-unprovable y)
(define (g x) `(is-unprovable (value-of (',x ',x))))
> (g 'x)
(is-unprovable (value-of ((quote x) (quote x))))
> (g g)
(is-unprovable (value-of ((quote #<procedure:g>) (quote #<procedure:g>))))
> (equal? (g g) (eval (cadr (cadr (g g)))))
#t
>
証明できないということは証明できない ＝ （証明できないということは証明できない）ということは証明できない。
こういう意味なのだろうか？頭が痛くなりそうだ。