@jun0inoue ごめんなさい、あれは思いっ切りネタツイートでございましたｗ　しかし、考案から僅か五日たらずで google の検索結果を五千件強にしてしまう Vipper の機動力は凄いものです。 http://t.co/rcgciPKj

posted at 19:15:07

@jun0inoue まあ、「n が整数のとき」とか言ってるわりには、ハーベンス関数（t=xtanhΦ/tanh^2Φ+1-(v^2/c^2) だそうです）の式に n が見当たらないですし……そんなもんですｗ

posted at 19:51:20

ですよねー。寝ることと死ぬことの最大のコツを、日々だらだらと実践してゆきたいと思いますｗ　RT @jun0inoue 寝る事の最大のコツは起きてる事です(死)

posted at 05:50:22

@jun0inoue これはひどいｗ　いえ、まあ、普通はそうですよねー。貴重な証言どうもです。数学そのものに関して（良かれ悪しかれ）思い入れが強い人は、哲学方面から手を出した人とか、非プロパーの人に多い気がしますね。むしろ個人的には、数学の本質はその無節操性にある、とか思ったりｗ

posted at 06:18:36

@jun0inoue 関係ないですが、基礎論厨にしては珍しく、当方は「0 は微妙に自然数じゃない」派、ですｗ

posted at 06:20:41

@jun0inoue ご、ごめんなさい……。結構、素朴な自然数に関する直観とか信じちゃってるところがあるんですよねｗ （含めた方が便利というのは認めます）

posted at 07:53:04

RT @jun0inoue: @Taroupho 0 が素朴な直観で捉えられないと言うのは甘え。 …いや、調子乗りましたすんませんw

posted at 08:24:47

@jun0inoue 毎度お世話になっておりますｗ　えーと、式の意味が微妙に取りにくいため確認させていただきますと、まず #φ は1階論理の論理式 φ のゲーデル数に対応する ZFC の対象式、と読んで大丈夫ですよね？　そして、T が1階論理の形式的体系を表わす、と。

posted at 07:38:33

