Edit Comment on
20070313-1
n[0] = "さかい"; m[0] = "ロッサーの不完全定理がどうして成り立つのか私も不思議です。
聞くところによると、ゲーデル文とは違う論理式を考えるらしいですが……"; d[0] = "2007-03-14 18:55:33"; n[1] = "通りすがり"; m[1] = "http://en.wikipedia.org/wiki/J._Barkley_Rosser
「この命題は証明できない」がゲーデル文だとすると
「この命題の証明が存在すれば、
この命題の否定のより簡単な証明が存在する」
がロッサー文だそうです。
ロッサー文が証明できれば、矛盾が導かれます。
しかし、ロッサー文の否定
「この命題の否定の証明が存在し、
それより簡単なこの命題の証明は存在しない」
が証明できると、ロッサー文の証明も存在することになり
やはり矛盾が導かれます。
ちなみに、ロッサー文もしくはその否定のいずれかが
真であっても、実際に証明できない限り、矛盾は導かれません。
その意味で、ロッサー文はパラドックスではないということです。
"; d[1] = "2007-03-15 08:58:25"; n[2] = "かがみ"; m[2] = "さかいさん、こんにちは。どうも色々いい加減なことを書き、申しわけございませんでした。うーん、不完全性定理もう一度勉強した方が良いかも>私。そもそも理論内部で理論をコード化できることは、不完全性定理のきもなわけで、当然モデルの中でも出来るわけなのに、その辺りを超準モデル内での部分モデルの定義不可能性と混同して、あれやこれや混乱してしまいました。今回は色々勉強になりました。ありがとうございます。"; d[2] = "2007-03-15 11:58:52"; n[3] = "かがみ"; m[3] = "通りすがりさん、こんにちは。ローサーの不完全性定理は丁度前原先生の「数学基礎論入門」でさらっと定義を復習しました。面白いことに「自分自身の整合性が証明できない」という第二不完全性定理に対する「クライゼルの注意」 (「解釈を変更すれば整合性を証明できる」と解釈できないことはない」にも関連しているようです。面白そうですので、「あさって」の日記に教えて頂いたことを含め、何か書こうかと考えています。どうもありがとうございます。"; d[3] = "2007-03-15 12:02:16"; n[4] = "Standard Model"; m[4] = "標準的自然数に関してはかがみさんの以前の記事からちょっと考えていたのですが、何となくω無矛盾であるような超準モデルも存在しそうな気がします。知識が足りずきちんと検証出来ないのが残念ですが。
モデルの議論をするときにはsemanticsのレベル(≠metaのレベル)で外延性公理だとか選択公理だとかを暗黙にもしくは明示的に仮定しているわけで、標準的自然数というのはそのレベルでの集合論の公理によって定義された普通の自然数(つまりω)ということで良いんじゃないかな、と。
勉強中なので適当な事しか言えないのですが、多分semanticsの議論と言っても、所詮ある理論のsyntaxを集合論のsyntaxによって(ShoenfieldのMathemtical Logicの4.7 INTERPRETATIONSのような意味で)interpretしているだけだと思います。Tarskiによる真偽の定義とかと同じで、モデルや真偽の定義自体は超越的なものでも気にする事ないんじゃないかな、と。"; d[4] = "2007-03-24 20:06:26"; n[5] = "かがみ"; m[5] = "Standard Model さん、コメントありがとうございます。いまいち的確な返事になっていませんが、今考えていることを
http://evariste.jp/kagami/diary/0000/200703.html#20070324-1
に記載しました。すみません、ほんと見当はずれかも。"; d[5] = "2007-03-25 04:47:04"; n[6] = "かがみ"; m[6] = "(2008年6月26日) この日のコメント欄に集中的にスパムが入るので、この日のみ書き込み禁止致します。ご意見があるかたは、最新の日記のコメント欄にこちらを引用しての記載をお願い致します。"; d[6] = "2008-06-26 02:31:07";
(password)