数学基礎論・数理論理学のスレッド その7
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2010/11/11(木) 22:13:5719世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学のスレッド その6
http://kamome.2ch.net/test/read.cgi/math/1265884076/
0321１３２人目の素数さん
2011/02/16(水) 10:59:40ありがとうございます！
0322１３２人目の素数さん
2011/02/17(木) 17:43:46rankとdegreeについての二重帰納法を用いるものがありますよね？
証明図の変形によるrankとdegreeの減少を精密に評価することで、
何ステップ以内に変形が終わるか、あらかじめわかるのではないかと思ったのですが、
どうも無理な気がしてきました。
実際どうなんでしょうか？
よろしければお知恵をお貸し下さい。
0323１３２人目の素数さん
2011/02/17(木) 19:03:27Girard の Proof theory and Logical comlpexity には
その方法で評価がされています。
また、もっとスマートに二重帰納法を回避する方法ですが Gentzen の
自然数論の無矛盾性証明の論文の最後の方に、数学的帰納法がなければ
ωを 3 に置き換えればよいというようなことが書いてあったと思います。
0324１３２人目の素数さん
2011/02/17(木) 20:36:27ご回答ありがとうございます。図書館で調べてみます。
＞ωを 3 に置き換えればよい
というのは、無矛盾性証明において証明図に順序数を対応させたのと同様に、
LKのカット除去でも証明図に、例えば自然数3＾（3＾（1+1））を対応させる、ということでしょうか。
この方針で試みてみようと思います。
0325１３２人目の素数さん
2011/02/17(木) 23:25:04あれ、ということはロビンソン算術の無矛盾性は有限の立場で示せるということ？
0326１３２人目の素数さん
2011/02/18(金) 13:37:43なんでx=y→x'=y'じゃなくて
x'=y'→x=yなのか教えてください
0327１３２人目の素数さん
2011/02/18(金) 13:57:580328１３２人目の素数さん
2011/02/18(金) 15:47:050329１３２人目の素数さん
2011/02/18(金) 15:54:02演繹するか公理で仮定することになる。
0330１３２人目の素数さん
2011/02/18(金) 15:58:300331１３２人目の素数さん
2011/02/18(金) 16:28:40なにがいいの？
0332１３２人目の素数さん
2011/02/18(金) 16:43:54？
0333１３２人目の素数さん
2011/02/18(金) 16:47:140334１３２人目の素数さん
2011/02/18(金) 17:22:53〜じゃだめなの？＝〜でいいだろ。
ということだから、いいってのはどういう意味でいいっていってんのかってこと。
0335１３２人目の素数さん
2011/02/18(金) 19:20:420336１３２人目の素数さん
2011/02/18(金) 19:34:060337１３２人目の素数さん
2011/02/18(金) 19:39:50そんなうまく質問できるくらいなら質問してない
初めてペアノの公理見たんだよ
なんでx=y→x'=y'じゃなくてx'=y'→x=yなのかわかるように教えてください
0338１３２人目の素数さん
2011/02/18(金) 19:47:260339１３２人目の素数さん
2011/02/18(金) 19:48:08これは後者関数の単射であることを意味する。
ペアノの公理からこれを除くと、ループを許すことになる（例えばこんなの↓）。
0→1→2→3→1→2→3→1→2→3→…
形式的な話をすれば、体系内で帰納的関数を構成する際などにこの公理を用いる。
もちろん、それ以外の場面でも。
上でも指摘されてるけど、
x=y→x'=y
これ↑は単なる代入可能性を意味する、等号の公理の一部。
0340１３２人目の素数さん
2011/02/18(金) 20:00:42x=y → x'=y'
ならば、
0→1→2→3→4
となるんじゃない？3の次は3'(=4)だけでしょ？
0341１３２人目の素数さん
2011/02/18(金) 20:06:45x'=y'→x=yを仮定しないと、3' が 1 になり得るという話
0342１３２人目の素数さん
2011/02/18(金) 20:12:23それだけだと、
3'のまえが3じゃないとこから複数本繋がってきてもいい。
0343１３２人目の素数さん
2011/02/18(金) 20:13:21新しく生まれる自然数が、先に生まれた自然数のいずれとも異なるように、
言い換えれば、自然数を一直線に並べるために必要な公理なんだよ
もし単射でなかったら、直前の世代にあたる自然数が一通りに決まらない
例えば、1の直前が 0 と 0''' ということもあり得る。
0344１３２人目の素数さん
2011/02/18(金) 20:22:270345１３２人目の素数さん
2011/02/18(金) 20:22:34x'=y'→x=yがなくてその逆だと
Z/nZでも条件満たしちゃうでしょ。
Z/nZが何なのか分からないなら先に初等整数論を勉強してね。
0346１３２人目の素数さん
2011/02/18(金) 20:51:38やっぱり皆の言うようにやらないとダメだ
ただどっちも似たような話で、
0'=1，1'=2，2'=3，……，〜'=n、n'=1みたいな状況が生じちゃうってこと
0347１３２人目の素数さん
2011/02/18(金) 20:57:05x≠yのときについては何の制約も掛けて無いから。
0348１３２人目の素数さん
2011/02/18(金) 20:58:58a=b だからって、a と b が「記号列として同じ」であるとは限らない
等号の公理：反射律および代入可能性を満たす限りにおいて、a と b が異なる記号列であってもよい
だから、1の直前が 0 と 0''' である、つまり論理式 0=0''' が証明可能、という状況もある（かもしれない）
0349１３２人目の素数さん
2011/02/18(金) 20:59:18まず「単射」という概念を理解した方がいい。
ググればいくらでも出てくるだろう。予備知識は必要ない。
それでも分からなかったらここで聞いても無駄。
0350１３２人目の素数さん
2011/02/18(金) 21:03:00その条件は3の後はかならず3'にしかいかないということを言ってるだけで
3'の前がかならず3になってるとは言ってないからだよ。
後者の条件はお前がどうしても外したがってるx'=y'→x=yのほう。
0351１３２人目の素数さん
2011/02/18(金) 21:24:25またこの流れか。
0352１３２人目の素数さん
2011/02/18(金) 21:28:40芯の通った思想を感じる本だね。楽しくなってくる。
0353１３２人目の素数さん
2011/02/18(金) 21:53:00竹内の本がありがたく感じる。
もちろん良い本だけど。
0354１３２人目の素数さん
2011/02/18(金) 21:54:39どのみち、分からん君が置き換えたがってる等号公理からは出ないが。
0355１３２人目の素数さん
2011/02/18(金) 21:57:11それだったら同じ理屈で、x'=y'→x=y だと
1の次が2だったり3だったりしてしまうのでは？
0356１３２人目の素数さん
2011/02/18(金) 22:04:20∀x x'≠0という公理があるから特に0≠0'=1。
ところが1'=1'' だとすると1'=(1')'→1=1'だから1=1'、
つまり0'=(0')'となって同様にして0=0'となって矛盾する。
0357１３２人目の素数さん
2011/02/18(金) 22:14:38まじで？
0358１３２人目の素数さん
2011/02/19(土) 05:24:220359１３２人目の素数さん
2011/02/21(月) 00:33:29.67島内さんの「数学の基礎」をよめばどうかな。
基礎論の初歩的なところを手取り足取り進めてくれるから。
中学生でも理解できるような歩みで。
0360１３２人目の素数さん
2011/02/21(月) 01:00:24.590361１３２人目の素数さん
2011/02/21(月) 07:25:58.310362１３２人目の素数さん
2011/02/21(月) 08:21:03.83p→qとその逆のq→pを混同してるかもしれないレベルなのに。
0363１３２人目の素数さん
2011/02/21(月) 17:07:35.54いや、それどころか自然数の公理系まで入ってるけど。
0364１３２人目の素数さん
2011/02/21(月) 17:19:04.08その本の目的がいまいちぴんと来ない。
読みてはどんな人がターゲット？
0365１３２人目の素数さん
2011/02/21(月) 23:51:21.860366１３２人目の素数さん
2011/02/22(火) 17:07:57.67>>326に勧めてるじゃんw
0367１３２人目の素数さん
2011/02/22(火) 23:35:42.320368１３２人目の素数さん
2011/02/23(水) 08:02:56.58ZFCやMKは有限でないが、NGBは有限。
排中律を公理にするかは１階述語論理での話で、
むしろ背理法なしで無矛盾な集合論を展開できるかということ。
答えはYes。
0369１３２人目の素数さん
2011/02/23(水) 08:14:46.300370１３２人目の素数さん
2011/02/23(水) 10:13:34.910371１３２人目の素数さん
2011/02/23(水) 12:09:40.310373１３２人目の素数さん
2011/02/23(水) 20:04:38.060375368
2011/02/23(水) 21:10:09.87ジャクソンとショーアのlow basic theoremより
recursive degreeを下げることで不完全性定理は成り立たないようにできる！
0376１３２人目の素数さん
2011/02/23(水) 21:15:08.730377１３２人目の素数さん
2011/02/23(水) 21:27:56.540380１３２人目の素数さん
2011/02/23(水) 22:21:36.12It 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.
0382１３２人目の素数さん
2011/02/23(水) 23:43:01.36いやlow basis theoremのはずなのにスペル間違ってたから
きっと内容分かってないんだろなと思ってからかっただけだよ
というかジャクソンってもしかしてJockuschのことじゃないだろうな？
0383１３２人目の素数さん
2011/02/23(水) 23:52:38.94ヒルベルト達の言う有限の立場で示せる命題と言うのは、
或る特定の自然数に対する命題（Δ0式）とか、
或いは変数 x を使って x に対して成り立つ命題を証明することで
「任意の x に対して〜〜」を示す、とか、つまりかなり直截的に証明できるものなので、
∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、
そういう凝った証明は出て来ないんじゃないかと思います。
従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、
背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。
だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。
0384１３２人目の素数さん
2011/02/24(木) 00:02:15.70∀x P(x)を仮定して背理法によって∃x ¬P(x)を示すとか
0386368
2011/02/24(木) 00:21:42.85ああそうだよ、内容なんてわかってないよ。
俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、
最近shoenfieldを読み始めたばかりだよ。
low basis theorem についてはある人のブログで知ったんだよ、問題あるか？
0387１３２人目の素数さん
2011/02/24(木) 00:26:29.370388１３２人目の素数さん
2011/02/24(木) 00:26:46.53¬∀x〜〜という論理式がそもそも出て来ない。
だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。
あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
0389１３２人目の素数さん
2011/02/24(木) 00:28:01.310390１３２人目の素数さん
2011/02/24(木) 16:44:00.270391１３２人目の素数さん
2011/02/24(木) 20:11:19.86話の展開をわかりやすくするためだろ。
0392１３２人目の素数さん
2011/02/24(木) 20:28:22.40往々にしてトンデモだったりするから困る
0393１３２人目の素数さん
2011/02/24(木) 21:04:17.78www 本当杉て困る。
0394368
2011/02/24(木) 22:45:14.870395368
2011/02/24(木) 23:12:50.35論理学をやったことない人がいる。
0396１３２人目の素数さん
2011/02/25(金) 12:41:58.62寝言は寝てから言え
0397１３２人目の素数さん
2011/02/25(金) 12:44:27.440398１３２人目の素数さん
2011/02/25(金) 13:40:21.63>>395-396の流れを読め。
0400１３２人目の素数さん
2011/02/25(金) 20:18:53.14あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。
非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
0401368
2011/02/25(金) 22:19:27.88キューネンとかウッディンとかの本読んでるけど、
論理学のテキストまったく読んだことない人間でも
読めると思うけど？
実際に自分が読めてる。
論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。
実際に直感的に明らかな論理学の結果しか使わないし。
何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
0402１３２人目の素数さん
2011/02/25(金) 23:35:13.210403368
2011/02/25(金) 23:57:02.29forcing axiom, and the non-stationary ideal
0404１３２人目の素数さん
2011/02/27(日) 01:20:35.00> 公理的集合論(略)の研究者で
実際に何やってる人?
組合せ論的な構成可能集合の研究とか?
0405１３２人目の素数さん
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が成立し得るというふうにとれます。
その意味で正しいのでしょうか？
普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、
思えるんですが。
0406１３２人目の素数さん
2011/02/27(日) 21:42:08.97∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から
∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。
ちょっと読み進めばそのことが書いてあるはず。
0407１３２人目の素数さん
2011/02/27(日) 21:43:42.25"集合" ξ_{n+1} の補集合を考えれば、
s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
0408１３２人目の素数さん
2011/02/27(日) 21:53:53.94>>407
ありがとうございます。
ちゃんとした理屈があることが分かり、安心しました。
内包公理や補集合をヒントに理解してみます。
0409１３２人目の素数さん
2011/03/03(木) 15:09:48.69何の役にもたたないのにｗ
0410１３２人目の素数さん
2011/03/03(木) 16:30:05.360411368
2011/03/03(木) 21:57:25.77点集合トポロジーだったかなんだったか。
>>409
俺もそうだけど、別にいいじゃん知ったか。
知ったかでも博士とれちゃう国あるんだよ、世界には＾＾
0412１３２人目の素数さん
2011/03/03(木) 22:08:12.18邪魔なんで
0413368
2011/03/03(木) 22:34:23.08こんな俺でも
ここじゃちょっとは役に立つと思って助言してる。
なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる
人間みるとつい助けたくなっちゃう。
0414１３２人目の素数さん
2011/03/03(木) 22:55:43.28じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？
0416368
2011/03/05(土) 23:12:13.84知らなかった定理が結構ある。
0417１３２人目の素数さん
2011/03/06(日) 06:14:59.410418368
2011/03/07(月) 21:37:05.07まぁ本来啓蒙書なんで。
その割には証明がある丁寧な本程度と考えた方が。
0419１３２人目の素数さん
2011/03/16(水) 18:44:12.04まあ仕方ないかな。
0420１３２人目の素数さん
2011/03/16(水) 18:46:10.16■ このスレッドは過去ログ倉庫に格納されています