数学基礎論・数理論理学のスレッド　その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/ 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のことじゃないだろうな？ 383 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 23:52:38.94 ] >>367 ヒルベルト達の言う有限の立場で示せる命題と言うのは、 或る特定の自然数に対する命題（Δ0式）とか、 或いは変数 x を使って x に対して成り立つ命題を証明することで 「任意の x に対して〜〜」を示す、とか、つまりかなり直截的に証明できるものなので、 ∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、 そういう凝った証明は出て来ないんじゃないかと思います。 従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、 背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。 だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。 384 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:02:15.70 ] 訂正 ∀x P(x)を仮定して背理法によって∃x ¬P(x)を示すとか 385 名前：368 mailto:sage [2011/02/24(木) 00:14:58.16 ] >>384 ∃x ¬P(x)は∀x P(x)の略記じゃないんですか？ 386 名前：368 mailto:sage [2011/02/24(木) 00:21:42.85 ] >>382 ああそうだよ、内容なんてわかってないよ。 俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、 最近shoenfieldを読み始めたばかりだよ。 low basis theorem　についてはある人のブログで知ったんだよ、問題あるか？ 387 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:26:29.37 ] 議論・喧嘩してるわけでもないのに、なんで名前固定してんのこの人 388 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:26:46.53 ] 仮に∀x P(x)を仮定して〜〜みたいな議論がそもそも無いので ¬∀x〜〜という論理式がそもそも出て来ない。 だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。 あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。 389 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:28:01.31 ] くあんてぃふぁいあふりー 390 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 16:44:00.27 ] 素人でこの方面興味持つ奴は概ね基地外 391 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 20:11:19.86 ] >>387 話の展開をわかりやすくするためだろ。 392 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 20:28:22.40 ] というかロジックの場合、他分野では優秀な数学者が 往々にしてトンデモだったりするから困る 393 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 21:04:17.78 ] >>392 www 本当杉て困る。 394 名前：368 mailto:sage [2011/02/24(木) 22:45:14.87 ] まともに勉強していないからに決まっている。 395 名前：368 mailto:sage [2011/02/24(木) 23:12:50.35 ] 集合論研究者でさえ 論理学をやったことない人がいる。 396 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 12:41:58.62 ] いまどき素朴集合論のみで食ってる研究者なぞおらんわ 寝言は寝てから言え 397 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 12:44:27.44 ] いや、普通の数学の専門家は可算濃度と連続濃度の算法しか分からんのが結構いる。 398 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 13:40:21.63 ] >>397の「いや」へ >>395-396の流れを読め。 399 名前：368 mailto:sage [2011/02/25(金) 19:53:26.53 ] >>396 公理的集合論やモデル理論の研究者で ロジックをやったことがないといのは 結構あるぞ。 400 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 20:18:53.14 ] いやモデル理論はロジックの一部だし。 あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。 非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。 401 名前：368 mailto:sage [2011/02/25(金) 22:19:27.88 ] 知識あれば良いけど、 キューネンとかウッディンとかの本読んでるけど、 論理学のテキストまったく読んだことない人間でも 読めると思うけど？ 実際に自分が読めてる。 論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。 実際に直感的に明らかな論理学の結果しか使わないし。 何だかんだで代数、位相、測度、基数の方がメインな道具に見える。 402 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 23:35:13.21 ] Woodinって何読んでんの 403 名前：368 mailto:sage [2011/02/25(金) 23:57:02.29 ] The Axiom of determinacy, forcing axiom, and the non-stationary ideal 404 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 01:20:35.00 ] >>399 > 公理的集合論(略)の研究者で 実際に何やってる人? 組合せ論的な構成可能集合の研究とか? 405 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:35:27.99 ] 基礎論を勉強し始めたど素人ですが、どなたか教えてください。 前原「数学基礎論入門」で、「等号の基本性質」の節の冒頭にある、 次の記述意味が分かりません。 >sとtがn階の対象式である場合には、s=tは、 >∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) >という論理式の略記法であった。 ここで、_{n+1}により下付き文字をあらわしました。 この定義ですと、t∈ξ_{n+1}でかつ、¬(s∈ξ_{n+1})となるξ_{n+1}が 存在した場合でも、論理式s=tが成立し得るというふうにとれます。 その意味で正しいのでしょうか？ 普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、 思えるんですが。 406 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:42:08.97 ] ξ_{n+1} の前に ∀ があるので、適切な内包公理の下で、 ∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から ∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。 ちょっと読み進めばそのことが書いてあるはず。

---

---

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

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