id:nucさんのところのエントリに反応してみるよ

個人的な意見だが、「連続体仮説」(continuum hypothesis)が何なのか理解できない人に、ペンローズの仕事を批判する資格はないと思う。

「連続体仮説が何なのか」を本当に理解している人って、Woodin以外にいるんですか？特に、世界の多様性がどうのとかいう問いかけに対して、連続体仮説が持っている意味について語れる人なんて。

うは、forcing required ですか。この夏に結構がんばって理解しようとして(生半可に分かっているとも言い難いけれども)、でもたぶん「数学的手法として非常に面白いが」「世界観を変えるものではない」と思いました。

id:nuc さんとかk.inabaさんが理解しようとしてわからないほどforcingは難しいものではないはずで、そうなっちゃうのはちと問題だなぁと。いや、真面目に細かいところをつめようとすると大変なのですが、大枠はそんなに厄介なものではないはずです。ただ、ぶっちゃけて大枠だけ書いたような文章がないというのが困ったものなわけですが。

ゲーデル文がどうのとか。最初に断っておくと、この茂木氏の議論は反機械論とかいう文脈ですでに使い古されたものです。『ゲーデルと20世紀の論理学』第一巻でも飯田先生が議論していました（とはいえ、飯田先生の文章自体は全体的に誠実なものであるけれども、反機械論のところは個人的には迷走気味だと思っていますが）。

まず第一に「計算システム」という言葉が曖昧で困るんですが。まあ、証明器だと考えて好意的に読めば特に間違えている部分はないと思います。ただ、「「私は証明できない」という意味を持つ」というのがどういうことか、そして自然数論の標準モデルと非標準モデルの話が出てこなければ、ごまかし気味であるのは確かだろうと。
復習しておくと、標準モデルというのは要するに私たちが自然数だと普段思っている0, 1, 2, 3, ...だけが自然数になっているモデル、非標準モデルというのはそうでない変なのが自然数だと思っているモデルのことです。んで、G(F)が「自分自身が証明できない」という意味を持つというのは、G(F)の証明をコードしているようなゲーデル数が存在していないということになります。
完全性定理があるので、G(F)が証明できないということは、G(F)が成り立たないようなモデルが存在するということです。そのモデルの中では、G(F) の証明をコードしているようなゲーデル数が存在しているわけです。もしそのゲーデル数が標準的な普通の自然数ならば、少々手間はかかるかもしれませんが、有限の操作でデコードして本物の有限の証明に直すことが出来ます。そうなると、全てのモデルでG(F)が成り立たないことになって矛盾してしまうわけです。つまり、このゲーデル数は、標準的でない変な自然数だからデコードできないんです。
つまり、G(F)が真だというのは、扱っているモデルが標準モデルであることを仮定してようやく出てくる結論なのです。すなわち、ゲーデルの不完全性定理の系として、帰納的に記述できる自然数論を含む公理系では非標準モデルを排除できないということが導かれる、と。本人が理解しているかはともかく、そこを説明しなくてもいい読者を想定しているとは到底思えないのですが。
とりあえず、「人間の数学者を計算によって完全にシミュレートできる」の方も、「計算」を「証明」で置き換えれば間違ってはいないです。でも、これは飯田先生の議論に対する反論にもなるのですが、なぜ「計算」というか機械に出来ることが数理論理学の意味での証明だけだと言い切れるのでしょうか？そうでない推論が含まれていればゲーデルの不完全性定理は（少なくともそのままでは）成り立ちません。「証明器には出来ないけれども人間に出来ることはある」というのはゲーデルの不完全性定理から確かに導かれますが、それをもって「機械には出来ないけれども…」は飛躍していると思います。っていうか、そこの飛躍自体が「人間は機械ではない」という反機械論の主張そのものを必要としていると思うのですが。

F にさせているのはその体系の中でモデルが空集合でないことを示すことなのに、
人は F のモデルを表現できる系を用意しているだけ。

ちょっと微妙。ゲーデルの不完全性定理は、モデルというか意味論というか、そういうものなしに記述することが出来ます。ですので、一行目は完全性定理から結果的に正しいのですがちょっと危ういです。好意的に読めば間違いではないですが、かといって茂木さんの主張の反論になっているかというと、うーん。
まあ、そんなところで。