ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (20)
前回の記事についてTwitterで泣きを入れてみたところ
なんと結城先生直々にリプいただけました
2乗が出てくるからくりがつかめました
いただいたリプ
「部分論理式の総数」で押さえているようです。添付画像は岩波文庫『不完全性定理』の当該部分（ゲーデルの論文）からの引用です。 pic.twitter.com/rFetoHCsBe
— 結城浩 (@hyuki) 2017年10月15日
本
ではゆっくり考えてみます
xにいたる論理式列の長さは、xの部分論理式の総数以下である
「部分論理式」というのが何なのかは書いてありませんが
論理式の中に含まれる、論理式の形をした部分ということでしょう
前回ちょっと作ってみた∀z1((¬(x2(0)))∨(y2(f0)))で言えば
(¬(x2(0)))∨(y2(f0))、y2(f0)、¬(x2(0))、x2(0)がそれにあたると思われます、
あ、数学っぽく考えれば∀z1((¬(x2(0)))∨(y2(f0)))自身も含んでそうですね
そうすると5つ
この場合、論理式列の長さは以下の通り5ですから一致してますね
x2(0) | ¬(x2(0)) | y2(f0) | (¬(x2(0)))∨(y2(f0)) | ∀z1((¬(x2(0)))∨(y2(f0)))
論理式の生成ルールを1回適用すると論理式列がひとつ長くなると同時に
新しい論理式がひとつでき、
捨てない限りその論理式はxに現れるはずですから部分論理式となります
なので通常は論理式列の長さと部分論理式の数が一致しそうです
論理式列の長さが部分論理式の総数より少なくなるのは・・・
えーと？またわからない？
じゃあ部分論理式はどれくらい作れるのかと考えてみると
長さ1の部分論理式：(たかだか)(len x)個
∀z1((¬(x2(0)))∨(y2(f0)))だと、∀、z1、(、・・・が
部分論理式になりうるとして
最大限に見積もってもxの長さまでしかないですよ、ってこと
実際には長さ1の論理式はありえませんが
いや、論理式の形をしてなくても数えるルールなのかな？
それなら論理式列の長さの方が短くなる
「たかだか」がついてるのは(と(のように一致するものは
ひとつと数える、とか？
同様にして
長さ2の部分論理式： (len x)-1個 (∀z1 z1( ((・・・)
長さ3の部分論理式： (len x)-2個 (∀z1( z1(( ((¬・・・)
:
:
長さ(len x)の部分論理式: 1個 (∀z1((¬(x2(0)))∨(y2(f0))))
合計で(len x)×((len x)+1)/2個 ≦ (len x)^2、となるので
論理式の列の長さは(len x)^2を超えることはない
というのが2乗のでてくるしくみでした
実際のところは2乗のオーダじゃないと思いますがそこは割り切ってるんでしょうね
