数学基礎論・数理論理学のスレッド　その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/ 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}) が導ける。 ちょっと読み進めばそのことが書いてあるはず。 407 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:43:42.25 ] >>405 "集合" ξ_{n+1} の補集合を考えれば、 s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K. 408 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:53:53.94 ] >>406 >>407 ありがとうございます。 ちゃんとした理屈があることが分かり、安心しました。 内包公理や補集合をヒントに理解してみます。 409 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 15:09:48.69 ] 知ったかぶりのバカが集まるすれですね 何の役にもたたないのにｗ 410 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 16:30:05.36 ] 自己紹介ご苦労 411 名前：368 mailto:sage [2011/03/03(木) 21:57:25.77 ] >>404 点集合トポロジーだったかなんだったか。 >>409 俺もそうだけど、別にいいじゃん知ったか。 知ったかでも博士とれちゃう国あるんだよ、世界には＾＾ 412 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 22:08:12.18 ] だったら無駄に名乗らないでください 邪魔なんで 413 名前：368 mailto:sage [2011/03/03(木) 22:34:23.08 ] >>412 こんな俺でも ここじゃちょっとは役に立つと思って助言してる。 なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる 人間みるとつい助けたくなっちゃう。 414 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 22:55:43.28 ] >>413 じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？ 415 名前：368 mailto:sage [2011/03/03(木) 23:09:52.65 ] >>414 pcfはJechに載ってるだろう。 予備知識などいらん！ 416 名前：368 [2011/03/05(土) 23:12:13.84 ] 志賀の無限からの光芒って面白いね。 知らなかった定理が結構ある。 417 名前：１３２人目の素数さん mailto:sage [2011/03/06(日) 06:14:59.41 ] 証明抜きが多かった記憶 418 名前：368 [2011/03/07(月) 21:37:05.07 ] >>417 まぁ本来啓蒙書なんで。 その割には証明がある丁寧な本程度と考えた方が。 419 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 18:44:12.04 ] 東北大学のサイト落ちてますねえ。 まあ仕方ないかな。 420 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 18:46:10.16 ] 被災地域の大学生、教員でアボーンした人どれだけ居るのやら。 421 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 19:09:28.70 ] 田中一之さん、東北大学だよね。心配ですねえ。 422 名前：１３２人目の素数さん mailto:sage [2011/03/17(木) 13:19:17.80 ] 今東北にロジックの学生どれくらいいるの？ 423 名前：１３２人目の素数さん mailto:sage [2011/03/17(木) 13:24:44.90 ] 学徒動員。福島原発に突入せよ。 424 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:11:10.98 ] 質問です。 命題論理のごく初歩的なところをやっているんですが、 replacement theoremとstrong replacement theoremの違いがわかりません。 wff Aを何回か含むwffをC[A]とし、C[A]の中のいくつかのAをwff Bで置き換えた結果をC[B]とする。このとき、 replacement theorem：AとBが論理的同値ならばC[A]とC[B]も論理的同値 strong replacement theorem：(A←→B)→(C[A]←→C[B])はトートロジー なぜ、後者のほうが「強い」のでしょうか？ 425 名前：368 [2011/03/18(金) 22:19:34.59 ] strong replacement theorem なんて初めて聞いた。 426 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:22:50.44 ] それはお前が無知なだけ 427 名前：368 [2011/03/18(金) 22:45:13.30 ] >>426 そんなら425をサクッと説明しちゃってくださいよ。 428 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:50:59.58 ] なにこの糞数字コテ 429 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:56:57.07 ] 「A→Bが証明可能」　⇒　「Aが証明可能⇒Bが証明可能」 だけど、逆は一般には成り立たないことに なぞらえてるのでは？

---

---

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

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