「無矛盾を表す文」とクライゼルの注意について

@igaris

P=NP予想を解決するために P=NP という命題を形式化したとき、形式化の仕方によって証明可能になったり証明不可能になったりする可能性はあるのだろうか。

@igaris

とすると、P=NP の真偽は、何をもって信じればよいのだろう。

@igaris

「無矛盾性を表す文」も、形式化の仕方によっては証明可能になるのでしたよね、たしか。証明可能性述語の性質がポイント。

Takayuki Kihara @tri_iro

クライゼルの注意によって、証明できると主張されている文は、おおよそ『矛盾は証明できない ∨ 矛盾と無矛盾の両方の証明が存在する』（正確にはもう少し強い主張）という形なので、果たしてこれを「無矛盾性を表す文」と言えるのか。

Takayuki Kihara @tri_iro

「クライゼルの注意」のことなら、あれを「無矛盾性を表す文」と言うのは無理があると思うんですけどね……。 RT @igaris: 「無矛盾性を表す文」も、形式化の仕方によっては証明可能になるのでしたよね、たしか。証明可能性述語の性質がポイント。

@igaris

@tri_iro そうなのですか。どのような理由で無理があると言えるのかは、私は存じないのですが。

Takayuki Kihara @tri_iro

@igaris つまり、クライゼルの定理の主張の文が証明できたとしても、導けることは「自分は無矛盾であるか、あるいは、矛盾も無矛盾も証明しちゃうよ」ってことなのです。

@igaris

@tri_iro 一つ目のコメントが反映されておらず、見逃しておりました。「矛盾も無矛盾も証明しちゃうよ」だったら、矛盾しているってことですよね。なるほど。そうなのですか。

Takayuki Kihara @tri_iro

@igaris 正確には、『自分は無矛盾である or 矛盾も無矛盾も証明するが無矛盾の証明の方が簡単』という文なので、一応、「どっちかというと無矛盾に近い」という感じのニュアンスは込められてはいます。でも、やっぱり「無矛盾性を表す文」とは言い難いと思います。

@igaris

@tri_iro ふむー。詳しくは本を読んでみないと分かりませんが、参考になりました。ありがとうございます。今は実家ゆえ、東京（っていうか神奈川）に戻ったら本を読み返してみます。

Takayuki Kihara @tri_iro

しかし、通称「クライゼルの注意」と呼ばれるものの元ネタ（初出）を知らないので、なんともいえない。

Takayuki Kihara @tri_iro

クライゼルの注意の初出を巡ってとりあえず日本語Wikipediaの「不完全性定理」を見てたら、「パリーハリングトン原理」とかいう記述があって何のことかと思ったけど、「パリス・ハーリントン (Paris-Harrington)の定理」のことか！

Takayuki Kihara @tri_iro

ハーリントン先生は、うちのT先生の師匠です。

はやし @t_hayashi

Wikipedia の「不完全性定理」の項でパリス＝ハーリントンの定理が「パリーハリングトン原理」と記述されてる、だって？ (via @tri_iro) 信じられん。

Takayuki Kihara @tri_iro

どうやってあのロッサー文もどきを「無矛盾性を表す文」として解釈できるかよく分からないので、クライゼルがどう説明しているか調べようと思ったんだけど、それに関する英語の記述がぜんぜん見つからない。クライゼルの注意に関する日本語の記述だけはちょこちょこ見つかるんだけども。

Takayuki Kihara @tri_iro

「クライゼルの注意」をどう解釈すればいいか、あるいは「クライゼルの注意」の初出をご存知の方は教えていただけると嬉しいです。

yoriyuki @yoriyuki

@tri_iro Feffermanの論文とか、Boolosの本とかには何か書いていないでしょうか。

Takayuki Kihara @tri_iro

@yoriyuki 情報ありがとうございます。Fefermanの論文はどれのことか分かりませんが、Boolos本をちょっと読んでみます。

yoriyuki @yoriyuki

＠tri_iro Fundamenta Mathematicaeの論文です。いや、どちらも読んだ事ないんですが…

Takayuki Kihara @tri_iro

@yoriyuki ありがとうございます。ちょいと眺めてみます～。

はやし @t_hayashi

@tri_iro ぼくの師匠の論文 http://bit.ly/6arg1s によると、[Kreisel 1960] にいわゆる「クライゼルの注意」と呼ばれているものと対応する記述があるようです。これが果たして初出かどうか、ちょっと分かりませんが、いちおうお知らせして起きます。

Takayuki Kihara @tri_iro

@t_hayashi どうも情報ありがとうございます。あとでチェックしてみます。

Takayuki Kihara @tri_iro

あ、なんか勘違いしてた気がしてきた。もうちょいちゃんと考えてみよう。

Takayuki Kihara @tri_iro

クライゼルの注意が言うことは理解できたけど、でも納得はいかないなー。「証明可能性述語」の定義の変更は認められるレベルだけれど、そのまま素朴に「無矛盾性」の定義を変更したら、無矛盾性の意味が弱まりすぎて、証明できても不思議でないように見えてくる。

Takayuki Kihara @tri_iro

つまり、『矛盾するならば、必ず「0≠1」より「0=1」の方が先に証明されるはずだ』という謎の要請が求められているように思うんだけど、どうなんですか。