2007-03-13 [長年日記]
λ. 不完全性定理に関して混乱中 (3)
前回のエントリで元々の疑問は大体解決しました。 色々とコメントや言及をありがとうございます。
特に、竹内さんと通りすがりさんのコメント、かがみさんのエントリ(モデルでの真偽, さらにω矛盾)は疑問を解消する上で大いに役立ちました。
また、あろはさんにも二つのエントリで言及していただきました。
以下、色々と余談みたいなものを。
何故こんな疑問を持ったか?
そもそも、何故こんな疑問を持ったかというと、きっかけはTaejun(태준)さんという方のブログTaejunomicsの「数学と法律はかなり近い？」というエントリに以下のように書いてあったこと。
述語論理の公理系に、等号の公理と数の公理が加わっただけで、その体系は数学の公理系になります。 ちなみに、この二つを加えることによって、完全な述語論理の体系が、不完全になってしまうらしく、これをゲーデルの不完全性定理というそうですね。 （完全とは、その公理系が妥当な論理法則の全てを証明することが出来る事を指します）
これに「完全性定理と不完全性定理の『完全性』は違う意味*1で、等号の公理と数の公理を加えることによって『完全性』が損なわれるわけではない」というような内容のコメントを書こうとして、「そういや、算術の体系に完全性定理を適用するとどうなるんだっけ?」と思い、9日の混乱(不完全性定理に関して混乱中)に至ったのでした。
不完全性定理に言及することについて
あろはさんの二つのエントリは幾つか勘違いしている気がするけど、それはとりあえず横に置いておいて、ちょっと別の話を。
あろはさんは真なのに証明できない命題 ？？？というエントリで「数学をちゃんとやってない俺が書いて良いような内容じゃないし… おこがましすぎる」と書いている。 けど、不完全性定理自体は基礎的な定理だし、前提知識も少ないので、ちょっと論理学を勉強すればすぐに理解できるはず。 「おこがましすぎる」等と言う前に、ちょっと勉強すれば良いだけだと思います。
実際、今回使ったのは向井先生の「数学と論理」*2という授業で得た知識くらいで、この授業は主に学部1年生が履修する授業です。
「通りすがり」さんの問題
「通りすがり」さんのコメントの「あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です」について考えてみる。
T ⊢ provable([G])→G と仮定する。 T ⊢ G≡¬provable([G]) より T ⊢ ¬provable([G])→G 。 T ⊢ provable([G])∨¬provable([G]) なので T ⊢ G 。 これは第一不完全性定理に矛盾するので、背理法より T ⊬ provable([G])→G 。 というわけで、T ⊢ provable([P])→P は一般には言えない。
次に、あるPについて provable([P])→P の否定が真であるモデルMを考える。 すなわち M ⊧ T∪{¬(provable([P])→P)} で、¬(provable([P]→P) ≡ provable([P])∧¬P だから、 当然 M ⊧ provable([P]) かつ M ⊭ P になる。 モデルが非健全という言い方には少し違和感を感じるけど、言わんとすることは理解できる。
残る疑問点
今回のことで不完全性定理についてだいぶ理解を深められた気がするが、まだ残っている疑問も幾つかある。
その一つはロッサーの不完全性定理が何故成り立つのかという事。 ゲーデルの証明ではω無矛盾性を条件としていたが、後にロッサーがω無矛盾性を無矛盾性に弱めている。 今回、ω無矛盾性を条件としたのは、これが何故成り立つのか知らなかったから。 聞くところによると、ゲーデル文とは違う文を考えるらしいが……
あとは、論理学にまつわるトンデモ言説「自分自身の無矛盾性を主張する文は証明できない」の以下の記述について。
標記の主張は、自分自身の無矛盾性を主張するすべての文は、証明できない、ということになってしまします。これは少くとも、通常ゲーデルの不完全性定理の対象とされるペアノ算術では正しくありません。実際に、自分自身(つまりペアノ算術)の無矛盾性を主張している(と理解できる)が、しかしペアの算術で証明できてしまう文が存在するのです。
これらはまたの機会にでも考える。
【追記】 と書いたら、かがみさんの「ロッサーの不完全性定理」でどっちも解決してしまった。もきゅ(´・ω・`)
*1 「完全性」の複数の意味については、檜山さんの「完全性／不完全性」は多重定義のし過ぎ！」を参照のこと。
*2 数学と論理(2006)に2006年度の講義資料がある。私が履修した2001年度とは内容もだいぶ変わってるけど。
＞非健全という言い方には少し違和感を感じるけど、<br>確かに・・・普通は「不健全」といいますね。
ところで、無矛盾性を健全性として定義した場合、どんな算術的述語Pを持ってきても、任意の命題XについてP("x")⇒Xが成り立つようには出来ません。なんでかというと、NP⇔¬P("NP")なる命題が構成できるからです。つまり、論理は不健全さを許容するわけです。神はトンデモも許容されているということか・・・(´-ω-`)
まあ、普通は無矛盾性は、P("x")⇒¬P("¬x")のように表すでしょうから、その場合、不完全性定理に抵触しない抜け道が存在するってことでしょう。（健全なら無矛盾だろうけど、逆は真ではない。このあたり、様相論理の公理のTとDの違い）
> 確かに・・・普通は「不健全」といいますね。 <br><br>違和感を感じたのはそこではなくて、健全性は通常は「T |- φ ならば M |= φ」のように「構文的な証明可能性」と「意味論的な真偽」との関係についての性質として定義されるのに、ここではモデルに対して使っている点です。<br># もしくは、証明可能性については我々にとっての証明可能性ではなくMの中から見た証明可能性を考えているのに、真偽についてはMの中から見た真偽(?)ではなく我々にとっての真偽を考えている点と、言うことも出来るかも。<br><br>> ところで、無矛盾性を健全性として定義した場合、<br><br>ここの部分は良くわかりませんでした。<br><br>> どんな算術的述語Pを持ってきても、任意の命題XについてP("x")⇒Xが成り立つようには出来ません。なんでかというと、NP⇔¬P("NP")なる命題が構成できるからです。つまり、論理は不健全さを許容するわけです。神はトンデモも許容されているということか・・・(´-ω-`)<br><br>「神はトンデモも許容されている」という表現は面白いですね。<br>トンデモが許容されるのは超準モデルでのことだと思うので、私は自分が住んでいるのが標準モデルであることを願ってます :-)
＞健全性は通常は「T |- φ ならば M |= φ」のように「構文的な証明可能性」と「意味論的な真偽」との関係についての性質として定義される<br><br>そうですね。私のいう「健全性」の定義は、証明可能性をT |- φではなくてM |= provable("φ")に置き換えてしまってます。<br><br>＞証明可能性については我々にとっての証明可能性ではなくMの中から見た証明可能性を考えている<br><br>という指摘は正しいでしょう。（ただし真偽についてはMの中で考えていると思いますが）
> ただし真偽についてはMの中で考えていると思いますが<br><br>この辺りはまだ混乱中なのですが、Mの中での証明可能性が「M |= provable("φ")」であるのなら、Mの中での真偽は「M |= true("φ")」にしなくてはならないのではないかと思ったのです。<br># 書いてみて気付いたのですが、この場合 truth の undefinability が問題になるのかな……
述語trueの定義は、任意の命題φについてφ⇔true("φ")だから、M |= φでもM |= true("φ")でも同じです。<br>で、このような述語が算術的に定義できないというのが、タルスキの定理で、これはゲーデルの不完全性定理と同様の方法で示せます。つまり、定義可能だと対角化によってφ⇔¬True("φ")なる命題が構成できるので矛盾する、というわけです。
おそーいコメントですが、「数学と法律はかなり近い？」について。<br>最高裁では「少数意見」や「反対意見」があるので、一意にまとまらない事からもわかるように、法律の解釈や適用、および事実の認定には個人差があって、二つが近いとはおもえないのです。なお素人考えであることを付け加えておきます。