私はゲーデルのあら探しをしてやっつけてしまいたい衝動に駆られるが、
「~を証明できない」⇔「~を証明できる、は証明できない」と定義してしまったら、
G「Gは証明できない」
⇔
G「Gは証明できる、は証明できない」
⇔
G「¬Gは証明できない」
あっと驚くことに、これだけでG⇔¬Gが言えてしまいます・・・.
《寸 劇》
アインシュタイン「では、証明できても、証明できなくても、とにかく、ゲーデル命題はゲーデル命題だ、ということでいいのかね?」
ゲーデル「そうです、そもそもゲーデル命題ではゲーデル命題を証明できないこと自体が証明できません・・」
アインシュタイン「そしてゲーデル命題は数学の無矛盾性と同値だと?」
ゲーデル「それを私が証明しました!」
アインシュタイン「それはヒルベルトプログラム相手の当てこすり以外に何か意味を持つのかね?」
ゲーデル「と、申されますと?」
アインシュタイン「数学の無矛盾性は数学体系外の言葉なのではないかね?」
ゲーデル「それも、私が、ゲーデル命題は数学命題であると証明いたしました・・」
アインシュタイン「ふ~っむ!」
G「Gは証明できない」
⇔
G「Gは証明できる、は証明できない」
⇔
G「¬Gは証明できない」
あっと驚くことに、これだけでG⇔¬Gが言えてしまいます・・・.
《寸 劇》
アインシュタイン「では、証明できても、証明できなくても、とにかく、ゲーデル命題はゲーデル命題だ、ということでいいのかね?」
ゲーデル「そうです、そもそもゲーデル命題ではゲーデル命題を証明できないこと自体が証明できません・・」
アインシュタイン「そしてゲーデル命題は数学の無矛盾性と同値だと?」
ゲーデル「それを私が証明しました!」
アインシュタイン「それはヒルベルトプログラム相手の当てこすり以外に何か意味を持つのかね?」
ゲーデル「と、申されますと?」
アインシュタイン「数学の無矛盾性は数学体系外の言葉なのではないかね?」
ゲーデル「それも、私が、ゲーデル命題は数学命題であると証明いたしました・・」
アインシュタイン「ふ~っむ!」
このブログへのコメントはmuragonユーザー限定です。