ゲーデルの不完全性定理

ゲーデルの不完全性定理の考察をする。

考えなければいけないのは
①ゲーデル数計算法、
②何を示せばいいのか、
である。

[①について]
ゲーデル数計算法は単純に論理式と自然数が1対1に対応するような単射な写像を構成することである。（全射でなくてもいい）

さてこのとき論理式の構成法を精密に組み上げる必要はない。

論理式は記号列なので、ただの記号列から自然数への単射な写像を構成すれば自動的にその写像は論理式から自然数への単射な写像になる。記号列全体集合に定義された写像を論理式全体への制限写像にするだけなので。

記号は可算無限個存在するとする。変数記号や自然数記号などどうしても可算無限個必要になるので。

そして記号列は必ず有限長であることにしなければいけない。

Symbolsを記号全体、Natを自然数全体、Seg(n):={k|k∈Nat ∧ k<n}とし、Map(X,Y)を集合Xから集合Yへの写像全体とし、φ∈Map(Seg(n),Symbols)とすれば、φは長さnの記号列を表わすことが出来る。

φ∈Map(Seg(n),Symbols)のとき
len(φ)=n :⇔ φ∈Map(Seg(n),Symbols)

Union(X):={y|∃z(y∈z ∧ z∈X)}は集合族Xの和集合を表わすとし、
Strings:=Union({ Map(Seg(n),Symbols) | n∈Nat ∧ n≧1 })
が記号列全体を表わすことになる。

Stringsは可算無限個の集合なので、Natへの単射は存在できる。
それをgn∈Map(Strings,Nat)ということにする。
つまりgnがゲーデル数演算になる。

もっと具体的にしよう。
記号全体Symbolsの整列集合を考えると、SymbolsからNatへの単射snの存在が得られる。
primを小さいものの順番に並んだ素数列とする。
prim(0)=2, prim(1)=3, prim(2)=5, ...
φを記号列とすると、
gn(φ):=Times({ (i,exp(prim(i),sn(φ(i)))) | i∈Seg(len(φ)) })

以下は備考：
exp(m,n)は累乗法で、mのn乗。
exp(m,0):=1
exp(m,suc(n)):=mul(m,exp(m,n))

mul(m,n)は乗法で、mとnの積。
mul(m,0):=0
mul(m,suc(n)):=add(m,mul(m,n))

add(m,n)は加法で、mとnの和。
add(m,0):=m
add(m,suc(n)):=suc(add(m,n))

sucはNatの後者写像

f∈Map(Seg(n),Nat)のとき、
f={(0,f(0)),(1,f(1)), ... ,(n-1,f(n-1))}
Times(f):=mul(f(0),f(1), ... ,f(n-1))。

ちなみに写像primは集合論的に表記できる。
prim:=Intersect({ X | (0,2)∈X ∧ ∀m∀n∀l(((m,n)∈X ∧ l=min({k|k∈Nat ∧ ∀s∀t((s,t∈Nat ∧ s≦m ∧ (s,t)∈X) ⇒ tはkを割り切れない)})) ⇒ (suc(m),l)∈X)
})
Intersect(X):={y|∃z(y∈z ∧ z∈X) ∧ ∀z(z∈X ⇒ y∈z)}

[②について]
ゲーデルの不完全性定理では何を示したか。

φは自由変数を1つだけ含む論理式とする。
このとき自由変数を含まない論理式（閉論理式）Gが存在して、
G⇔φ[gn(G)]
が成立する（つまり証明できる）。

驚異的なことにφは何でもよく、
Probable[x]を「ゲーデル数xの閉論理式は証明できる」という論理式としておき、
その論理式の否定に対応する閉論理式Gが存在して、
G⇔￢Probable[gn(G)]
が成立する。（くどいようだが、これが証明可能ということである）

これはGが証明可能ならば同時にGが証明できないことが言えてしまう。
矛盾が発生するからGは証明できないことにするしかない。

以下、Gの構成法を示す。

x,y,zは自然数とする。
次のような自然数上の関数を定義する。
substi(x,y)=z :⇔ ∃v∃φ(vは変数 ∧ φ[v]は自由変数vを一つだけもつ論理式 ∧ gn(φ[v])=x ∧ gn(φ[y])=z)

substi関数の機能を言葉で説明すると、
xから自由変数を1つ含む論理式を抽出し、
その自由変数をyで置き換え、置き換えた論理式のゲーデル数zを求める
という関数である。

このとき注意してほしいことは、
φ[v]でvが変数のときは、φ[v]は自由変数vを一つだけ含む論理式で、
φ[y]でyが自然数のときは、変数vをyに置き換えた論理式（閉論理式）と認識しておいてほしいということである。
（数理論理分野では本当に表記方式の問題が壁になる）

yは任意の自然数を動けるが、xは自由変数を1つだけ含む論理式のゲーデル数に制限される。ご注意を。

φ[v]を自由変数を1つだけ含む任意の論理式とする。
次のような論理式ψ[v]を用意する。
ψ[v]:⇔φ[substi(v,v)]

自然数xを次のように与える。
x:=gn(ψ[v])

論理式Gを次のように与える。
G:⇔φ[substi(x,x)]
Gは閉論理式であることに注意。

substi(x,x)=yを検討する。
substiの第一引数より、
xの定義からx=gn(ψ[v])なのでψ[v]を取り出して、
vをxに置き換えて、ψ[x]のゲーデル数がyである、となる。
gn(ψ[x])=y

ψの定義まで戻って、
ψ[x]⇔φ[substi(x,x)]⇔G
substi(x,x)=y=gn(ψ[x])=gn(G)
G⇔φ[substi(x,x)]⇔φ[gn(G)]

つまり
任意のφから、φ→ψ→x→Gという順序で上記のように構成すれば、
任意のφに対して
G⇔φ[gn(G)]
が成立するようなGが得られる。

Gの構成法はAIから教えてもらった。
AIはすごい。