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

まだちょっとすっきりしない

M23をもういちど考え直す

(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 x)は
最後の要素がxと一致する、"基本論理式"から組み上げた"論理式"の列、
のゲーデル数の上限

この論理式の列をE1、E2、・・・、En(=x)と書くことにすると
そのゲーデル数は2^E1*3^E2* ... *Pk^Ek* ... *Pn^En

Pk(1≦k≦n)≦Pnは明らか

そしてNot、Or、Forallはすべて与えられた論理式に記号を
追加するので組み立てられていく論理式は長くなっていく一方
作ったけど使わないといった無駄なことをしない限り
登場する論理式の中ではxが最大となるはず

したがって

2^E1* 3^E2* ... *Pk^Ek* ... *Pn^En

は

Pn^ x*Pn^ x* ... *Pn^ x* ... *Pn^En

を超えることはないと言える
ここまでは問題ない
あとはnが(len x)^2を超えないことを言えればいいんだけどここが問題

どうにもイメージが湧かないのでいったん定義に戻って考え直す

Ekは

(A) 基本論理式 a(b) である
か、すでに組み立てられた論理式Ei、Ej(1≦i,j≦k)を使っった以下の式のいずれか
(B1) ¬(Ei)
(B2) (Ei)∨(Ej)
(B3) ∀v(Ei)

ちょっくら具体的に作ってみる

(1) x2(0) : (A)より
(2) ¬(x2(0)) : (1)と(B1)より
(3) y2(f0) : (A)より
(4) (¬(x2(0)))∨(y2(f0)) : (2)(3)と(B2)より
(5) ∀z1((¬(x2(0)))∨(y2(f0))) : (4)と(B3)より - Xとする

(len X)=24だから(len X)^2=576
5ステップで作った論理式のステップ数の上限が576っていうんだからかなり富豪
ていうか２乗してなくても富豪

(A)〜(B3)までを論理式の長さの点から見てみる

(A) 基本論理式は最低4記号からなる
(B1) 与えられた論理式に¬、(、)の3記号を追加
(B2) 与えられた論理式に(、)、∨、(、)の5記号を追加
(B3) 与えられた論理式に∀、v、(、)の4記号を追加

ゲーデルの証明の中では無駄な論理式を作って捨てるようなことはしないと
考えて問題なさそうなので
そうすると作った論理式が縮んだり消えたりすることはなく
(A)で導入した基本論理式や(B1)〜(B3)で追加した記号はすべて
xの中に現れる（はず・・・）

逆に、与えられた論理式を組み立てるための列もなんら悩むことなく構成できそう

そう考えると、列の要素がひとつ増えるたびに、最終的にできあがる論理式は
最低でも3記号分増えることになる
つまりnの上限は(len x)÷3ってことになってしまう
大雑把な上限の話をしてるんだから÷3は省くとしても
２乗がついてるのはさすがに意味があるはずだよなあ