数学基礎論・数理論理学　その13

1 名前：１３２人目の素数さん mailto:sage [2012/06/24(日) 01:38:43.25 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その12 http://uni.2ch.net/test/read.cgi/math/1332549969/ 331 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 19:39:31.92 ] ただ無矛盾性が強い体系というのは、 要はモデルを作る能力が強いということなので 一般的にはそれより弱い体系の或る命題が 証明出来るか出来ないかを判定することが出来る場合が多いかと 332 名前：１３２人目の素数さん [2012/08/11(土) 19:44:51.53 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 333 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 19:57:19.54 ] >>331 せいぜい言えるのはそこまでだろうな。 「未解決問題の独立的解決をするのにZFC+巨大基数公理からの独立性を言えば十分」 というのは明らかに言いすぎ。 334 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 19:59:31.00 ] P=NPのこと言ってるんだからZFCから独立なら 一応解決で良いと思うんだけどね 335 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 20:06:22.80 ] 問題の発端となった>>286は Grothendieck universe を使う分野の未解決問題のことを言っていたと思われ 336 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 20:14:13.22 ] どうでもいいけど325は勉強して出直して来た方がいいと思う 337 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 20:42:01.78 ] 記述計算量理論からわかるとおり 計算量クラスのPもNPもΔ^0_1にすら到達しない。 どちらのクラスの命題の記述も、 PAどころかその断片のIΣ_1（原始再帰的関数全体と同等）で十分。 さらに算術さえ不要で、2階述語論理に推移閉包か最小不動点演算子を加えれば記述可能。 当然命題の記述にZFCなんかは大きすぎる。 PとNPの包含関係は必ずしも集合論で記述する必要はない。 PでないNPを記述すれば十分で、最悪でも命題を算術化すれば十分だし それよりもはるかに簡単に記述されるかもしれない。 338 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:14:28.12 ] 算術で記述されたとして、証明は必ず算術でできるの？ 339 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:17:49.74 ] 例えばIΣ_1は原始再帰的関数を再帰的に証明可能だから、 これを算術化すれば原始再帰的関数より低い階層のすべての 命題についての命題が記述されうる。 340 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:21:57.55 ] P＝NP や P≠NP が算術で記述されたとして、P＝NP や P≠NPの証明はZFCで出来れば必ず算術でできるの？ 341 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:36:23.19 ] 算術からP≠NPが証明されるならば、ZFCからP≠NPが証明される。 これの対偶をとる 342 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:42:09.81 ] >>341はミス。 算術で独立命題になる可能性がある 343 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 21:42:10.63 ] あほくさ 344 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/11(土) 22:58:55.04 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 345 名前：１３２人目の素数さん [2012/08/11(土) 23:17:17.92 ] ホルホル 346 名前：１３２人目の素数さん mailto:sage [2012/08/11(土) 23:19:40.80 ] 一昔前に日本人がP=NP問題の算術からの独立性を示したと噂になったがその後どうなったん？ 流石に算術からの独立性では懸賞金は貰えなかったんか？それとも間違ってたんか？ 347 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/11(土) 23:21:35.04 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 348 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 00:25:26.57 ] 算術というのを一階算術だとすると 一階算術からの独立性証明では「通常の数学」から独立とはみなされないと思う。 それでも十分賞賛される結果だろと思うけどね。 二階算術とか高階算術とかだとどうなんだろう。 超準解析業界では「通常の数学」はＶ_{ω}(ω)で つまり高階算術で展開可能というコンセンサスがあるみたいだけど。 高階算術からの独立性が示されてZFCからの独立性は示せていないような場合、 懸賞金を出すか出さないか揉めるんじゃないかな。 349 名前：１３２人目の素数さん [2012/08/12(日) 07:12:19.99 ] P＝NPがZFCから独立ということはありえないような気がする。 一つでもPなNP完全問題を見つければよいだけだから。 P≠NPならZFCから示せないと言うのならわかる。 これは超越的な方法を使う必要がありそうだから。 350 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/12(日) 07:22:11.47 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 351 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 09:33:52.47 ] >>346 その話は噂の主がその噂は事実ではありませんとメーリングリストで宣言して終わりだったと記憶している 352 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 10:56:10.57 ] >>349 その「PなNP完全問題」へのP時間では判定不能な超準的な入力の不存在を示すのに 超越的な論理式に関する帰納法が必要になったりしない？ 353 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/12(日) 11:21:32.16 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 354 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 13:32:55.25 ] >>348 数学の表舞台で再び活躍とまでは言わなくても そんな風にロジックがキャスティングボートを握れる場面が 現実に起きたらどれだけいいことか 355 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 13:55:41.76 ] 確かにそういうことで揉めてくれたら 多くの数学者が「一体どういうこと？」って興味を持ってくれるだろうし 解決と看做すかどうかの論争に参戦する為に勉強もして貰えるかもね。 単にロジックの技法が未解決問題の解決に役に立ちましたってだけより 宣伝効果は高そうだ。 356 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/12(日) 14:35:33.84 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 357 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 15:06:44.45 ] Ｖ_{ω}(ω)の（ω）って何？ 358 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 16:22:36.92 ] ωから出発して冪集合繰り返す von Neumann 階層をωまでってことだろ。 超準解析だったら実数全体Rから出発すべきとも思ったが、同値だったな。 359 名前：１３２人目の素数さん [2012/08/12(日) 17:19:31.53 ] Frege's Theorem [Hardcover] Richard G. Heck (Author) www.amazon.com/Freges-Theorem-Richard-G-Heck/dp/0199695644 ついに出版された、新フレーゲ主義のバイブルが。 ヒュームの原理などにも言及、ロジックマニアなら買いでしょ。 360 名前：１３２人目の素数さん [2012/08/12(日) 18:00:38.66 ] メレオロジーに新フレーゲ主義にオントロジーに形式の法則にプロトセティク。 我々のロジックはあらたなパラダイムへとシフトしようとしているのである。 361 名前：１３２人目の素数さん [2012/08/12(日) 19:01:23.46 ] 糞吹いた。 未だにプリンキピアマテマティカを評価しているのか PMは頓挫したよ、体系が複雑でつぎはぎだらけになって 今はヒルベルトがPMから論理だけを抽出して ゲーデルが完全性という重要な概念を生み出したから 論理と数論が一体化したような体系は研究対象にならない。 よって現在販売中のPMの３冊組は買うだけカネの無駄 買うのは哲学科のみ 362 名前：１３２人目の素数さん [2012/08/12(日) 19:30:44.20 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　この板って馬鹿ばかりね 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 363 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 21:39:21.60 ] 質問です 例えば群であれば、ある位数nの群すべてを多項式時間で見つけ出す アルゴリズムは存在しているといえるのですか？ 364 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 22:33:17.37 ] nが2のべきの時に位数nの群の同型類の個数はやたら大きくなるから そもそも個数自体が多項式で抑えられるか疑問だと思う たぶん無理 位数256の群は56,092個 位数512の群は10,494,213個 位数1024の群は49,487,365,422個 www.icm.tu-bs.de/ag_algebra/software/small/number.html 365 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 22:35:56.38 ] >>361 PMそのままじゃなくて、今風のtype thoeryのことでしょ。> 新フレーゲ主義 366 名前：１３２人目の素数さん mailto:sage [2012/08/12(日) 23:40:11.79 ] P vs NPの話が出て来たので、相乗りしてちょっと質問です。 CNFSAT -> 2SATの還元手法って誰か論文書いていたりします？ （もちろん指数規模になってもOKです） 教科書レベルだと言及しているものが無いので、論文でまとまっているものが あるようでしたら読んでみたいです。 367 名前：１３２人目の素数さん [2012/08/13(月) 01:45:47.31 ] >>365 集合を用いずに数学を展開したと主張する 論理主義者の末裔です。 数オペレータと呼ばれる哲学的概念が自然数を大体すると主張しています。 368 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 02:08:39.88 ] >>361 APALやJSLで"Frege system"とかで検索してみ。 数は少ないが最近でもきちんとした研究対象になってる。 偏狭な知識の開陳は恥ずかしいよ。 369 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 06:56:37.21 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 370 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 06:57:24.46 ] P vs NP uni.2ch.net/test/read.cgi/math/1344808587/ 371 名前：１３２人目の素数さん [2012/08/13(月) 07:24:42.84 ] フレーゲシステムも新フレーゲ主義もフレーゲの定理もPMもすべて別物 372 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 07:37:17.25 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 373 名前：１３２人目の素数さん [2012/08/13(月) 07:43:49.69 ] 新フレーゲ主義もフレーゲの定理は関係あり 374 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 08:05:38.50 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 375 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 09:07:03.42 ] Frege systemは証明論 新フレーゲ主義,フレーゲの定理は分析哲学 PMは古典 376 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 10:26:17.52 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 377 名前：１３２人目の素数さん [2012/08/13(月) 11:56:52.27 ] 男の場合、相手が自分よりイケメンでも、金持ちでも、力強くても、頭良くても、女口説くのがうまくても、金稼ぐのがうまくても、 それはそれで辛いことはお互いにわかっています。だから友情も成立します。 有能ということは、利用されるということで、頂点目指す、パワーゲームの中のコマとして綱渡りさせられるということです。 ボルトもカレリンもオバマもプーチンも凄い妥協の上で生きてることは、思いどおりにならない中で死ぬ思いしてるのは誰だって知ってます。 自分に才能ないからと拗ねて駄目になる奴こそが駄目で、互いに限界知った上で居所見つけて頑張るのが男のやるべきことです。 女性の場合は例え美人でも相手があることですから、好きな大切な相手がこちらに好意を持ってくれるとは限らない。確率は増えますが。 また、その相手が浮気もせずしっかり働いて尽くしてくれるかは、博打みたいなもんです。美人の相手が一番成功してくれるかなんか全くわかりません。 また、人間関係というものは顔よりはちょっとした気立てや、合う合わないがいくらでもあります。美人より不美人の方が幸せなことは珍しくもなんともありません。 でも幸せだろうが何だろうが、美人じゃなければ負けですよね。 親が美人に生んでくれなかった瞬間から欠陥品ですよね。 どんなにいい男捕まえてようが仕事で成功しようが幸せだろうが、美人じゃなかったら女として負けですよね。 有能だろうが頭良かろうが性格良かろうが男がよってこようが、成功しようが、ブスだったら駄目ですよね？女としての価値は劣りますよね？ 後は欠陥品の自分をいかに高く売りつけるか。もともと良品美品には劣りますよね。 質問 ・欠陥品としてラベリングされて生きていくのはどういう感覚ですか？ ・絶対かなわない美人とは友達になれますか？あるいはその逆とは。 相手が自分よりは美人でもよくみりゃ自分もそこそこで、 人によっては自分を選ぶ場合には友情は成立すると思いますが、 釣り合いのとれない相手と友情はありですか？ ・どんなに努力しても美人にはかなわないさだめをどう思いますか？ 378 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 12:05:22.56 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 379 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 15:32:56.46 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ' 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' | 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　あなた、ブスね 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 380 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 15:58:22.94 ] PMってラッセルとホワイトヘッドでしょ？ フレーゲの論理主義の思想を受け継いでいるわけだけれども。 論理主義繋がりでいいのなら確かに Basic Law V とかヒュームの原理とかが最近の証明論の研究対象になってる。 381 名前：１３２人目の素数さん [2012/08/13(月) 16:21:40.32 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 382 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/13(月) 16:21:56.58 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 383 名前：１３２人目の素数さん mailto:sage [2012/08/13(月) 20:31:54.45 ] >>380 ヒュームの原理って2階論理で数学を展開する公理ですよね？ どんな風に研究対象になるんでしょうか。 384 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 07:03:31.60 ] 第５原理やヒュームの原理に関する最近の論文↓ （正式にはまだ出版されていないけど） Sean Walsh Comparing Peano arithmetic, Basic Law V, and Hume's Principle dx.doi.org/10.1016/j.apal.2011.12.016 参考文献を辿って他の論文にもあたってみるべし。 385 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 08:13:25.05 ] どっちかっていうと数学の研究としての狙いより 分析哲学としての狙いの方が大きいと思うけどね 386 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 08:18:52.71 ] 数学の研究としての狙いって何ですか？ 387 名前：STS446 [2012/08/14(火) 08:35:18.63 ] そうですね。 証明論におけるフレーゲ原理というより フレーゲ原理の証明論的研究ですね。 メレオロジーにしてもそうなんですけど 研究の動機付けが自然言語的なところからきていて、 数学への興味からきてるわけじゃないんですよ。 既存のペアノ算術とか集合論とか一階述語論理とかの 代替になるような体系の研究はそういうものが多い。 388 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 08:36:45.66 ] 数学への興味って何ですか？ 389 名前：baka描 ◆ghclfYsc82 mailto:age [2012/08/14(火) 08:38:30.71 ] 描 >14 名前：１３２人目の素数さん ：2012/08/07(火) 17:39:00.96 > >>13 > 旧コテ猫あらため描つまりお前自身の事だろ、増田哲也に限り無く近い人間｡ > 筑波大学で痴漢と言えば増田哲也だから連続性も明らかになってるから > わざわざ限り無く近い人間なんて呼び方しなくていいんだけどな > 390 名前：１３２人目の素数さん [2012/08/14(火) 10:24:02.83 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 391 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 14:06:30.16 ] 自然科学であれ経済や哲学であれ他分野からの動機付けがあるというのは 数学理論が無意味な抽象に進んでないことを示す一つの指標。 なければいけないものでもないが、他分野からの動機があるということは その理論の数学としての価値を上げこそすれ、下げるものではない。 少なくとも他分野からの動機は数学としての価値とは独立であろう。 数学的理由（トリビアルだとか既存の一般論に含まれるとか）を挙げて 数学として価値が低いと論じるのならまだしも 他分野からの動機があることを恰も数学として価値が低い根拠のように論じるのは 歪んだ価値観というよりほかない。 392 名前：１３２人目の素数さん [2012/08/14(火) 14:42:45.10 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 393 名前：STS446 [2012/08/14(火) 14:51:14.13 ] 価値が低いなんて言及はない。 数理論理学と体裁が似たものをすべて数学カテゴリーに入れるんだったら、 最近の普遍文法UGや、言語論や、形式的オントロジーなんかも論理学研究ということになるが、 やはり記述論理学DLなんかが数学とはとても思えない。 それは計算論や証明論とは違う。 394 名前：１３２人目の素数さん [2012/08/14(火) 15:26:20.09 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 395 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 15:31:17.30 ] >やはり記述論理学DLなんかが数学とはとても思えない。 >それは計算論や証明論とは違う。 「やはり基礎論なんかが数学とはとても思えない。 それは解析学や代数学とは違う」というのと同じく 自分の主観で「とても思えない」と宣言しているだけだな。 396 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 20:21:20.54 ] S.シャピロの「数学を哲学する」読んでみたら意味が分かると思うけど、 数学的にはトリビアルとしか言いようの無い論理学研究でも 数学の哲学的に意味のある分析をやっていることがあるという場合は 結構あるんだよ。虚構主義とかタイプ理論とかがそういった例に挙げられている。 別に哲学よりだからダメだと言っているわけじゃない。 それにトリビアルだから無価値だ、じゃほとんど同義反復で説明になってないし 数学的価値のあるなしは論理的に説明できるようなものでもない。 397 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 22:18:00.13 ] 質問です 不完全性定理の、他の人が発表したよりエレガントな証明というのは具体的に どういうものなのですか？ それは「ゲーデルコーディングなど編み出さなくても 不完全性定理なんてものは証明可能だったのだよ、へへん」という類のものなのですか？ もしそうでないのならゲーデルは哲学的なものをあくまで勤勉に数学的に扱おうとした 結果として成功したことになりますよね？ 398 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 22:39:54.25 ] 連投すみません 質問はつまり命題の数値化というコンセプト無しであんな定理がそもそも 証明可能なのか、ということです 399 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 23:22:36.86 ] ゲーデル数化/算術化ない証明なんてない。 400 名前：１３２人目の素数さん mailto:sage [2012/08/14(火) 23:53:37.89 ] タブロー法（真理の木）は？ 算術化してないと思うけど。 401 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 01:36:41.05 ] 不完全性定理の証明法の話してるんだよね？ 402 名前：１３２人目の素数さん [2012/08/15(水) 07:44:25.10 ] 第一不完全性定理だけなら 再帰的分離不能からゲーデル数化なしで証明できる。 403 名前：１３２人目の素数さん [2012/08/15(水) 07:47:17.46 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 404 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 09:18:50.79 ] >>396 【道場破り】哲学者の語る数学【殴り込み】とかいって別スレ立てる？ 虚構主義というのはヒルベルトの形式主義そのものに対する批評なのかな？ 例えばリーマン幾何学はその虚構かもしれないけど一般相対論に利用されて 実際に理論の予測通りの現象が皆既日食時に観測されたりしたよ？ 数学が 単なる道具に過ぎないと言うのならともかく虚構というのはどうかと思う。 405 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 09:23:00.31 ] マルティン＝レーフの型理論もトリビアルなんだろうか？ 406 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 09:44:07.99 ] 型理論がトリビアルかどうかを語るのにプログラミング言語は外せないから このスレ行って聞いてみたら？ uni.2ch.net/test/read.cgi/math/1329138054/ 407 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 14:06:43.00 ] マルティン＝レーフが彼の哲学に基づいて型理論を提案した本は 確かに数学的にはトリビアルな内容しかない。 その後彼の型理論が計算機科学や証明論の研究対象になったが そういう研究がトリビアルと言える程に俺は頭よくない。 証明論的にヒュームの原理を分析しているWalshの論文も 同様だろうと断定的にはいえないがそうだと推測する。 408 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 14:22:42.20 ] Intuitionistic Type Theoryの時点でトリビアルでなくなってると思うが。 409 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 14:43:51.94 ] 408は407よりも頭よくないってことだろｗ 410 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 14:48:50.92 ] ITTは体系の定義してるだけの本 数学的な定理と言えるものは皆無 トリビアルとかノントリビアルとか以前の問題 411 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 16:00:32.11 ] >>410 そのことを>>407は「数学的にはトリビアルな内容しかない」と表現したのでは？ というわけで「数学的にはトリビアルとしか言いようの無い論理学研究でも 数学の哲学的に意味のある分析をやっていることがあるという場合」ってことで一件落着ですね。 412 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 16:25:56.90 ] 一件落着って誰か異議唱えていたのか？ つーか>>407は>>391と同一人物だろ？たぶん 哲学の動機を逃げ道にして数学的に下らん研究が大量にあるってのは>>391の大前提で 「だからって哲学の動機を数学的につまらん根拠にするな！」ってことだろ あほなSTSが>>396で仮想の敵に向かって騒いでた 一件落着と思ってるのは当人だけ 413 名前：STS446 [2012/08/15(水) 16:27:39.22 ] マルティンレーフの構成的型理論は 集合論抜きで数学を構築しようという試みだろう。 しかしながら記述集合論の例では一階述語論理と等価な体系で、 むしろそれを自然言語に合致しない部分について制限を加えたうえで、 ウェブセマンティックスに例えばOWLなんかに転用しようとされている。 これが数学や論理学というならば、建築でのJIS規格での強度計算なんかも 数学や物理学となってしまう。 情報科学は形式化の試みが著しい分野であり、 理論計算機以外での形式化には気を付ける必要があろう。 414 名前：１３２人目の素数さん [2012/08/15(水) 17:10:00.89 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 415 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 17:33:24.69 ] >>413 要するに全部工学でしょ。哲学含めてｗ 416 名前：１３２人目の素数さん [2012/08/15(水) 19:06:56.57 ] 型理論はなかなか面白い数学的結果が知られているんだけど （λキューブとか圏論絡みで） オントロジー工学の記述論理は違う。 例えばFLとかALは論理学の理論名ACA_0やZFCとは見た目は同じだが、 言語仕様のまとめという意味合いが強い 417 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 19:21:44.60 ] 要するにお経でしょ。哲学って 418 名前：１３２人目の素数さん [2012/08/15(水) 19:33:41.31 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 419 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 19:39:42.86 ] お暇な方はどうぞ。哲学や形而上学は本来はこういう用途に使うものと思われます www.kt.rim.or.jp/~tro/tubu/tubu-men.htm 420 名前：１３２人目の素数さん [2012/08/15(水) 20:09:53.69 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 421 名前：STS446 [2012/08/15(水) 20:31:53.79 ] 哲学大いに結構でしょう。 バーワイズのウソつきのパラドクスの考察は非常に面白いね。 第二不完全性定理の原因が一階述語論理のタルスキの真偽条項モデルにあるって話とか。 422 名前：１３２人目の素数さん [2012/08/15(水) 21:58:54.41 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 423 名前：１３２人目の素数さん mailto:sage [2012/08/15(水) 22:59:06.76 ] fictionalismってのはハートリー・フィールドって人が提唱してる哲学的立場ね 別に俺が提唱してる訳じゃない 424 名前：１３２人目の素数さん [2012/08/16(木) 05:48:54.55 ] : : : : : :／／: : : : : : : : : :／!! /　＿／　　　　 　 　 　 ∨ : : : : : : : | : : : ／／: : : : : : : : : :／ ヽ|ﾚ', ∧　￣”¨ヽ、￣￣￣　 ∨: : : : : : : !. .:／／ : : : : : : : : : ／-=ﾆ .||/厶≠=- 　 　 ＼ー…=ｧ'´:|: : : : : : : :|i : : : : : : : : : : : : ／/　 ﾑｚ- ､　＼　　　　　　　 ＼.　/ 　 |: : : : : : : :||i .: : : : : : : : : :／　/ 　 |ﾚ’↑i,＼　＼＿_ ＼　　　 �]-=≦: : : : : : : : |! : : : : : : : :／-=7ｆ　/ 〃 / !　}iﾊ＼　＼　＞'ヽ.　　　∨ /|: : : : : : : : || : : : : : ／　　 /亅/ 〃 ,//'　/} |　 )ﾊィj,厶ｯｧ! ＼　　∨小: : : : : : : /! .: : :／ 　 　 /　j/　/　//} _厶=j　 ﾉ} 癶ﾄ=ﾂ | |　|＼　／: : : : : : : : :∧ : : {. 　 　　/　,/　　　//ｲ!i斗ﾓｘ　 　 　 }　　ﾉｲ∨　 / /: : : : : : : : : /∧ : : 》､　　 /　,/　 , ／/ /水ゞｚﾂ　　､　　　　 丿　　/ /: : : : : : : : : : : /∧ : : : ∧／ 　/　 /:/ ｲ／/j　ﾄ､　 　 　 _ _.　　イ　　 ∨ /: : : : : : : : : : :/ : 〉 : : :/ : ＼_,/　 /:/ ／ ./V　i| ,ヘ._　　 ｀　 　 ,:| 　 　 ∨∧ : /: : : : : : : :∨ : : : : : : /ｲ 　 |/{　||,rヘ.|／厶イｲ≧=-　 イ:/　　　 〈ﾍ.　∨: : : : : : : : :|l : : : : : : : :|　　j≧xｲ : : : `ー=ﾆ∠ベ'…ｰ‐v′　　 ／〉ﾍ.　＼: : : : : : :/! .＼: : : : : |　 /: : : : : : : : : : : : : : :≧ ）　.／　 ,．＜　‐＜厶ト､＼: : : //| ..／＼ : : |. /{: : : : : : : : : : : : : : : : :/ ／,．＜＞‐=＝=‐＜.ﾏ: : : : : //ノ '　　　 ＞:! |小.: : : : : : : : : : : : //＞'ﾞ´　 //　　　　　　　　　∨≧=ァ′ . ＞'／ /'|｜ゞ＝一: : : : : /＞',．-=ｘ.　 i/　　　　　　　 　 　 ∨//ﾉ . ／　 / ！|　`'＜.: : : : : 厶イ　　　　 ＼!　　　　　　　　　　　 |//l| / 　 ,/　　|.|　　　 /`'＜/　　　　　 　 　 ∨　　　　　　　　　　 ; :/l| 　　/　 　 |.| 　 　 {　ﾘ　|　　　　　　　 　 ∧　　　　　 　 　 　 /: : l| 425 名前：STS446 [2012/08/16(木) 08:58:07.31 ] 虚構主義とか哲学ごっこしてるんじゃねよ坊や。 論理学はフレーゲの算術の基礎原理と概念記法からはじまった。 厳密には言語記号論と呼ばれる裏論文が17世紀末頃からキリスト教圏を中心に出回っていた。 ブールやドモルガンの活躍のはるか以前だな。 論理主義はフレーゲにより創始されたが ポーランド系概念論理学派の登場によってグチャグチャにかき回された。 そしてS・ブラウンの形式の法則によるブール代数の新解釈・・・。 世界ネットワーク、概念グラフ、意味論ネットワーク、 新フレーゲ主義、ライトの基数オペレータ、記述論理、フォーマルオントロジー・・・。 426 名前：１３２人目の素数さん [2012/08/16(木) 09:16:04.43 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 427 名前：１３２人目の素数さん mailto:sage [2012/08/16(木) 23:12:11.53 ] ZFCの公理のコードを （計算可能なように、例えば閉論理式を文字列として見て辞書順になるように） 並べて{’φi’}（i∈ω） とする。（ここで’a’は┌ a ┐の代用のつもり） 以下簡単のためにψi≡φ0∧φ2∧……∧φi とする。 さらに ’ψi’を満たすモデル M_i |= ’ψi’を取って M_i たちの超積をとり、M とすると、φnを満たさない M_i はn個以下で任意のnに対して有限なので MはZFCのモデルとなる。 つまりZFC |- ∃M ( M |= ZFC) となることが示された。 って議論は、たぶんどこかおかしいと思うんですけど、どこがおかしいんでしょうか。 <i , ’ψi’>_{i} ってただの帰納的関数で具体的にプログラム組めるくらいなので 当然こういう関数は可算モデルだろうが何だろうが最初から持っているはずですよね。 (1) ’ψi’をパラメータとして使うことが許されてもなお、 i の関数として ψi をみたすモデル M_i は取れない？ (2) V と任意の閉文について真偽を等しくするelememtary submodel M 自体は作れるが M が φi を満たすことの証明に公理 φi の使用が必要なので、M がZFCのモデルとなることは示せない？ 細かい事情が分からないので誰か分かる人御教示ください 428 名前：１３２人目の素数さん mailto:sage [2012/08/17(金) 01:48:30.40 ] 巨大基数の初等埋め込みの存在みたいに クラスのモデルが存在するという意味なら ZFC |- ∃M ( M |= ZFC) でも全然問題ないんだけどね 429 名前：１３２人目の素数さん mailto:sage [2012/08/17(金) 06:59:49.57 ] >>427 問題は(1)です。 関数という言葉をどういう意味で使っているのか分からないけれど、 その関数の全域性はZFCでは証明できません。 ω無矛盾と無矛盾の違いと同じことなので、参考にすると良いと思います。 430 名前：１３２人目の素数さん [2012/08/17(金) 08:09:55.00 ] ＞そしてS・ブラウンの形式の法則によるブール代数の新解釈・・・。 単なるブール代数の別表記、しかも読み辛い ＞世界ネットワーク、概念グラフ、意味論ネットワーク、 誰でも思いつくような言葉の図式、概念グラフはベン図よりも弱い ＞新フレーゲ主義、ライトの基数オペレータ、 既に構成的型理論がある、また新しいアイデアではない ＞記述論理、 一階述語論理の別表記 431 名前：１３２人目の素数さん mailto:sage [2012/08/17(金) 08:15:46.54 ] STSの戯言は誰も興味ないからAA野郎と同じくスルーでよい 432 名前：１３２人目の素数さん [2012/08/17(金) 11:24:28.96 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 433 名前：１３２人目の素数さん mailto:sage [2012/08/17(金) 17:00:54.87 ] >>428 モデルが存在したらZFC自身の無矛盾性が証明できるだろｗバカか？ 434 名前：１３２人目の素数さん [2012/08/17(金) 17:43:36.02 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 435 名前：１３２人目の素数さん mailto:sage [2012/08/17(金) 20:32:52.39 ] 良く考えたら M_i の存在を言う段階で公理φ_i の使用が必要なので 一気に全部証明はできませんね。 ω矛盾と事情が同じということは何となく分かりますが、 それでも’ψi’をoracleとして与えられてもモデルの中に i に対応して M_i を作る手段が無いというのは不思議な感じがします 第二不完全性の周辺は（Peano算術でも）私はなかなか直観が働かなくて Loebの定理なども未だに明らかだという感覚がありません 正しそうに思えることの否定が証明できたり 間違ってそうに思えることが証明されていたりするので勉強しないとダメなんでしょうね 436 名前：STS446 [2012/08/17(金) 21:00:01.14 ] >>431 才能への嫉妬というやつか。 俺は既存の計算機科学の研究課題しか書き込んでない。 もし俺のはったりを主張するなら CSの一部研究は否定されなければならないだろう。 437 名前：１３２人目の素数さん [2012/08/17(金) 21:07:01.26 ] 才能（笑い） 438 名前：STS446 [2012/08/17(金) 21:24:13.86 ] >>427 M_iがφ_iのモデルならその超積がモデルになるのは自明。 ＞つまりZFC |- ∃M ( M |= ZFC) となることが示された。 この結論がいきなり出てくるのがおかしい。 439 名前：１３２人目の素数さん [2012/08/18(土) 01:19:59.42 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 440 名前：１３２人目の素数さん mailto:sage [2012/08/19(日) 10:14:56.80 ] こんにちわ。たいかくせんろんぽういがいの、ことなるむげんのうどをつくる ほうほうをみなさんたくさんみつけてください。 しげのり 441 名前：STS446 [2012/08/19(日) 12:01:37.88 ] そうですね。 メレオロジーや形式の法則についてははったりですね。 恐らくそれらについて書かれた書物は存在しない。 なぜならばはったり研究ですから。 もちろん晩年のパースが入れ込んでいた存在グラフについてもそうですね。 それらはブラウンの形式の法則と同じ平面的幾何に論理を落とし込む作業ですね。 フレーゲにしても同様な作業を概念記法や算術の基本性質において行った。 しかしながら量化演算子については現代にも残ったのです。 442 名前：STS446 [2012/08/19(日) 12:06:50.59 ] >>441 いえ、存在しています。 メレオロジーの洋書はありますね。 絶版になって高額で取引されています。 パースの書物は全くないですが、元論文はネット上に全文公開されています。 フレーゲについては全集が出ていますね。 ブラウンについては邦訳がありますね、 大澤という社会学者が訳出していますね。 443 名前：１３２人目の素数さん [2012/08/19(日) 12:52:02.55 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 444 名前：STS446 [2012/08/19(日) 12:58:13.23 ] >>442 確かにそうですね。 しかし私が問題としているのはそういったことではないのです。 我々数理論理学の素人がなぜそういった分析哲学もどきの形式化固執症状にかかってしまうかです。 例えば件の大澤や宮台といった人物も形式化固執に陥って例の形式の法則を訳出しました。 形式化はある種の病気ではありますが、何よりも我々にとって神秘性や本物性をもたらすのではないでしょうか。 445 名前：１３２人目の素数さん [2012/08/19(日) 13:34:09.33 ] 俺「…」妹「…」俺「…」 が途中から 俺「…」俺「…」俺「…」 になるコピペを思い出した 446 名前：１３２人目の素数さん [2012/08/19(日) 14:17:35.00 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 447 名前：１３２人目の素数さん mailto:sage [2012/08/19(日) 14:32:50.65 ] こんなに分かりやすい自演は久しぶりに見たｗ 448 名前：STS446 [2012/08/19(日) 15:10:22.03 ] >>444 やはり不勉強からきているのではないでしょうか。 たとえば私は最近、ファルスの切断とか無限次元Lie環とか グロタンディーク宇宙といった言葉を頭に浮かべてしまいます。 これはこれらのタームが無力的な語感を持つからではないでしょうか。 マルグリスとかアレオパギダとかハインリヒオフターディンゲンとか・・・。 いずれにしろこれらは数理論理学の正確な理解を妨げますからね。 クレパの木とかクレぺリオンとかアロンシャインとか頭を離れない言葉です。 こういったタームに大澤らは感染してしまったのでしょう。 しかしながら初期のロジシャン共はこの世界の原理とかを図式化したかったんでしょうね。 今ではロジックとは計算になってしまいましたが（笑 449 名前：１３２人目の素数さん mailto:sage [2012/08/19(日) 17:38:27.23 ] ブール代数の性質って 0と1の存在、交換則、分配則、 a∧¬a=0、a∨¬a=1の8つと 0≠1から全部導けるらしいがやたら面倒臭いなこれ 450 名前：１３２人目の素数さん mailto:sage [2012/08/19(日) 17:43:54.50 ] 　　　　　　　≫＼ミ三ﾐﾉﾉ／-､ 　　　　／〃〃〃〃〃ヾ≦ミ三ﾐ､ 　　　彡‖‖〃〃从从从ヾヾミﾐﾐ 　　　‖‖‖从从从从从从从》》》 　　 从从‖ﾍ从从从从从从从从ﾐ 　　从: : : :|≡r-ヾヽ､从从从从从ミﾄ 　　ヾ : : : |l　| `・ゝ ﾉr──-､从≪ 　　 ヾ从|!|　 `─‐/　l, `・ゝ }从ト　　　　　　　 ＿＿＿＿＿＿＿ 　　　 ﾉｿﾄ 　　　ゝ・_．〉─-'从ﾄ､＿ノ　　　　／ 　　　　八　　 ,-‐-ﾆｭ､　　 /ヾミ彡　　　　＜　 割とマジでヤンキーになりたい /￣// |: ＼　　 ｀ー‐'　　/(＿　　　　　　　　＼＿＿＿＿＿＿＿ 　‖ﾊ　|　　 '　,,__　　 _ノ/. 451 名前：１３２人目の素数さん [2012/08/19(日) 18:03:46.85 ] 誰だ、お前？ 452 名前：１３２人目の素数さん [2012/08/19(日) 18:23:46.08 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 453 名前：STS446 [2012/08/19(日) 18:45:15.65 ] 今度からはったりやめるわ 数学的に正しいことだけ言う >>449 0≠1はブール代数の定義に入らないよ 実際0＝1は最小のブール代数{0}になる。 それから0と1は補元の略記だから 分配律、交換律、補元の3つだけあれば良い。 454 名前：１３２人目の素数さん [2012/08/19(日) 19:33:13.87 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 455 名前：１３２人目の素数さん [2012/08/19(日) 21:36:11.59 ] >>453 それは流儀の問題だから否定しなくてよい。 456 名前：１３２人目の素数さん mailto:sage [2012/08/19(日) 22:59:46.62 ] というか純粋数学者が書く本でブール代数と定義する場合、 かなり余計な公理が入ってることが多いよね 457 名前：１３２人目の素数さん [2012/08/20(月) 00:31:28.98 ] 層も群とか環の構造要らないしね 458 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 14:57:01.30 ] 質問です 「無限巡回群」は存在しますか 459 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 17:50:10.29 ] 追記です 質問の意図は「もし存在するのならそれは数直線と同じと言えるか」です 460 名前：１３２人目の素数さん [2012/08/21(火) 18:50:52.77 ] >>458 「整数全体の集合は無限巡回群じゃない」と見なしてるの？ 461 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine.co.jp [2012/08/21(火) 19:06:01.11 ] 　お前たちは、定職に就くのが先決だろがああああああああ！！！！！！！！！！！！！！！ 　ニート・無職の、ゴミ・クズ・カス・無能・虫けらのクソガキどもがあああああああああ！！！！！！！！！！！！！！！！！！ 462 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 20:01:34.89 ] >>460 無限加群だと思うのですが巡回群なのですか？ 463 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 20:35:20.96 ] 巡回群の定義書いてみなよ 464 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 22:35:02.44 ] >458 検索ぐらいしなよ。Wikipediaにすら解説あるじゃないか。 465 名前：１３２人目の素数さん mailto:sage [2012/08/21(火) 23:32:37.96 ] 失礼しました。教科書を読み進めて確認もしました。つまり lim[n→∞] Zn という定義でしかないということですか？ 466 名前：１３２人目の素数さん [2012/08/22(水) 00:19:53.76 ] >>465 ただ一つの元で生成される無限群が無限巡回群だ。limitとか不要。 467 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 00:47:06.56 ] 僕は単に整数は無限に伸びているだけだが実数は稠密なうえに無限に 伸びている、みたいなことを考えただけです。腰を入れて勉強します 468 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 00:52:48.72 ] 一般向けの解説書を読んでも正確な理解は得難いと思う 469 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 01:24:53.04 ] 失礼。有理数ですら稠密ですね。もう消えます 僕は高校の時に例の正三角形を使った2=1の証明を知って無限が根こそぎ 嫌いになったいきさつがあって今勉強し直しているところです 470 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 01:25:21.49 ] 数学の式は雰囲気で書いちゃいかんよ >>465とか>>467とか 471 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 06:52:43.29 ] >>469 それが証明になってないことは理解できたのか？ 472 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 09:54:51.20 ] >>471 いえ、どこがおかしいのか今でも理解できていません およそ無限に関わる数学は入試に通るためだけ、単位を取るためだけの 勉強しかしなかったので何ひとつモノになっていません 473 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 10:30:57.20 ] 高校の時の先生は中間値の定理（だったかな？）だけを自明のものとして 他の定理を全て導き出すということをやってくれましたが「どうも腑に落ちない」 と思って聞いていました 474 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 11:00:29.73 ] そんないい先生にあたって、未だその状態じゃ数学向いてないから諦めろ。 475 名前：１３２人目の素数さん mailto:sage [2012/08/22(水) 11:24:32.00 ] 諦めたうえで趣味でやり直してるだけです。もし僕の問題意識に何らかの意味が あるのなら皆さん自由に論文書いてください。僕は何の権利も主張しません 476 名前：STS446 [2012/08/22(水) 11:49:32.35 ] 上で話題になったように、 無矛盾な理論が矛盾したいると証明することができる。 奇妙なことに ロッサー文を使うと、 矛盾した理論の無矛盾性を証明してしまうことが出来てしまう...。 477 名前：１３２人目の素数さん [2012/08/22(水) 22:14:25.35 ] 北田均の「不完全性への道」って本ってトンデモなの？ 以下の様な記述があった。 ゲーデルはゲーデル数化において、メタな自然数nを使って ゲーデル数nを定義してるから、ゲーデルの証明は完全には 統語論的ではない。だからヒルベルトの有限主義を否定することは できない。 これは間違い？ ゲーデルはメタな自然数論の意味に影響を受けた証明を してしまっているとも書いてあったな。 478 名前：１３２人目の素数さん mailto:sage [2012/08/23(木) 01:19:03.15 ] >>477 第二不完全性定理の証明を一度でも読んでりゃ絶対にこんな間違い犯さないんだけどな 479 名前：１３２人目の素数さん [2012/08/23(木) 02:06:14.41 ] 読んだけど理解できなかったんじゃないの？ 480 名前：１３２人目の素数さん mailto:sage [2012/08/23(木) 11:57:56.52 ] p.154 の順序数の不等式が圧巻。 しかも、誤植ではあり得ない。というのは Feferman を引用してあり、 Feferman の論文に右辺の epsilon 0 未満の順序数が現れており、 そこまでの construction で完全になるということが証明されているから。 このバカ先生は、construction が分岐していることを無視、コード化も 無視し、脳内爆発変換の結果、これが Church-Kleene の omega 1 より 大きくなると書いている。私は、沢山のことを理解できず、自分の夢を 語っている大バカだと白状してるのと同じ。 この人、東大で講義してるの？ 481 名前：１３２人目の素数さん mailto:sage [2012/08/23(木) 13:17:25.21 ] なまじっかプロの数学者、しかも東大准教授なだけに、角の三等分家よりもタチが悪いな…… 482 名前：１３２人目の素数さん mailto:sage [2012/08/25(土) 15:27:16.28 ] Walshの論文のステータスが出版になってるね。 この論文で著者のWalshは国際的な賞を貰ってるみたいだね。 www.sciencedirect.com/science/journal/01680072/163 483 名前：１３２人目の素数さん mailto:sage [2012/08/25(土) 18:43:03.83 ] >>482 そう、フレーゲの論理主義の概念は今でもロジックの中で評価されているテーマだということ 484 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 00:56:44.28 ] 直観主義や構成主義の研究が盛んなのに比べて論理主義は地味なのは確かだよな。 もちろん研究が盛んじゃないから価値が低いなんて言ってしまうと 基礎論全般が価値が低いことになってしまうからそんなこと言う気はないが。 485 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 02:21:10.72 ] フレーゲではないけど、論理主義起源ってことでいいのなら 可述性（と非可述性）の研究は盛んじゃないかな？ Predicative やそれに類する単語の入ったタイトルの論文は 毎年大量に出ている。 486 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 11:39:44.02 ] また便乗質問ですが「可述的」と「構成的」の違いって何なのでしょうか？ どちらも人によってニュアンスが違いそうなことは分かるのですが この二つはどういう使い分けがなされているのでしょうか？ 詳しい方がいたらご教示ください。 487 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 16:35:19.72 ] en.wikipedia.org/wiki/Impredicativity 可述的ってのはxの存在を保証するために そのx自身を含む集合Xをxの定義に使わないこと。 ラッセルの逆理などに出て来る集合はこの性質を満たさないので 非可述性が様々な逆理の原因なのではないかと考えられたという歴史的事情がある。 ただし実数の集合Sの上限sup Sの定義なんかも非可述的になってしまうので 可述的な範囲では古典的な数学を展開するには制限が強過ぎると思われていて 構成可能性と違い証明論以外の人が問題として取り上げることはあまり多くない。 488 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 16:50:13.60 ] >ただし実数の集合Sの上限sup Sの定義なんかも非可述的になってしまうので >可述的な範囲では古典的な数学を展開するには制限が強過ぎると思われていて クソワロた。いつの時代の「思われていて」だ？ 未だにそんなこと思ってるのはその後の逆数学の成果も知らないバカのみ。 489 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 17:24:41.35 ] いや逆数学は証明論だろ 490 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 17:28:54.61 ] 自分の無知の言い訳モードに入ったか？ 「思われていて」の主語が非専門家だと言うのは無理がある。 491 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:03:56.45 ] ＞構成可能性と違い証明論以外の人が問題として取り上げることはあまり多くない。 ってのは構成可能性は非専門家の解析学者とかでも気にすることがあるとか 証明論では実数論の可述的部分を研究したりするとか、 そういうこと込みで言ってるんだがな 492 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:11:55.47 ] 無知だと指摘された「...と思われていて」の部分への言い訳に全くなっていない。 493 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:13:40.18 ] 芸風を変えたのか？スレタイ氏 494 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:21:08.84 ] どうでもいいが>>487=>>491(=スレタイ氏?)は 構成可能性(constructibility)と構成性(constructibity)の区別が出来ていないように見受けられる 495 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:22:16.92 ] 失礼、タイポした。 ×constructibity ○constructivity 496 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:34:12.89 ] >>490=>>492 確かに主語をはっきりさせずに「...と思われていて」と書けば 関係する分野の第一線の研究者に思われているという意味でしょうが、 >>487では直後の「証明論以外の人」に思われている、 という意味なのではないでしょうか？ 証明論以外の人が逆数学の結果を一切知らないとも考えにくいと思いますが。 497 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 18:39:22.07 ] 一部を除いて自分と同じくらい無知なはずだってか？ 構成可能性と構成的の違いも知らんほど無知なSTSらしい発想だな。 498 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 19:02:19.08 ] 専門的でマイナーな用法を別にすると、 単にconstructiveは直観主義関係で使って constructibleはゲーデルのL関係で使うというだけじゃないの？ ただ田中尚夫の公理的集合論とか、ゲーデルと20世紀の論理学とかは constructive setを「構成的集合」と訳してるけどね。 細かいニュアンスがどうという以前に使う文脈が違うから 訳語が間違っていると言って問題になったりもしてないはずだよ。 499 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 19:06:01.09 ] あと「構成性」って名詞は日本語としてこなれてない気がするんだよね >>497とかになると無意識に形容詞に変えちゃってるけど 500 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 19:41:16.82 ] 非可述性を避ける為に導入されたのが分岐型理論。 階層αまでに定義された集合を使って定義された集合が階層α＋１をなす。 可述的とはこの階層の外側を考えないこと。 この階層にでてくる集合を構成可能的と呼ぶ。 従って可述的＝構成可能的。 501 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 19:49:17.38 ] >>498 直観主義関係のconstructiveを「構成可能的」と訳した文献はありますか？ 502 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 20:02:50.03 ] 直観主義の「構成的」とゲーデルのLの「構成可能的」は 専門的な細かいニュアンスが重要になるとき以外には 相互に入れ替え可能な言葉だとすると >>487の「可述性」と「構成可能性」の違いの説明は >>500の指摘しているように意味不明では？ 「xの存在を保証するためにそのx自身を含む集合Xをxの定義に使わない」 ってゲーデルのLの説明にもなってしまうんだから。 503 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 20:15:24.30 ] >>491 >構成可能性は非専門家の解析学者とかでも気にすることがある これは本当でしょうか？文献などを教えていただけますか？ 504 名前：STS446 [2012/08/26(日) 20:25:09.50 ] なんか上のが私と勘違いしているようだが違うな。 非可述主義ってのはΠ^1_1以下の階層のことだ。 つまり自然数モデルでの充足可能性とω^CK_1未満の証明の長さが トレードオフできる世界。 逆数学のBig FiveではΠ^1_1-CA_0に該当するな。 ちなみに逆数学は証明論というより再帰理論だな。 実際Big Fiveに対応するチューリングマシンがあるからな。 さて、構成的は排中律の排除。 証明の長さはω^ω未満。 さらに可述主義は一般にε_0未満の証明の長さに対して述べられるな。 だから 構成的⊆可述主義⊆非可述主義 ってのが正しい理解だな。 505 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 20:37:00.12 ] わ、本物のSTSだ！とりあえずスルーで 506 名前：１３２人目の素数さん mailto:sage [2012/08/26(日) 23:24:31.46 ] >>502 なに、無理な言い訳を重ねているだけだろ そんなに追及したらかわいそうじゃないかｗ 507 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 00:36:57.71 ] 素人質問です 面は直線と１対１対応できるが空間は不明という理解で合ってますか もしそうならそれは論理が真か偽かの２値だからですか 508 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 00:42:34.84 ] 面って何？直線って何？空間って何？ それらをはっきりさせてくれないと１対１対応できるかどうかは分からないよ！ 509 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 00:54:40.91 ] 直線は自然数濃度であれ実数濃度であれ一次元のものです 面は二次元のものです。空間は三次元以上のつもりで書きました 510 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 01:00:06.89 ] 追記です 測度論の話で「次元の厳密な定義」というものがあるらしいということは 聞いたことがあります。僕はそれを理解できるほど数学力がありません 511 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 01:17:14.54 ] さらに追記です 測度に関しては最近ようやく少しだけ勉強することができましたが、ひとまずは、 「一匹の蝿が壁に止まっていた。その蝿は部屋の反対側の壁に移動した。蝿が その過程で天井に止まった確率はいくらか」の類だとしておきます 512 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 01:19:39.70 ] 〜の類 へー、有名な例なんですかそれ 513 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 01:27:28.09 ] >>512 www.amazon.co.jp/dp/4875930631/ これで読みました 514 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 02:11:12.54 ] 487の「構成可能性」でゲーデルのLについて言及したつもりは全くありません。 Lを連想する方がこんなに多いとも思いませんでした。 今回、可述主義と構成主義は違うから大雑把に同じ訳語で訳すなと 言いたい方がいらっしゃるのは了解しましたが、 両者を同じものだとして混同していたわけではないです。 私も"constructive"、"constructivism"であれば「構成的」「構成主義」と訳します。 ただ"constructivity"という「名詞」は「構成的であること」と訳さずに 構成可能性と訳すかも知れないというだけです。 似たような話で言うと、holomorphicもregularも私は「正則」であると訳しますが 二つの概念の区別ができていない訳ではないし、 regular expressionは正規表現と訳しますけど、だからといって normal spaceとregular spaceを混同している訳じゃないのと同様だとお考え下さい。 >>501 直観主義に関する日本語の文献は一般啓蒙書を除いてほぼゼロに等しいと思います。 そもそも"constructive"を「構成可能的」と敢えて長くは訳しません。 逆に"constructivity"を「構成性」と訳した文献も無いと思います。 （"constructivism"を「構成主義」と訳した文献ではありません） たぶんほぼゼロに近いのではないかと思いますが。 515 名前：１３２人目の素数さん [2012/08/27(月) 02:56:13.75 ] >>514 「紛らわしい書き方してスマン」で済む話なのに。 516 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 06:24:16.01 ] >>500 つまり ZF+"V=L" は可述主義数学ということですか？ 517 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 06:34:18.93 ] >>514 検索してみると constructivity を構成性と訳した文献は幾つもかかりますよ。 例： 直観主義論理と構成性. 一方、直観主義論理は証明がアルゴリズム的内容を持つことを最大の特徴とする（構成性、 constructivity）。 www.kurims.kyoto-u.ac.jp/~terui/birth.pdf 518 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 06:52:35.21 ] というかLの要素を構成的集合と呼んだりすると IZFとかCZFとかのモノホンの構成的集合論の研究してる人は 困ったりしないんだろうか まあ集合論というよりも証明論の一分野だろうけど 519 名前：507 mailto:sage [2012/08/27(月) 08:04:44.73 ] おはようございます ひとまず自然数濃度であれば３次元以上でも１対１対応がつけられるのか どうかだけでも教えてください。３次元の場合は対角面が正三角形になるのは 想像がつきますが、４次元の場合は立方体になるのですか？ 520 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 09:46:15.89 ] >>507、519 大学２年くらいで履修する素朴集合論の範囲なんだろうが 君の理解は根本的なところでわやくちゃになっている その為質問内容もめちゃくちゃで答えようがない 「リンゴ１００グラムは太陽より甘いですか？」のような 電波な質問になってる 521 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 10:35:47.32 ] >>520 証明論のスレなのは分かっているつもりです。しかし証明論が何故必要 なのかというと連続体仮説に挑戦するためではないのですか？ 522 名前：STS446 [2012/08/27(月) 11:07:22.07 ] >>519 面や空間の積集合を次元と考えるんだったら 自然数は何次元とでも対応できます。 もちろん実数も。 >>521 ファック、全然違います。 証明論はヒルベルトやゲンツェンによる 無限を扱う数学を有限的な記述で体系化する試みから始まっています。 523 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 11:12:56.71 ] >>522も違う種類の電波なので回答を信じないように。 電波が電波に磨きをかけてどうするよ。 524 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 12:47:34.42 ] >>518 IZFは直観主義集合論であって構成的集合論とは呼ばれない。 構成的といえばCZF。最初のCはconstructiveの略だし。 ちなみにIZFのIはintuitionisticなんで、そのまんまだな。 525 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 15:17:00.86 ] >>522 自然数はなんとなく何次元でも対応づけられそうな気がしなくもありませんが 実数は本当に対応づけられるのですか？対応づけられるのですか？ 526 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 16:19:18.55 ] 結果だけ言うとR^3とRは一対一に対応するよ R×RとRとの間に一対一対応があるのだから R^3を(R×R)×Rと考えて、括弧内で一度Rに対応させて再度対応させれば良い 同様にQ^3とQも一対一対応するしZ^3とZも一対一対応する これで分からなかったらちゃんと説明してある本読んでね 527 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 16:42:26.90 ] >>526 いえ、その説明で理解できました。ありがとうございました 528 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 17:13:01.05 ] >>516 ゲーデルのLは確かにラッセルの分岐型理論から来ているので ZF+V=Lを可述的といえないこともないとは思う。 しかし順序数を所与としているのでそこが問題。 つまり可述主義では構成可能階層を ZFCの意味での任意の順序数長さまで延ばせるのか？ということ。 可述的集合論の決定版探しはいまでも決着ついていないと思うけれど 上でちょっと話題になってるCZFやKPωなんかは可述的といわれる。 529 名前：１３２人目の素数さん mailto:sage [2012/08/27(月) 18:44:36.27 ] 可述主義と構成主義が話題になっているみたいなので一言言わせてもらいたい。 上のほうで「構成主義に比べて可述主義はあまり興味を持たれていない」 みたいなことが書いてあったが両者を分けるのはナンセンスだ。 何故なら構成主義の研究では可述性がいつも問題になるから。 >>528が言ってるとおり構成的集合論CZFは可述的だし、 Martin=Loefの直観主義型理論でも可述性は重要なポイントだ。 可述的でないことがIZFが構成的と呼ばれない理由に挙げられるくらい。 だから最初の>>486の質問は鋭いところを突いていて簡単に答えられるものではない。 530 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 10:14:55.93 ] 構成的と可述的が同じ概念で可術的と構成可能も同じとな 推移律より構成的と構成可能は同じになるがもはや禅問答だな 531 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 10:34:31.72 ] 同じとは書いてないだろ。アホだなあ。 532 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 16:24:52.63 ] 普通の数学では選択公理を使うか使わないか、 背理法を使うか使わないかなどは興味の対象になるけど 使う論理式がΠ2、Σ2以上の量化を使うかどうか、 というのは大抵気にしないし、気にしてられないな それに背理法と言われているのは良く見ると否定導入であることが多い 533 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 18:12:15.28 ] 普通の数学でΠ5やらΣ4やら複雑な論理式出てこないのでは？ 基礎論でだって出てくることはないと思う 一般のnに対してΠnとかΣnとか言うことはあっても 534 名前：STS446 [2012/08/28(火) 18:49:37.29 ] 出てくるよ Woodin基数＋αからΣ4以下の理論は連続体仮説偽　とか。 Q＋Σ_10-帰納法 |- Con(Q＋Σ_9-帰納法)　とか。 Δ_1理論の不完全性はΠ_2とかω無矛盾はΣ_3　とか。 535 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 19:00:33.48 ] デムパはスルーで 536 名前：１３２人目の素数さん [2012/08/28(火) 19:15:01.03 ] > STS446 お前自己懺悔して筆を折ったんじゃなかったのか? 537 名前：１３２人目の素数さん mailto:sage [2012/08/28(火) 19:24:26.13 ] 基礎論スレのポッポと呼ぶことにしよう 538 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine.co.jp [2012/08/28(火) 19:45:09.78 ] 　お前たちは、定職に就くのが先決だろがあああああああああああ！！！！！！！！！！！！！ 　ニート・無職の、ゴミ・クズ・カス・無能・虫けらのクソガキどもがあああああああああ！！！！！！！！！！！！！！！！ 539 名前：STS446 [2012/08/28(火) 21:19:39.28 ] 懺悔したのは空間論理（メレオトポロジー）についてだけ まともな内容については書いてくよ 540 名前：１３２人目の素数さん [2012/08/28(火) 22:46:41.53 ] >>539 今度またおカマみたいなクソ懺悔したら承知せんぞ． 性根入れてお前の思うCSの研究課題をまとめて言ってみろ． また口先だけで言ってるのかどうか見てやるから． 541 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 06:16:00.99 ] 741 ： STS446 ： 2012/03/04(日) 22:31:58.43 　　この数学フォーラムに書き込むのはこれで最後にします。 　　以降プログラム技術などのフォーラムに移る予定ですが、 　　恐らくこれからは匿名で活動したりメーリングリストで内輪の活動になると考えています。 　　これまで多くの書き込みを行ったのは、 　　順序構造の研究などに専念されている数学サイドの方々に、 　　計算機・哲学サイドの大局的な視野や物語というものを紹介したかったからでした。 　　それはある意味では成功したし、別の意味では不快感を与えるだけに終わったのかもしれません。 　　しかし現在私が数学サイドの述べる非古典論理（例えば部分構造論理や直観主義論理） 　　の話を耳にするたびに、一般性のない不自然な形式化の仕方に疑問を感じます。 　　しかしそれは皆さんの興味の対象があくまで数学だからなのかもしれません。 　　私には非可算濃度だとか巨大基数だとかは内実のないシンボリック操作としての興味しかありません。 　　やはり論理というよりCoqのような構成的な型体系の中ですべての言語を展開するのが自然に思えます。 　　以上。 542 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 06:17:59.80 ] ＞この数学フォーラムに書き込むのはこれで最後にします。 543 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 13:16:26.66 ] 言っちゃ何だがこの種のキチガイが前言をキッチリ守ったのを見たことがない 544 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 13:19:51.21 ] いや全く 545 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 14:41:04.38 ] まさに鳩ぽっぽだな 546 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 14:53:23.04 ] ネタでもそうでなくても、コテが本物でも偽物でも内容的に詰めればよろしい 547 名前：STS446 [2012/08/29(水) 17:00:35.14 ] 本物だよ。 確かに以前断筆宣言したのは事実だが余りに低レベルな書き込みが多いので、 復活がこのフォーラムのためになると考えた。 メレオロジーやオントロジーみたいな空間系論理が糞ってのは重々承知。 書き込み内容が充実していれば構わないだろう？ 548 名前：１３２人目の素数さん mailto:sage [2012/08/29(水) 17:09:07.30 ] 内容は支離滅裂で充実とはほど遠いぞ そしてお前の書き込みこそレベルが低い、っつーか電波だからそれ以前の問題だ。 549 名前：STS446 [2012/08/29(水) 21:45:55.15 ] >そしてお前の書き込みこそレベルが低い、っつーか電波だからそれ以前の問題だ。 内容が理解できていないだけかと＾＾； 550 名前：１３２人目の素数さん mailto:sage [2012/08/30(木) 13:32:22.39 ] 基地外への対処法はスルーしかないってことだな 551 名前：１３２人目の素数さん mailto:sage [2012/08/30(木) 16:23:55.62 ] そうなんだけど、スルーしてたら鳩ポッポみたいに 自分に都合のいいように「思いを受け取った」とか言い出すからな この手の輩は 552 名前：１３２人目の素数さん mailto:sage [2012/08/30(木) 16:38:19.91 ] 「むしろ叱咤激励だと思って感謝をして今まで以上に」とかなｗ 553 名前：１３２人目の素数さん [2012/08/30(木) 18:22:07.13 ] >>549 >>441-442>>444>>448についての釈明を求める 554 名前：１３２人目の素数さん mailto:sage [2012/08/30(木) 19:02:31.63 ] 相手なんかしたらだめだよ 555 名前：STS446 [2012/08/30(木) 21:58:06.41 ] そうですね、なんだかんだで色々書き込んできましたが、 問題点１：自明のことや大したことでもないことに 専門用語を並び立て飾り立てること。 問題点２：不勉強、理解が浅いから知っていることだけ書き込む。 結果書き込みの内容が支離滅裂になる。 以上2点が問題だと考えられます。 私は上記のような状態を脱しました。 556 名前：１３２人目の素数さん [2012/08/30(木) 23:11:46.28 ] >>555 >>553に答えてない 557 名前：STS446 [2012/08/31(金) 06:58:39.31 ] >>553の意図がわかりませんね 558 名前：１３２人目の素数さん [2012/08/31(金) 08:28:31.81 ] >>557 自演してるから 559 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 10:37:25.24 ] 公園で一人ベンチに座ってるキチガイがブツブツ自問自答してるのを見たことない？ その類だろ。 気持ち悪いので近づかないのが吉。 560 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 17:34:25.01 ] 普通の数学でΠ5やらΣ4やら複雑な論理式出てこないってことでおk？ 基礎論でもΠ5やらΣ4に属する＊具体的な＊論理式は出てこないってことでおk？ 561 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 19:13:43.76 ] 構成的、可述的、更正可能の違いは「簡単に答えられるものではない」で終わりなの？ 562 名前：１３２人目の素数さん [2012/08/31(金) 19:17:40.84 ] >>560 コンパクトとか局所環とかの定義をベタに書けばそれくらい複雑になるでしょ 563 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 19:20:08.34 ] Lの元は構成可能 STSは更正不可能 564 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 19:49:35.75 ] >>562 どういう言語を念頭においているのか知りませんが ZFCだったら冪集合をパラメータにしてΔ0になりますが？ 565 名前：STS446 [2012/08/31(金) 20:10:20.70 ] そうそう 普通の数学がZFCだとするなら 数学の命題はどれも有界量化子文だから。 算術的階層の上の方や解析的階層使いたいなら 算術や2階算術使わんとね 566 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 20:12:30.80 ] STSは更正不可能 567 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 20:27:44.38 ] 通常、群とか環とかの話をする場合、 暗黙の内に想定される言語は決まっていて 群の言語とか環の言語とか呼ばれる。 群や環のelemenaryな性質とはそういう言語で記述可能な性質。 しかし環の局所性はelementaryな性質ではなくその言語では記述できない。 位相空間に至っては暗黙の内に想定される言語などない。 >>562はまず言語を明示するべきではないだろうか。 568 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 21:31:02.38 ] 一般の位相空間論になると、もう集合論が暗黙のうちに仮定されていると 考えないとどうしようもないんじゃないだろうか 569 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 21:50:03.38 ] 位相空間って、集合族に対する公理じゃないの？ 集合の公理無しで位相空間は成立するの？ 570 名前：１３２人目の素数さん [2012/08/31(金) 22:01:48.57 ] >>567 文句は「普通の数学」と言った人に言ってくれ 571 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 22:13:21.80 ] >>570 「普通の数学」と言った香具師に責任はない。Δ0でないと主張したわけじゃない。 責任があるのは「普通の数学」に出てくる論理式が、Σ5とか複雑になると主張した君だ！ 572 名前：STS446 [2012/08/31(金) 22:13:25.83 ] 位相空間はIΣ_1＋Δ^0_1-帰納法だけで十分。 573 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 22:14:38.62 ] また電波のSTS… 574 名前：１３２人目の素数さん [2012/08/31(金) 22:16:46.00 ] >>571 「普通の数学」と言う言葉が厳密ではないから、そんなにきちんとしたことは言わなくても良いでしょ？ 575 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 22:24:53.00 ] >>574 きちんとしいているいない以前の問題だろ？ Σ5論理式がどう表れるのかさっぱり分からない。 576 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 22:48:01.36 ] 素人ですが「普通の数学」とは「不完全性定理の言う不完全な数学」のこと、 ではだめなんですか？ 577 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 22:52:37.74 ] 「きちんとしたことは言わなくても良い」は「滅茶苦茶を言っても良い」と同義ではない。 厳密でない言葉をそれなりに納得できる厳密な意味を与えれば正しい、というものでなければならない。 従って>>562は「それなりに納得できる厳密な」定義を、想定している言語に対して与えられなければならない。 578 名前：STS446 [2012/08/31(金) 23:28:46.22 ] ペアノ算術のω無矛盾性はΠ^0_3 余無限な再帰的可算集合のインデックス全体の集合はΣ^0_3 最小のチューリング次数のジャンプ集合に属する再帰的可算集合のインデックス全体の集合はΣ^0_4 頻出するのだとここら辺位 例えΣ^0_5でもそれより低い階層で表現できる可能性もあるし 579 名前：１３２人目の素数さん mailto:sage [2012/08/31(金) 23:48:17.84 ] >>561 ZFC:　　　構成的−　可述的−　構成可能− ZFC+V=L:　構成的−　可述的−　構成可能＋ KPω:　　 構成的−　可述的＋　構成可能− KPω+V=L: 構成的−　可述的＋　構成可能＋ CZF:　　　構成的＋　可述的＋　構成可能− ?:　　　　構成的＋　可述的＋　構成可能＋ ?:　　　　構成的＋　可述的−　構成可能− ?:　　　　構成的＋　可述的−　構成可能＋ 誰か最後の３つを埋めてくれ。 580 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 00:09:20.71 ] たとえば有界な関数が〜〜と言っただけで、 （実数論として）Σ2の式が出て来るんだから Σ3くらいの量化は普通に考えることになる 実数と自然数の部分集合を同一視する場合はさらに複雑になる 581 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 02:06:29.62 ] >>580 >たとえば有界な関数が〜〜と言っただけで、 >（実数論として）Σ2の式が出て来るんだから 「実数論として」の意味が分からんない 実数構造を「素直」に表現した言語を考えたら 「有界な関数が存在して」とかΣ2以前にそもそも論理式で表現できないし 582 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 02:22:55.86 ] >>577, >>581 分かっている人が説明のためにきちんとしない話をするのと 分かっていないバカ(574=580)がその真似をし電波になっていることの違い がクリアに見出せる例かと。 583 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 04:52:33.01 ] 例えば超準解析で実数体 R と任意の実関数 f たちを付け加えた構造を考えて その上の論理式考えたりするけど、 あんな感じで考えると普通に数学の問題を考えているときの量化の仕方と 形式的な論理式としての量化の複雑さがほぼ一緒になると思うけど。 （あくまで"便宜的に"与えた一例）。 理論が公理化可能じゃないとか素直じゃないとか言われても知ったことじゃない。 言語とか論理式ってのはロジックを一般の数学に応用するときに 便宜的に定義するものであって、応用される側から見たら そんなに本質的なものじゃないと思うんだけどね。 一般的な代数学や解析学では量化の複雑さを制限したりもしないし、 それ以前に言語を敢えて固定してその範囲で議論したりもしないように思う。 しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 定式化がやりにくいのはロジックの表現力がダメだからで、代数学や解析学の責任じゃない。 584 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 06:37:40.34 ] >理論が公理化可能じゃないとか素直じゃないとか言われても知ったことじゃない。 論理式で書けない概念についてΣ2だのΣ5だのって意味をなさないってこと分かってる？ 意味をなさない問題を議論していることになって「知ったことじゃない」じゃ済まないんだが。 （脇道に逸れるが、理論とか公理化可能など全く関係ない。 こいつが理論と言語、公理化可能と言語での表現可能を混同していることが分かる。） >言語とか論理式ってのはロジックを一般の数学に応用するときに >便宜的に定義するものであって、応用される側から見たら >そんなに本質的なものじゃないと思うんだけどね。 本質的でないのはその通りかもしれないが、 それならΣ2かどうかΣ5かどうかの議論はもっと本質的ではないことになる。 議論には乗ってきながら自分が不利になるとその議論の土台を壊すことを人は負惜しみと呼ぶ。 >しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 >定式化がやりにくいのはロジックの表現力がダメだからで、代数学や解析学の責任じゃない。 定式化しづらい性質を考えることについて誰も誰の責任も追及していない。 責任を追及しているのは、しづらい定式化をしないまま （定式化を前提とした概念である）Σ5などの複雑な論理式が出てくると主張したこと。 Δ0で済むと主張する側は、集合論という定式化を与えてそう主張している。 定式化しづらいのであれば、尚の事、具体的な定式化を明示してからΣ2だのΣ5を云々すべき。 585 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 06:51:34.85 ] >>562 その上でもう一度聞きたい。 どのような定式化の下で、コンパクト性や環の局所性がΣ5以上になるのか？ 定式化しづらい概念だからこそ、定式化を暗黙の了解に出来ない。 それ説明しなければ、Σ2だのΣ5だの言っても聞き手にはさっぱり分からない。 586 名前：STS446 [2012/09/01(土) 08:18:18.89 ] >>583 ＞あんな感じで考えると普通に数学の問題を考えているときの量化の仕方と ＞形式的な論理式としての量化の複雑さがほぼ一緒になると思うけど。 私の経験では普通の数学の問題に出現する量化は すべて∊で制限されたΔ^0_1文のみですね。 そうすると形式的な論理式もΔ^0_1になるので、 あなたのΣ2だのΣ5が出てくると言う主張と矛盾します。 ＞しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 実際一階論理の枠組みを超えた命題はあります。 それは大抵「部分集合の全体が〜〜の性質を満たす場合・・・」、 だとか2階の数学的帰納法の不足から生じます。 しかしもしも一階のZFCから展開できないのならば、 その数学的命題は素朴集合論にも基づかないことになりますね。 つまり同時に数学は集合論から展開されないということも意味します。 とはいえ2階のZFCというのもあり、モデルもありますよ。 587 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 08:59:21.46 ] あくまでTh(N)が再帰的に公理化可能でない、という意味での 公理化不可能性について言っているんであって すぐ上に素直なやり方じゃないというレスがあったこともあって 公理化できないことは或る意味で超越的であるということだから その点自然じゃないから不満だというレスが想定されるので書いただけ。 論理式で書けないことと公理化可能なことが同じだと誰が言った？ あのさあ、574≠580だし、俺は「Σ5などの複雑な論理式が出てくる」 とは言ってないんだが…… ちょっと上の方でもそうだったんだが 勝手に別人のレスと俺のレスをくっ付けて 588 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 11:00:54.99 ] 見分ける方法無いだろ。コテハン付けろや。 589 名前：１３２人目の素数さん [2012/09/01(土) 11:55:32.59 ] >>588 めちゃくちゃすぎる 590 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 13:07:07.45 ] >あくまでTh(N)が再帰的に公理化可能でない、という意味での >公理化不可能性について言っているんであって >すぐ上に素直なやり方じゃないというレスがあったこともあって >公理化できないことは或る意味で超越的であるということだから >その点自然じゃないから不満だというレスが想定されるので そんな想定している時点で、何が問題になっているのかまるっきり分かっていないことがバレバレ。 591 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 13:46:07.69 ] >>587 言い負かされそうになると別人ってことにするのは２ちゃんでは常套手段だよね コテハンつけとかなきゃそう言い張っても誰も嘘は見抜けんから 592 名前：１３２人目の素数さん [2012/09/01(土) 14:57:11.97 ] >>591 私は574だから君がめちゃくちゃを言ってることがわかる。 593 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 15:00:59.27 ] とうとうこのスレにもゆとりモンスターが現れたか 594 名前：594 mailto:sage [2012/09/01(土) 16:09:04.19 ] 5=9-4 595 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 17:28:11.86 ] 俺も同一人物説に賛成したいところ。 587は「574≠580」と主張しているってことはどちらか一方は自分だと言ってる。 >>580だとすると「Σ5などの複雑な論理式が出てくる」とは言ってなくても Σ2に言及しているのだから言い訳にならない。 >>574だとすると>>580に向けられた>>581に対して >>583でそんなムキになって反論するのか分からない。 まあもっとも>>590でも指摘されているように おばかなゆとりモンスター君の考えることはこちらの想像の斜め上なので こんな推測は無意味なのかもしれないが。 596 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 17:37:57.25 ] >>595 誰も何も言っていないのにいきなり「〜〜の責任じゃない」とか言い出す香具師の思考回路に関して なんで「そんなムキになって反論するのか分からない」とか幾ら検討を重ねても無意味では？ 597 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 18:29:38.42 ] >>579 CZF+V=L が 構成的＋　可述的＋　構成可能＋ に該当するんじゃない？ CZFでゲーデルのLは定義できないんだっけ？ 598 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 19:50:49.81 ] たとえば微分積分の授業で 各点連続は∀∃∀の形の多重量化を用いて定義するのに対して 一様連続は〜〜と教師が言っていたとして、 　「ちょっと待って下さい、今の場合、どういう言語を想定しているんですか？ 　集合論の言語を想定しているなら今挙げたような複雑な量化は出て来ない事は明らかだ。 　この質問にもし答えられないとしたらナンセンスなことしか言っていないことになる！」 とか言い出したら、もう基礎論キチガイと思われても仕方ないレベルだと思うんだが…… もちろん、明確に特定の言語を想定して居なくても、先生のremarkには十分意味はあるわけで。 599 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 20:22:13.52 ] 結論を出すための努力を放棄している例を出されてもなぁ…… 相手を罵倒するのが目的だろ、これ。 もっとマトモな例は無いの？ 600 名前：STS446 [2012/09/01(土) 20:26:02.76 ] >>598 すいませんが 貴方が例示した各点連続も一様連続も 公理的集合論ではΔ^0_1論理式だということは分かりますか？ そのうえで、それらがΣ2だのΣ5になるだのと主張されているので、 それなら一体どんな体系（言語）において各点連続や一様連続がΣ2だのΣ5論理式になるというのか尋ねているんだと思いますよ。 601 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:08:25.67 ] ＞もう基礎論キチガイと思われても仕方ないレベル わざわざ基礎論スレに出てきて突っ込まれたら逆ギレしてこれかよｗ なんというゆとりモンスターっぷり 「保健所に訴えてやる！」って話も今なら信じられる 602 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:14:28.91 ] 超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん きちんと論理式として表現できてるでしょ それをマトモに感じるかどうかは知らんけど ZFC上Δ0やΔ1であっても、それより弱い理論での量化の階層を考えることには （ロジックとしては）意味があると思うけど。 （尤も普通の数学では事実としてそんなこと一切気にしていない、という流れではあるが。） 一番簡単な例で言うとPeano算術の部分理論のreflectionを考えたりするときに 各階層ごとの真理述語とかを定義したりするでしょ。 ZFCの言明としてはΔ0なんだからそれらの言明も本当はΔ0なんだ、というのは違うと思う。 あと多重量化（つまりΣ2ないしΠ2より複雑な式）は普通の数学に表れるとは言ったが Σ5論理式が現れるなんて言ってないし、そういう例を頑張って探してくるつもりもないからね。 だいたい元から労力がやたら掛かるから言明ごとにこれはΣいくつ、これはΠいくつ、 と分類したりしない、と言う話なんだから。 603 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:23:26.83 ] 560 ：１３２人目の素数さん：2012/08/31(金) 17:34:25.01 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないってことでおk？ 　　基礎論でもΠ5やらΣ4に属する＊具体的な＊論理式は出てこないってことでおk？ 562 ：１３２人目の素数さん：2012/08/31(金) 19:17:40.84 　　>>560 　　コンパクトとか局所環とかの定義をベタに書けばそれくらい複雑になるでしょ このやり取りでは>>562はコンパクト性や局所性は「Π5やらΣ4やら」になると主張していると読み取れるが、 >>602は>>562とは別人だと言いたい？ 604 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:30:55.67 ] ＞超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん ＞あと多重量化（つまりΣ2ないしΠ2より複雑な式）は普通の数学に表れるとは言ったが どう突っ込んで良いのか分からんが、超準解析でやるような言語の設定だと （上付添字なしの）Σ2とかΠ2とかって普通は定義しないんだが。 少なくとも標準的な定義はないのだからΣ2やΠ2の定義を与えるべき。 こういう多種の言語の場合、どの種の量化かが問題になるので Σ^m_nみたいにどの種の量化を数えるのかを上付添字で明示するの普通。 >>580は別人なのか本人なのか知らないけど、それを見ていると そういうこと全く分かっていないで書いてるな、ということがよく分かる。 605 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:53:06.62 ] 570 ：１３２人目の素数さん：2012/08/31(金) 22:01:48.57 　　>>567 　　文句は「普通の数学」と言った人に言ってくれ 571 ：１３２人目の素数さん：2012/08/31(金) 22:13:21.80 　　>>570 　　「普通の数学」と言った香具師に責任はない。Δ0でないと主張したわけじゃない。 　　責任があるのは「普通の数学」に出てくる論理式が、Σ5とか複雑になると主張した君だ！ 574 ：１３２人目の素数さん：2012/08/31(金) 22:16:46.00 　　>>571 　　「普通の数学」と言う言葉が厳密ではないから、そんなにきちんとしたことは言わなくても良いでしょ？ このやりとりでは>>574と>>570は同一人物を推測できるが >>570は最初に「普通の数学」という言葉を出した>>532ではない顔をしている。 そしてゆとりモンスター君は>>574か>>580のいずれかだと>>587で主張しており >>580の方だとすると言い訳にならないので>>574なのだろう。 ところがゆとりモンスターは>>602で 「だいたい元から労力がやたら掛かるから言明ごとにこれはΣいくつ、これはΠいくつ、 と分類したりしない、と言う話なんだから。」と自らを>>532だと認めている。 何が言いたいかというと、都合が悪くなると別人の振りしている疑いが濃厚だということ。 606 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:03:29.65 ] >>602 Σ2とかΠ2とかは、sort(種)が一つの言語に対して定義するもの だから many-sort(多種)の言語では例にならないんだよ いや>>604と同じことなんだが 607 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:20:57.73 ] 俺様定義でしかないのに標準的な定義だと勘違いして 断りもなく俺様定義で話を続けるってのは素人と駆け出しにはよくあること。 608 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:41:25.97 ] 超準解析って型理論とかmany-sortedな言語による定式化しかないんだっけ？ 609 名前：STS446 [2012/09/01(土) 22:50:46.21 ] many-sortedや二階算術やNFやZFC^2ならΣ^1_nとかΠ^1_nになるだけ。 610 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 23:09:20.71 ] >>608 そりゃone-sortedに直したければできるだろう。 問題は、「超準解析で表れるような」と言っただけで 特に断りもなくone-sortedの言語を考えられるかということだろ。 こういうのはone-sortへの直し方次第でかなり変わってくるんだし。 611 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 00:17:41.65 ] 実数とか実数上の関数とかその関数とかをone-sortで表現する方法って集合論以外に有名なものある？ 通常のmany-sortをone-sortに書き換えたら、もう殆ど集合論と同じ代物だよね。 超準解析でもIST(internal set theory)とかあるけど、完全に集合論だし。 いずれにせよ標準的でないないし有名でない定式化を使うのなら説明が必要。 その説明をしようともしないで俺様用語法で教皇突破しようとするからゆとりモンスターと呼ばれるんだ。 612 名前：喜田だ mailto:sage [2012/09/02(日) 00:35:40.79 ] フーリエ積分作用素について語ろうよ 613 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 01:55:35.51 ] 基礎論スレでフーリエ積分作用素の何を語るっていうんだい？ 614 名前：１３２人目の素数さん [2012/09/02(日) 02:24:31.96 ] 実部・虚部ともに有理数の複素数と自然数は1対1に対応する。 その対応をFとしてF(n)がジュリア集合に入っているようなn全体の集合の算術的階層はどこだろう。 Fはそんなに複雑でなければ本質的な問題にはならないよね。 615 名前：STS446 [2012/09/02(日) 06:09:01.49 ] >>614 Δ^0_1 desuyo 616 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 07:36:23.36 ] たとえばユークリッド平面幾何でいうなら 〜〜は直線である、〜〜は点である、というような述語を用意して 対象領域は一つにしてしまうone-sortedな方法と、 それぞれの対象領域を別に用意するmany-sortedなやり方がある。 こういうのを「集合論と同じ代物」とは言わないんじゃないの？ 外延性公理やら分出公理やら選択公理やら冪集合の公理やらがあるわけじゃないんだし この例じゃなくてもmany-sortedとone-sortedの相互変換は同様に出来る 617 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 08:20:54.38 ] ついでにはっきり言っとくと普通の数学だと Σ_4^ZFとかΠ_5^ZFとかそういう性質は 滅多に出て来ないだろうね。たぶん。 618 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 14:15:16.50 ] >>616 だから公理とか公理化とか関係ないって言ってるのに あふぉだなー 619 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 16:31:33.89 ] >>616 実数、実数値関数、実数値関数の関数などのsortを持つ言語にそのやり方を適用しちゃうと 「関数である」とか複雑であるべき式が原始論理式になってしまうよ？ しかも高階の量化（関数量化）も低階の量化（実数量化）も区別せずに数えてΣnを定義するわけ？ もちろんそう定義するのは自由だけど、断りなしに「Σ2」とか言われて想像できるような 標準的な言語でないことは確かだよね。 それともまた別人だと主張するのかな？ 620 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 16:57:09.12 ] なんで「関数である」が複雑である「べき」なのか理解できない 621 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 17:22:44.65 ] どうして 「問題は、「超準解析で表れるような」と言っただけで 特に断りもなくone-sortedの言語を考えられるかということだろ。 こういうのはone-sortへの直し方次第でかなり変わってくるんだし」(>>610) とか 「いずれにせよ標準的でないないし有名でない定式化を使うのなら説明が必要。 その説明をしようともしないで俺様用語法で教皇突破しようとするからゆとりモンスターと呼ばれるんだ」(>>611) とか 「もちろんそう定義するのは自由だけど、断りなしに「Σ2」とか言われて想像できるような 標準的な言語でないことは確かだよね」(>>619) とかに反論しないの？無理やり作った例を幾らあげても意味ないよ。 622 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 19:06:48.95 ] 普通に数学（たとえば実解析やらRiemann幾何やら）をするときに 量化の複雑さによって性質を区別したりしない、という発端から来てる話で、 たとえば各点連続は実数値のみに関する∀∃∀の形の量化だとか そういうことを言っているのに、なんでZFCとか二階算術とかの体系の話にしようとするのさ ロジックだとよくそういう体系で論理式の複雑さを制限して議論するのは知ってるよ。 でも今はそういう話はしていないし、 個人的には普通の数学者は実解析をやるときに量化の複雑さは気にしないというときに どの形式体系についての量化の複雑さを考えないのか、という疑問の持ち方がおかしいと思う 623 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 19:55:51.50 ] >>622 >たとえば各点連続は実数値のみに関する∀∃∀の形の量化だとか >そういうことを言っているのに これは実数論の言語を使ってもΠ3だ。 （集合論以外の）標準的な言語ではΣ2ともΠ2ともいえないような例を >>562や>>580で挙げたからこんな問題になっているんだろ？ どさくさにまぎれて例をすりかえるなよ。 624 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:23:43.01 ] 532 ：１３２人目の素数さん：2012/08/28(火) 16:24:52.63 　　普通の数学では選択公理を使うか使わないか、 　　背理法を使うか使わないかなどは興味の対象になるけど 　　使う論理式がΠ2、Σ2以上の量化を使うかどうか、 　　というのは大抵気にしないし、気にしてられないな 　　それに背理法と言われているのは良く見ると否定導入であることが多い 533 ：１３２人目の素数さん：2012/08/28(火) 18:12:15.28 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないのでは？ 　　基礎論でだって出てくることはないと思う 　　一般のnに対してΠnとかΣnとか言うことはあっても 560 ：１３２人目の素数さん：2012/08/31(金) 17:34:25.01 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないってことでおk？ 　　基礎論でもΠ5やらΣ4に属する＊具体的な＊論理式は出てこないってことでおk？ 562 ：１３２人目の素数さん：2012/08/31(金) 19:17:40.84 　　>>560 　　コンパクトとか局所環とかの定義をベタに書けばそれくらい複雑になるでしょ 580 ：１３２人目の素数さん：2012/09/01(土) 00:09:20.71 　　たとえば有界な関数が〜〜と言っただけで、 　　（実数論として）Σ2の式が出て来るんだから 　　Σ3くらいの量化は普通に考えることになる 　　実数と自然数の部分集合を同一視する場合はさらに複雑になる 625 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:24:34.38 ] 最初の>>532だけの段階では>>622の言うとおり 「普通の数学者は実解析をやるときに量化の複雑さは気にしないというとき」 といえるかもしれない。 しかしそれに対するレスやそのまたレスを踏まえるとそうではない。 これらレスと超訳すると以下のような感じ。 >>532「普通の数学では複雑さは気にしないし気にしていられない」 >>533>>560 「細かく見てみたらΠ5やらΣ4に行くものはないんじゃない？」 >>562 「いやコンパクト性や局所性はそれくらいになる」 >>580 「ほら実数論ではこんな単純なものでもΣ2になる」 言語もはっきりさせずに「Π5やらΣ4に行くかいかないか」 「単純なものでもΣ2になるかならないか」を議論すべきだというのか？ 626 名前：１３２人目の素数さん [2012/09/02(日) 20:29:49.34 ] >>623 完備距離空間なら、Xがコンパクトとは、任意のε＞0に対してXの有限集合{x_1,…,x_n}があって任意のx∈Xに対して1≦k≦nが存在してxとx_kの距離がε未満、ということだから∀∃∀∃だね。 627 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:44:05.30 ] 実数論の言語では「有限集合{x_1,…,x_n}があって」は表現できないと思うんだ 628 名前：１３２人目の素数さん [2012/09/02(日) 20:46:26.98 ] >>627 実数論に限定する理由は？ 629 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:51:44.67 ] 実数論でなくてもいいけど言語を決めないで∀∃∀∃と言っても意味ないでしょ。 ある言語では∀∃のものがある言語では原子論理式になったりするんだから。 まず議論の前提をはっきりしようや。 630 名前：629 mailto:sage [2012/09/02(日) 20:52:37.36 ] 6=2*√9 631 名前：632 mailto:sage [2012/09/02(日) 20:53:36.40 ] 6/3=2 632 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:15:09.54 ] ほんとにこいつゆとり君だなー 633 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:21:17.60 ] >>622は言語を指定するのを諦めたように見えるが 超準解析がどうのと言ってたのは撤回したんだろうか？ 634 名前：１３２人目の素数さん [2012/09/02(日) 21:57:23.91 ] >>629 じゃあ数学の教科書で∀とか∃とか書いてあるのは意味無いの？ 厳密じゃないというのならわかるけど 635 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:59:03.78 ] あふぉはもはやスルーしかなさそうだな 636 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:01:23.00 ] >>634 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 637 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:32:26.15 ] 局所環の例は俺が挙げた例じゃないから知らない そもそもイデアルやら位相をどうやって述語論理で扱えば良いのか知らない 少し解析になれれば「充分大きな M があって x, y < M のとき〜〜」というだけで、 理解がより困難になったりはしないが、これだってきちんと言うと 「∀N∈R. ∃M∈R. N＞M ∧ ∀x, y. x ＜M∧y＜M⇒〜〜」 なので、 すぐΠ3くらいにはなる。 有界な関数がどうのこうのと書いたときに言いたかったのはこういう感じの事で、 三重量化、四重量化はざらにあるということ自体は正しいと思っている。 関数の話になると確かにどういう量化なのかが不明瞭なのでこの例は取り下げる。 638 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:50:11.26 ] 「普通の数学」では一階論理で「定式化をしづらいような性質・対象も平気で考える」と言っていたのに、 今度は定式化しやすい性質・対象だけ考えることにしてその範囲の言語を持って来てΠ3だとかってか？ 随分と都合のいい話だな、おい。 639 名前：１３２人目の素数さん [2012/09/02(日) 22:59:26.27 ] >>533は普通の数学で論理式の話としてΣとかΠを出して来てるんだから、完備距離空間でのコンパクトの定義を出してきても問題ないじゃん。 「一見そう見えるけど実はそう簡単にはいかない」という話ならわかるけど。 640 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:06:22.94 ] >>637 あんたΠ3やΣ3と三重量化を混同してるんじゃないか？ Δ0には有界量化が何重にも入っているんだお 641 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:15:06.67 ] そうそう、言語がはっきりしてなければ有界量化が何なのか分からないのだから そもそもΣnの定義が定まらないよね。 642 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:30:59.86 ] >>639 >完備距離空間でのコンパクトの定義を出してきても問題ないじゃん。 誰かがその定義が問題だなんて言ったのか？ 言語をはっきりさせずにその定義が∀∃∀∃と言ったのが問題なんでしょ。 そんな調子なら、いい加減、俺も他の人と同じくスルーするよ。 643 名前：STS446 [2012/09/02(日) 23:37:23.00 ] 公理的集合論では>>626や>>637などの例にある数学的命題はΔ^0_1と同等になる。 算術的階層が単なる論理式中の∀と∃の交互の繰り返し回数だと誤解しているのではないだろうか。 集合論では数学的命題は∃ｘ∊ｙR(ｘ)のようになったりするが、 R(ｘ)がΔ^0_1なら、∊による有界量化したものも原始再帰的になるのである。 算術的階層がなぜ算術的とよばれるか考えてみるべきだろう。 644 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:12:23.01 ] >>640,>>641 算術や集合論では確かに bounded quantifier はΔ0に自由に表れていいわけだけど モデル論で出てくるような言語（実数閉体の理論など）で定義するときは Δ0は量化のない論理式とすることが多い。 言語がはっきりしなければどっちの流儀を採用するのが普通なのか判断できない、 ということなら全くもってその通り。 やっぱり言語を明示せずΣいくつと言うのは問題あり。 645 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:37:02.60 ] >>640 ZFCにおける論理式の階層の話は（私は）してない あなたはその話をしているのかもしれないけど 646 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:39:26.39 ] というか普通の数学では言語をはっきり固定して議論しない、 がFAかと イデアルの昇鎖列が有限ステップで止まるといったときに そんなことを考えるのはルール違反だという訳にもいかんし 647 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 01:59:13.76 ] >>645 それでどの言語で論理式の階層の話をしているんだい？ 「ZFCではない」以上のこと何も言ってないよね？ それじゃΣとか言っても意味をなさない >>646 んじゃ普通の数学の議論で出てくる概念をΣいくつとか言うのも無意味 がFAだろう 648 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 02:06:57.53 ] 言語を固定させないことにはΣnは意味をなさない って当然のことがなんで分からないのかが分からない 649 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 06:05:33.58 ] >>646 「超準解析で表れるような」実数、実数値関数などなどのsortを持つ言語で十分だろ？ 「普通の数学」では量化は全部タイプがついているんだから。 通常の数学はmany-sortなのに、Π3とかΣ2とかone-sortを前提にした用語を不用意に使ったのが問題なだけ。 自分の不用意発言を根拠に「普通の数学では言語をはっきり固定して議論しない」とか勝手に結論出すなよ。 650 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 08:12:18.90 ] 646はイデアルの話をしているけど 極大イデアルとかを別のsortで扱っても、かなり集合論的な議論を 援用せざるを得ないようになると思うよ 位相空間論を一階述語論理で取り扱う困難とそんなに変わらないと思う 651 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 18:07:15.68 ] イデアルの議論なんて二階の言語で十分表現できる。 （逆数学でイデアルが難なく扱えるのと同じこと。） 二階の言語は元のsortとそれら元の集合のsortを持つmany-sorted言語だから その意味では確かに「集合論的」なのかも知れないけれど、 階数によるsortの制約が全くないZFのような本格的な集合論は必要ない。 652 名前：STS446 [2012/09/03(月) 19:22:45.50 ] 2階の言語って普通は2階述語論理のことですね。 多領域論理は普通、型の概念が定義されていませんから1階論理ですね。 特に多領域論理で2階算術と呼ばれる体系は「集合論的」ではなく「解析的」とよばれますね。 2階算術の論理式は解析的階層でΠ^1_nとかΣ^1_mとなりますから。 653 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 07:05:44.67 ] もりさがっとるな 654 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 10:33:58.56 ] 　Maximal ideal あるいは Prime ideal の全体を考えれば、３階になる。主イデ アル環に制限しなければ　Zariski topology を使えないことになる。２階算術に 制限するのは無理がある。逆数学はまあそのへんでよいということなのかも 知れない。 655 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 11:11:06.57 ] すみません、また質問です >>466がこないだ理解できたのですが、 半直線と円は自然数として同一視するのですか？ 656 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 12:05:39.87 ] いくらゆとりでもいい加減スレ違いなことを悟れ 657 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 12:36:41.21 ] 独学で勝手に数学を勉強している者や、計算機工学の後で数学を やり直している者はどのスレで質問すればいいですか 658 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 13:15:11.31 ] つ　雑談スレ 659 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 13:31:37.33 ] >>658 なぜですか？ 660 名前：ＳＴＳ446 [2012/09/05(水) 16:15:37.87 ] よく再帰理論とかで高い算術的階層が出現するが、 これらを記述する言語は一体何なのかという疑問はある。 内包公理や帰納法はどうなっているのか。 そう考えると今回のような混乱は当然の思える。 おそらくは再帰的クラスや再帰的枚挙可能クラスの関係を基準として、 この関係にいくつ量化子をつけていくかと言う事だろうが、 この量化子は「ある〜」「すべての〜」といった自然言語、 つまり通常の数学で使われる議論の略記なのだろう。 この通常の数学での略記が形式的体系での記号と誤解されることで 今回のような議論が生じた。 661 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 17:23:50.04 ] >今回のような議論が生じた。 って、自分がその議論の中で完全に相手にされてなかったってことに気づけよ 662 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 17:35:32.22 ] >>654 >Maximal ideal あるいは Prime ideal の全体を考えれば、３階になる。 ３階の元一つ考えるだけなら３階量化は必要ないので２階で十分。 問題なのはMaximal ideal あるいは Prime ideal の全体の部分集合を走る量化がある場合。 そういう例としてZariski位相を挙げたんだろうけど、基本開集合が単純な形をしているので 開集合や閉集合上を走る量化も実際には２階の言語で十分表現できてしまう。 663 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 20:34:06.32 ] 代数幾何とか微分幾何とかをやる場合に二階「算術」で行うのは人工的な制限だと思う 664 名前：STS446 [2012/09/05(水) 23:38:56.56 ] 実際に二階算術じゃ扱えないコホモロジーとかもあるんよ。 Big Fiveも元々は算術的階層の強さ毎に帰納法と内包公理をQに加えていった結果生じている。 これらがたまたま集合・位相〜解析学の基本定理の強さ程度だったってわけさ。 もし1階算術サイドに話をすすめるなら内包公理は不要で、 帰納法の制限や帰納法の形態の種類によって QとPAの間に限定算術的階層と呼ばれるものが生じる。 2階算術の場合は、Qを内包公理で2領域に分離して拡張したものだな。 3階算術ならば2つ目の分離公理か3つの領域を同時に扱うような公理が必要になるな。 いずれにしろこれらは論理における高階とは違う。 領域が無数に分岐することで見かけ上どのような数学命題でも記述可能に拡張可能。 実際3階算術や高階算術なんかも研究されている。 665 名前：STS446 [2012/09/05(水) 23:56:58.89 ] >>664 とはいえ、もともと二階算術ってのは「人工的」なものなのですよね。 どれだけ算術を強めればどれだけの定理が証明可能か。 数学のある命題にはどれだけの公理の強さが必要か。 それを集合論のような複雑なものではなく、 古典数学的な簡素な公理である必要がある。 それらはダイレクトに再帰理論的な研究対象だからね。 まぁ代数幾何とか微分幾何レベルまで巨大化した世界には余り向かないね。 666 名前：STS446 [2012/09/06(木) 00:01:51.26 ] >>665 というより、そもそも数学の命題を テキスト通りそのまま論理式にするのがナンセンスなんだよね。 ダミー量化子使えば算術的階層なんて無限に引き上げられるし、 そもそも集合論的命題はほとんどが論理的に同値なΔ^0_1文が存在するしね。 667 名前：１３２人目の素数さん [2012/09/06(木) 00:25:21.71 ] >>666 自分との対話やめい 668 名前：１３２人目の素数さん [2012/09/06(木) 00:29:11.81 ] >>665の ＞それを集合論のような複雑なものではなく、 ＞古典数学的な簡素な公理である必要がある。 ＞それらはダイレクトに再帰理論的な研究対象だからね。 ここの文意が通らない。書き間違えですか？ 669 名前：STS446 [2012/09/06(木) 01:44:19.17 ] 訂正させてもらうと、 古典数学的に簡素な公理である必要があるのは、 再帰理論的な研究対象として扱えるようにするため。 例えば算術的階層に理論をはめ込むために、 帰納法をΣ_n文といった具合に制限している。 これは集合論では使えない手法 670 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 02:23:24.01 ] >>663 この話になった>>649から直前の>>662までよく読んでみな。 「二階」という言葉は出てきているが誰も「二階算術」とは言っていない。 （STSをスルーしていないのなら別だがｗ） >>651が二階の言語の例である二階算術を使う「逆数学」に言及しているが 「...のと同じこと」と距離をおいた書き方をしている。 >「超準解析で表れるような」実数、実数値関数などなどのsortを持つ言語で十分だろ？ という話から「二階」が話題になっているのだから、 「二階実数論」を想像するのなら分かるんだが、 どこから二階算術が出てきたんだ？ 二階の言語なんてどんなものにも定義出来る。 イデアルの話をしたければ通常の環の言語の２階拡大で十分。 671 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 03:03:19.58 ] Spec R（R:可換環）に位相を入れる話が それで自然にできる？ 672 名前：１３２人目の素数さん [2012/09/06(木) 04:39:40.73 ] umu 673 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 05:28:08.30 ] >>651 ｘが集合のときｘ∪{ｘ}も集合って、集合の直観に合ってる？ 「要素も集合」より要素と集合がはっきり分かれている方が「集合論」として自然でない？ 674 名前：STS446 [2012/09/06(木) 07:36:43.77 ] 二階算術は普通は2階の言語とはよばんゃろ。 2階の言語ってのは命題自体を量化可能な言語を言うんであって。 つまり命題を量化可能な2階述語論理のことやな。 二階算術は多領域論理の一種としてみられる。 高階算術で型理論が使われているが これは領域の分類のための識別子として用いられている。 675 名前：STS446 [2012/09/06(木) 08:13:42.50 ] 2階算術なんかは本来は2階の言語とかではなく Γ^1_n級とかいう。（ΓはΣやΠやΔの一般化） 3階算術ならΓ^2_n級、ｎ階算術についてΓ^(ｎ-1)_n級になる。 例えば2階算術で有名なBig Fiveは、 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_1-分離公理 ほら、かなり人工的だろ？ 公理の重複を許して同値な体系に置き換えてみるともっとよくわかる。 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理＋Σ^1_1-分離公理 ほら人工的だろ？ ちなみに Q＋Σ^0_n-帰納法 だけなら限定算術のIΣ^0_nになる。 帰納法は厳密には4種類あって、BΣ^0_nなどになったりする。 676 名前：STS446 [2012/09/06(木) 08:15:45.39 ] >>675訂正 ＞3階算術ならΓ^2_n級、ｎ階算術についてΓ^(ｎ-1)_n級になる。 　3階算術ならΓ^2_n級、ｎ階算術についてΓ^2_(ｎ-1)級になる。 677 名前：STS446 [2012/09/06(木) 08:33:44.30 ] ちなみに体系の同値性を≡であらわすと以下の等式が成り立つ。 Π^0_1-分離公理 ≡ Σ^0_1-選択公理 ≡ Σ^0_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Σ^0_1-分離公理 ≡ Π^0_1-選択公理 ≡ Π^0_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Π^2_1-分離公理 ≡ Σ^2_1-選択公理 ≡ Σ^2_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理 いやぁ中途半端で不思議な定理だよね。 帰納法とか内包公理とか選択公理とか従属選択公理とか分離公理なんてのはこうやって定量化するんだよね。 678 名前：STS446 [2012/09/06(木) 08:35:51.26 ] >>675訂正 ＞Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 ＞Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理＋Π^1_1-内包公理 679 名前：STS446 [2012/09/06(木) 08:42:13.96 ] >>673 あんたは集合論で冪集合使わんのか？ 680 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 17:58:38.80 ] ぽっぽの意味不明なカキコミを禁止する方法はないものか 681 名前：STS446 [2012/09/07(金) 07:15:41.68 ] とはいっても算術的階層とか解析的階層とかって あんまり論理式を測る尺度として優れているとも思えんのだけれどもね。 そこから何か非自明な結果が出てきたともきかんしねん。 682 名前：STS446 [2012/09/07(金) 18:32:20.04 ] >>680 意味が分かるように日々学習を怠らないって選択肢は考え付かないかな？ まずは再帰理論もしくは計算論という名の分野の学習を薦める。 CooperのComputable Theroyって本が出てるから良かったら買うと良いよ。 日本語のPDFでも結構東北大の田中さんがいいものを書いてるから読んでみな。 最終的には相対化された算術的階層などが登場する。 言語の階層の最下部には計算量理論が存在していて チョムスキー階層や多項式時間階層や非決定性の時間空間階層がある。 上に行くと原始再帰的クラス、一般再帰的クラスがあり、 ここから算術的階層がはじまって上に行くにつれてウルフラムの階層や 限定算術的階層やらブール階層やらが登場、 やがて解析的階層に突入してそれらが様々な理論に相対化されてゆく。 そこから上はどれだけ強力な理論を使うかに依存しており、 公理的集合論だとかさまざま巨大基数の追加した体形への相対化が考えられ、 やがて最高峰に矛盾した体形への相対化が存在する。 有限モデル理論における記述計算量理論とかも覚えておくと良い。 PvsNP問題を限定算術的階層に対応させて解決しようと言う試みもある。 日々精進、自戒とアドバイスの二重の意味を込めてね。 683 名前：１３２人目の素数さん mailto:sage [2012/09/07(金) 20:21:04.83 ] いや普通の人は自分と会話したりしないから 684 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 07:35:16.45 ] 少し前に様相論理に関して自信満々に語っていた内容は致命的に間違っていると ものの見事に論破されていた。 それに懲りずにまだ自信満々に自説を偉そうに語っていたら 誰もその内容を信用しないだろうし、 誤りを見つけても誰もわざわざ指摘しようとは思わないだろう。 名前欄の「STS446」は「スルー対象」を表すマーカー。 685 名前：STS446 [2012/09/08(土) 16:07:05.83 ] あとリンドストルムの量化子とかもでとらんかな。 本当は決定可能クラスってのもかなり複雑に入り組んでていて、 ま、説明しがたいほど広大なんだけどね。 AC^0＝FO＝DTIME(log(n))⊆ThC^0⊆NC^1⊆DSPACE(log(n))＝L＝SL ⊆DSPACE(log(log(n)))⊆NSPACE(log(n))＝NL⊆sAC^1⊆AC^1⊆NC ⊆P＝Π^P_0⊆NP＝Σ^P_1⊆PH⊆PSPACE⊆EXPTIME⊆EXPSPACE ⊆Δ^0_0 これは分岐を省いた簡単な階層だけど これが実際はPPとかBPPとか#Pとかそれらの相対化とかが絡んだりして 複雑な階層を構成しているんだ。 もちろん当初の形式言語も本当は チョムスキー以外の階層があることが知られているんだよ。 Type0＝Σ^0_1＝RE⊆Δ^0_1＝R＝RE∩co-RE＝CLH1⊆Type1＝IL⊆CLH2⊆Type2⊆Type3 とにかく世界は広大でその分類は難しいんだ。 686 名前：STS446 [2012/09/08(土) 16:09:36.88 ] おっと逆だった、すまない。 訂正 ＞Type0＝Σ^0_1＝RE⊆Δ^0_1＝R＝RE∩co-RE＝CLH1⊆Type1＝IL⊆CLH2⊆Type2⊆Type3 Type0＝Σ^0_1＝RE⊇Δ^0_1＝R＝RE∩co-RE＝CLH1⊇Type1＝IL⊇CLH2⊇Type2⊇Type3 687 名前：STS446 [2012/09/08(土) 16:15:31.75 ] それから注目すべき点は Σ^0_1以降から圧倒的に形式体系の表現能力が拡張される点だね。 算術って言うとΔ^0_1を超えちゃう、つまり決定不能になるんだけど それで高階の算術という解析的階層が出現する。 でも集合論の登場、つまりレヴィの階層と呼ばれる、 ZFなどに相対化された形式的な階層は遥かに高い表現能力を獲得するんだ。 最頂点の矛盾した体形への相対化へと向かって世界は広がっていく。 現実の物理学的な世界なんかをはるかに引き離してね！ 688 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 17:20:52.18 ] つーかSTS氏は自分で「専門書をちらっとかじっただけでろくに理解してません」って自分で暴露してなかったか？ 689 名前：STS446 [2012/09/08(土) 17:26:15.09 ] >>688 そりゃメレオロジーの話。 再帰理論は俺の専門だし限定算術なんかもやっとるよ。 690 名前：１３２人目の素数さん [2012/09/08(土) 17:34:10.64 ] >>689 限定算術の話で質問したいのですが、 素数が無限個あることの証明はどのくらいの限定で可能なのでしょうか？ 691 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 18:49:58.13 ] >>688 これのことだな？ 289 ： STS446 ： 2012/04/29(日) 07:39:01.09 　　まず初めに謝罪します。 　　私は「考える人」であり「超越論的数学者」であり、 　　「山之内彰」であり、「超越論的数学天使」であり、 　　「おさーん」でありました。 　　様相論理の件で論破されてのも私でした。 　　それではなぜこのような悲劇に至ったのかをお話ししましょう。 　　まず私は数学の素人です、論理学もまだ不完全性定理まで進んでいません。 　　しかしそれでも計算機の本（とりわけ赤間先生や人工知能関連）を読んでいると、 　　すぐにわかったようなレスができるようになりました。 　　そこでメレオロジーやオントロジーや記述論理といった 　　形式化オタクの文化を学習していきました。 　　ですから私は何もしらない単なる素人でしかないのです。 692 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 19:25:09.04 ] ４ヶ月半前に不完全性定理を知らなかった奴が再帰理論の専門家になっているとは 衝撃的な速度の出世だな 693 名前：STS446 [2012/09/08(土) 20:50:57.65 ] 今は原論文も現代的証明も両方とも理解してる。 とはいえ不完全性定理はほとんど証明追ってたから。 どっちかというと projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.lnl/1235416274 こいつで理解深めていたって感じだね。 再帰理論はその前からやってた、例のCooper本とか黄色の分厚いので学習した。 ランダムネスとかのも結構読んでるよ 694 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 21:06:00.29 ] いやいや、不完全性定理についてきちんと勉強していない 再帰理論の専門家とか論理的に不可能だから。自称専門家ならあり得るけど。 695 名前：STS446 [2012/09/08(土) 21:26:01.10 ] ここでいう不完全性定理の証明を追うってのは 算術化を完ぺきに自分で構成するってこと。 696 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 21:59:55.77 ] もういいだろ。 ご丁寧に本人がスルーすべき対象を識別してくれるんだから、 そいつは放置しといても無問題。 「STS446」って書いてあったらスルーすること。 あと新しく来た人が真に受けないように>>691のコピーを定期的に貼ること。 697 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 22:13:22.52 ] 四か月で専門家になりましたってレスがおかしいことくらい 気付ける常識人になれると良いね 698 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 22:14:37.82 ] 考えない人って選択公理の話題はこのスレでするのが適当って言って スレ住人全員から失笑を買った奴だろｗ 699 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 22:27:04.76 ] 155 名前：スレタイスレ446[sage] 投稿日：2012/01/07(土) 22:20:46.89 >>139 ＞そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？ 掲示板を読んでいる人間が、隣に座って同じ本を一緒に読んでいる様を想像して書きます。 また、投稿欄に書いた文章を決して読み返さないこと。 （レス数を減らしてじっくり書き込む時間をとるのがベストなのかもしれない。） ＞前スレの「考える人」と同じ臭いを感じる。 確かに文体が似ていますね。 考える人（＝考えない人）というコテハンは、このスレのその5辺りから時折出没していますよ。 >>140 以後、レスの数は減らします。 700 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 22:39:45.98 ] ＳＴＳが現れ始めたのはこのスレの５か６あたりから いろいろコテを変えて自演してることがばれているが その５以降のこのスレでコテを名乗っているのはほとんどこいつ自身の 自演と思って間違いない。（修辞がほとんど同じで数学的な間違いもほぼ類似） 特徴として終始一貫して「どこか勘違いしてる」ことが挙げられる。 長文の上勘違いも甚だしいレスばかりなので読む意味は全くない。 にもかかわらずコテハンを自演に従ってコロコロ変えるのでいちいちＮＧするのも 面倒くさいというまことに迷惑極まりない存在である。 701 名前：701 mailto:sage [2012/09/08(土) 22:44:39.98 ] 7^0=1 702 名前：STS [2012/09/08(土) 23:09:24.53 ] >>700 なるほど。 では直近の再帰理論に関する書き込みの中から 「勘違い」に相当する個所を挙げ、 それが「どう」勘違いなのかを説明したまえ。 703 名前：１３２人目の素数さん mailto:sage [2012/09/08(土) 23:24:23.67 ] 俺はお前の担当教官でも何でもない。 どうしてもと言うなら相応の報酬を用意してから言え。 大体お前のレスははツッコミどころが多すぎて添削するにしても手に負えないんだよ。 704 名前：１３２人目の素数さん mailto:sage [2012/09/09(日) 00:02:03.45 ] >>620 亀レスだけど「関数である」を原子論理式と扱ってしまうと ∀ｘ∃ｙＡ(ｘ,ｙ) は ∃ｆ∀ｘ(ｆは関数である∧Ａ(ｘ,ｆ(ｘ))) と書けてしまう。 だから>>619で批判されているようなΣnの定義を使うと どんな概念でもΣ2以下で表現できることになる。 >>619は「そう定義するのは自由だけど」と言っているけど、 こんな定義をしてもΣnの階層が崩壊するのでこんな定義しても意味がない。 705 名前：STS [2012/09/09(日) 00:37:41.73 ] >>704 スコーレム化がまちがっとるよ ∀ｘ∃ｙＡ(ｘ,ｙ)　と等価なのは ∀ｘ(Ａ(ｘ,ｆ(ｘ)))　だよ。 あなたの書いたものは2階述語論理への翻訳だね。 ところで ∀ｘ∃ｙＡ(ｘ,ｙ)　がΠ_2だとすると、 ∀ｘ(Ａ(ｘ,ｆ(ｘ)))　もΠ_2だよ。 Ａ(ｘ,ｆ(ｘ))　がΣ_1だからね。 Ａ(ｘ,ｙ)　がΔ_1でもスコーレム関数がΣ_1なので Ａ(ｘ,ｆ(ｘ))　はΣ_1になるの。 706 名前：１３２人目の素数さん mailto:sage [2012/09/09(日) 02:21:55.37 ] これまたスルーのし甲斐のあるレスだな 707 名前：STS [2012/09/09(日) 06:51:43.12 ] >>704-705 おっと素面の状態で読んでみたら 全然ちがう話しだったなｗ失敬失敬＾＾； 708 名前：１３２人目の素数さん mailto:sage [2012/09/09(日) 18:54:37.68 ] >>704 言語なんて決めないでもΣnの階層は意味を持つ！ って言ってたゆとり君（だっけ？）は逃げちゃったみたいだよ 709 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 04:02:20.77 ] >>704 非標準的な定義をする前に標準的な定義がどうしてそうなっているのか理解しとけって話だな 新しい定義を提唱した直後にその定義が無意味だと指摘されることほど数学者にとっての屈辱はない 710 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 07:53:38.74 ] しかしえてしてそういうことはよくあるんだな 学会で何度もそういう場面に出くわす 711 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 14:05:10.59 ] んだな 712 名前：STS [2012/09/10(月) 15:12:08.19 ] 俺もそういう状況には辟易している。 定義されている理由を知るのはいいかもね 713 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 15:38:07.99 ] おま（略） 714 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 16:01:39.38 ] この業界ではSTSは Structural Theory of Sets の略なんでなコテに使わんでくれるかな？ スレッドの綴りは thread であって S で略すのはおかしい スレタイスレの積りならTTTだろが 715 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 16:26:26.20 ] それは以前も指摘されてたと思うが 基地外だからしょうがない 716 名前：TTT [2012/09/10(月) 18:53:50.75 ] STSってのは俺が考えたんじゃないよ。 以前誰かがスレタイスレ446を略して STS446と呼んだので皮肉ってつけた名称さ、深い意味はない。 >>713 お前も似たようなものだろうと言いたいのだが、 俺はそれほど低レベルな部分では間違えない。 717 名前：TTT [2012/09/10(月) 18:54:58.26 ] 訂正 ＞お前も似たようなものだろうと言いたいのだが、 お前も似たようなものだろうと言いたいのだろうが、 718 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine.co.jp [2012/09/10(月) 19:29:47.04 ] また、お前か！　２０代の、ニートの、女性恐怖症の、ゴミ・クズ・カス・無能・虫けらのクソガキ！ 　死ね！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！！ 719 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 20:36:17.24 ] TTTって桟橋みたいでかっこ悪い 720 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 21:08:11.90 ] 目糞が鼻糞を嗤う 721 名前：１３２人目の素数さん mailto:sage [2012/09/10(月) 21:14:46.82 ] 学会で朝一発表の人が次の発表者の批判をしてるの見たことある 俺は「お前らどっちもトンデモだよ」と思ったけどいい大人だから 声には出さなかった。 722 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 00:25:30.01 ] 実数以外に実関数に関する量化を考えているのだから、 たとえば任意の関数 f が与えられたときに別の関数 g := F(f) が存在してA(f, g)が成り立つ、 （たとえば「任意の連続関数に対してそのフーリエ変換が存在する」とか）、 みたいなものも出て来るわけで、「どんな概念でも」というのはおかしいと思うんだけど。 それに実数値のみに関する量化を考えても、かなり強い形の 選択公理が公理として入っていないと同値にならない。 723 名前：１３２人目の素数さん [2012/09/11(火) 00:43:45.05 ] 何か年内にとんでもない事態が 発生するんじゃないか？ 最近そんな夢ばかり見る。 724 名前：１３２人目の素数さん [2012/09/11(火) 01:20:15.93 ] 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 725 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 02:43:00.35 ] >実数以外に実関数に関する量化を考えているのだから、 >たとえば任意の関数 f が与えられたときに別の関数 g := F(f) が存在してA(f, g)が成り立つ、 >（たとえば「任意の連続関数に対してそのフーリエ変換が存在する」とか）、 >みたいなものも出て来るわけで、「どんな概念でも」というのはおかしいと思うんだけど。 実数値関数は考えてもよくて実数値関数の関数は考えてはいけないの？ 超準解析をやるときは普通は任意の有限階の関数考えると思うけど。 >それに実数値のみに関する量化を考えても、かなり強い形の >選択公理が公理として入っていないと同値にならない。 あれー、これまで「普通の数学では」って言ってなかった？ 「普通の数学」で選択公理は認めるんじゃないの？ 教養の授業では連続と一様連続の違いをδ(ｘ,ε)とδ(ε)関数使って教えてたけどね。 都合が悪くなると基礎論の考え方持ち出すのかな？ 726 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 04:51:19.76 ] 普通の数学の議論をロジックの言葉で表現してみるとって話なんだから 選択公理を認めるのは確かに当然だ罠 727 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 12:11:59.33 ] >>722はスコーレム化とか勉強しとくべきだな。 728 名前：TTT [2012/09/11(火) 18:30:35.34 ] 衝撃的な事実が判明した。 つまりメレオロジーは現代で言う記述集合論なのだ！ 729 名前：TTT [2012/09/11(火) 18:32:37.69 ] 基本的にメレオロジーとかでやりたい部分ってのは 位相にうまく論理学をのせるという話しだったが、 記述集合論は集合位相から測度まですべてを統括してしまったのだ。 730 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 19:21:38.77 ] TTTって桟橋みたいでかっこ悪い 731 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 19:34:59.62 ] まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、 どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。 その時点で、既にメタ数学的な基礎論の話であって、普通の数学の話ではない。 その上で、別に選択公理を認めちゃいけない、と言っているのではなくて、 ∀ｘ∃ｙが∃ｆ∀ｘに変わってしまうから問題だ、と言っても 「そういう操作を可能にする公理を採用してしまっているのなら」当然でしょ、という話で。 私は725さんと違って超準解析についてこれは普通のやり方、これは別法、 これは普通じゃないやり方だ、と言えるくらいいろいろ知っている訳じゃない。 それでも、言語を決めてそのモデルを考えることはどのformulationでもやるけど、 関数の関数の関数に対しての選択公理とかの公理を数え上げて、 一つの理論として考えるということは（個人的には）あまりやらない気がするんだけど。 超準解析では普通many-sortedな言語で任意の有限階の関数考える、というのは あなたが勉強した本ではそうなっていました、というだけの話じゃないの？ 732 名前：TTT [2012/09/11(火) 20:24:16.69 ] >>731 ＞まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、 ＞どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。 ＞その時点で、既にメタ数学的な基礎論の話であって、普通の数学の話ではない。 本来Σ2論理式はメタ理論的な定義だよ。 ある理論Tと論理式Fを持ってきて、 FがTの定理であるかを判定することが計算可能か、再帰的加算かというメタ定理がある。 これらのメタ定理がΔ1とかΣ1とか呼ばれる。 そしてそのメタ定理そのものを判定するメタ定理をΣ2とかΣ3とかで定義するわけさ。 だから「どの理論の上でのΣ2論理式なのかが問題になる」というよりも、 ある理論が「Σ2論理式を表現できるか否か」が問題なわけです。 733 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 22:50:56.37 ] TTTって桟橋みたいでかっこ悪い 734 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 04:22:27.63 ] >>731 お前が自分の用語法をはっきり説明できればいいだけ。 お前が意味不明な用語法（実数と実数値関数がある言語でΣnとか）使ったから みんなでなんとか補完して意味を取ろうとしてるがうまく行かないと議論している。 お前がきちんと説明できればいいだけのことだ。 735 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 14:05:09.92 ] >まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、 >どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。 通常の数学で出てくる概念はどれだけ複雑になるかって話だったと思うが、 通常の数学では同値で区別しない概念を区別して論理式の選択によって複雑さが変わるのなら Π3とか複雑になるのは簡単に書ける概念なのにわざわざ複雑になる論理式を選んだから当然という以上のものではない。 普通の数学で区別しない概念を同じ複雑さにするには、 通常の数学で認めるもの（選択公理など）が含まれる理論の上での同値を考えるのは当然だろう。 （理論を設定してその上での同値を考えるという君の好きな考え方に立てば。 数学的には同値だが、「標準的」なモデルでの同値で考えてもいいので。） 普通の数学を反映していない理論を持ち出した反論にどんな意味があるんだね？ >超準解析では普通many-sortedな言語で任意の有限階の関数考える、というのは >あなたが勉強した本ではそうなっていました、というだけの話じゃないの？ 部分集合や関数が出てくる普通の数学を表現できる言語として 「超準解析でやるような」言語を君（ら）が出してきたと記憶しているが、 それが君の言うとおり関数の関数（汎関数）も表現できないような言語だったら そもそも「定式化をしづらいような性質・対象も平気で考える」普通の数学を 表現できないことになるんだがね。 736 名前：１３２人目の素数さん [2012/09/12(水) 19:13:03.88 ] ABC予想は証明されたのか。 京大数理研の望月新一さんの５００ページの大論文についての、 ネイチャー誌のニュース記事： 「もし正しければ、２１世紀数学の最も驚くべき成果の一つとなるであろう」 www.nature.com/news/proof-claimed-for-deep-connection-between-primes-1.11378 737 名前：TTT [2012/09/12(水) 19:20:08.90 ] 補足しとくけど、論理的同値な命題はすべて同じ算術的階層だよ。 算術的階層を定義するときに、対象の論理式の量化子の繰り返しを直接数えるのでなく、 対象の論理式と論理的同値な論理式の量化子の繰り返しを数えるとなっているから。 例えばダミー量化子付きの命題とそれを外した命題があったとき、 それらは論理的に同値だから量命題は階層を共有する。 Σ3とΠ2だったらそれぞれΣ3かつΠ2になる。 そうすると∃∀∃文がΠ2になるし∀∃文がΣ3になる。 それからチャーチの提唱で計算側に移ろう。 ある命題がチューリング機械でYesかNoで判定が可能なこと、 ある命題がチューリング機械でYesの判定だけが可能なこと、 ある命題がチューリング機械でYesかNoで判定が可能かどうかをYesかNoで判定可能なこと、...。 計算可能な集合のジャンプの階数　＜----＞　算術的階層 738 名前：TTT [2012/09/12(水) 20:27:11.50 ] そうだな、ΣｎとΠｎがメタ理論上の概念であることの分かりやすい例をあげよう。 存在例化限定2階述語論理では∀文が全く証明できない。 とはいえ、この場合は例えば存在例化限定2階述語論理における論理式が、 2階述語論理でΠｎとなる論理式である場合は、この∀文はΠｎとなる。 また別の例がある。 Tで∀ｘ∃ｙ（ｘ＜ｙ）が証明可能で、∃ｙ∀ｘR（ｘ、ｙ）が証明不可能としよう。 そして、Tの拡大T'で、∀ｘ∃ｙR（ｘ、ｙ）＜--＞∃ｙ∀ｘR（ｘ、ｙ）が証明可能としよう。 するとT'で∀ｘ∃ｙR（ｘ、ｙ）がΔ2になる。 これはTではΔ2ではないというか？ 否、TにおいてもΔ2なのである。 739 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 23:21:25.39 ] いや、あなたが∀ｘ∃ｙで始まる論理式と∃ｆ∀ｘで始まる論理式が同値になるから 全ての論理式はΣ2になってしまう、と言ったんでしょ。 これは「Σ2の形の論理式と同値であることが示せる論理式を 全てΣ2論理式扱いする用語法」だと思う （私にはそうとしかとれないけど、もし違うなら違うと言ってください）。 一方であくまで冠頭標準形の形だけに注目する定義の仕方もあって、 算術に関する本でもそういう定義をしていることは普通にある。 PA-Σ1論理式、Q-Σ1論理式、IΣi-Σ1論理式とか ZF-Σ1論理式、ZFC-Σ1論理式、ZFC+「Mahlo基数の存在」-Σ1論理式とか そういう風に似たようで少し違う概念が山のように出て来ても困る場合だって普通にあるでしょう？ 私はこっちの流儀で考えている。それだけの話。 数学的な公理と、論理記号や等号に関する純粋に論理的な公理には身分の違いがある。 論理に関する公理だけを用いて冠頭標準形に直せることには意味がある。 これは私は、通常の数学がどうとかいう問題じゃなくて、普通の数学でも 数学的な公理なのか純粋に論理的な帰結なのかは一応区別すると思う。 740 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 23:33:42.66 ] Σ1⊂Σ2⊂Σ3⊂Σ4⊂… 741 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 03:27:34.85 ] >>739は>>735の後半への反論は諦めたの？前半にしか反論してないけど 742 名前：TTT [2012/09/13(木) 08:01:51.00 ] >>739 例えば理論Ｔの中に、∃ｘＲ（ｘ）があったとして、 述語Ｑで、∃ｙＲ（ｘ、ｙ）＜--＞Ｑ（ｘ）となっているとすると、 Ｔ-Σ1論理式を考えると、∃ｙＲ（ｘ、ｙ）が証明不可能なので、 Ｑ（ｘ）も証明不可能となって結局丸く収まるんですね。 ですから一つの算術的体系の中だけならば冠頭標準形の形だけに注目しても問題ないわけなんです。 しかしこの定義ではメタ理論に広げると、Σ1＜--＞Σ0となりおかしくなってくるわけですね。 こういった定義は個別の体系内での狭い議論でしか通用しないんです。 743 名前：TTT [2012/09/13(木) 08:17:18.19 ] とはいえ通常の算術階層は 述語ＲやＱがΔ1であることを仮定していますから、 「冠頭標準形の形だけに注目する定義の仕方」 がどういったものかによりますが。 もしも述語部分がΔ1ならば、同値な定義はすべて同じ階層という私の定義と同じものでしょう。 そうでないなら同一体系内でしか使えない狭い定義でしょう（そんなものは見たことありませんがね）。 744 名前：TTT [2012/09/13(木) 08:41:12.95 ] >>743 それよりも計算量クラスがもうすぐ500種類を超えそうですな。 qwiki.stanford.edu/index.php/Complexity_Zoo これからは、Δ1より下側の時代ですよね。 算術的階層など古い古い。 745 名前：TTT [2012/09/13(木) 10:48:30.22 ] >>744 私も何回かワード使って全体像をマッピングしようと試みたんですが。 Ａ３で入りませんね、図面用の紙幅じゃないと駄目でした。 数学者どもが次数構造とか二階算術とか巨大基数のマッピングに 現をぬかしている間に計算機屋どもが物凄い勢いでマッピングを広げちゃった。 だから数学者はΔ1より下は怖くて触れない。 Δ1より上と違ってシンプルじゃないんだよ。 746 名前：１３２人目の素数さん [2012/09/13(木) 12:21:53.09 ] >>743-745 なにこれこわい 747 名前：TTT [2012/09/13(木) 13:25:12.16 ] >>745 ここにマッピングがあるね。 www.math.wisc.edu/~jmiller/Menagerie/ComplexityZoo.pdf ＰｖｓＮＰとかの同値性が示されたら一気に階層が潰れる可能性もあるけど。 色つきなんかで見るとわかり易い www.math.ucdavis.edu/~greg/zoology/diagram.xml ただし再帰理論なんかもランダムネスなんかが登場してかなり大きくなってきた。 www.math.wisc.edu/~jmiller/Menagerie/bn1g.png www.math.wisc.edu/~jmiller/Menagerie/bn1g.pdf それに逆数学＆限定算術も結構頑張ってかなりのリスト化が完成した。 math.berkeley.edu/~damir/zoo/just_rm.pdf 図式も一つじゃおさまらないレベルに到達してるしね。 math.berkeley.edu/~damir/zoo/diag_rm.pdf math.berkeley.edu/~damir/zoo/diag_rm_om.pdf math.berkeley.edu/~damir/zoo/diag_rm_non.pdf math.berkeley.edu/~damir/zoo/diag_rm_weak.pdf math.berkeley.edu/~damir/zoo/diag_hs_2007.pdf math.berkeley.edu/~damir/zoo/diag_dh_2009.pdf 意外と頑張ってるのが様相論理かな。 home.utah.edu/~nahaj/logic/structures/systems/ 巨大基数は頑張りが足りないかな？ websupport1.citytech.cuny.edu/faculty/vgitman/images/diagram.jpg 748 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 14:21:11.17 ] >>739 >数学的な公理と、論理記号や等号に関する純粋に論理的な公理には身分の違いがある。 >論理に関する公理だけを用いて冠頭標準形に直せることには意味がある。 >これは私は、通常の数学がどうとかいう問題じゃなくて、普通の数学でも >数学的な公理なのか純粋に論理的な帰結なのかは一応区別すると思う。 特に後半の一文は何を言いたいのか分からないのだけれども ∀∃で定義した連続性と modulus f continuity で定義した連続性が 別の概念であるという「普通の数学者」がいたら連れてきて欲しい。 彼らは論理式で表してから概念を把握するのではない。 概念が先にあってそれを基礎論屋が論理式で表示してるんであって 論理的公理だけで同値だったら同一の概念、 数学的公理が必要なら別の概念などと考えているわけじゃない。 749 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 18:14:08.62 ] つーか選択公理を論理的公理ではなく数学的公理とするのが標準的になったのは ロジック業界でもかなり後になってからじゃないの？ ε計算とかあった（いまでも研究されてるのかもだけど）わけだし。 ロジシャンの間でも定まってなかった論理的公理と数学的公理の区別なんて 「普通の数学者」にとっては知ったことではないんじゃない？ 750 名前：TTT [2012/09/13(木) 18:47:28.61 ] >>743 ＞とはいえ通常の算術階層は ＞述語ＲやＱがΔ1であることを仮定していますから、 これは再帰理論での定義だねΔ1ってか計算可能関係で定義される。 構文論的に定義する場合は再帰的にＲがΣｎのとき∀ｘＲ（ｘ）がΠｎ＋1と定義する。 レヴィの階層とか言われている。 数学の命題ってのは集合論だとほとんどがΔ0とかΔ1になるね。 Δ1以下にならないと任意の推移的可算モデルで充足しないからね。 濃度とかモデルとか射影階層に言及すると一気に階層が上がるけどね。 751 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 18:52:45.03 ] 少し前に話題になってた論理主義は選択公理どころか ヒュームの原理を使って算術を論理的公理から導くとか 果ては集合論すら論理的公理に還元できるとかいう主張 752 名前：TTT [2012/09/13(木) 19:26:23.18 ] そもそも数学と論理の公理ははじめ混同されてた。 ヒルベルトが一階論理を抽出したころには、 選択公理は整列可能定理やツォルンの補題との同値性もわかっていて 普通に数学の定理だった。 論理学の公理だと思われていた時代なんてないだろうな。 753 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine.co.jp [2012/09/13(木) 19:48:42.41 ] 　お前たちは、定職に就くのが先決だろがああああああああああああああ！！！！！！！！！！！！！！！！！！！！！！！！ 　ニート・無職の、ゴミ・クズ・カス・無能・虫けらのクソガキどもがあああああああああああ！！！！！！！！！！！！！！！！！！！！！！！！！！！！！ 754 名前：TTT [2012/09/13(木) 20:17:53.93 ] あと例の新論理主義者共が狙っていたのは 自然数の論理学的還元で 2階述語論理＋ヒュームの原理はペアノ算術より弱いからね。 755 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 20:58:42.54 ] これだけ書いても誰にも相手して貰えないってのは 逆人徳がすごすぎると思う って言うか出だしが出落ちに近かったから今更誰にも相手にしてもらえなくても しょうがないよな 756 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 21:51:05.55 ] 2ちゃんでコテ名乗るようなやつは、実社会で認められることが少ないやつ。さらに自演なんかする奴に至ってはほとんど病気だわな。 数学板なんかよりVIPとかの方が相手してもらえるよ。さあいったいった。 757 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 23:19:24.52 ] なんでTTTは自分と会話してるんだ 精神異常者なのか？ 758 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 23:49:37.06 ] 博士の愛したなんとかと同じ病気なんじゃね？ 759 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 00:26:55.65 ] 　　そだ　 |------､｀⌒ｰ--､ 　　れが　 |ﾊ{{　}} ）））ヽ､l l ハ 　　が　　　|､{ ﾊリﾉﾉﾉﾉﾉﾉ）､ l l 　　い　　　|ヽヽｰ､彡彡ﾉﾉﾉ}　　に 　　い　　　|ヾヾヾヾヾヽ彡彡} 　や 　　!! 　　 /:.:.:.ヾヾヾヾヽ彡彡} l　っ ＼＿＿／{ l ii | l|} ﾊ､ヾ} ﾐ彡ﾄ 彡ｼ ,ｪ､､､ヾ{{ヽ} l|l ｨｪ=ﾘ､シ} |l lミ{　ﾞｲｼﾓ'ﾃ､ミヽ}ｼｨ=ﾗ'ｧ､ }ﾐ}} l ヾﾐ　　 ￣~'ｨ''': |ﾞ:ｰ.￣ 　 lﾉ/l | | ヾヾ　　 " 　: :　!､ 　｀　　lｲﾉ l| | 　>lﾞ､　　　　ｰ､,'ｿ 　 　 /.|}､ l| | :.lヽ ヽ 　　ｰ_ ‐-‐ｧ'　 /::ﾉl ﾄ､ :.:.:.:＼ヽ 　 　 二"　 /::// /:.:.l:.:. :.:.:.:.:.::ヽ:＼　　　 　/::://:.:,':.:..:l:.:. ;.;.;.;.;;.:.:.:.＼｀ｰ-- '" //:.:.:;l:.:.:.:l:.: 760 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 01:58:05.11 ] ε計算はいまでも研究されている： www.sciencedirect.com/science/article/pii/S0168007212000802 ヒルベルトによって導入されたらしいな。 761 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 06:32:28.89 ] ε計算(Epsilon calculus)は確かに通常よりも強い形の選択公理を含んだ論理体系と言えるだろうね。 これに限らず証明論でよく使われるω規則を含んだω論理（WoodinのΩ論理ではなく）なんかも このω規則は論理的公理の側面と数学的公理の側面があって両者の「身分の違い」ははっきりしない。 最近の入門書では論理的公理と数学的公理の区別が本によって食い違うことは（等号公理の扱いを除けば）ないだろうけど そこから少し発展した内容を勉強してみるとその区別は結構曖昧なものだと気づかされると思うよ。 762 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 07:24:21.09 ] >>739が言ってるのは論理式だけを見て複雑さを定義して論理式間の同値を考慮しないって話で >>748は「数学的な概念」（＝論理式の同値類？）に対して複雑さを定義しなければいけないって話ではないかと。 「普通の数学に表れる」と言ったときにどちらがまともかは言わずもがなだと思う。 前者の意味で複雑になってもそれは数ある論理式の表現の仕方の中でわざわざ複雑なものを選んできたからに過ぎず意味がないことになるわけで。 >>739は用語法の違いってことで逃げようとしているけど、場にそぐわない用語法持ち出しても正当化にはならないと思う。 なんか上の方のレスと同じこと言ってるけど。 763 名前：⊥⊥⊥ [2012/09/14(金) 11:43:58.16 ] >>744 ただしその中のほとんどが不当に水増しされた階層だということに注意。 例えばＥＥＥはＤＴＩＭＥ(2^2^2^o(n))といった具合に、 大抵はDTIMEやDSPACEの言い換えでしかない場合が多い。 こういった記述の仕方が素人への可読性を低下させている疑惑もある。 計算量ではそのクラスの特性に見合った名称をつける場合があるが、 これによって直感的な階層の高低の把握が邪魔されていることが多々ある。 764 名前：TTT [2012/09/14(金) 12:22:36.90 ] 基本的に決定性と非決定性（確率やランダム）なチューリング機械を 領域と時間で組合せ論的に作って分類しているだけだから。 それにオラクルを用いたものや論理体系の表現能力を組み合わせた図式だね。 確かに名称のせいで何をやっているのか分からくなってるね。 765 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 14:44:49.84 ] >>762 なるほど。つまり 「たとえば有界な関数が〜〜と言っただけで、 （実数論として）Σ2の式が出て来るんだから Σ3くらいの量化は普通に考えることになる」 というのはΣ2の式でも表現できるのに あえてΣ3の論理式で表現したからΣ3の量化が出てきた と>>739は言ってるわけね。 766 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 16:08:04.04 ] おまいら執拗すぐる。739の言い分がナンセンスだってのはもう十分分ったから。 767 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 17:01:39.61 ] じゃあ普通の数学を形式化したら多重量化はほとんど出て来ないって言いたい訳ね？ 768 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 19:18:35.22 ] ∃ｘ(ｘ＝ｘ)とか、等号がない場合には∃ｘ(Ａ∨¬Ａ)って論理的公理？ 769 名前：TTT [2012/09/15(土) 20:21:26.72 ] Ａが述語変数なら論理公理（どういった公理の論理体系かによるけど）ですね。 述語が定数になると理論固有の公理になります。 770 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 20:31:57.82 ] たとえそれと同値な論理式が公理に入っていたとしても その論理式自身が公理に入ってなければ公理とは言わない 771 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 20:37:02.31 ] もし∃ｘ(ｘ＝ｘ)が論理公理なら ＺＦＣの公理に空集合公理は要らないのでは？ 分出公理があれば空集合公理は導けるはず 772 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 21:03:19.23 ] >>771 どうやって導くの？ 773 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 22:04:43.91 ] どうも767もスルー対象に認定されたようだなｗ 専門用語を正しく使えないゆとり君は専門板の専門スレなんか来ちゃダメ。 774 名前：１３２人目の素数さん [2012/09/15(土) 22:22:24.27 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 775 名前：TTT [2012/09/15(土) 22:40:45.68 ] >>768 あなたの提示した論理式は、恐らく一階述語論理のものでしょうが、 一階述語論理の公理はいくつものタイプが考えられるんです。 基本的にそれらが証明する論理式はすべて同じなんですが、 何を公理とするかは決まっていないんです。 776 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 00:08:02.26 ] >>761 等号公理に限らず、∃ｘ(ｘ＝ｘ)みたいなのでも食い違うのでは？ 論理的公理（から導れること）と数学的公理（同）の区別は今でも流儀によるでしょう。 「普通の数学でも数学的な公理なのか純粋に論理的な帰結なのかは一応区別する」なんてのは論外で。 777 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 10:39:46.03 ] 778 名前：１３２人目の素数さん [2012/09/16(日) 12:38:40.63 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 779 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 12:49:43.76 ] >>772の回答は？ 780 名前：１３２人目の素数さん [2012/09/16(日) 15:20:10.21 ] ∃ｘ(ｘ＝ｘ)は等号付き一階述語論理の論理的公理だけで出てくるよ。 空集合公理は内包性公理だけで出る。 内包性公理の任意論理式にｘ≠ｘを入れるだけ。 逆に等号なし一階述語論理でもZFCによって等号と同等のものが使えるようにもなる。 ∀ｘ∀ｙ（∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｙ）-＞ｘ＝ｙ） ∀ｘ∀ｙ（-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｙ）） ｘ≠ｘ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ） 内包性図式により ∃ｙ∀ｘ（ｘ∊ｙ＜--＞ｘ∊ｚ∧ｘ≠ｘ） ∀ｘ（ｘ∊ｙ＜--＞ｘ∊ｚ∧ｘ≠ｘ） よって ｘ≠ｘ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ） ｘ∊ｚ∧ｘ∊ｙ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ） 781 名前：TTT [2012/09/16(日) 15:24:09.42 ] >>780 の下半分の論理式はミス 782 名前：TTT [2012/09/16(日) 16:15:44.19 ] とはいえ内包性（分出）公理は見かけ上だけなので 実際には外延性公理によるユニーク性をもって 空集合が定義されたとする見方も多い。 さらに分出公理中の集合は無限公理で得られる集合を使う必要がある。 無限公理でなくとも集合の存在を示す∃ｘ(ｘ＝ｘ)を使うことが出来る。 例えこれが論理公理でも見かけ上区別できないから問題ない。 そこから>>771の発言が来ているのだろう。 783 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 16:16:14.54 ] 他の人がちゃんとスルーできるようにコテ付けとけ 784 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 18:23:02.31 ] ZFCだったら∃ｘ(ｘ＝ｘ)が純粋な論理的帰結であろうとなかろうと 無限公理Infと分出公理から空集合の存在は示せるので空集合公理は冗長。 集合論の入門書ではZF(C)-Infなども考えるから入れているんだと思う。 それでも∃ｘ(ｘ＝ｘ)がいえれば不要な訳で ∀xA(x) -> ∃xA(x) が論理的帰結になる自然演繹やヒルベルト流体系の入門書とは 異なる立場に立っているというか、 少なくとも∃ｘ(ｘ＝ｘ)の身分に関して中立であろうとしているといえると思う。 785 名前：１３２人目の素数さん [2012/09/16(日) 21:53:42.62 ] 　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_ 　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、 　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ 　　　　　/　　　／:::::／　　　　　　　　　　　＼ 　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 | 　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 | 　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ| 　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　 　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。 .　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。 　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。 　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて 　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。 　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は? 　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？ 　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼ .　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼ 　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 | 　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､ 　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣| 　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿| 　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/ 　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/ 786 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 05:38:24.54 ] ∀xA(x) -> ∃xA(x) が論理的帰結にならないような証明体系ってどんなのがあるの？ 787 名前：１３２人目の素数さん [2012/09/17(月) 08:44:05.78 ] レベル堕ちたなこのスレ 788 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 14:32:19.88 ] >>786 ∀xA(x) -> ∃xA(x) や、同じことだけど∃ｘ(ｘ＝ｘ)を妥当式にしない流儀は 空な構造も含めたいっていうモデル理論的観点からの場合が多い。 だから証明体系と言っていいのかだけど、 空構造を許す意味論での妥当式はすべて公理というようなモデル理論的に定義した体系が 「よく出てくる例」になるんじゃないかな。 789 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 16:06:19.02 ] >>72 ＞形式体系ZFCを外側から見たメタレベルでは ＞１、φが証明可能である ＞２、φの否定が証明可能である ＞３、φは独立である ＞４、ZFCが矛盾している ＞のいずれかである。 ４が正しいなら１も２も正しくなるがね 逆にいえば、４でない場合に限り、任意の命題φについて １，２，３の３つの場合がありえるというわけだ。 ところで実は、４でない場合、４を示すつもりのZFCの命題が３になる。 ここでわざわざ「つもり」と書いたのは、ZFC内では、ZFCの無矛盾性を 完全に表現できないのである。つまり、ZFCが無矛盾であっても、 それを表わしたつもりの式が偽となるモデルが存在し得るわけだ。 790 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 16:20:49.38 ] 「PAはモデルをもつ。したがって、完全性定理により無矛盾である。」 これって正しいですか？ 791 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 17:26:00.91 ] 話題を無理やり切り替えるために昔のネタを引っ張り出してきた？ 792 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 18:53:44.41 ] >>786 きっとTTTが、君の求めるような体系について 半分正しくて半分勘違いに基づいた解説をしてくれるだろうよ。 色んな体系の解説を沢山読んではいるようだから。 読んだからって勘違いだらけなのは見ての通りだがｗｗ 793 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 19:11:55.00 ] 人を貶すしか能のない792みたいなのはどうにかならんのかなあ 786の質問のどこに792みたいに言われなきゃならない要素があるんだか 794 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 16:45:31.20 ] >>784 >>788 集合論やモデル理論の人は∀xA(x)→∃xA(x)や∃ｘ(ｘ＝ｘ)を恒真とは考えないってことですか？ 795 名前：TTT [2012/09/18(火) 22:53:11.57 ] >>794 ∀xA(x)→∃xA(x)は恒真になる。 ∃ｘ(ｘ＝ｘ)は述語論理の式なので恒真じゃない。 796 名前：１３２人目の素数さん [2012/09/18(火) 23:00:50.33 ] 韓国を国際司法裁判所へ引きずり出す署名へご協力ください 　 staff.texas-daddy.com/ 半角英数で本名でお願いします、漢字とかイニシャルはNGです 違うアドレスで家族の名前でもおkです ステアドでもおｋ 台湾の人も署名してくれてます 日本政府に圧力をかけましょう 797 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 23:29:34.53 ] いくら署名したって韓国政府の同意がなきゃ駄目なんじゃ 798 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 23:30:41.02 ] >述語論理の式なので恒真じゃない。 ？ 799 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 00:54:29.17 ] ZFCGってなに？ 800 名前：800 mailto:sage [2012/09/19(水) 01:10:44.35 ] うそ　800 801 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 04:21:11.13 ] どこに書いてあったの？ たぶんその本なり論文なりに定義してあると思うよ 802 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 05:16:04.23 ] generalized Cantor hypothesis 803 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 06:15:57.18 ] >>794 集合論者はZFCの公理（上で言われているように弱めることはよくあるが）の下でしか考えない。 集合論の公理を全部取っ払うことはまずないので「数学的な公理なのか純粋に論理的な帰結なのか」なんて気にしない。 804 名前：TTT [2012/09/19(水) 09:31:04.95 ] >>798 恒真ってのは命題論理で個々の原始論理式の真偽値と無関係に式全体が真になることだから。 ∃ｘ(ｘ＝ｘ)が真になるには、モデルの領域中にこの式を満たす個体がないと駄目。

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

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