@jun0inoue すると、ZFC 上の T に関する可証性述語を Bew(x) として、最初のメタ定理は「任意の論理式 φ に対して、(T |- φ)⇔(ZFC |- Bew(#φ)) となる」のことと理解してオーケーでしょうか。でしたら、確かに両者は同じものと言えそうです。

posted at 07:39:18

@jun0inoue えー、このメタ定理は……証明可能なんですかねｗ　これが、もし (ZFC |- φ)⇔(ZFC |- Bew(#φ)) の形をしていたら、真理述語の定義不能性に反してしまい証明出来ない感じですが、当座は左辺を T の範囲で考えていますから、何とも微妙なｗ

posted at 07:40:24

@jun0inoue それと、完全性定理に限定して言えば、ZFC 上の T に関して完全性定理を示すには、「モデル」とか「充足関係」とかを ZFC の言葉で定義しないといけないわけですが、「充足関係は ZFC では定義出来ない」という話を風聞したような。間違っていたらすみません。

posted at 07:41:38

@jun0inoue 仮に先のメタ定理が証明可能で、完全性定理など ZFC で形式化可能とすると、好きなときに1階論理に敷かれている ZFC を仮定したり、その逆を仮定したりしてよい、ということになるのでしょうかね。なんだか、直観的には不思議な感じがしてしまいますねー。

posted at 07:43:40

@jun0inoue 申しわけない、色々勘違いしていた気がします。T は「任意の」理論でしたね（1階述語計算の頭しかなく、多少混乱しておりました）。可証性述語に関しても、閉包したことしかないため、違和感に引っぱられてしまいました。ご説明感謝します。

posted at 21:39:24

@jun0inoue で、本題の (T |- φ)⇔(ZFC |- Bew(#φ)) ですが、ごめんなさい、これは成立しますね、確かｗ　不完全性定理によって成立しないのは、(￢(T |- φ))⇔(ZFC |- ￢Bew(#φ)) の方でしたか。真理述語の話などは勘違いでしたｗ

posted at 21:46:56

@jun0inoue 本筋から逸れますが、真理述語の定義不能性に関しては、意味論を介入させずとも定式化できた記憶があります。T |- φ⇔P(#φ) なる P は存在しない、という形で。対角化定理から A⇔￢P(#A) な A が存在して、一方 A⇔P(#A) となり矛盾します。

posted at 22:04:32

@jun0inoue ……これは別の話だったかも。自信ないです。一般的には (T |= φ)⇔(T |- P(#φ)) の形をよく見かけますね。両者とも「Tarski の定理」という名前で紹介されていた気がします。どういう関係なんだろう？

posted at 22:10:56

@jun0inoue さて、何だか当初の疑問をすっかり忘れてしまった感じですｗ　えーと、例のメタ定理は成立するとして、ただ証明可能性は可証性述語では表現されなかった筈ですが……これでよかったんでしたっけ。結局、不完全性定理の理解の浅さに足を引っぱられている気がしますねー。

posted at 22:21:42

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

posted at 23:19:28

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

posted at 23:31:48

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

posted at 23:41:28

@jun0inoue すみません、アレフが出せずオメガで表記しましたｗ　丁寧なご説明、有難うございました。なるほど納得です。もっとも、基数は順序数の部分クラスなので、任意の有限順序数 n に対して n⊂κ⊂ω となる κ が存在しないことを言えば、基数の場合に通用する気も。

posted at 07:14:11

@jun0inoue 順序数なら、κ⊂ω の仮定から x∈ω－κ なる有限順序数 x が存在してしまうことを利用して、矛盾を導けそうです。……それとも、構成から自明……でしょうか？　順序数の定義もうろ覚えになってますｗ

posted at 07:23:13

わーっ、またも誤解を招く表現をしてしまったようですみません！　順序数はノイマン式に構成されたものを考えていて、x∈ω－κ は順序数演算ではなく差集合のつもりでした。例によってバックスラッシュが（ｒｙ　RT @jun0inoue 無限順序数って引き算できるんでしたっけ。

posted at 16:03:40

@jun0inoue しかし仰る通り、最小に取っているのだから証明の必要はなさそうですね。連続体仮説なら連続体濃度の構成が順序数や基数の構成と独立なので一筋縄にゆきませんが、ω_0 の構成は定義とべったりですもんね。お騒がせしました、また勉強して出直しますｗ

posted at 16:12:34

@jun0inoue この度は混乱を招いてすみませんでした。自戒を込めてまとめておきましたｗ　http://t.co/EdjVvXo

posted at 21:26:15

河野氏の＜態度＞を擁護する気は毛頭ありませんが、自然数や偶数について話をすることは、一般には「数学」と呼ばれる話題の範疇だと思いますし、氏は「濃度」や「全単射」などとは言わず、「大きさ」とか「質」とか言っているので、超限集合論とは全然関係ない話なのでは。 @jun0inoue

posted at 00:42:22

氏の寓話は、ただ無限集合における部分集合関係について表現したものなのかも知れませんし、擁護しようと思えば幾らでも擁護出来ますが、濃度の話と取るのが自然なのは同意です。当方は「数理哲学的に興味ぶかい」と言っただけで、数学クラスタを批判したつもりはありません。 @jun0inoue

posted at 02:57:25

「自衛隊は暴力装置」と似たような話で、一方はただ暴力の機能を備えた国家の装置だと述べているだけなのに、批判と受け取られることがあります。当方は「数学とは非反省的な本質を備えた装置」だと考えており、その好例として、あのまとめが目に留まっただけなのです。 @jun0inoue

posted at 03:03:45

RT @jun0inoue: これはよく聞く話。でもじゃあ正則性公理は何のために導入されたの? wikiには位数に使うとかあるけど、理由としてはad-hocすぎ。直感的な公理でもないし。QT @Taroupho なるほど、正則性公理は、別にラッセルのパラドクスを排除するために導入されたわけではないのですね。

posted at 01:09:07

RT @kururu_goedel: @jun0inoue @Taroupho 昔書いた記事です。adhocであっても、与える制約に比べてもたらすものがはるかに多いのです。http://t.co/qBDbrNO

posted at 16:01:53