Lisperのためのゲーデルの不完全性定理の反証不可能性について考えてみた

Lisperのためのゲーデルの不完全性定理では、(g g)が証明も反証もできないことが示されていない。証明できないほうはいいとして、反証できないことがすぐに理解できなかった。unprovable-pとvalid-proof-pだけで反証不能なことが証明できるの？

ちょっと考えてみた。
(g g)の否定が証明可能だとすると、

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

の否定が証明可能ということなので、

(valid-proof-p
 (eval
  ((lambda
     (x)
     `(unprovable-p
       (eval
        (,x ',x))))
   '(lambda
      (x)
      `(unprovable-p
        (eval
         (,x ',x)))))))

ところがこれは、gの主張である

(unprovable-p (eval (,x ',x))))

と矛盾する。したがって(g g)は反証不可能。

こんな感じだろうか？

で、(g g)の形式的な決定不能性はいいとして、これをもってゲーデルの不完全性定理が証明できた、とは依然としていえないんじゃないだろうか。なぜなら、S式からなる形式的な系について、unprovable-pとvalid-proof-pがあるということ以上に何も情報がないから。それだけの情報では、この系が不完全性定理の前提条件を満たすかどうか確かめようがない。と思う。S式で自然数が作れるのは確かだけど、すべてのS式からなる系では当然無矛盾性を満たさないし。1階の述語論理に対応するS式のセットを再帰的に用意して、そこでunprovable-pとvalid-proof-pを（Lispの意味論を使わず形式的に）定義すればいいのだけど、簡単ではなさそう。（追記：Lispの実装にこだわらなければ、比較的わかりやすく形式化できるようです→howm wiki - 不完全性定理.改。Lispでゲーデルの不完全性定理が証明できる！のようなインパクトはないですが、「Lispを含む再帰的可算な公理系は不完全」の証明になってそう）

だからたぶんチャイティンの元記事は、不完全性定理のフレーバーをLispならS式で表せるぜ、という話であって、それは、不完全性定理のフレーバーを自然言語ならうそつきのパラドクスで表せるぜ、という話と大きく違わないのではないかと思った。