ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (18)

「10.8.4 変数・記号・論理式」の続き

なにごともなかったかのように続けてみる

定義23 xは論理式である

(define (M23 x)
  (expt (P (sqr (len x))) (* x (sqr (len x)))))

(define (IsEndedWith n x)
  (= (elm n (len n)) x))

(define (IsForm x)
  (∃ n ≦ (M23 x) (and (IsFormSeq n)
                      (IsEndedWith n x))))

M23はいったいどういう意味だろう

まずIsFormから考えてみる
nが"基本論理式"から組み上げた"論理式"の列で、nの最後の要素がxと一致する、
ってことだな

これとM23の形を見比べてみる
(sqr (len x))番目の素数を使ってるところを見ると、
論理式の列の長さは長くても(sqr (len x))だと言いたいのでしょう

そしてそれぞれの論理式は基本論理式かまたはそれまでに出現した論理式をもとに
NotかOrかForallで作られ、最終的にできあがるのがxなので
無駄さえなければxが最大であるはず

つまりここで(P (sqr (len x)))をPとｋ書くことにすると
まじめに計算すれば2^?*3^?*5^?*...*P^?となるところを
上限が大きくて困ることないよね！と
P^x*P^x*P^x*...*P^xにしてしまってるということのように思われます

ということはあとはxを作るのに必要な論理式の数が多くても
(sqr (len x))だとわかればいいわけですがうーん
xに含まれる記号が(len x)個で、
ありえないけど仮にすべての記号が1文字からなる論理式であるとして、
その論理式を組み立てるのには最大でも(len x)個の論理式からなる列があればよい、
ってことかなあ
まだちょっとすっきりしない