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

定義32 "(a)→(b)"、"(a)∧(b)"、"(a)⇄(b)"、"∃x(a)"を得る関数

(define (Implies a b)
  (Or (Not a) b))
(define (And a b)
  (Not (Or (Not a) (Not b))))
(define (Equiv a b)
  (And (Implies a b) (Implies b a)))
(define (Exists x a)
  (Not (ForAll x (Not a))))

そのまんま

便利なだけの定義だから本来不要なんだけれどもこれがないと証明自体めんどくさいから
ということ

定義33 xを、nだけ"型持ち上げ"したもの

(define (typelift n x)
  (Min y ≦ (expt x (expt x n))
       (∀ k ≦ (len x)
          (or (and (not (IsVar (elm x k)))
                   (= (elm y k) (elm x k)))
              (and (IsVar (elm x k))
                   (= (elm y k)
                      (* (elm x k)
                         (expt (prime 1 (elm x k)) n))))))))

えーと
どう読むのかな

まず出てくるy ≦ (expt x (expt x n))は見るからに超絶贅沢な感じの式
中身を理解してから戻ったほうがよさそうな気がする

∀ k ≦ (len x)はxに含まれるすべての記号について、ということ

orのひとつめの項は、変数じゃなければそのままにしておくよ、ということ

ふたつめの項がポイントのはず
(elm x k)は今見ている変数
たとえばx1なら17、x2なら17^2
(* (elm x k) (expt (prime 1 (elm x k)) n))
(prime 1 (elm x k))は17を取り出している
17をn乗して元の数にかければ、たしかにnだけ型持ち上げしたことになりますね
理解
ここでprimeを使っているということはやっぱり素数指数表現の歯抜けは認めてるということだなあ

じゃあy ≦ (expt x (expt x n))は何か
(expt x n)はたぶん(expt (prime 1 (elm x k)) n)よりも確実に大きな数、
ということでしょう

xの各記号がすべて変数で、それらをすべてnだけ型持ち上げしてもまだ
それより大きな数が(expt x (expt x n))ということなのではないかと

テトラ「ゲーデルさんはこの証明をコンピュータがない時代にやったんですよね……」

式を考えたこともすごいけど、
それが合ってる（すくなくとも間違いだと指摘されない）というのがすごい
ここって大丈夫？と思うところもちゃんとそれで辻褄があっているっぽい
（自分が気づく範囲では、だけど）

テストできてたうちはまだなんとか安心できたけど
動かせなくなったらもう細かいところがあってるかどうかなんてまったく言いきれそうにない