1 名前:132人目の素数さん 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/
338 名前:132人目の素数さん mailto:sage [2011/02/18(金) 19:47:26 ] 君の現在の理解力を越えてるようだね。
339 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:00:42 ] >>339 x=y → x'=y' ならば、 0→1→2→3→4 となるんじゃない?3の次は3'(=4)だけでしょ?
341 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:06:45 ] >>340 x'=y'→x=yを仮定しないと、3' が 1 になり得るという話
342 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:12:23 ] >>340 それだけだと、 3'のまえが3じゃないとこから複数本繋がってきてもいい。
343 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:13:21 ] 感覚としては、後者関数を使って自然数を次々と生成していくわけだが、 新しく生まれる自然数が、先に生まれた自然数のいずれとも異なるように、 言い換えれば、自然数を一直線に並べるために必要な公理なんだよ もし単射でなかったら、直前の世代にあたる自然数が一通りに決まらない 例えば、1の直前が 0 と 0''' ということもあり得る。
344 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:22:27 ] x=y → x'=y' なのになぜ3の前が複数になりうるの?
345 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:22:34 ] 今の場合反例モデルが作れるからそれで説明するけど x'=y'→x=yがなくてその逆だと Z/nZでも条件満たしちゃうでしょ。 Z/nZが何なのか分からないなら先に初等整数論を勉強してね。
346 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:51:38 ] ごめんボケてた>>345 はx'≠0が必要だって話だw やっぱり皆の言うようにやらないとダメだ ただどっちも似たような話で、 0'=1,1'=2,2'=3,……,〜'=n、n'=1みたいな状況が生じちゃうってこと
347 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:57:05 ] >>344 x≠yのときについては何の制約も掛けて無いから。
348 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:58:58 ] >>344 a=b だからって、a と b が「記号列として同じ」であるとは限らない 等号の公理:反射律および代入可能性を満たす限りにおいて、a と b が異なる記号列であってもよい だから、1の直前が 0 と 0''' である、つまり論理式 0=0''' が証明可能、という状況もある(かもしれない)
349 名前:132人目の素数さん mailto:sage [2011/02/18(金) 20:59:18 ] >>344 まず「単射」という概念を理解した方がいい。 ググればいくらでも出てくるだろう。予備知識は必要ない。 それでも分からなかったらここで聞いても無駄。
350 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:03:00 ] >>344 その条件は3の後はかならず3'にしかいかないということを言ってるだけで 3'の前がかならず3になってるとは言ってないからだよ。 後者の条件はお前がどうしても外したがってるx'=y'→x=yのほう。
351 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:24:25 ] 久しぶりにスレが伸びていると思ったら またこの流れか。
352 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:28:40 ] 竹内・八杉の『証明論入門』 芯の通った思想を感じる本だね。楽しくなってくる。
353 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:53:00 ] 和書しか読まないから 竹内の本がありがたく感じる。 もちろん良い本だけど。
354 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:54:39 ] 何か他の条件から後続関数の単射性が言えれば仮定しなくても良い。 どのみち、分からん君が置き換えたがってる等号公理からは出ないが。
355 名前:132人目の素数さん mailto:sage [2011/02/18(金) 21:57:11 ] >>350 それだったら同じ理屈で、x'=y'→x=y だと 1の次が2だったり3だったりしてしまうのでは?
356 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/18(金) 22:14:38 ] >>356 まじで?
358 名前:132人目の素数さん mailto:sage [2011/02/19(土) 05:24:22 ] x≠y → x'≠y'
359 名前:132人目の素数さん mailto:sage [2011/02/21(月) 00:33:29.67 ] 基本的なこと分からない人は、 島内さんの「数学の基礎」をよめばどうかな。 基礎論の初歩的なところを手取り足取り進めてくれるから。 中学生でも理解できるような歩みで。
360 名前:132人目の素数さん mailto:sage [2011/02/21(月) 01:00:24.59 ] あれε記号使ってたような
361 名前:132人目の素数さん mailto:sage [2011/02/21(月) 07:25:58.31 ] shenfieldのmathematical logic1冊で充分だろ。
362 名前:132人目の素数さん mailto:sage [2011/02/21(月) 08:21:03.83 ] >>326 にShoenfield薦めるとか頭おかしいとしか思えん。 p→qとその逆のq→pを混同してるかもしれないレベルなのに。
363 名前:132人目の素数さん mailto:sage [2011/02/21(月) 17:07:35.54 ] >>360 いや、それどころか自然数の公理系まで入ってるけど。
364 名前:132人目の素数さん mailto:sage [2011/02/21(月) 17:19:04.08 ] >>359 その本の目的がいまいちぴんと来ない。 読みてはどんな人がターゲット?
365 名前:132人目の素数さん mailto:sage [2011/02/21(月) 23:51:21.86 ] 広く浅く学びたい趣味人だろう。
366 名前:132人目の素数さん mailto:sage [2011/02/22(火) 17:07:57.67 ] >>364 >>326 に勧めてるじゃんw
367 名前:132人目の素数さん mailto:sage [2011/02/22(火) 23:35:42.32 ] 有限の立場では、背理法の無制限な使用は認められますか?
368 名前:132人目の素数さん mailto:sage [2011/02/23(水) 08:02:56.58 ] 有限の立場ってのは有限公理化可能ってことだとするなら、 ZFCやMKは有限でないが、NGBは有限。 排中律を公理にするかは1階述語論理での話で、 むしろ背理法なしで無矛盾な集合論を展開できるかということ。 答えはYes。
369 名前:132人目の素数さん mailto:sage [2011/02/23(水) 08:14:46.30 ] こりゃまた斬新な答えだ
370 名前:132人目の素数さん [2011/02/23(水) 10:13:34.91 ] 有限の立場は人の数だけあるとは言うが…
371 名前:132人目の素数さん mailto:sage [2011/02/23(水) 12:09:40.31 ] 少ない脳味噌を如何に活用するかってことなんですね。
372 名前:368 mailto:sage [2011/02/23(水) 19:56:25.65 ] >>369 >>371 文句があるなら論破してみろ。
373 名前:132人目の素数さん mailto:sage [2011/02/23(水) 20:04:38.06 ] どこから手をつけろと言うんだw
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 名前:132人目の素数さん mailto:sage [2011/02/23(水) 21:15:08.73 ] basicってことはadvancedとかもあるの?
377 名前:132人目の素数さん 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 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/23(水) 23:43:01.36 ] >>378 いやlow basis theoremのはずなのにスペル間違ってたから きっと内容分かってないんだろなと思ってからかっただけだよ というかジャクソンってもしかしてJockuschのことじゃないだろうな?
383 名前:132人目の素数さん mailto:sage [2011/02/23(水) 23:52:38.94 ] >>367 ヒルベルト達の言う有限の立場で示せる命題と言うのは、 或る特定の自然数に対する命題(Δ0式)とか、 或いは変数 x を使って x に対して成り立つ命題を証明することで 「任意の x に対して〜〜」を示す、とか、つまりかなり直截的に証明できるものなので、 ∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、 そういう凝った証明は出て来ないんじゃないかと思います。 従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、 背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。 だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。
384 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/24(木) 00:26:29.37 ] 議論・喧嘩してるわけでもないのに、なんで名前固定してんのこの人
388 名前:132人目の素数さん mailto:sage [2011/02/24(木) 00:26:46.53 ] 仮に∀x P(x)を仮定して〜〜みたいな議論がそもそも無いので ¬∀x〜〜という論理式がそもそも出て来ない。 だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。 あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
389 名前:132人目の素数さん mailto:sage [2011/02/24(木) 00:28:01.31 ] くあんてぃふぁいあふりー
390 名前:132人目の素数さん mailto:sage [2011/02/24(木) 16:44:00.27 ] 素人でこの方面興味持つ奴は概ね基地外
391 名前:132人目の素数さん mailto:sage [2011/02/24(木) 20:11:19.86 ] >>387 話の展開をわかりやすくするためだろ。
392 名前:132人目の素数さん mailto:sage [2011/02/24(木) 20:28:22.40 ] というかロジックの場合、他分野では優秀な数学者が 往々にしてトンデモだったりするから困る
393 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/25(金) 12:41:58.62 ] いまどき素朴集合論のみで食ってる研究者なぞおらんわ 寝言は寝てから言え
397 名前:132人目の素数さん mailto:sage [2011/02/25(金) 12:44:27.44 ] いや、普通の数学の専門家は可算濃度と連続濃度の算法しか分からんのが結構いる。
398 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/25(金) 20:18:53.14 ] いやモデル理論はロジックの一部だし。 あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。 非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
401 名前:368 mailto:sage [2011/02/25(金) 22:19:27.88 ] 知識あれば良いけど、 キューネンとかウッディンとかの本読んでるけど、 論理学のテキストまったく読んだことない人間でも 読めると思うけど? 実際に自分が読めてる。 論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。 実際に直感的に明らかな論理学の結果しか使わないし。 何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
402 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/27(日) 01:20:35.00 ] >>399 > 公理的集合論(略)の研究者で 実際に何やってる人? 組合せ論的な構成可能集合の研究とか?
405 名前:132人目の素数さん 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 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/02/27(日) 21:43:42.25 ] >>405 "集合" ξ_{n+1} の補集合を考えれば、 s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
408 名前:132人目の素数さん mailto:sage [2011/02/27(日) 21:53:53.94 ] >>406 >>407 ありがとうございます。 ちゃんとした理屈があることが分かり、安心しました。 内包公理や補集合をヒントに理解してみます。
409 名前:132人目の素数さん mailto:sage [2011/03/03(木) 15:09:48.69 ] 知ったかぶりのバカが集まるすれですね 何の役にもたたないのにw
410 名前:132人目の素数さん mailto:sage [2011/03/03(木) 16:30:05.36 ] 自己紹介ご苦労
411 名前:368 mailto:sage [2011/03/03(木) 21:57:25.77 ] >>404 点集合トポロジーだったかなんだったか。 >>409 俺もそうだけど、別にいいじゃん知ったか。 知ったかでも博士とれちゃう国あるんだよ、世界には^^
412 名前:132人目の素数さん mailto:sage [2011/03/03(木) 22:08:12.18 ] だったら無駄に名乗らないでください 邪魔なんで
413 名前:368 mailto:sage [2011/03/03(木) 22:34:23.08 ] >>412 こんな俺でも ここじゃちょっとは役に立つと思って助言してる。 なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる 人間みるとつい助けたくなっちゃう。
414 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/03/06(日) 06:14:59.41 ] 証明抜きが多かった記憶
418 名前:368 [2011/03/07(月) 21:37:05.07 ] >>417 まぁ本来啓蒙書なんで。 その割には証明がある丁寧な本程度と考えた方が。
419 名前:132人目の素数さん mailto:sage [2011/03/16(水) 18:44:12.04 ] 東北大学のサイト落ちてますねえ。 まあ仕方ないかな。
420 名前:132人目の素数さん mailto:sage [2011/03/16(水) 18:46:10.16 ] 被災地域の大学生、教員でアボーンした人どれだけ居るのやら。
421 名前:132人目の素数さん mailto:sage [2011/03/16(水) 19:09:28.70 ] 田中一之さん、東北大学だよね。心配ですねえ。
422 名前:132人目の素数さん mailto:sage [2011/03/17(木) 13:19:17.80 ] 今東北にロジックの学生どれくらいいるの?
423 名前:132人目の素数さん mailto:sage [2011/03/17(木) 13:24:44.90 ] 学徒動員。福島原発に突入せよ。
424 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/03/18(金) 22:22:50.44 ] それはお前が無知なだけ
427 名前:368 [2011/03/18(金) 22:45:13.30 ] >>426 そんなら425をサクッと説明しちゃってくださいよ。
428 名前:132人目の素数さん mailto:sage [2011/03/18(金) 22:50:59.58 ] なにこの糞数字コテ
429 名前:132人目の素数さん mailto:sage [2011/03/18(金) 22:56:57.07 ] 「A→Bが証明可能」 ⇒ 「Aが証明可能⇒Bが証明可能」 だけど、逆は一般には成り立たないことに なぞらえてるのでは?
430 名前:132人目の素数さん mailto:sage [2011/03/18(金) 23:05:57.04 ] だって、replacement theoremとstrong replacement theoremは同値じゃん。 なんでstrongなのかわからん
431 名前:132人目の素数さん [2011/03/19(土) 00:31:55.49 ] そういうときは wff、置換、論理的同値、トートロジー の定義を書いてみよう。 書いているうちにわかる場合が多いよ。
432 名前:132人目の素数さん mailto:sage [2011/03/19(土) 00:33:29.97 ] なにその万能な回答
433 名前:132人目の素数さん mailto:sage [2011/03/19(土) 00:44:12.36 ] 万能文化猫娘
434 名前:431 [2011/03/19(土) 00:50:10.47 ] え、割と有効なやり方だと思うんだけど
435 名前:368 [2011/03/19(土) 08:09:26.45 ] まぁ確かに定義を書くことで 頭が整理されるってことは結構あると思う。
436 名前:132人目の素数さん mailto:sage [2011/03/19(土) 09:44:19.26 ] strong replacement theoremというのは一般的な呼び方じゃないと思う。 別の名前が付いている訳でもないけど。 AならばBというのとA→Bはトートロジーだというのでは 後者の方が強い気はするよね。 トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。
437 名前:132人目の素数さん [2011/03/19(土) 11:07:58.09 ] ジェフリー『形式論理学』の決定可能、決定不可能のくだりで 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える(たとえば、関数記号+を和の関係を表す述語に置き換える)結果、それが言えるという意味ですか? それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語(=11は定理だが、(自由な表れの述語Aに関して)A11が定理は言えない)は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか どなたか、お教えください よろしくおねがいします
438 名前:368 [2011/03/19(土) 11:58:48.45 ] >>437 > ジェフリー『形式論理学』の決定可能、決定不可能のくだりで > 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える(たとえば、関数記号+を和の関係を表す述語に置き換える)結果、それが言えるという意味ですか? > それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語(=11は定理だが、(自由な表れの述語Aに関して)A11が定理は言えない)は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか > どなたか、お教えください > よろしくおねがいします 言葉の定義とかも書かないとわからないと思いますよ。 普通の数理論理学のテキストにない用語が多いですから。