>>113

> でも ゲーデル文 = ¬Pr(g(ゲーデル文)) という不動点だから

でもこれって違うの？別にゲーデル文Gが

　　　　　 ¬
　　　　　　｜
　　　　−Ｐｒ−−
　　　｜　　　　　｜
　　　　−−｜−
　　　　　　s(s(...... 0)) = g(G)

ってなってるわけじゃない？

定義はn = g("ゲーデル数Sub(x,g(x),x)をもつ式は証明できない"), g(G) = Sub(n,g(x),n) だと思うけれど。
そもそもSubってSubって関数だけから定義できる項になるわけじゃなくて文Sub'(x,y) (⇔ y = Sub(x,g(x),x)) でエンコードするんでしょ。だからもとの"ゲーデル数Sub(x,g(x),x)をもつ式は証明できない"からして

　　　　　 ∀y
　　　　　　　　　｜
−⊃−−
　　　　　　｜　　　　　 ｜
　　　　　Sub'(x,y)　　　¬　
　　　　　　　　　　　　　｜
　　　　　　　　　　　−Ｐｒ−−　
　　　　　　　　　　｜　　　　　｜
　　　　　　　　　　　−−｜−
　　　　　　　　　　　　　 y

じゃないか？ってことはGもそういう形（x を s(s..(0)) = g(n) にかえた形）をしている。。。。