不完全性定理の"帰結"に関する話題

@ytb_at_twtさんのゲーデル検定に端を発する、不完全性定理の帰結ってなんなの?という話題。
5
ぼんてんぴょん(Bontenpøn) @y_bonten

@hymathlogic ゲーデル文自体の構成過程やその内容が体系によって異なるために、「決定不能文の実例」というと「特定の体系における、ゲーデル文が表す命題」という意味に取れてしまうのですね。連続体仮説は「ZFCにおける、おそらくゲーデル文とは別の実例」なのですね。

2013-10-06 17:52:55
ぼんてんぴょん(Bontenpøn) @y_bonten

ゲーデル文自体の体系ごとのバラエティを見誤っていたために、「そんなもん実例がゲーデル文そのもののわけないやん」という思い込みがあった。

2013-10-06 17:56:19
ぼんてんぴょん(Bontenpøn) @y_bonten

ってことはアレか、ゲーデル文を「自然数論を埋め込んだZFC」で構成して解釈すれば、ムチャクチャ複雑だけれど私たちに意味の分かる命題になるってことかな。

2013-10-06 17:59:38
Hiroyasu Kamo @kamo_hiroyasu

@y_bonten @noukoknows 「理論T'が理論Tを含む」の定義は、「Tの論理式からT'の式への写像が存在し、その写像はTで証明可能な論理式をT'で証明可能な論理式に移す」です。ZFCはPAを含みます。

2013-10-06 18:02:28
ぼんてんぴょん(Bontenpøn) @y_bonten

@kamo_hiroyasu @noukoknows ちゃんと「含む」に定義があることに思い至っていませんでした。ありがとうございます。

2013-10-06 18:03:27
このツイートは権利者によって削除されています。
ぼんてんぴょん(Bontenpøn) @y_bonten

@functional_yy あぁ、埋め込み作業は経験したことがあるのに、すっかり忘れていました。

2013-10-06 18:06:14
Hiroyasu Kamo @kamo_hiroyasu

@y_bonten @noukoknows 細かいことをいうと、構文論的に含むのと意味論的に含むのがありますが、一階述語論理では両者は一致しますので、ZFCとPAの場合は違いを気にする必要はありません。

2013-10-06 18:09:44