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

1 名前：１３２人目の素数さん mailto:sage [2012/01/02(月) 23:04:29.50 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その10 uni.2ch.net/test/read.cgi/math/1319895756/ 401 名前：１３２人目の素数さん [2012/01/28(土) 23:12:03.45 ] 講義です。 その先生が独特に使うのでしょうか…。 もう途中から何言ってるのか、って感じで困ってたんです。 最後に課題を出されまして…。 専門ではなく教養なので、おそらくそこまで難しいことは言ってないとは 思うですが…。 402 名前：１３２人目の素数さん [2012/01/28(土) 23:21:09.89 ] >>397 素直に考えると 4番が量化記号がダブって束縛しているのでおかしいけど、 論理式の定義によるからなぁ 403 名前：１３２人目の素数さん [2012/01/28(土) 23:32:22.22 ] 397です。レスありがとうございます。 もうすこし追記します。その先生によると Lpの論理式（Ｆ）とは、次の(1)〜(4)を繰り返し適用して構成される 有限の記号列のことである。 (1)各atomic formula　αはＦである。 (2)αはすでにＦであるとわかっている⇒（¬α）もＦである。 (3)α,β∈Ｆ⇒(α⊃β）,(α∧β）,（α∨β）∈Ｆ (4)α∈Ｆ⇒（∀xα）∈Ｆ というのが定義のようです。 素人にゆっくり教えてやろうという講義ではなく、先生の独り言的な講義 だったため、素人のこちらは全くわかりませんでした…。 404 名前：１３２人目の素数さん [2012/01/28(土) 23:39:56.36 ] >>403 わきからごめん。 >もう途中から何言ってるのか こういう状態でこの宿題だけやっても、という気はするが、参考までにコメントするよ。 ｢Ｌｐの論理式である｣というのは、直感的には，｢文法に合った式である｣という意味だよね。 ここに貴方が書いた定義に照らすとすれば、(1)-(4)はどれも文法に合っていると思う。 しかし、ふつうの定義では，(1)(2)は（かろうじて）文法に合っているが、(3)(4)は文法に 合っていない（Lpの論理式でない）と思われる。というのは、，(3)は定数cが限量変数に 使われているし、(4)は（402も言うように）zとxが限量変数としてダブって使われている から。どうかな？ 405 名前：１３２人目の素数さん [2012/01/28(土) 23:44:17.61 ] >>403 その定義だと1が論理式じゃないね。 ∃記号が¬∀¬と交換できないなら。 406 名前：１３２人目の素数さん [2012/01/28(土) 23:53:13.97 ] 皆さん、ありがとうございます。 404さんもおっしゃる通り、この状態では…ということはわかっていますが、 どうしてもこの単位が必要という現状です。 頼りにするのがこの板だけというまわりもあてにならない状況で申し訳あり ませんが、お付き合いいただけると幸いです。 先ほどの質問につきましては、いただいたアドバイスを元に選びます。 もうひとつだけお願いします。 質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。 という質問です。 「代入」というテーマで授業した内容からだと思いますが、もう途中から 何言ってるのかわかりませんでした…。 すみませんが、よろしくお願いいたします。 407 名前：１３２人目の素数さん [2012/01/29(日) 00:00:41.31 ] >>406 とりあえず言えることは、 >>397のような問題は通常、 「論理式の定義から作れるものはどれか？」ということが問うているので、 >>403のような定義から作れるか試してみろってことです。 ＞質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。 NOです。 束縛された変数には代入できないです。 ※直感的理解 ∃yP(y,a)：yは束縛されている、aは束縛されていない。 408 名前：１３２人目の素数さん [2012/01/29(日) 00:18:37.92 ] 407さん、ありがとうございます。 ちょっとわかったような気がします。 とすると、 ∀xＰx⊃∀yＲ(x,y)において、freeに現れているxにzを 代入した論理式を書きなさい。 という問いに対しては、∀xＰx⊃∀yＲ(z,y) と答えればよろしいのでしょうか。 もはやこんな感じ、という理解しかできませんが…。 409 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 00:58:59.64 ] >>397 通常の形成規則にしたがえば、論理式(wff)である記号列は(2)だけで、(1),(3),(4)はwffsではない。 410 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 05:19:36.48 ] うぇるふぉーむどふぉーみゅら 411 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 07:11:11.50 ] 圏論による数学の基礎について語ろう！ 412 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 08:33:10.32 ] 上のほうで圏論と集合論（巨大基数）の関係が話題になってたけど、 圏論を他の代数構造同様に（クラスサイズっていう違いはあるが）集合論の中で実現して っていう話だから数学の基礎としての圏論というのとはなんか違うな。 413 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 10:23:59.82 ] >403だけ？∀に関する他のルールは無いの？ 普通に考えれば∀zが入れ子になっている(4)が怪しいけど、 仲間外れというなら束縛したwの出て来ない(1)も怪しい。 414 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 10:38:06.58 ] 量化記号がダブるとか、∀zが入れ子になるとか、束縛したwが出て来ないとか そんな理由で論理式にしないなんてことよくするの？ 415 名前：１３２人目の素数さん [2012/01/29(日) 11:04:29.57 ] >>414 とにかくあれは問題のための問題（悪問）と思う。 実際に使うために論理式を書く場合は、変数はダブらないように書くし、 中に出てこない変数を束縛するなんてこともしないだろ。 416 名前：１３２人目の素数さん [2012/01/29(日) 11:08:55.44 ] そうだな。あんなことをやってるから教養は要らないってことになる。あれは文系かな？どうせ論理を教えるならもっと違うやりかたがあるがな。 417 名前：１３２人目の素数さん [2012/01/29(日) 12:44:33.77 ] 圏論上の形式的議論を圏論だけでできるんですか？ 述語論理は当然のように使っているようにみえるんですが、これでは圏論は自立していないと いうことにはならないのですか？ 418 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 13:06:57.12 ] 集合論だって述語論理は使っている。 述語論理の上のレベル（というか非論理的公理）として、 集合論などのほかの「数学の基礎」から自立できているかが問題。 述語論理から独立させようなんて誰も考えてないよ。 419 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 14:55:33.43 ] そうだけど、集合論におけるメタ数学的議論は集合論で形式的に扱う事が出来るけど 圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難があるし、 その全ての側面を扱うのは難しいと思う 420 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 15:19:53.03 ] >圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難がある 慣れの問題でしかない、という説もある。そしてその説には一理ある。 421 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 16:12:47.01 ] 前にちらっと話題に出てきた STS (Structural Theory of Sets) は、 述語論理から独立させて、様相命題論理で集合論を記述しようという話。 つまり比喩的に左側が機械語側、右側がユーザー側として階層をまとめると、 >>412が圏論と巨大基数の話に関して言ったこと： 一階述語論理　−　集合論　−　各数学（圏論もこの一つ） 数学の基礎として圏論 一階述語論理　−　圏論　　−　各数学 STSの目指すもの 様相命題論理　ー　集合論　−　各数学 422 名前：１３２人目の素数さん [2012/01/29(日) 17:40:49.18 ] >>418 >述語論理から独立させようなんて誰も考えてないよ。 だったら圏論は述語論理の単なるマクロ集であって、共通の基盤言語だなんて言い方は しないほうがよいのではないですか？ 423 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 17:53:39.66 ] >>412 こんなんあるでよ www.math.ucla.edu/~asl/bsl/1303/1303-002.ps RELATING FIRST-ORDER SET THEORIES AND ELEMENTARY TOPOSES 424 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 18:07:13.66 ] >>422 なんか色々なことをごっちゃに理解しているように見受けられるな。 「圏論が数学の共通の基盤言語」というのは、 数学の色々な構造から共通の性質を抜き出すのに便利というプラグマティックな話であって 「圏論は数学の基礎として数学と述語論理の橋渡しとなる」というのとは また別の話だと俺は理解しているのだが。 425 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 18:30:21.14 ] いや、巷で「数学の基礎」と言われていることの中身を突き詰めれば >>422の言うとおりマクロ集ということでしかないのでは？ もちろん、それは集合論が数学の基礎というときも同様だけど。 ＞なんて言い方はしないほうがよいのではないですか？ 「集合論が数学の基礎だ」とか「圏論が集合論に代わる基礎となり得る」とかというのは、 ある意味使い古された言い回し。ここの住人が言い出したことではないので、 こんなところで「その言い方はおかしい」と言っても始まらない。 426 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 18:52:36.82 ] >>425 「数学の基礎」と「数学の共通の基盤言語」は同じ意味内容だと主張したいの？ 427 名前：１３２人目の素数さん [2012/01/29(日) 19:32:32.95 ] 数学の共通言語はTEXだよ 428 名前：１３２人目の素数さん [2012/01/29(日) 22:07:17.38 ] 圏論は所詮モデル論なんだよ。しかし言語の本質はシンタックスだ。 だから圏論は、共通も何もそもそも言語ですらないんだよ。 同じことは集合論にも言える。 わかるかな。 429 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 22:08:49.88 ] ↑あふぉ 430 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 22:41:02.09 ] シンタックスだのセマンティクスというのは メタレベルからオブジェクトレベルをいじる場合の手段の区分。 一階述語論理 − 集合論or圏論 − 数学各論 という階層は、 オブジェクトレベル、メタレベル、メタメタレベルなどの 一つのレベルの中での話。 （オブジェクトレベルの一階述語論理は、 セマンティクスだろうとシンタクスだろうとメタレベルの数学各論の一つになる。） 一つのレベルの中でセマンティクスだのシンタクスだの言うのは無意味。 431 名前：１３２人目の素数さん [2012/01/29(日) 22:58:00.44 ] >>430　ややこしいな 432 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 23:04:50.75 ] 基礎付けの話になると、最終的にどっかで循環にならざるをえないからな。 それを尤もらしい美辞麗句で隠したのが、メタレベルと対象レベルの分離、ともいえるわけだｗ 433 名前：１３２人目の素数さん mailto:sage [2012/01/29(日) 23:54:17.46 ] >>430 なるほど。数理論理学を学ぶために最低限必要なセンスとして ＊シンタックスとセマンティクスが区別できること ＊オブジェクトレベルとメタレベルが区別できること ＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること の３つを伺っていましたが、最後の区別がよく分かりました。 434 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 00:02:11.87 ] ＞＊シンタックスとセマンティクスが区別できること ＞＊オブジェクトレベルとメタレベルが区別できること ＞＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること これ至言だな 435 名前：１３２人目の素数さん [2012/01/30(月) 00:18:37.06 ] シンタックスとセマンティックがはじめに理解すれば良い メタな視点は後から考えれば良いし、ロジック学習の基礎において必須でもない。 436 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 00:19:16.47 ] ソースは誰？ぐぐったら鴨さんのはてなが出てきたけど、これが初出？ 437 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 00:23:44.56 ] 俺様勉強法を語って自分の無理解をひけらかしちまう馬鹿＝435、哀れだなｗｗ 438 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 00:36:52.08 ] >>430で言われているように、 シンタックス（構文論）もセマンティクス（モデル論）もどちらもメタ的な視点の話なので、 良い子の皆さんは435のいうことを真に受けてはいけませんよ 439 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 00:48:22.65 ] そんなことより、圏論による基礎の話はどうなった？ >>423のリンク先の論文の評価を聞きたい。 440 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 05:32:38.82 ] >>432 ともいえる、なんて控えめである必要はなく、そう断言してしまってもいいと思う というか「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」なんて 基礎付けの本質を突いた至言だと思う、鴨さんの３つの区別と並んで。 441 名前：435 [2012/01/30(月) 07:17:42.79 ] はじめはメタな視点を意識する必要がないという話しだが。 >>438の考えを認めるとすべての数学はメタな視点に基いている。 メタを意識する必要が出てくるのは不完全性定理や内部モデルから。 442 名前：１３２人目の素数さん mailto:sage [2012/01/30(月) 07:40:09.73 ] 435=441 のいうことが正しい。 430 に書いてあることは、形式論理の研究者のなかにさえ、そのように 思っている人がありが、無限連鎖に陥るだけで、意味を考えることができ ない。 443 名前：１３２人目の素数さん [2012/01/30(月) 09:06:38.39 ] 学部教養レベルの確認が一段落したら、圏論によってシンタックスとセマンティックスの 区別がなくなるという話もしようぜ。 444 名前：名無しさん [2012/01/30(月) 18:58:02.88 ID:Nob3XfwW] ちょうど話題が出たんで、甲鳥さんのページで質問です。 ttp://taurus.ics.nara-wu.ac.jp/staff/kamo/shohyo/logic-2.html ＞著者は、また、自然数論は完全性定理が成り立つには強すぎる体系である旨の ＞主張もしている。それも大違いである（こちらは、かなり広まっている誤解だ ＞が、どんなに広まっていようと、専門家に一言相談すれば「それは間違ってい ＞る」と言ってもらえるのだから、言い訳にはならない）。一階ペアノ算術（自 ＞然数の加減乗除と大小比較ができて数学的帰納法が自由に使えるが、関数一般 ＞や集合一般を自由に扱うことはできない世界と思って、ほぼ間違いない）は一 ＞階述語論理上の公理系なので、完全性定理が適用できる。したがって、一階ペ ＞アノ算術の公理系から証明可能な式全体と、一階ペアノ算術の公理系が真とな ＞るすべての解釈で真となる式全体は、一致する。これを、「一階ペアノ算術は、 ＞一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」という。 という部分ですが、 「一階ペアノ算術は、一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」 というのは本当に成り立つんでしょうか？今一書いてあることが理解できないのですが。 445 名前：名無しさん [2012/01/30(月) 19:03:08.17 ID:qQ0NhdK4] >>444 もちろん本当だと思うが、どう理解できないの？ 446 名前：444 mailto:sage [2012/01/30(月) 19:44:03.54 ID:???] あぁ勘違いしていた。 完全性定理は論理だけに関する定理だった。 447 名前：名無しさん [2012/01/30(月) 20:09:26.65 ID:ZFRpVEeB] >>443 こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場 448 名前：444 mailto:sage [2012/01/30(月) 20:37:41.38 ID:???] 林さんの数理論理学では 述語論理の完全性と古典算術の完全性を別の定理として区別していますね。（独言 449 名前：名無しさん [2012/01/30(月) 20:58:41.96 ID:qQ0NhdK4] >>447 駆け出しだな 450 名前：名無しさん mailto:sage [2012/01/30(月) 21:05:58.07 ID:???] ＞圏論によってシンタックスとセマンティックスの区別がなくなる 別にそんなこと無いですけど…… と書こうと思ったら既出だった 451 名前：名無しさん mailto:sage [2012/01/31(火) 05:56:45.85 ID:???] 専門家をバカにできるとは 441=442 はアスペか？隔離スレからでてくんな。 452 名前：435 mailto:sage [2012/01/31(火) 07:13:02.56 ID:???] どうでもいいことだが、>>442は別人。 453 名前：名無しさん mailto:sage [2012/01/31(火) 07:35:35.85 ID:???] >397　Ｌｐの論理式でないのはどれか。 (1)∀w∀x∃zＲ(x,z) (2)∀xＰx⊃∀xＲ(x,c) (3)∀xＰx⊃∀cＲ(x,c) (4)∀z∀x(∀xＰx⊃∀zＲ(zz)) コピペなら明瞭に(4) R(zz) はwww 誤植でR(z,z)にしても「R(z)三R(z,z)」は未だ証明されてない よーするに　ここでの単位は　とらぬのが正解 あふぉ　が伝染って　後遺症で困るとおも晴れri 454 名前：名無しさん mailto:sage [2012/01/31(火) 07:46:24.58 ID:???] どうも本当にアスペが隔離スレから出てきたようだな 455 名前：名無しさん mailto:sage [2012/01/31(火) 10:16:28.28 ID:???] >>441 通常の数学（特に代数構造など）の話でも、 ★そういう見方をすれば★メタ的な視点に立っているものが多い、 ということに気づけないようでは数理論理学のお先真っ暗。 456 名前：名無しさん mailto:sage [2012/01/31(火) 18:12:14.65 ID:???] とりあえず宣言しとくけど 今夜0時までに 田中の数学基礎論講義の5章までの定理をすべて Coqで証明するよ＾＾ 457 名前：名無しさん mailto:sage [2012/01/31(火) 19:23:22.88 ID:???] すげえ！ 458 名前：名無しさん mailto:sage [2012/01/31(火) 23:52:26.53 ID:???] Definition P1(a b:Prop):Prop:= a->(b->a). Definition P2(a b c:Prop):Prop:= (a->(b->c))->((a->b)->(a->c)). Definition P3(a b:Prop):Prop:= (~b->~a)->(a->b). 今日はここらへんまでかな。 459 名前：名無しさん [2012/02/01(水) 09:29:56.50 ID:S/Q8pgaI] スレの勢いからして もうそろそろ次スレの季節だな 460 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 00:08:01.24 ] Record L_PA:Type:= language (Func:Set) (Rela:Set) (arity:Func+Rela->nat). 今夜はここまで 461 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 04:30:22.70 ] ＞430 に書いてあることは、形式論理の研究者のなかにさえ、そのように ＞思っている人がありが、無限連鎖に陥るだけで、意味を考えることができない。 馬の耳に念仏だな、こりゃ。念仏の「こころ」がまるで分かっちゃない。 馬＝442 念仏＝「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」 462 名前：１３２人目の素数さん [2012/02/02(木) 05:28:18.34 ] 圏論話は終了か？ 463 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 07:31:16.88 ] ┌∩┐(◣_◢)┌∩┐ 上の方にある、 一階述語論理　−　集合論　−　各数学 の図式は古典的で、考えているのは数学屋だけ。 実際には一階述語論理　−　集合論の間の区別は曖昧。 464 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 11:50:41.14 ] 参考文献を上げて下さい 465 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 18:25:33.46 ] ┌∩┐(◣_◢)┌∩┐ この本にZFCを一階論理で厳密に展開しているので参考にすること。 Axiomatic Set Theory (Graduate Texts in Mathematics) [Paperback] Gaisi Takeuti (Author), Wilson M. Zaring (Author) www.amazon.com/Axiomatic-Theory-Graduate-Texts-Mathematics/dp/0387900500 466 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 18:32:31.58 ] >>423 （圏論的意味での）イデアル全体とか取っているのは、 そのトポスが集合論の世界に含まれている前提での話。 「一階述語論理と数学をつなぐ」という意味での 「基礎としての圏論」の研究とは言いがたい。 467 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 19:58:10.03 ] 463が言ってる集合論ってまさか 「集合と位相」で習うようなことじゃないだろうか 468 名前：１３２人目の素数さん [2012/02/02(木) 20:43:10.06 ] >>467 だから言っただろ。駆け出しがうようよしてんだよ 469 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 21:34:56.20 ] ┌∩┐(◣_◢)┌∩┐ 一階述語論理の言語にZFCの公理系を添加したものと∈-モデルからなる数学は、 厳密に分離することが出来ない、これは実際に展開してみないと気付きにくい。 例えばキューネンなどの本では述語論理の箇所が省略されているので気付けない。 >>465の本の冒頭が参考になる。 470 名前：１３２人目の素数さん mailto:sage [2012/02/02(木) 22:25:47.07 ] 「∈-モデルからなる数学」って何のこと言ってるの？ そもそも>>469では述語論理＋ZFCとその上の数学とを 厳密に区別できないと言っているのに対して >>463では述語論理と集合論（ZFC）とは区別できないと 少し別のことを言っているように思うんだが 集合論は数学をやる上での基本的な言葉みたいなものだから 基本的な論理と一体だとか言うのは普通の数学やってる人達で、 却って情報系・哲学系の人とか数学でもロジックやってる人は 集合論（ZFC）の公理と述語論理の公理は別のレベルのものだとして明確に区別すると思う （一部の新論理主義の立場に立つ哲学者等を除く） 471 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 04:35:23.02 ] 他人には意味不明な用語法を断りなしにするのは、トンデモか駆け出しの証拠ｗ 472 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 06:24:32.83 ] >>463 等号公理は、一階述語論理の公理なのか、集合論の公理なのかはっきりしない、 とかそういう意味で区別が曖昧と言っているのかな？ それはイエメンとサウジアラビアの国境が未画定（つまり曖昧）だから 国家としてのイエメンとサウジアラビアの区別が厳密に区別できない と言っているようなもので的外れ。 473 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 07:11:59.26 ] >>466 確かにイデヤールの部分はそうなんだけど、 かなりの部分は一階述語論理の直上のものとして理解できるでしょ、 elementary topos というのは正にそれ故に意義のある概念。 集合論に依存していいのなら Grothendieck topos で十分だった。 その論文では「canonical injection である」という述語が、 集合論と同じ表現力を持たせる為に圏論側で必要な「述語記号」だと言ってる。 とはいえ、集合論に依存している部分とそうでない部分をごちゃ混ぜにしているのは確かに問題。 圏論による基礎を標榜している指導的な研究者である著者達がこんな書き方をするから、 「圏論は集合論に変わる基礎」と言っても 一階述語論理　−　集合論　−　圏論　−　各数学 みたいに「屋上屋を重ねる」ような無駄なこと、っていう印象を持たれてしまう。 474 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 07:21:18.20 ] ┌∩┐(◣_◢)┌∩┐ Oh,Motherfucker!（＾＾； 等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。 475 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 07:25:41.91 ] 問、等号なし一階述語論理でZFC外延公理から以下を導け： ∀x(x∈a ⇔ x∈b) ⇒ (a∈c ⇔ b∈c) 476 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 08:05:16.63 ] ＞等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。 こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場 477 名前：１３２人目の素数さん [2012/02/03(金) 10:06:55.24 ] >>473 >みたいに「屋上屋を重ねる」ような無駄なこと それ以前に、圏論が述語論理（λhol含む）や集合論のような共通言語には到底なりえんのじゃないかな。 言語（道具）にしては難しすぎるし奇妙すぎる。 478 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 16:04:59.16 ] >述語論理（λhol含む）や集合論のような共通言語 述語論理上の理論である集合論と述語論理を並列な言語としてる時点でアウト！ 479 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 17:27:53.50 ] >等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれる 「等号なし」とは、等号記号が言語に入っていないのか、記号はあるが等号公理が入っていないのか。 中身以前に、自分の発言に必要な情報が欠けていて多義的であることに気づかないってのは、やっぱり駆け出しの証拠だ。 謙虚に勉強しなおすがよろしかろう。 ちなみに、前者だとすると、標準的な外延性公理がそもそも記述できない。 後者ならば>>475の言う通り。どちらにしてもおかしい。 480 名前：１３２人目の素数さん [2012/02/03(金) 18:12:32.14 ] >>478 あんたもそういう区別がやっとできるようになった駆け出しだな。 もっと大事なことを言えよ。 481 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 19:14:49.34 ] 欠けた情報は集合論という言葉に対してもそう。 一階述語論理上のZFC⇒集合論だが逆は成り立たん。 482 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 19:39:41.34 ] ┌∩┐(◣_◢)┌∩┐ Suck me! 等号公理を抜いた一階述語論理。 こいつさんに2項述語＝をぶち込むさかい。 483 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 00:23:06.52 ] Require Import Classical_Pred_Type. Section Generic. Variable U:Set. Require Export Le. Require Export Lt. Require Export Plus. Require Export Gt. Require Export Minus. Require Export Mult. Require Export Between. Require Export Peano_dec. Require Export Compare_dec. Require Export Factorial. Require Export EqNat. Require Export Wf_nat. Require Import Decidable. Goal forall n, n<=n. Goal forall n, n<=n->n<=n. Goal forall n m, n<=m->m<=n. Goal forall n m, n<m->m<n. Goal U=U. Goal exists n,n<n. Theorem A0:forall(a b c:nat),a=b->a=c. Proof. intros. 先ずは準備っと。 484 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 02:08:35.82 ] >>473 「数学の基礎としての○○論」の研究なんてのはきょうび流行らない。 元祖の集合論でも、数学の基礎としての集合論の研究なんて久しく聞かないね。 485 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 04:09:04.46 ] 482を恥の上塗りというのだなｗｗｗ 486 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 05:08:41.52 ] >>485 同感。 ところでmother fuckerの┌∩┐(◣_◢)┌∩┐って 馬鹿さ加減というか無知さ加減が以前の「考える人」と良く似てると思うのだが。 487 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 06:18:45.27 ] >>484 確かに。部外者が想像する集合論と、実際に集合論で研究されている内容には差異があるかも。 数学の基礎として集合論を志すと、研究の現場に行ってみると 「こういうことをやりたかったのではない！」と思うだろうな。 　　たしかに専門分野としての集合論は「集合というものの性質を定める規約集」ではなく「累積階層という対象の構造を探求する研究」になっていますね。 とはキューネン本の訳者の言。 488 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 06:47:41.58 ] >>486 禿堂 489 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 09:32:19.48 ] (*鶏慣れのために算術命題をチェック。*) Goal forall (n m : nat)(f : nat -> nat), (S n = S m) -> n = m->f n = n -> S (f (f n)) = S m -> n = m. intros. rewrite H1 in H2. rewrite H1 in H2. apply H0. Qed. 490 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 11:17:47.41 ] スレチですまんのだけど、Coqだと Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x. という風に等号を定義するだけで（ちなみに上記の意味は、「Type Aの変数xに対して x=x（eq A x xのこと）の証明が存在することを仮定し、その証明をeq_reflと名づける」といった感じ。） eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, eq A x y -> P y というような等号公理が導かれてしまうけど、これってどういう原理なの？ わかりやすい説明とか文献あったら教えてくだされ。エラいひと！ 491 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 12:25:40.34 ] >>481 欠けた情報：⇒の意味 怪しげな記号の使い方をするのもトンデモや駆け出しの証拠ｗ 492 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 13:27:08.40 ] >>473 >かなりの部分は一階述語論理の直上のものとして理解できる とすると、ZFC その他一階述語理論としての集合論と同じく、 一階述語理論としての圏論がある筈だけど、そんなん聞いたことないぞ 493 名前：１３２人目の素数さん [2012/02/04(土) 13:34:28.50 ] >>491 それはつまらん言い掛かりにしか見えない 494 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 18:53:42.74 ] >>491 いや、言いがかりではなく481は何を言いたいのか分からん。 自分で読み返してみてそれに気づけないのなら真性駆け出し。 玄人に質問の意図を伝えられない素人の図、だなｗｗ 495 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 19:14:08.17 ] Awodeyの教科書に 集合論は数学の基礎だというのと 圏論は数学の基礎だというのは意味合いが違うよ的な話が書いてあるよ 496 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 19:19:34.73 ] こういうのこそ2chらしくていい 俺は「真性」は大歓迎よ もっと自己主張してほしい 497 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 19:36:05.78 ] 「集合論の公理系」と「ZFC（＋追加公理）」は イコールじゃないよというようなことを言いたいんだろうけど、 handbook of set theoryとかJechとかは 事実上ZFCかその保守拡大のBGのことしか書いてないよ 良くてMKにちょっと言及するくらい 498 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 19:41:01.53 ] 結局、「⇒」で何を言おうとしているのかが分からないことが原因。 499 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 19:53:43.05 ] 多分 一階述語論理にZFCの公理を加えることだけが 集合を展開する唯一の手段ではない、という趣旨かと。 500 名前：１３２人目の素数さん mailto:sage [2012/02/04(土) 20:42:18.03 ] >>495 定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。 他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。 「集合論は数学の基礎」というのも、Simpson 的な意味で言われる場合もあって、 Awodey が彼の本で言及しているような意味とは必ずしもならない。 結局のところ、言われている文脈を考慮しなければ、どういう意味かは分からない。 しかし「ひねっていない」言葉の意味、というか伝統的なオーソドックスな意味というのがあって、 特に断り書きがないような場合には暗黙の了解的にその意味で理解すべき、というのがある。 それが「数学各論と一階述語論理を繋ぐ」という意味だし、 これがオーソドックスだからこと Awodey が対比の為に言及している。 （オーソドックスでなければわざわざ対比に使わない。） このオーソドックスな意味での「圏論による基礎」は、 オーソドックスなだけにかなり長いこと研究されている。 いまどき流行らないというのは認めざるを得ないところだが。

---

---

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

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