ゲーデルの不完全性定理の証明のアレを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
とk書くことにすると
まじめに計算すれば2^?*3^?*5^?*...*P^?
となるところを
上限が大きくて困ることないよね!と
P^x*P^x*P^x*...*P^x
にしてしまってるということのように思われます
ということはあとはx
を作るのに必要な論理式の数が多くても
(sqr (len x))
だとわかればいいわけですがうーん
x
に含まれる記号が(len x)
個で、
ありえないけど仮にすべての記号が1文字からなる論理式であるとして、
その論理式を組み立てるのには最大でも(len x)
個の論理式からなる列があればよい、
ってことかなあ
まだちょっとすっきりしない