数学基礎論・数理論理学のスレッド　その7

1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その6 kamome.2ch.net/test/read.cgi/math/1265884076/ 282 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 21:38:41 ] え、じゃあnandはどこの用語なんだ 283 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 21:41:48 ] 電子工学 284 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 21:44:02 ] ググったら「NAND型フラッシュメモリ」というのが出てきた 285 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 21:44:57 ] 論理回路も知らんのか・・・ 286 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 21:48:39 ] >>283 あ、そうか。サンクス。 287 名前：１３２人目の素数さん [2011/02/13(日) 22:22:27 ] >>276 > 自分が習った体系しか無いと思うとは、おめでたいやつだ。 他にあるってこと自体は知っていた。 ただ俺はHKといった。 HKは普通、 公理１　A→B→A 公理２　(A→B→C)→(A→B)→A→C 公理３　((A→B)→A)→A 公理４　¬→A 推論規則１　A, A⊃B → B 　（MP） だろう？ 今はBCIとかBCKとかBCKW...とか言われてるのを知らのか？ 288 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 22:27:43 ] 今、論理学で若手の有力株と言えば？ 数学畑の人と哲学畑の人と両方教えて 289 名前：１３２人目の素数さん [2011/02/13(日) 22:44:54 ] 聞いたことないな。 集合論ならいるけど。 290 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 22:49:33 ] 集合論か・・・ 一応教えてください 291 名前：１３２人目の素数さん [2011/02/13(日) 22:59:25 ] >>290 ttp://twitter.com/#!/kururu_goedel 292 名前：１３２人目の素数さん mailto:sage [2011/02/13(日) 23:59:22 ] すみません、スレ違いなのは承知しているのですが質問させてください。人間のクリアランスが倍になったら薬物の半減期はどれだけになるか教えてください。 293 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 00:07:39 ] スレ違いどころか板違いだろ。 294 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 00:09:13 ] わろたｗ 295 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 00:18:58 ] すいませんが、 DIAMOND: A PARADOX LOGIC (2ND EDITION) (Series on Knots & Everything) www.amazon.co.uk/DIAMOND-PARADOX-LOGIC-Knots-Everything/dp/981428713X この本で扱ってるDiamondって様相論理の可能性演算子と、 連続体仮説の一般化の方のとどちらでしょうか？ 296 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 01:14:20 ] HKってそういう意味じゃなくてたぶんHilbert式のcalculusのことを ドイツ語の頭文字をとって一部の教科書がそう読んでるだけじゃないの？ BCKとかのBとかCとかはそれぞれ一つの公理図式の名前だけどHKはそうじゃないでしょ。 松本和夫の本とかにもHKとか名付けてあるけど当時BCK論理とかがあったはずもないし。 一般的には、ほとんどの規則を推論規則として定式化する Gentzenの自然演繹とかシーケント計算とかに対して modus ponensとか汎化規則とかしか推論規則が無くて、 あとは公理として規則を立てるような体系のことをHilbertスタイルというように思う。 というか ＞公理４　¬→A これ意味分からんのだが。論理式になってないし。 297 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 02:14:03 ] > ＞公理４　¬→A > これ意味分からんのだが。論理式になってないし。 否定ではなくて、矛盾のつもりなのでしょう。 298 名前：１３２人目の素数さん mailto:sage [2011/02/14(月) 23:24:24 ] 集合論て難しいですか？ 299 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 07:29:29 ] 公理的集合論に最低限必要な武器は、 ・素朴集合論 ・線形代数学 ・位相空間論 ・一階述語論理学 ・グラフ理論 ・群/体 ・ルベーグ積分 ・公理的な確率/統計 ・関数論 などだ。難しいと感じるかは当人のセンス次第だ。 300 名前：１３２人目の素数さん [2011/02/15(火) 09:25:54 ] >>298 「難しい」と書いて「たのしい」と読むんだぞ 301 名前：１３２人目の素数さん [2011/02/15(火) 09:27:02 ] ごめんsage入れ忘れた 302 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 09:28:30 ] 再度すまんorz 303 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 11:44:47 ] >>298 シェラハというイスラエルの爺さんの頭脳レベルを調べてみなされ。 304 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 12:09:53 ] どうやって調べるんですか？ 305 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 12:14:05 ] シェラハを貶めるつもりは毛頭ないが、 この文脈では、論文を量産できるほど簡単な分野であるかのようではないか 306 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 12:15:20 ] >>304 ja.m.wikipedia.org/wiki/サハロン・シェラハ?wasRedirected=true 307 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 17:45:24 ] 高校生のための質問スレからこちらに誘導されてきました。 「ラッセルのパラドックス」を解決した「グロタンディーク宇宙」とはどんなものなんですか？ ウィキ読んでもさっぱりわかりませんでした(笑) 308 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:02:17 ] 別にGrothendieck universeとRusselのパラドックスはほとんど関係ないけども。 どこで読んだのそれ？ 309 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:09:38 ] ウィキペディアの数学基礎論あたりにそんな変な記述があって笑った記憶があるｗｗ 310 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:11:35 ] >>307 普通のZFでもラッセルのパラドクスは構成できないよ。 311 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:24:20 ] >>299 今ではそれに付け加えて、 ・数論 ・代数的トポロジー ・モデル理論 ・チューリング/メドベージェフ還元 ・計算量複雑性・再起理論 ・不完全性定理（四則演算並みの頻度で多用） ・論理学の代数化定理周辺 までが求められる。 シェラーとかいう人は確か特異基数仮説周辺で有名な人じゃなかったっけ？ （私も全然ついていけてないです... 312 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:29:10 ] またメドベージェフ君のレスか 313 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:43:42 ] >>299 なんで集合論に確率が必要なん？ てきとうに挙げただけちゃう？ 314 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:46:32 ] >>313 カントール空間とかポーランド空間とか使うからでしょ。 メドヴェージェフ還元に＾＾ 315 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 21:57:46 ] メドヴェージェフって言いたいだけちゃう？ 316 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 22:02:03 ] チューリング次数におけるポストの定理が メドベージェフ次数のおけるプールエルクリプキの定理に該当！ 317 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 22:19:31 ] トリンドルちゃんて言いたいだけちゃう？ 318 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 23:23:44 ] ミッチェル次数もあるよ＞＜ 319 名前：１３２人目の素数さん mailto:sage [2011/02/15(火) 23:27:25 ] メドベージェフ次数とかは、どの本で勉強すればいいのでしょうか？ 320 名前：１３２人目の素数さん mailto:sage [2011/02/16(水) 07:20:38 ] 電子版では シュプリンガーから Kripke Models, Distributive Lattices, and Medvedev Degrees Sebastiaan A. Terwijn が出てる。 紙媒体は多分まだない。 321 名前：１３２人目の素数さん mailto:sage [2011/02/16(水) 10:59:40 ] >>320 ありがとうございます！ 322 名前：１３２人目の素数さん mailto:sage [2011/02/17(木) 17:43:46 ] LKのcut除去定理の証明で、証明図を変形していき、 rankとdegreeについての二重帰納法を用いるものがありますよね？ 証明図の変形によるrankとdegreeの減少を精密に評価することで、 何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、 どうも無理な気がしてきました。 実際どうなんでしょうか？ よろしければお知恵をお貸し下さい。 323 名前：１３２人目の素数さん mailto:sage [2011/02/17(木) 19:03:27 ] できます。 Girard の Proof theory and Logical comlpexity には その方法で評価がされています。 また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の 自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ ωを 3 に置き換えればよいというようなことが書いてあったと思います。 324 名前：１３２人目の素数さん mailto:sage [2011/02/17(木) 20:36:27 ] >>323 ご回答ありがとうございます。図書館で調べてみます。 ＞ωを 3 に置き換えればよい というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、 LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。 この方針で試みてみようと思います。 325 名前：１３２人目の素数さん mailto:sage [2011/02/17(木) 23:25:04 ] ＞数学的帰納法がなければωを 3 に置き換えればよい あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ？ 326 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 13:37:43 ] ペアノの公理で、 なんでx=y→x'=y'じゃなくて x'=y'→x=yなのか教えてください 327 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 13:57:58 ] 前者はあらゆる関数に成り立つべき性質(等しいものの代入法則)で自明とも言えるが、後者は違う。 328 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 15:47:05 ] >>326が自然数の公理に必要な理由を教えてください。 329 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 15:54:02 ] x+1=y+1 ならば x=y でないと困るでしょ。 演繹するか公理で仮定することになる。 330 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 15:58:30 ] x=y → x'=y' じゃだめなの？ 331 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 16:28:40 ] >>330 なにがいいの？ 332 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 16:43:54 ] >>331 ？ 333 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 16:47:14 ] A かつ ¬Aが良い 334 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 17:22:53 ] >>332 〜じゃだめなの？＝〜でいいだろ。 ということだから、いいってのはどういう意味でいいっていってんのかってこと。 335 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 19:20:42 ] 自然数の公理として機能しないのかどうかってこと 336 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 19:34:06 ] だからどう自然数の公理として機能してると主張してるのかってこと。 337 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 19:39:50 ] しらんがな そんなうまく質問できるくらいなら質問してない 初めてペアノの公理見たんだよ なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください 338 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 19:47:26 ] 君の現在の理解力を越えてるようだね。 339 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 19:48:08 ] x'=y'→x=y これは後者関数の単射であることを意味する。 ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。 0→1→2→3→1→2→3→1→2→3→… 形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。 もちろん、それ以外の場面でも。 上でも指摘されてるけど、 x=y→x'=y これ↑は単なる代入可能性を意味する、等号の公理の一部。 340 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:00:42 ] >>339 x=y → x'=y' ならば、 0→1→2→3→4 となるんじゃない？3の次は3'(=4)だけでしょ？ 341 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:06:45 ] >>340 x'=y'→x=yを仮定しないと、3' が 1 になり得るという話 342 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:12:23 ] >>340 それだけだと、 3'のまえが3じゃないとこから複数本繋がってきてもいい。 343 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:13:21 ] 感覚としては、後者関数を使って自然数を次々と生成していくわけだが、 新しく生まれる自然数が、先に生まれた自然数のいずれとも異なるように、 言い換えれば、自然数を一直線に並べるために必要な公理なんだよ もし単射でなかったら、直前の世代にあたる自然数が一通りに決まらない 例えば、1の直前が 0 と 0''' ということもあり得る。 344 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:22:27 ] x=y → x'=y' なのになぜ3の前が複数になりうるの？ 345 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:22:34 ] 今の場合反例モデルが作れるからそれで説明するけど x'=y'→x=yがなくてその逆だと Z/nZでも条件満たしちゃうでしょ。 Z/nZが何なのか分からないなら先に初等整数論を勉強してね。 346 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:51:38 ] ごめんボケてた>>345はx'≠0が必要だって話だｗ やっぱり皆の言うようにやらないとダメだ ただどっちも似たような話で、 0'=1，1'=2，2'=3，……，〜'=n、n'=1みたいな状況が生じちゃうってこと 347 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:57:05 ] >>344 x≠yのときについては何の制約も掛けて無いから。 348 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:58:58 ] >>344 a=b だからって、a と b が「記号列として同じ」であるとは限らない 等号の公理：反射律および代入可能性を満たす限りにおいて、a と b が異なる記号列であってもよい だから、1の直前が 0 と 0''' である、つまり論理式 0=0''' が証明可能、という状況もある（かもしれない） 349 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 20:59:18 ] >>344 まず「単射」という概念を理解した方がいい。 ググればいくらでも出てくるだろう。予備知識は必要ない。 それでも分からなかったらここで聞いても無駄。 350 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:03:00 ] >>344 その条件は3の後はかならず3'にしかいかないということを言ってるだけで 3'の前がかならず3になってるとは言ってないからだよ。 後者の条件はお前がどうしても外したがってるx'=y'→x=yのほう。 351 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:24:25 ] 久しぶりにスレが伸びていると思ったら またこの流れか。 352 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:28:40 ] 竹内・八杉の『証明論入門』 芯の通った思想を感じる本だね。楽しくなってくる。 353 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:53:00 ] 和書しか読まないから 竹内の本がありがたく感じる。 もちろん良い本だけど。 354 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:54:39 ] 何か他の条件から後続関数の単射性が言えれば仮定しなくても良い。 どのみち、分からん君が置き換えたがってる等号公理からは出ないが。 355 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 21:57:11 ] >>350 それだったら同じ理屈で、x'=y'→x=y だと 1の次が2だったり3だったりしてしまうのでは？ 356 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 22:04:20 ] >>355 ∀x x'≠0という公理があるから特に0≠0'=1。 ところが1'=1'' だとすると1'=(1')'→1=1'だから1=1'、 つまり0'=(0')'となって同様にして0=0'となって矛盾する。 357 名前：１３２人目の素数さん mailto:sage [2011/02/18(金) 22:14:38 ] >>356 まじで？ 358 名前：１３２人目の素数さん mailto:sage [2011/02/19(土) 05:24:22 ] x≠y → x'≠y' 359 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 00:33:29.67 ] 基本的なこと分からない人は、 島内さんの「数学の基礎」をよめばどうかな。 基礎論の初歩的なところを手取り足取り進めてくれるから。 中学生でも理解できるような歩みで。 360 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 01:00:24.59 ] あれε記号使ってたような 361 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 07:25:58.31 ] shenfieldのmathematical logic1冊で充分だろ。 362 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 08:21:03.83 ] >>326にShoenfield薦めるとか頭おかしいとしか思えん。 p→qとその逆のq→pを混同してるかもしれないレベルなのに。 363 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 17:07:35.54 ] >>360 いや、それどころか自然数の公理系まで入ってるけど。 364 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 17:19:04.08 ] >>359 その本の目的がいまいちぴんと来ない。 読みてはどんな人がターゲット？ 365 名前：１３２人目の素数さん mailto:sage [2011/02/21(月) 23:51:21.86 ] 広く浅く学びたい趣味人だろう。 366 名前：１３２人目の素数さん mailto:sage [2011/02/22(火) 17:07:57.67 ] >>364 >>326に勧めてるじゃんw 367 名前：１３２人目の素数さん mailto:sage [2011/02/22(火) 23:35:42.32 ] 有限の立場では、背理法の無制限な使用は認められますか？ 368 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 08:02:56.58 ] 有限の立場ってのは有限公理化可能ってことだとするなら、 ZFCやMKは有限でないが、NGBは有限。 排中律を公理にするかは１階述語論理での話で、 むしろ背理法なしで無矛盾な集合論を展開できるかということ。 答えはYes。 369 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 08:14:46.30 ] こりゃまた斬新な答えだ 370 名前：１３２人目の素数さん [2011/02/23(水) 10:13:34.91 ] 有限の立場は人の数だけあるとは言うが… 371 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 12:09:40.31 ] 少ない脳味噌を如何に活用するかってことなんですね。 372 名前：368 mailto:sage [2011/02/23(水) 19:56:25.65 ] >>369>>371 文句があるなら論破してみろ。 373 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 20:04:38.06 ] どこから手をつけろと言うんだｗ 374 名前：368 mailto:sage [2011/02/23(水) 20:22:42.56 ] >>373 言い訳乙＾＾ 375 名前：368 mailto:sage [2011/02/23(水) 21:10:09.87 ] 全員まとめてかかってこい！ ジャクソンとショーアのlow basic theoremより recursive degreeを下げることで不完全性定理は成り立たないようにできる！ 376 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 21:15:08.73 ] basicってことはadvancedとかもあるの？ 377 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 21:27:56.54 ] 結局、有限の立場で背理法はOKなの？ 378 名前：368 mailto:sage [2011/02/23(水) 22:13:03.52 ] >>376 basicってのは日本語では恐らく基底とか基数に該当するので基本とかではないです。 379 名前：368 mailto:sage [2011/02/23(水) 22:19:23.25 ] >>377 有限の立場の立場を明確にせよ 380 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 22:21:36.12 ] Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. 381 名前：368 mailto:sage [2011/02/23(水) 22:59:50.96 ] >>377 述語の数を増やせばできます。 382 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 23:43:01.36 ] >>378 いやlow basis theoremのはずなのにスペル間違ってたから きっと内容分かってないんだろなと思ってからかっただけだよ というかジャクソンってもしかしてJockuschのことじゃないだろうな？

---

---

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

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