ゲーデルの証明不能命題

質問

不完全性定理（形式的体系においてその公理と推論規則を使って証明も否定もできない論理式Ａが存在する。）にいう論理式Ａには例えばどんなものがあるのでしょうか？
　いまだ解かれていない数学上の難問がありますが、これらが論理式Ａであるかどうかは、結局のところ証明できた時点でしか判定できないのでしょうか。

回答No.1

uzo · ベストアンサー

例示はできないと聞いています。

ドキアデス『ペトロス伯父とゴールドバッハの予想』（早川書房）に
ゲーデルが不完全性定理を証明したときの、
ある数学者の受けた衝撃のエピソードが紹介されていて
なかなか迫力がありました。
特におっしゃる疑問の後段については、
同様の疑念を主人公の数学者（ゴールドバッハ予想に取り組んでいる）
が抱き、それに対して、フォン・ノイマンから
「証明不可能かどうか知ることは不可能であることを証明しました」
という手紙が主人公に届き、打ちのめされる姿を描いており、
なかなか鮮烈でした。

お礼

ご回答ありがとうございました。
ご指摘の本を読んでみます。
フェルマー予想を最終的に証明したワイルズなども
証明可能な方に賭けたのですね。

回答No.3

aster

ゲーデルの不完全性定理で出てくる、ある公理系では、必ず、その公理系の定理であることと、その否定が定理であるような命題が「構成できる」という時の、「構成できる命題」は、構成できるという前提での議論で、構成できるなら、そのような命題は、公理系内では、真とも偽ともどちらも言えるので、真偽判断ができないのです。

従って、「具体的な例」というものは、証明の構成上ありません。或る特定の公理系で、真とも偽とも判断できない命題というのは具体的にありえると思いますし、提示できます。

しかし、「いかなる公理系」でも、形式的構成で、その公理系では真偽判断不能な公理系内の命題が必ず存在するというのは、一般的な話で、あくまで、これは素人の意見ですが、ゲーデルの証明は、証明になっていないというのが私見です（わたしは、直観的構成的な考えになります）。

ある形の命題を形式的な形で述べてみて、そういう命題は、真だとすると、その結果、偽となり、偽だとすると、その結果、真になるというのが証明で、ここでは、「具体的な命題」を構成するという話は一切ありません。

これは、ラッセルのパラドックスと言われる、「自分自身を要素として含む集合」を考えると矛盾が出てくるというのと、似ています。そういう集合は具体的にどういう集合かというと、そんな集合は具体的に考えられないのです。

そういう集合が「ある」とすると、パラドックスが出てくるのですが、集合Ａがそういう集合だとすると、その要素を外延的に列挙すれば、あるいは定義的に定めれば、Ａは具体的に表現できそうですが、外延的に考えると明らかなのですが、Ａが具体的に定義されるには、その前に、Ａが定義されていないといけないということになります。

ラッセルのいう自分自身を含む集合は、まさに、この「自分自身を含む集合」という定義でしか定義できず、具体的に挙げることができません。

それと同様なことというか、ゲーデルの証明に出てくる、真偽決定不能の命題も、そういう定義の仕方で定義しているので、具体的には、構成できないのです。（証明法からして、「あるとすれば」ですから、構成はされていません）。

また、そんな命題があると、矛盾になるので、「ない」とも言えません。何故なら、矛盾するそういう命題が形式的に（どんな形かは一切言及なく）考えられるのですが、これが「矛盾」するので、証明が成立するというのが、ゲーデルの不完全性定理だからです。

＞いまだ解かれていない数学上の難問がありますが、これらが論理式Ａであるかどうかは、結局のところ証明できた時点でしか判定できないのでしょうか。

これは、また別の話です。ある定理が証明可能かどうか、というのは、「実は定理か、そうでないかの証明の問題」で、ゲーデルのいう形式命題がそれに妥当するとかしないとかとは、まったく別問題です。

定理か定理でないか、証明できていない、というのは、人間の知力の限界の問題で、あるいは、知力の限界の彼方に、定理とも定理でないとも証明できない命題だったということが分かるというような「数学理論」が出てくるかも知れません。

しかし、それはゲーデルの定理とは、一応別の話です。何故なら、ゲーデルの定理は、知力の限界の内側の話だからです。すでに、ゲーデルの定理は証明されていて、その証明で使っている、形式的な命題定義の形は分かっています。

回答No.2

ranx

ユークリッド幾何学における第５公準（平行線の公理）などは、その例と考えてよいと思います。
あとは、カントールの予想なども集合論の枠内では証明できないことが証明されていますね。
証明可能性を示す一般的な手順は存在しないとしても、個々には証明不可能を証明できる場合も
あるということだと思います。