到達不可能基数の存在
そう、それでペンローズの「不完全性定理を利用した強いAI論への反駁」の何が問題なのかをようやく理解したもののこれを説明するのは大変だ。
「到達不可能基数の存在は ZFC から独立である」
これは論理学の専門家でもよく勘違いしてしまう誤りです。というのは、到達不可能基数の存在は、通常の数学がすべて展開できるとされる ZFC から導くこと (つまり証明すること)は出来ません。これは有名な事実ですが、この事実を念頭に、つい「独立である」と言ってしまうようです。
ある命題がある公理系から独立であるというのは (標準的な論理学の用語法では)、その命題の肯定も否定も公理系から導かれないことです。つまり、到達不可能基数の存在が ZFC から独立である為には、その存在が ZFC から導かれないだけではなく、その不存在もまた ZFC から導かれないことが必要なのです。
ZFC から到達不可能基数の不存在が導けない、というのは、背理法がありますから、 ZFC に到達不可能基数の存在を主張する公理を追加した公理系が無矛盾であることと同値になります。しかしこれは証明できないことが知られています。つまり、少しややこしくなりますが、「『ZFC から到達不可能基数の不存在は証明できない』ということは証明できない」ということが証明されている訳です。
とこう書いてしまうと、少し知識のある方から、何を前提にしての話なのかが曖昧であるし、例えば巨大基数公理を仮定すればそれは証明できるではないか、などと言われてしまうかもしれません。通常、数学の言明でとくに前提となる体系が明示されていない場合には前提となる公理系は ZFC であるという暗黙の約束事がありますが、独立性などの議論の際には ZFC が無矛盾であること (これは ZFC からは導かれない)も暗黙の仮定に含めて良いことになっています。「『ZFC から到達不可能基数の不存在は証明できない』ということは証明できない」と述べたのは、『ZFC から到達不可能基数の不存在は証明できない』という主張は、 ZFC の無矛盾性を仮定してもなお証明できないという意味です。
巨大基数公理を仮定すれば、というのは、 ZFC に巨大基数公理と呼ばれる公理を追加した体系の無矛盾性を仮定すれば、という意味ですが、これはいま述べた暗黙の約束事に反しています。また巨大基数公理の一番弱いものが到達不可能基数の存在ですから、巨大基数公理の無矛盾性を仮定してそこから、『ZFC から到達不可能基数の不存在は証明できない』こと、つまり ZFC に到達不可能基数の存在を追加した公理系の無矛盾性を導いても、単なる同語反復に過ぎず、意味のないことなのです。従って巨大基数公理を仮定して云々、は無理な言い訳としか言えません。
うわー、これは普通に勘違いしてた。たしかに、こうしないと「矛盾は ZFC から独立」も真になっちゃうのか!!
「『ZFC から到達不可能基数の不存在は証明できない』ということは証明できない」ということが証明されている
というのは、背理法で ZFC|-Con(ZFC+I) となって ZFC+I|-Con(ZFC) から ZFC|-Con(ZFC) で矛盾かな。
独立性などの議論の際には ZFC が無矛盾であること (これは ZFC からは導かれない)も暗黙の仮定に含めて良いことになっています。「『ZFC から到達不可能基数の不存在は証明できない』ということは証明できない」と述べたのは、『ZFC から到達不可能基数の不存在は証明できない』という主張は、 ZFC の無矛盾性を仮定してもなお証明できないという意味です。
あたりには闇を感じた、っていうかやばいよ、この分野下手に手をだすと首が飛ぶよ。
