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

Ryota Akiyoshi（秋吉亮太） @georg_logic

@tri_iro それってロッサー述語ですよね？ええ、その謎の要請のせいで簡単に無矛盾性が証明できるから、それを形式化すればTが無矛盾でも証明できるかと

Ryota Akiyoshi（秋吉亮太） @georg_logic

今、対象とする理論をTとする。Tは第二不完全性定理が成り立つ理論とする。このときT_Rをロッサー述語が表すような証明述語とする。 T \vdash Con_T_R　かどうかを考える際にはTは無矛盾としてよい（そうでなければT \vdash Con_T_R　は明らか）

Ryota Akiyoshi（秋吉亮太） @georg_logic

Tが無矛盾という仮定の下ではTとT_Rの外延、すなわち定理の集合は一致する。それ故、T_Rを表すロッサーの証明可能性述語にたいして（不完全性定理で登場する）表現定理が証明できるため、ロッサー証明述語で第Ⅰ不完全性定理が証明できる

Ryota Akiyoshi（秋吉亮太） @georg_logic

しかしながら、ロッサー述語の「謎の要請」により、T_Rの無矛盾性は簡単に証明できる。これを形式化すれば T \vdash Con_T_R　となる。ちなみにこのような事例から、第二不完全性定理は証明述語の定義の仕方に依存するため、「内包的」とも言われる

Ryota Akiyoshi（秋吉亮太） @georg_logic

@tri_iro あー、僕も初出は知らないですが、ロッサーの不完全性定理の論文のレビューとかかもしれません。ちなみに他にもこういう述語は作れて、T_Mを「Tで証明できてなおかつ0=1の証明ではない」としてもいいです（モストフスキ）

Ryota Akiyoshi（秋吉亮太） @georg_logic

さらにT_{T}を「Tでカット使わずに証明できる」とするTakeutiによる例もあります。

Ryota Akiyoshi（秋吉亮太） @georg_logic

Fefermanの例はArithmetization of metamathematics in a general setting, Fund. Math., vol. 49, pp. 35-92, 1960かな

Ryota Akiyoshi（秋吉亮太） @georg_logic

http://math.stanford.edu/~feferman/papers.html　にある"My route to arithmetization"にFefermanの解説がある

Takayuki Kihara @tri_iro

@georg_logic 詳しい解説ありがとうございます！なるほど、勉強になりました。

Ryota Akiyoshi（秋吉亮太） @georg_logic

@tri_iro いえいえお役にたてれば幸いです

Takayuki Kihara @tri_iro

しかし、モストフスキの方の述語はもっと気持ち悪いなあ。

Takayuki Kihara @tri_iro

一般に証明可能性述語は自分だけでなく他の再帰的公理化可能理論に対するものも内部で定義できるわけで、そのとき、矛盾する理論もまともに扱いたい。そのとき、矛盾を素朴に『0=1は証明できない』と定義すると、標準モデルでですら、普通の意味での矛盾と異なる意味になってなんか嫌だ。