数学基礎論・数理論理学　その11

1 名前：１３２人目の素数さん mailto:sage [2012/01/02(月) 23:04:29.50 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その10 uni.2ch.net/test/read.cgi/math/1319895756/ 321 名前：１３２人目の素数さん mailto:sage [2012/01/17(火) 06:40:24.56 ] つまり、0-sharp cardinal は cardinal でないこともあるってことだね。 322 名前：１３２人目の素数さん mailto:sage [2012/01/17(火) 17:16:10.88 ] 312の定義に意味を持たせるには if“V ⊨ κ is a φ-cardinal”then“κ is in L” であればいいので、“κ is cardinal”である必要はないのね。 323 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 01:46:48.73 ] >>321, >>322 普通に>>320は、最初に「For a cardinalκ, 」を補えばいいだろうが！ 324 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 04:32:03.92 ] 基礎論最大の未解決問題ってなんなのでしょうか？ 325 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 05:51:34.40 ] >>323 では 0-sharp cardinal の存在と（通常の意味の）0-sharp の存在は同値？ 326 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 08:50:07.59 ] >>324 間違いなく「P対NP問題」でしょう。 基礎論の各分野での最大の未解決問題となると、分かりませんが。 327 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 17:46:55.71 ] >>325 Silver indiscernible は順序さえ保てば自由に動かせて 非可算基数はすべて Silver indiscernible なのだから、 critical point を特定の非可算基数になるような L から L への elementary embedding なんて (0^\sharp の存在から)簡単に作れる。 328 名前：１３２人目の素数さん [2012/01/18(水) 18:30:36.14 ] 自動定理証明系で 証明仮定（証明図）がすべて出力できるソフトウェアはありますか？ 329 名前：１３２人目の素数さん [2012/01/18(水) 19:17:07.58 ] >>328 自分で作れば良い。全ての図を少しずつ列挙し、 同時に一方ではそれらが証明図になって居るかどうか少しずつ判定すれば良い。 330 名前：１３２人目の素数さん [2012/01/18(水) 19:39:04.24 ] >>329 それって普通の対話型証明ソフトと変わらないですよね？ 私は公理からの論理式のシーケント列を見たいのです。 331 名前：１３２人目の素数さん mailto:sage [2012/01/18(水) 23:53:47.48 ] 　３２８の件　スルー　お願いします 332 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 01:45:57.11 ] >>327の言う通りなので、 κ is a real-sharp cardinal if for any a⊂ω, there is a non-trivial elementary embedding j: L[a] → L[a] whose critical point is κ と定義すれば、“∀a⊂ω(a-sharp exists)”も real-sharp cardinal の存在と同値になって>>312の定義が適用できる！ dagger についても同様。 333 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 03:32:01.91 ] >>326 > >>324 > 間違いなく「P対NP問題」でしょう。 P≠NP?問題は計算機科学の問題で基礎論の問題じゃないだろが。 そいつを基礎論の問題なんて言ったら「問題を横取りするな」って計算機屋が怒るぞ。 そもそも数学の基礎付けとは全く無関係な問題だ。 そのうち、代数屋あたりが解きそうだな。 結局、ロジシャン自慢のBounded Arithmeticでは歯が立たなかったし。 334 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 04:12:12.63 ] また「基礎論＝数学の基礎付け」とか言う香具師がでてきなすった。 隔離スレが過疎っちまって構って欲しいのか？ 335 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 06:15:01.51 ] >>312の定義を適用するために、 通常では何らかの性質を持つ基数の存在として記述されない巨大基数公理を そういう形に書き換えてたいようだけど、 そもそも>>312の定義がおかしくないかい？ “is consistent”というメタレベルの言明を挟んでいるのだから、 “V ⊨ κ is a φ-cardinal”と“L ⊨ κ is a φ-cardinal”で出てくる 二つのκが同じもの、というのが意味をなさないよ。正しくは if “V ⊨ ∃κ(κ is a φ-cardinal)”then“L ⊨ ∃κ(κ is a φ-cardinal)” ではないかな？ 336 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 06:18:15.00 ] 間違えた、正しくは if “V ⊨ ∃κ(κ is a φ-cardinal)” is consistent, then so is “L ⊨ ∃κ(κ is a φ-cardinal)” ではないかと。 337 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 08:04:14.89 ] 大学入ったら基礎論やりたいんですがまず何を勉強したらいいですか？ 細かい分野としては逆数学とか証明論などに興味があります、よろしくお願いします 338 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 08:37:31.42 ] >>337 まず君がいまどのレベルなのか教えてくれないと、アドバイスしようがないだろ。 339 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 08:59:26.46 ] >>333 Bounded Arithmetic で歯が立っていないのは事実だが、 かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。 そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、 常に他分野の技術によって解決される可能性は開けている。 よって、未解決問題がどの分野に属しているかは、 その問題自体がどの分野の言葉で記述されているかで決めるべき。 ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある 理論計算機科学の問題。 340 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 09:42:40.42 ] 巨大基数スレが二つも乱立しているというのに、 巨大基数ネタで一番盛り上がっているのは結局このスレというのは、 なぜなのだろう？ 341 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 13:34:20.78 ] 結局みんなアスペが嫌いなのよ。 巨大基数スレは、アスペが独立スレ立てろと言い出したから、 なんとなくみんなそっちに書きたがらないｗ 342 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 16:51:42.44 ] >>339 チンコに歯立てるなよ 343 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 19:44:37.71 ] 一般向けの本で、高校レベルの知識で理解可能と書いてあるのに、 実際読んだら？の嵐だったよ。 いきなり「標準形」って出てきてどんどん展開していく。 そこに「標準形」の説明はない。俺には理解できなかった。 やさしい入門書あったら、教えてね。 344 名前：１３２人目の素数さん mailto:sage [2012/01/19(木) 21:30:53.85 ] 入門書で金をどぶにすてることから「がくもん」がはじまるのかな 自分で失敗したほうが身につくと思われます　んちって 345 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 04:23:36.09 ] >>343 齋藤正彦 数学の基礎―集合・数・位相 (基礎数学) で肩慣らししてみたら？（基礎論やらなくても必要な部分） 346 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 04:41:38.68 ] >>341 アスペだけじゃなく、スレ立てた主も、 教えてもらおうって相手を見下してる偉そうな香具師だったからな。 あっちのスレでアホ丸出しのタワゴトをのたまっているが、 誰も好き好んであのスレ主の相手したいとは思わんだろ。 347 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 07:32:42.59 ] >>333>>339 ゲーデルがテューリングがでてきたころ、そのような問題がふれている ということが書いてあるのを読んだことがある。だから、古い問題では あるのだけれど、計算機科学ができてから特に大きな問題になったと いうことだろう。 348 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 12:43:08.27 ] >>339 > >>333 > Bounded Arithmetic で歯が立っていないのは事実だが、 > かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。 > そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、 > 常に他分野の技術によって解決される可能性は開けている。 > > よって、未解決問題がどの分野に属しているかは、 > その問題自体がどの分野の言葉で記述されているかで決めるべき。 P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。 計算機科学が数理論理学と関係なく生み出して来た言葉で書けるぞ。 Boolean Circuitなんて考え方は基礎論とは全く独立な発想だからな。Razvorovも代数屋だし。 > ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある > 理論計算機科学の問題。 理論計算機科学が数理論理学の一分野という認識はお前みたいな基礎論屋の勘違い。 夜郎自大の基礎論屋らしい勘違いというか誇大妄想ではある。 理論計算機科学にはむしろ代数の辺境分野とでも呼ぶべき言語理論なども重要なコアパートとして含まれるし 普遍代数や圏論の応用分野でもあるのだから、理論計算機科学は数理論理学の一分野なんかじゃない。 むしろロクな問題もなくロクにポストもなかった基礎論屋が「計算機がらみなら問題も色々あるしメシも食えそう」って 理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。 基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とかが 計算機言語の型システムの高度化にも使えるという計算機屋の仕事が計算機科学側で流行り出してから、 慌てて基礎論屋が飛び付いてつまみ食いして計算機科学的には何の使い物にもならない瑣末な視点の論文を基礎論屋が粗製乱造して来たのが実態じゃないか。 型理論の論文は基礎論屋が乱入して来てからロクなのが出ていない。ずっと昔からやっていたMartin-L\"ofとかには当然ながら俺も敬意を表するが。 349 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 15:04:28.57 ] >P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。 >計算機科学が数理論理学と関係なく生み出して来た言葉で書ける 頑張れば書けるよね、それがどうした？ 代数の問題だって頑張って幾何の言葉や解析の言葉で書きなおせる場合が多い。 だからその問題が幾何や解析の問題だと言い出せばのはこじつけ。 >理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。 >基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とか 君の「俺様歴史観」によるとそういうことになるわけね。 あほらしくてわざわざ反論する気もしないな。 350 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 15:50:37.80 ] >>335-336 κを定数記号だと理解すれば、>>312はそのままで>>336の意味になると思うがの 351 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 18:43:54.93 ] >>346 >あっちのスレでアホ丸出しのタワゴトをのたまっている いや全く。 巨大基数（的）性質なのに、名前付けるのに「存在すれば」という仮定つけてる、 なんてのは巨大基数のなんたるかがまるっきり分かっていない証拠。 巨大基数に手を出す前にもっと勉強すべきことがあるだろう、って話。 352 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 19:00:06.15 ] >>345 ポチらせていただきました。どうもです。 353 名前：１３２人目の素数さん mailto:sage [2012/01/20(金) 19:20:12.86 ] >>350, >>336 俺は>>312の記述が間違っていて、 ZF(C) |- (∀κ:cardinal)[κ is a φ-cardinal → L ⊨ (κ is a φ-cardinal)] が small large cardinal の定義だと思っていた。 これだと０♯とか、そのままでは適用できなくなるでしょ？ 354 名前：１３２人目の素数さん mailto:sage [2012/01/21(土) 05:23:41.09 ] 結局、small large cardinal とか large large cardinal とかってなんなの？どの定義が正しいワケ？ 355 名前：１３２人目の素数さん mailto:age [2012/01/21(土) 07:05:59.08 ] スレタイスレ446氏はその後出てこないの？ また新たなネタをもたらしてくれることを期待しているんだが。 356 名前：１３２人目の素数さん mailto:sage [2012/01/21(土) 08:16:43.86 ] 自演乙 357 名前：１３２人目の素数さん [2012/01/22(日) 14:15:58.07 ] BBQ が止まっています BBX が止まっています ほんとに？ 358 名前：１３２人目の素数さん mailto:sage [2012/01/22(日) 23:14:40.29 ] >>353 実際にいままでに提案された巨大基数公理については、どっちの定義でも同じこと。 確かにゼロシャープとかの場合は、ちょっと定義をいじらないといけないけどね。 359 名前：１３２人目の素数さん mailto:age [2012/01/25(水) 01:20:09.09 ] スレタイスレ446氏まだー？ 360 名前：１３２人目の素数さん mailto:sage [2012/01/25(水) 06:40:43.46 ] 数学基礎論は、哲学的問題に数学を持ち込んだという意味で「数理哲学」と呼ぶべきものだと思う。 「数学に関する哲学」という意味での「数理哲学」は、一般的な「数理○○学」の用法から逸脱していて適切ではない。 361 名前：１３２人目の素数さん [2012/01/25(水) 12:10:51.99 ] 生命とか国家について考えてるわけじゃないから哲学とまではいかないだろう。 論理学のうち数理的にやれる部分を数理論理学と呼び、研究の発展とともに「数理的」の内容が変わっていく、って感じじゃないの？ 362 名前：１３２人目の素数さん [2012/01/25(水) 13:53:11.26 ] はっきり言って哲学とは関係ない。 皆、やりたいことをやっているだけ。 363 名前：１３２人目の素数さん [2012/01/25(水) 13:55:59.49 ] 世界 50 億人誰にでも分かる表現が可能なのが数学。 そうで無いのが哲学。 364 名前：１３２人目の素数さん [2012/01/25(水) 14:27:17.77 ] >>363 それはハッタリ的アフォリズムでしかない 365 名前：１３２人目の素数さん mailto:sage [2012/01/25(水) 15:00:35.87 ] 阿保リズム 366 名前：１３２人目の素数さん mailto:sage [2012/01/25(水) 15:08:25.72 ] >>361,363 現代哲学には大陸哲学と分析哲学があります。 生命や国家について語り人類に共通な真理とは限らないのは大陸哲学です。 擬似問題を切り捨て明晰さを重視し自然科学と親和性が高いのが分析哲学です。 数学の哲学は分析哲学の一分野です。 大陸哲学 ja.wikipedia.org/wiki/%E5%A4%A7%E9%99%B8%E5%93%B2%E5%AD%A6 分析哲学 ja.wikipedia.org/wiki/%E5%88%86%E6%9E%90%E5%93%B2%E5%AD%A6 数学の哲学 ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E3%81%AE%E5%93%B2%E5%AD%A6 367 名前：１３２人目の素数さん [2012/01/25(水) 15:23:12.95 ] >>366 ならなんでやたらドイツ語の基礎文献が多いんだ？ 368 名前：367 mailto:sage [2012/01/25(水) 15:37:44.69 ] ごめん、ちゃんと読んでなかった。 撤回する。 369 名前：１３２人目の素数さん mailto:sage [2012/01/25(水) 19:50:41.64 ] 哲学なら現代と限定するのはそもそもおかしくね 370 名前：１３２人目の素数さん mailto:sage [2012/01/25(水) 21:10:33.17 ] そのへんは、数学を現代数学と限定するのが本来おかしいのと一緒でしょ 最近有名になったサンデルとかの政治哲学とかも分析哲学よりだし 国家や生命についての問題は疑似問題に過ぎないというと語弊があるけどね 371 名前：１３２人目の素数さん mailto:sage [2012/01/26(木) 01:16:15.74 ] >>361 そうやって数学の扱える範囲を拡げたのが基礎論の大きな功績の一つ。 >>363 仮に「哲学」と「数学」の違いをそう定義するのなら、 基礎論以前には「哲学」でしか扱えなかったものが 基礎論によって「数学」として扱えるようになった、ということ。 372 名前：１３２人目の素数さん [2012/01/26(木) 07:54:25.48 ] -P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment). P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB). から P(e(x,x)) # label(Reflexivity). を証明。 ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 3.04 (+ 0.20) seconds: Reflexivity. % Length of proof is 19. % Level of proof is 8. % Maximum clause weight is 48. % Given clauses 588. 1 P(e(x,x)) # label(Reflexivity) # label(non_clause) # label(goal). [goal]. 2 -P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment). [assumption]. 3 P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB). [assumption]. 4 -P(e(c1,c1)) # label(Reflexivity) # answer(Reflexivity). [deny(1)]. 5A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)]. 5 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w)). [resolve(5A,a,3,a)]. 6A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)]. 6 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5)),v6)). [resolve(6A,a,5,a)]. 7A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u))) | P(w). [resolve(2,a,5,a)]. 7 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w))). [resolve(7A,a,3,a)]. 9A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5))) | P(v6). [resolve(2,a,6,a)]. 9 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6),e(v5,v6))). [resolve(9A,a,3,a)]. 10A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)]. 10 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x))). [resolve(10A,a,7,a)]. 373 名前：１３２人目の素数さん [2012/01/26(木) 07:55:12.82 ] 11A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)]. 11 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5)),v6)). [resolve(11A,a,7,a)]. 14A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)]. 14 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5))). [resolve(14A,a,3,a)]. 28A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x)). [resolve(2,a,10,a)]. 28 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),e(e(e(e(v5,e(e(e(v5,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)))). [resolve(28A,a,7,a)]. 35A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5))) | P(v6). [resolve(2,a,11,a)]. 35 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),v6),e(v5,v6))). [resolve(35A,a,3,a)]. 57A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)]. 57 P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6)),v7)). [resolve(57A,a,14,a)]. 374 名前：１３２人目の素数さん [2012/01/26(木) 07:56:01.55 ] 141A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)). [resolve(2,a,14,a)]. 141 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),v6),v7),e(v6,v7)),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). [resolve(141A,a,35,a)]. 262A -P(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6))) | P(v7). [resolve(2,a,57,a)]. 262 P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10)),e(v9,v10))). [resolve(262A,a,28,a)]. 589A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6)) | P(e(v5,v6)). [resolve(2,a,9,a)]. 589 P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),v5),e(w,v5)),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). [resolve(589A,a,141,a)]. 1754A -P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10))) | P(e(v9,v10)). [resolve(2,a,262,a)]. 1754 P(e(x,x)). [resolve(1754A,a,589,a)]. 1755 $F # answer(Reflexivity). [resolve(1754,a,4,a)]. ============================== end of proof ========================== 1階論理の証明は省略してもここまでの分量になる。 375 名前：１３２人目の素数さん mailto:sage [2012/01/26(木) 20:46:23.39 ] できたら正誤表もヨロ ・・・ともかくGJ・・・感謝 376 名前：１３２人目の素数さん mailto:sage [2012/01/27(金) 05:17:56.94 ] 巨大基数の数理哲学的な説明ってどうなってるの？ 377 名前：１３２人目の素数さん [2012/01/27(金) 17:09:37.81 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 378 名前：１３２人目の素数さん mailto:sage [2012/01/27(金) 17:11:12.67 ] 誰もお前みたいなブスとは付き合いたくねえ。 379 名前：１３２人目の素数さん [2012/01/27(金) 18:49:12.14 ] >>375 何に感謝したの？？ 380 名前：１３２人目の素数さん [2012/01/27(金) 20:32:41.33 ] ざっくり言って、第二不完全性定理は、もちろん第一不完全性定理の系で、 第一不完全性定理は不動点定理の単なる系なのだが、その不動点定理も、さらに なにかメタな洞察があって、そこからみれば自明な定理である、なんていう話は 聞いたことあるかな？ 381 名前：１３２人目の素数さん [2012/01/27(金) 20:50:55.45 ] 証明の仕方によっては 系になり得るけど 第二は第一と無関係に証明できるし 第一も不動点定理と無関係に証明できるからなぁー 382 名前：１３２人目の素数さん [2012/01/27(金) 22:09:35.94 ] >>381 たしかにそりゃそうなので前段は余計なことを言ったかもしれん。 ただ、オリジナル（ゲーデル）では380で書いた順番だったから それが一番自然な順序と言えなくもないだろう？ まあそれはよいとして、後段の、不動点定理が成り立つのはそりゃ当然だ、 と見えるようなメタな定理ってあるんかな？しつこくてすまんが。 383 名前：１３２人目の素数さん [2012/01/27(金) 23:06:23.03 ] 対角線論法や自己参照のイメージで良い。 似たような論法は計算論全般でよく出てくる。 384 名前：１３２人目の素数さん [2012/01/27(金) 23:48:39.49 ] >>383 それは分かるのだが、たとえば、ブラウワの不動点定理とラムダ計算における不動点定理に 共通する成立条件は何なのだろうか？あるいはこうした不動点定理を最も抽象化した定理って どんな形をしているんだろうか？という疑問なのだが。おかしいか？ 385 名前：１３２人目の素数さん [2012/01/27(金) 23:59:52.04 ] λ計算は数学の関数の性質をすべて抜き出せるからなぁ。 共通する性質はある程度の算術が作れるってところか。 386 名前：１３２人目の素数さん [2012/01/28(土) 00:12:55.57 ] >>384 >>385 圏論ではそういう抽象化をやってないか？ 387 名前：１３２人目の素数さん mailto:sage [2012/01/28(土) 00:18:05.71 ] やってます。 過去スレでも話題になってます。 388 名前：１３２人目の素数さん [2012/01/28(土) 00:28:57.03 ] >>387 スマン。どのあたり？ 389 名前：１３２人目の素数さん [2012/01/28(土) 09:43:01.73 ] 圏論好き集まれスレで話題になってるよ。 390 名前：１３２人目の素数さん mailto:sage [2012/01/28(土) 10:13:27.53 ] >379 萌え材につかいましたが・・・やはり問題あり? 391 名前：１３２人目の素数さん [2012/01/28(土) 11:13:10.57 ] >>386 >>387 >>389 Lawvereの定理のことを言ってるんだとしたら、あれはゲーデルや通常の不動点定理を それほど抽象化したものにはみえない。記法を換えただけにみえるのだが。 392 名前：１３２人目の素数さん [2012/01/28(土) 15:47:01.46 ] おほほ猫 393 名前：猫釣りは餌が重要 ◆MuKUnGPXAY mailto:age [2012/01/28(土) 17:39:40.18 ] ケケケ猫 394 名前：389 [2012/01/28(土) 18:44:03.24 ] >>391 同感。 結局は対角線論法が根源的な説明に思える。 395 名前：１３２人目の素数さん [2012/01/28(土) 18:45:33.95 ] >>393 あんた全てのスレッドを監視しとんのか？ あんたとは無縁じゃろう、この話題は。 396 名前：猫釣りは餌が重要 ◆MuKUnGPXAY mailto:age [2012/01/28(土) 18:58:07.71 ] >>395 何処を監視するのかは私の勝手なのでね。 猫 397 名前：１３２人目の素数さん [2012/01/28(土) 22:28:45.86 ] こんばんは。初めて書き込むのですが、論理学の質問をしたいと思って ネット上を探していたらここにたどりつきました。ご助力願います。 質問　Ｌｐの論理式でないのはどれか。 (1)∀w∀x∃zＲ(x,z) (2)∀xＰx⊃∀xＲ(x,c) (3)∀xＰx⊃∀cＲ(x,c) (4)∀z∀x(∀xＰx⊃∀zＲ(zz)) です。出題の意図がわかりかねまして質問しました。 どうぞよろしくお願いします。 398 名前：１３２人目の素数さん mailto:sage [2012/01/28(土) 22:41:40.23 ] 「Ｌｐの論理式」という表現は、貴方の持っている本特有の言葉遣いだと思われます。意味がわかりません。 399 名前：１３２人目の素数さん [2012/01/28(土) 22:47:25.20 ] すみません。 どうやらLpというのは「初等論理の言語」を表しているようで、 ⊃、¬、∧、∨、∀、∃を表すようです。 400 名前：１３２人目の素数さん [2012/01/28(土) 23:00:42.69 ] >>397 本？それとも講義？ 本なら書名を教えてくれない？ 401 名前：１３２人目の素数さん [2012/01/28(土) 23:12:03.45 ] 講義です。 その先生が独特に使うのでしょうか…。 もう途中から何言ってるのか、って感じで困ってたんです。 最後に課題を出されまして…。 専門ではなく教養なので、おそらくそこまで難しいことは言ってないとは 思うですが…。 402 名前：１３２人目の素数さん [2012/01/28(土) 23:21:09.89 ] >>397 素直に考えると 4番が量化記号がダブって束縛しているのでおかしいけど、 論理式の定義によるからなぁ 403 名前：１３２人目の素数さん [2012/01/28(土) 23:32:22.22 ] 397です。レスありがとうございます。 もうすこし追記します。その先生によると Lpの論理式（Ｆ）とは、次の(1)〜(4)を繰り返し適用して構成される 有限の記号列のことである。 (1)各atomic formula　αはＦである。 (2)αはすでにＦであるとわかっている⇒（¬α）もＦである。 (3)α,β∈Ｆ⇒(α⊃β）,(α∧β）,（α∨β）∈Ｆ (4)α∈Ｆ⇒（∀xα）∈Ｆ というのが定義のようです。 素人にゆっくり教えてやろうという講義ではなく、先生の独り言的な講義 だったため、素人のこちらは全くわかりませんでした…。 404 名前：１３２人目の素数さん [2012/01/28(土) 23:39:56.36 ] >>403 わきからごめん。 >もう途中から何言ってるのか こういう状態でこの宿題だけやっても、という気はするが、参考までにコメントするよ。 ｢Ｌｐの論理式である｣というのは、直感的には，｢文法に合った式である｣という意味だよね。 ここに貴方が書いた定義に照らすとすれば、(1)-(4)はどれも文法に合っていると思う。 しかし、ふつうの定義では，(1)(2)は（かろうじて）文法に合っているが、(3)(4)は文法に 合っていない（Lpの論理式でない）と思われる。というのは、，(3)は定数cが限量変数に 使われているし、(4)は（402も言うように）zとxが限量変数としてダブって使われている から。どうかな？ 405 名前：１３２人目の素数さん [2012/01/28(土) 23:44:17.61 ] >>403 その定義だと1が論理式じゃないね。 ∃記号が¬∀¬と交換できないなら。 406 名前：１３２人目の素数さん [2012/01/28(土) 23:53:13.97 ] 皆さん、ありがとうございます。 404さんもおっしゃる通り、この状態では…ということはわかっていますが、 どうしてもこの単位が必要という現状です。 頼りにするのがこの板だけというまわりもあてにならない状況で申し訳あり ませんが、お付き合いいただけると幸いです。 先ほどの質問につきましては、いただいたアドバイスを元に選びます。 もうひとつだけお願いします。 質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。 という質問です。 「代入」というテーマで授業した内容からだと思いますが、もう途中から 何言ってるのかわかりませんでした…。 すみませんが、よろしくお願いいたします。 407 名前：１３２人目の素数さん [2012/01/29(日) 00:00:41.31 ] >>406 とりあえず言えることは、 >>397のような問題は通常、 「論理式の定義から作れるものはどれか？」ということが問うているので、 >>403のような定義から作れるか試してみろってことです。 ＞質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。 NOです。 束縛された変数には代入できないです。 ※直感的理解 ∃yP(y,a)：yは束縛されている、aは束縛されていない。 408 名前：１３２人目の素数さん [2012/01/29(日) 00:18:37.92 ] 407さん、ありがとうございます。 ちょっとわかったような気がします。 とすると、 ∀xＰx⊃∀yＲ(x,y)において、freeに現れているxにzを 代入した論理式を書きなさい。 という問いに対しては、∀xＰx⊃∀yＲ(z,y) と答えればよろしいのでしょうか。 もはやこんな感じ、という理解しかできませんが…。 409 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 00:58:59.64 ] >>397 通常の形成規則にしたがえば、論理式(wff)である記号列は(2)だけで、(1),(3),(4)はwffsではない。 410 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 05:19:36.48 ] うぇるふぉーむどふぉーみゅら 411 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 07:11:11.50 ] 圏論による数学の基礎について語ろう！ 412 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 08:33:10.32 ] 上のほうで圏論と集合論（巨大基数）の関係が話題になってたけど、 圏論を他の代数構造同様に（クラスサイズっていう違いはあるが）集合論の中で実現して っていう話だから数学の基礎としての圏論というのとはなんか違うな。 413 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 10:23:59.82 ] >403だけ？∀に関する他のルールは無いの？ 普通に考えれば∀zが入れ子になっている(4)が怪しいけど、 仲間外れというなら束縛したwの出て来ない(1)も怪しい。 414 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 10:38:06.58 ] 量化記号がダブるとか、∀zが入れ子になるとか、束縛したwが出て来ないとか そんな理由で論理式にしないなんてことよくするの？ 415 名前：１３２人目の素数さん [2012/01/29(日) 11:04:29.57 ] >>414 とにかくあれは問題のための問題（悪問）と思う。 実際に使うために論理式を書く場合は、変数はダブらないように書くし、 中に出てこない変数を束縛するなんてこともしないだろ。 416 名前：１３２人目の素数さん [2012/01/29(日) 11:08:55.44 ] そうだな。あんなことをやってるから教養は要らないってことになる。あれは文系かな？どうせ論理を教えるならもっと違うやりかたがあるがな。 417 名前：１３２人目の素数さん [2012/01/29(日) 12:44:33.77 ] 圏論上の形式的議論を圏論だけでできるんですか？ 述語論理は当然のように使っているようにみえるんですが、これでは圏論は自立していないと いうことにはならないのですか？ 418 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 13:06:57.12 ] 集合論だって述語論理は使っている。 述語論理の上のレベル（というか非論理的公理）として、 集合論などのほかの「数学の基礎」から自立できているかが問題。 述語論理から独立させようなんて誰も考えてないよ。 419 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 14:55:33.43 ] そうだけど、集合論におけるメタ数学的議論は集合論で形式的に扱う事が出来るけど 圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難があるし、 その全ての側面を扱うのは難しいと思う 420 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 15:19:53.03 ] >圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難がある 慣れの問題でしかない、という説もある。そしてその説には一理ある。 421 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 16:12:47.01 ] 前にちらっと話題に出てきた STS (Structural Theory of Sets) は、 述語論理から独立させて、様相命題論理で集合論を記述しようという話。 つまり比喩的に左側が機械語側、右側がユーザー側として階層をまとめると、 >>412が圏論と巨大基数の話に関して言ったこと： 一階述語論理　−　集合論　−　各数学（圏論もこの一つ） 数学の基礎として圏論 一階述語論理　−　圏論　　−　各数学 STSの目指すもの 様相命題論理　ー　集合論　−　各数学

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef