数学基礎論・数理論理学のスレッド　その7

1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その6 kamome.2ch.net/test/read.cgi/math/1265884076/ 507 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 19:08:36.22 ] 予習が完了しました。 今夜からΩ-論理の説明をはじめましょう。 508 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 20:39:42.43 ] >>491で大抵答えられますって言ってたのは 勉強したら答えられるようになりますって意味だったの？ 勉強したての人間の説明は何が本質的なのか全然分かんないから勘弁してほしい 509 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 21:28:09.34 ] いえ、「Ω-論理以外」は何でも答えられるという意味である。 上記のリストにΩ-論理はない。 510 名前：１３２人目の素数さん [2011/04/06(水) 10:18:46.30 ] １０は３で割り切れないって言うけど１０人分のケーキを三人に分けることはできるんだが？ hatsukari.2ch.net/test/read.cgi/news/1302019119/l50 511 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 11:09:08.03 ] >>510 凄い発見だな！僕は自分の人生さえ割り切りが付かないぞ！ 512 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 22:33:49.35 ] 仏教論理もこのスレでいいの？ 513 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 23:42:36.65 ] >>512 現在仏教論理は主流ではないですね。 量化が特殊なので非常に研究が難しい。 イスラエルでマルグリス（超剛性定理で有名な）らにより 研究されているキリスト教的論理学との関連が指摘されています。 キリスト教的論理学の推論規則ではほとんどの仮定が落ちません。 514 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:01:16.27 ] インド論理⊇仏教論理∪易罫 515 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:03:17.55 ] 仏教論理は様相論理 516 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 13:06:25.30 ] 区体論はこのスレでいいんすか？ 517 名前：１３２人目の素数さん mailto:sage [2011/04/08(金) 20:06:05.60 ] >>494 > Taoのblogに載ってたようなcommon knowledge的な話とかかな？ え？ テレンス・タオってロジックにも進出しているの？ 天才に来られると萎縮するわ... 518 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:12:13.38 ] >>505 N型推論図（フレーゲ流）はNKなどの公理を持たない体系で、 仮定を落とすのを記述するのに使われることが多いです。 L型推論図はシーケント計算など仮定がない体系で使われます。 一般的な数学はNKのN型推論図などを用いると表現しやすいです。 シーケント計算のL型推論図は様々な論理式を 証明するのに下から辿れるので使いやすいです。 本によっては → が |― と書かれていたりしてまちまち。 またHKは仮定がないのでL型で書かれることが多いです。 （HKは公理の変形が複雑だが部分構造論理で使われるそうな） それから論理式の左側にtermと呼ばれるものをつけて、 証明の経路を辿れるようにしたものもありますね。 この際、NKの仮定をラムダ項に対応させることが出来、 カリー・ハワード対応と呼ばれることもあります。 仮定の落ちる回数に制限を設ける論理もあったと思います。 519 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:16:06.90 ] ま初歩的な証明論程度の質問ならなんでも 答えられるので何でも聞いて良いですよ。 520 名前：１３２人目の素数さん mailto:sage [2011/04/10(日) 21:52:24.80 ] 実は証明論に公理は不要である。 これを知らないから無駄な努力をしてしまう。 521 名前：１３２人目の素数さん mailto:sage [2011/04/13(水) 23:51:38.10 ] kamome.2ch.net/test/read.cgi/math/1293882228/980 岩波書店5月　『数学基礎論』新井敏康　著 ttp://www.iwanami.co.jp/hensyu/science/next.html 気合入ってるなあ　楽しみ みすずから出たトルケル・フランセーンの本もかなり良いよ。 ロジック専攻というレベルじゃなくて不完全性周りが まさに著者の専門だからかなり細かいことまで徹底的に書いている。 但し著者独自の主張じゃないか、と思うようなことも無いではないけどね。 訳者の田中先生って今どうしてるんだろうか。 今年春に東工大で講演会やるみたいな話あった気がするけどどうなってるのかな。 522 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 07:08:42.36 ] 微積分みたく入門書ばかりがどんどん増えていきますね。 メドベージェフ次数が日本に紹介されるまではまだかかるでしょうね。 523 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 08:18:58.10 ] 　　ま　　た　　お　　前　　か 524 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:12:25.74 ] 日本語の本は入門書のみで十分。 後は英語の世界。 525 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:20:30.70 ] >>521 内容は Shoenfield のと同じようなもん？ 526 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 20:55:12.37 ] >>525 Shoenfield は証明論がなかったですよ。 それから計算理論が何を指しているのかが分かりません。 ページ数が気になりますね。 解説を読む限り強制法にも触れてそうですね。 ただメドベージェフ還元まではいかないと思いますね。 527 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:34:06.56 ] 帰納関数論でしょ。 528 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:39:51.30 ] 原子帰納関数を導入してから、 ゲーデルが証明したのに近い不完全性定理を導入するってことですか。 算術的階層やペアノ算術までいくShoenfieldよりは進まないということかな。 529 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 22:15:29.27 ] ペアノ算術やらないわけない。 入門篇で原始帰納関数、基礎編で超限帰納法やるんじゃないだろうか。 530 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 00:58:48.51 ] 集合論をかなりやってから証明論に進む構成だから、 新井先生の専門とかから考えるなら、 再帰的Mahlo順序数とかを使うKP（ZFの断片）に対する順序数解析とかに 触れたりして現代の証明論を紹介したいのかな、とか思ってるんだけど。 PohlersのProof Theory: The First Step into Impredicativity（11章）とか RathjenのThe art of ordinal analysis www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf とかの後半（2.2. Set theories.以降）とか。 新井先生のarxiv.org/abs/1102.0596で言うなら4 Jäger以降の内容。 ちょっと希望的観測過ぎるか。 531 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 20:27:40.85 ] 順序数解析はやっぱり入れるんじゃないか 532 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 01:08:11.68 ] にわかで申し訳ないんですが、 モデル理論とはどのようなものなんでしょうか ゲーデルあたりの研究成果を元に生まれたとは聞いたんですが 533 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 07:46:53.79 ] 理論のモデルを研究することですね。 534 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 17:24:57.55 ] >>532 タルスキが最初だよ。 ゲーデルと並行して研究されてた。 535 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 22:55:12.90 ] >>533 >>534 なるほど 「モデル」がどういう意味なのか分からなくて困ってましたが 要は意味論のことなんですかね ありがとうございました 536 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 23:57:38.44 ] 正確には意味論がモデルと等しいわけではないですね。 1階述語論理の意味論は構造と呼ばれており、 この構造である理論のどんな論理式を解釈しても、 真になれば構造が理論のモデルになるとされますね。 つまりある理論を「まともに」解釈できる構造のことですね。 無矛盾な理論はモデルをもつ。 という完全性定理がモデル理論の初期の研究成果です。 それからコンパクト定理とレーベンハイム・スコーレムの定理は どんな本にも載っていますね。 例えば、 可能世界で有名なクリプキ構造は様相論理のモデル、 チューリング・マシンはある計算理論のモデル、 2^ωが型なしラムダ計算のモデルになったりしますね。 ハインティング代数やブール代数などの代数的構造を モデルにすることで、論理学を代数にする手法もあります。 モデル間の同型写像を考えて構造同士の関係・分類もできます。 連続体仮説のZFCからの独立性を証明する強制法のアイデアも 提供しておりますし、モデル自体をZFC上で形式化する研究もあります。 また様々な階数の述語論理を計算の複雑さの階層 （EXPとかPSPACEとかNPとか...）に対応させ、 算術的階層などと組み合わせて現代数学の全体像を浮かび上がらせる 記述計算量理論というものにもアイデアを提供してます。 大雑把にいって証明論に対して存在しているようにも思われます。 537 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 00:03:25.54 ] 訂正： つまりある理論を「まともに」解釈できる構造のことですね。 ↓ つまりある理論を「正当に」解釈できる構造のことですね。 まともでない解釈も存在しますからね。 538 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 11:25:13.19 ] なるほどなるほど 面白そうですね 丁寧にありがとうございました！ 539 名前：１３２人目の素数さん mailto:sage [2011/04/22(金) 21:46:08.83 ] 上の方で登場したヒルベルトの公理なんですが、 これっていくつ位存在するんですか？ リストみたいなものってありますか？ それから今使われてる公理はなぜ使われるようになったんですか？ 540 名前：１３２人目の素数さん mailto:sage [2011/04/23(土) 08:16:45.01 ] ベクトル空間の基底の取り方みたいなもので無数にあるよ たぶん自分で独自に選んで本書く人も多いんじゃないかな 541 名前：１３２人目の素数さん [2011/04/23(土) 11:40:28.66 ] 自称論理学者（ID:M/m1hILG）がとんでもない論理を展開中 yuzuru.2ch.net/test/read.cgi/edu/1291023518/l50 542 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 00:15:26.75 ] 例えばヒルベルト流命題論理の 含意断片論理（論理記号が'→'だけのもの）で、 大抵の教科書に出てくる公理のように メタ変数が3個で論理記号4個でカッコの付け方が正常な論理式の総数だけでも、 ざっと概算したところ100万個を超えた。 一般の命題論理の¬や∧、∨など5種類ほど加えると数十億に到達するらしい。 公理選択で重要なのは、「独立」を調べること。 MPを推論規則にもつとき、 A→A A→A→A A→A→A→A の3つで上の2つの文は下の文から証明可能なので公理に不要。 「完全性」「健全性」「独立」などの条件が重要で、 定理自動証明機械なども研究された。 歴史的にほとんどの証明体系が意味から出発している。 にもかかわらずそのほとんどが上記条件を満たすのである。 543 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 07:10:00.79 ] 数十億ではなく6億くらいですね。 カッコの付け方が位相みたいに、 シンプルに計算できないので正確ではないですが。 544 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:39:01.16 ] おい、公理系の独立性はたいして重要で無いだろ。 おまいは、命題論理の公理系学んだとき、その独立性チェックしたか？ 多くの教科書同様、完全性と違ってしてないはずだ。 545 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:57:23.11 ] 独立でなくてもいいのなら、明らかに無限通りあるからじゃない？ 546 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 20:39:31.01 ] 大抵の教科書に掲載されているHKの公理は、 ある程度意味のあるもの、 例えばLKとの同等性が示せるものだとかに 絞られているわけです。 つまり独立性を示す努力は本の著者というか、 「論理の歴史」が勝手に代替してくれているわけですね。 私が言いたかったヒルベルト流とは推論がMPだけという意味です。 そして独立性の証明は完全性よりはるかに煩雑です。 確かに必須ではありませんが、 無から公理を創造する場合は独立に近くする努力はするべきですね。 547 名前：１３２人目の素数さん [2011/04/24(日) 22:41:45.58 ] 論理学をやる人は高踏趣味があるのかやたら専門用語を散りばめた文章を書く。 少し解りにくいことも解っていて当然なような口ぶりだ。 548 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 22:53:10.92 ] 分かっている人ほど簡素な文を書く 分かったふりをする人は難解な文を書く 549 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 01:06:51.10 ] >544 重要でなければ強制法とかの技法も要らない気がするけど。 550 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 07:12:08.71 ] いや述語論理の独立性の話だろ Principia Mathemticaの公理なんか 独立じゃないことが数十年後に判ったんだぞ 551 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 11:42:06.24 ] 独立性の証明は難しいことが多い。 しかし証明が必要になることはまず無い。 552 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 16:59:17.12 ] 与えられた体系の中での命題の独立性と、 公理系そのものの独立性の話の話は区別しないと。 前者は気にするのが普通だし、重要な問題であることも多い。 後者はよほど特別なことがない限り、気にすることはない。 553 名前：546 mailto:sage [2011/04/25(月) 20:50:54.18 ] >>547 それは私のレスポンスに関するものでしょうか。 そうであるとしたら具体的どこに高等趣味があるのかを、 該当箇所の引用したうえで述べてください。 >>551 詳しそうなので質問します。 独立の証明の有益な方法はありますか？ それから証明する必要がないとはいえ、 テキスト中のHKは大抵独立だったり完全だったり 無矛盾だったりして、 「子供が安全に遊べるように人為的に作ったアスレチック」で あることが多いとは思いませんか？ >>548>>550>>552 同感です。 554 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:04:40.48 ] 自覚あるんだね 555 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:22:09.77 ] いつぞやこのスレで総スカンを食らったコテの匂いがプンプンする 556 名前：546 mailto:sage [2011/04/25(月) 21:23:12.91 ] >>554 ローマに入ればローマに従えというか、 論理学を語る時だけ独特の文体になることは確かだと思います。 しかし、文章の中に含まれる専門用語は他の数学に比べれば かなり少ないと思いますが？ （まさか専門スレッドでテクニカルターム禁止だというわけでもないだろうし。） それに難解なことなんか言ってないんですよ。 普通に1階述語論理までやっていれば言いたいことは 分かると思うんですが。 557 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:34:54.22 ] それを言うなら郷に入っては郷に従えだ 英語のことわざとごっちゃにするなよ、半可通 558 名前：546 mailto:sage [2011/04/25(月) 21:45:09.44 ] >>557 >郷に入っては郷に従えだ あえてローマに入ればローマに従え といったんですが。 意図的に日常さはんじをちゃめしごとと読んだり、 既出をガイシュツと呼んだりする、 当たり前だのクラッカーみたいなノリで言ったんですよ。 これに関して本気で突っ込むそちらの方が半可通なのでは？ 559 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:58:46.82 ] 図星みたいだ 560 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 23:02:07.21 ] これはみっともない 561 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 00:10:16.55 ] >>558 ばーか 562 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 07:15:02.06 ] どうでもいいことで何を議論してるんだか…… Shoenfieldの第一章の演習問題は独立性を公理それぞれに対して証明しているよね 著者がそういう細かいことにこだわる人だったのかもしれない 563 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:09:34.17 ] >>552 > 与えられた体系の中での命題の独立性と、 > 公理系そのものの独立性の話の話は区別しないと。 前者はどういう意味? ある形式系で命題が形式系の他の公理から独立なら それは公理として認めないと真には成り得ないけど? 後者の「公理系そのものの独立性」って公理系が何対して独立なの? 564 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:11:21.23 ] >>562 独立でない公理があるなら、それは公理としては不必要なんだから、 基礎論的な意識の強い学者は当然こだわるわな。 565 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 18:31:40.30 ] >>563 そういう根本的なことから理解出来てないと、ビックリする 566 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:05:38.43 ] いくつかの公理・推論規則と それから証明可能なすべての論理式の集合をS、T、 ある公理または推論規則をA、 S＝T∪{A} としたとき、 TでAが証明できない。⇒SでAは独立。 Aが任意⇒Sは独立。 独立性証明のテクニック⇒3値論理。 567 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:22:28.23 ] おー久しぶりだな「考える人」 正直もう二度と見たくなかったが。 568 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:25:18.26 ] 訂正： 誤 Aが任意⇒Sは独立。 正 上記条件プラスAが任意⇒Sは独立。 計算機科学とかでは体系が 独立じゃないと一般的に色々複雑になるらしい。 569 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:04:15.53 ] >>564 集合論のZFとかだと各公理は独立じゃなかったりするでしょ。 独立性が大事かどうかというと、あまり大事じゃない場合も多い。 少なくとも完全性に比べると些事。 >>566 一般的にはAも¬Aも証明できないときに「独立」という気がするけど。 反証可能な場合は普通は含めない。 あとAが任意って何が言いたいのか分からない。 任意の式Aが証明不可能だということはあり得ない。 三値の真偽値の割り当てで証明不可能性が証明できることもあるけど 証明できないことも多いと思う。 570 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:07:16.28 ] >>569 ここはエレキな人が多過ぎて困りますなあw 571 名前：566 mailto:sage [2011/04/26(火) 22:10:07.14 ] >>569 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Aを証明できないことをいう。 さらにその公理系Sの中のすべての公理と推論規則が独立なら 公理系Sは独立。 という主張をうまく書こうとしたところ変な文章になっただけです。 なぜ、「Aも¬Aも証明できないときに「独立」」という定義に しないかといえば、 ¬という記号が公理系で必ずしも定義されているか不明だからです。 （公理的集合論やるなら気にしなくてもいいかもしれませんが。） 例えば¬AがA→⊥のメタ理論的な略記だとしても、 ⊥が公理・推論規則に含まれていないために、 単なる命題変数になっている場合もあるかもしれません。 それから3値論理はそういう方法もありますよ、位に行っただけです。 一般的に独立を証明する巧い手段は知りません。 572 名前：１３２人目の素数さん mailto:sage [2011/04/27(水) 00:21:21.26 ] そういや、公理がそれぞれ独立なZFて誰か考えないのかな？ どうすれば良いのか想像もつかないけど…… 573 名前：１３２人目の素数さん [2011/04/29(金) 08:43:43.06 ] 数理論理学の組み合わせ論的研究の本OR分野を教えてください。 上の論理式の総数みたいなやつです。 574 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 09:47:53.77 ] www.amazon.co.jp/dp/4320122097/ 575 名前：１３２人目の素数さん [2011/04/29(金) 23:10:35.52 ] >>558 ＞意図的に日常さはんじをちゃめしごとと読んだり、 ＞既出をガイシュツと呼んだりする、 ＞当たり前だのクラッカーみたいなノリで言ったんですよ。 若者＝バカモノっていうのはホントだね。 ホルモンが無駄に出てるせいかな？ 576 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:29:08.45 ] >>558が若いのか結構年取ってるのかも分からないし 仮に若かったって若者が皆バカって訳じゃないと思うけどなあ 577 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:44:05.25 ] >>571 それ「独立 independent」じゃなくて普通に「証明不可能 unprovable」で良い話だよね 578 名前：１３２人目の素数さん [2011/04/30(土) 10:50:22.25 ] >>577 大抵の論理学の本に書かれている定義に準拠しているなら、 独立は証明不可能より条件が強いと思います。 独立性は「公理と推論規則に無駄がない」という主張です。 証明不可能は理論の持つ公理と推論規則だけで 特定の論理式の証明図が書けないという主張です。 579 名前：謝罪 mailto:sage [2011/04/30(土) 10:56:05.79 ] >>571 を読み返してみたところ間違っていました。 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Sで証明可能な式でTでは証明できないものが存在すること。 でした。 580 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 11:18:11.62 ] >>579 謝罪を受理しました。 では続きまして、『賠償』を求めます。 宜しくお願い致します。 581 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 12:13:51.50 ] まぁ独立性って言葉を使うから議論が起こるわけで、 単に公理と推論規則に無駄がないって言えばいいんだと思う。 加えて言うと、独立性はもちろんのこと、 完全性や無矛盾性さえ体系には必要ない。 582 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 16:41:03.73 ] ある公理が公理系に対して独立であるというのは、 公理系に肯定を付け加えても、否定を付け加えても矛盾しないってことです。 無駄がないとかアホか。 583 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 19:01:36.70 ] で結局どの独立がホントの独立なんよ。 584 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 19:56:17.91 ] 多分>>579は現代数理論理学序説(P56)に載っている奴だと思う。 これと>>582は同値だけど、こっちの方が良く見かける。 585 名前：１３２人目の素数さん [2011/04/30(土) 20:34:00.85 ] 否定のない論理体系も考えたいからややこしい言い回しをしてるんでしょ。 意図を明示しないでもってまわった記述をするから高踏的って言われるんだよ。 586 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:05:18.03 ] >>579 揚げ足ですが、 普通公理系って閉論理式の集合だから 推論規則は入らないと思いますよ。 形式体系とか言った方が無難だと思います。 587 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:08:55.34 ] >>577を独立って言っているケースもあるよね。 >>582より弱くなるはずだけど。 588 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:19:28.53 ] 否定のない体系では無矛盾性とかどうなるんだろう... 589 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:21:07.74 ] 現代数理論理学序説みたいに部分構造論理とかBCK論理の話とか、 様相論理みたいにS3とS5は証明できる式が違うとか そういうことをやりたい場合の独立性の話をしてた訳ね ヒルベルト式の述語論理に限って言えば、 ああいう体系の独立性を調べる作業は ただの面倒くさいだけのパズルに過ぎないと思う あと、カット除去定理があるからsequent計算のカット規則は「独立」ではないわけだけど だからといって無駄がある、というような見方が如何に浅薄かというのも 証明論の本によく書いてあると思うけどね カットを使わないと証明の長さが指数関数的に長くなる >>581 無矛盾性は大抵の場合は必要だけどね 590 名前：１３２人目の素数さん mailto:sage [2011/05/01(日) 07:36:51.86 ] >>589 > 現代数理論理学序説みたいに部分構造論理とかBCK論理の話とか、 > 様相論理みたいにS3とS5は証明できる式が違うとか > そういうことをやりたい場合の独立性の話をしてた訳ね この場合の独立性以外ってのは例えばどういったものがあるのでしょうか？ 591 名前：１３２人目の素数さん mailto:sage [2011/05/01(日) 09:26:47.68 ] 例えばShoenfieldの本の演習問題みたいなやつとか。 結果自体の意義としては、独立だと分かったからどうなの？ ということになっちゃうので、あくまで独立性を示すためには 新しい真偽値もどきを定義したりしてこういうことをやるんだよ、 というテクニックの習得のためだけに設けられた演習問題だと思う 592 名前：１３２人目の素数さん [2011/05/01(日) 22:58:39.80 ] BCK論理とか様相論理の各公理系についても、 体系の強さが相対的に比較できれば良いだけ。 ある論理式が証明できるかどうかに着目しているため、 体系自体の独立性が問題になることはない。 また否定のない体系ではすべての論理式が証明可能であるため、 あまり意味のない体系になる、零環やX/=みたいな 数学的に面白みのない構築物になる。 根源まで戻れば論理学も所詮組み合わせ論的構造の産物でしかないし、 意味のない構造が無数に作られる。 こういった主張をするのならばそれは、 「すべての数学はグラフ理論（または数論、2進数）で書きかえられる。」 といった、「数学は記号で書かれている。」といった主張と 同レベルの無意味な議論になってしまう。 もちろん根源はバベルの図書館的宇宙における カオス的情報の広がりへと到達してしまい 人類は自ら数学という精神活動を停止させることになる。 593 名前：１３２人目の素数さん [2011/05/01(日) 23:00:30.52 ] >>592 誤：また否定のない体系ではすべての論理式が証明可能であるため、 正：また否定のない体系ではすべての論理式が定理であるため、 594 名前：１３２人目の素数さん mailto:sage [2011/05/02(月) 01:39:50.54 ] たとえば BCK 論理ではすべての論理式が定理となると 書いていることに気づかないのかなあ。 595 名前：１３２人目の素数さん mailto:sage [2011/05/03(火) 12:31:38.14 ] すいませんが、 ススリン線を加えたZFでも ストリクト・ヴァイハードの定理は成り立つのでしょうか？ 596 名前：１３２人目の素数さん mailto:sage [2011/05/03(火) 22:00:08.65 ] 成り立つよ。 ¬SHならGCHやdiamondを加えたものでも成り立つ。 597 名前：１３２人目の素数さん mailto:sage [2011/05/04(水) 10:43:55.19 ] パタゴニアの庭とかいわれる順序が 入ったErdos Universeに非分岐独立なType構造を定義すれば、 ススリン仮説が無効化されること、 いわゆるパタゴニア予想が去年肯定的に解決された。 598 名前：１３２人目の素数さん mailto:sage [2011/05/05(木) 11:10:17.61 ] ﾊｲﾊｲﾜﾛｽﾜﾛｽ そのハッタリを張る能力を生かして、 数学なんかやってないでSFとかラノベとか書いた方が良いんじゃないか？ 599 名前：考えない人 mailto:sage [2011/05/05(木) 12:27:16.78 ] 公理の独立性がもしも証明されないのだとすれば、 すべての公理系の中に他の公理から 証明されるような公理が存在することになります。 この場合の被証明公理のformulaの変形、 つまりλ-formulaのβ-reductionを考えると、 無駄な関数適応や関数抽象が生じることになって、 エレガントではなくなるのではないでしょうか。 600 名前：１３２人目の素数さん [2011/05/05(木) 14:05:10.25 ] >>598 あんた良く俺が学生時代にSF幻想文学オタだったってわかったな。 やっぱ発想が似てくるものなのか。 601 名前："屁理屈王子" [2011/05/05(木) 22:02:37.49 ] おう、ｵﾂﾑいい>>1-1000 ok "勝てねぇヨゥ？">> ��c.2ch.net/test/-/soc/1297053366/67-�� みんな〜！！？(みんな〜！！？＾＞｀) 602 名前："世界的サディスト" [2011/05/06(金) 19:45:42.26 ] なんだ 《アインシュタイン共》 もう 【【【【【涙目】】】】】 か・・・・・ 603 名前：１３２人目の素数さん mailto:sage [2011/05/19(木) 21:43:03.06 ] 岩波書店　『数学基礎論』新井敏康　著 立ち読みしてたら、文献のところに HinmanのFundamentals of Mathematical Logicは大著だから 本書よりも記述が丁寧とか書いてあって焦った いやいやいや 604 名前：１３２人目の素数さん mailto:sage [2011/05/19(木) 22:54:44.24 ] もう出てるんだ。 amazonもう品切れで、中古が15,250円w >>603 あれ900ページあるもんね。 数式多いとはいえ、日本語500p.と英語900p.だと、 軽く倍以上のヴォリュームになる。 605 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 06:13:37.53 ] >>603 昨日買って読んでるけど、日本語でこれ程の内容が読める日が来て感動してる。これをきっかけに基礎論ブーム来ないかな。 606 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 17:09:24.34 ] >>605 来ない。 「基礎論」なんて勿体つけた哲学っぽい呼び方は時代遅れ、つうか「基礎論」なんていつの時代の呼び方だ。 今や変な色のついてない技術的な側面だけに着目した数理論理学が分野の呼び方としては適切だが （基礎論屋と称する連中のどれだけが実際に数学の基礎付けに本気で関心を持ってるんだよ？） Girardが「math logicは初めて応用分野を得た」と呼んだ応用分野としての理論計算機科学そのものが 今や瀕死の状態だから数理論理学も今となっては流行遅れの分野。 部分的にはモデル論とかで数学の他の分野との交流はあってそういう分野はそれなりに生きてるけど。 607 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 17:34:17.17 ] 別に数学の他の分野が特に流行ってる訳でもないけどね だいたい流行がどうとかで判断するのがおかしい

---

---

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

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