数学の基礎づけ

谷口一平 A.k.a.hani-an @Taroupho

あー、めたたたた……。

乙吉 @otu_kichi

@Taroupho ？ｗｗｗ　こんばんは。どうかされました？ｗｗ

Jun Inoue @jun0inoue

@Taroupho ほあっちゃぁ!!!

谷口一平 A.k.a.hani-an @Taroupho

@otu_kichi いえいえ、ご心配どうもです。「メタい話をしていて頭がいたたたた……」が自然に短縮されて、先のツイートになりましたｗ

乙吉 @otu_kichi

@Taroupho ｗｗｗ▽///

Jun Inoue @jun0inoue

@Taroupho そうですね。￢(T⊦φ)⇒(ZFC⊦￢Bew(#φ))を示そうとすると、￢(ZFC⊦Bew(#φ)) からZFC⊦￢Bew(#φ) と、メタな not をオブジェクトの not に移動させる段階で不完全性定理に噛みつかれます。

Jun Inoue @jun0inoue

@Taroupho それは完全性定理と(T,φ⊢Ψ)⇔(T⊢φ→Ψ)があるので結局同値な定義になるはずです。私の主張は、BewはあくまでTのモデルMの元の組み合わせで実現された#φの文構造だけを云々する述語なのに対し、PはφがM全体について真理を述べているか見ると言うことです。

Jun Inoue @jun0inoue

@Taroupho それは噂の(T⊦φ)⇔(T⊦P(#φ))にゲーデルの完全性定理を合成した物っぽいです。*不* 完全性定理とは「完全」の意味が違う奴。Tarski の名前がついてるのは謎ですが…Tarski は真理述語の定義不可能性の間違いではありませんか?

Jun Inoue @jun0inoue

@Taroupho 不完全性定理の理解の浅さについては全面的に同意します。現在、絶賛火傷中。ただ、件のメタ定理こそが「証明可能性は可証性術語で表わされる」という主張だと考えられます。そのメタ定理の # を証明する事が、ZFCに「自分は可証性の話をしています」と言わせる事。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue ああ、演繹定理……その発想は無かった（笑）　確かに、同値な定義ぽいですね。失礼致しました。(T |= φ)⇔(T |- P(#φ)) が Tarski で、これから簡単に導出できるので、変形版も Tarski の名前で呼ばれた感じなのでしょうね。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 確かに、Bew は文構造をチェックしているだけですが、P はモデル全体を範囲に取っているので、もっと超越的という気がしますね。ここら辺の話はまだ勉強不足で、よく追っかけられない感じなのですけれども。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 素朴な（？）疑問が数学の基礎付けの森に迷い込んでしまったらしいです。メタいです。「証明不能性は可証性述語の否定で表わされない」の裏返しと合わせて、不完全性定理の含蓄深いところですね。それにしても、毎回こんな初学者にお付合い下さり、申しわけないですｗ

Jun Inoue @jun0inoue

@Taroupho こちらこそ、今回は若干自分の力量を越えて勇み足しちゃった感が有るので申し訳ないです。もっとdefinitiveな答えを返せるといいんですが。私としては自分の理解のバグ出しになってるのでメリットあるんですけどね→http://t.co/R3cKesK