＞岩波の応用数学講座の奴が難しいというより
＞大事なところが抜けているというのには正直ほっとしました。

1に聞くけど、君は本当にそこが知りたかったの？
>>6で指摘したことってすっごく細かいことだと思うよ。

＞命題の真偽と証明可能性を摩り替えるというのは、
＞不完全性定理の証明自体には役立ったのかもしれないが、
＞誰かが言っていた不完全性定理の意味の理解の困難さに
＞繋がるのではと思います。

それは不完全性定理の”意味”をどう考えるかによるね。
例えば、完全な真偽の判定なんて無理ってことなら、
証明チェックなんて具体的に構成する必要はないんだよ。
どんな関数でもそんな特性をもたないことを示せばいい。
スマリヤンが「タルスキの定理のほうが簡単なのに」と
いってるのはそういうこと。