- 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/
- 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 ]
- 別に数学の他の分野が特に流行ってる訳でもないけどね
だいたい流行がどうとかで判断するのがおかしい
- 608 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 20:45:22.25 ]
- むしろ数理論理学は今でこそ応用計算理論を学習する際の必須科目になってるんだけどな。
これを体系的に学んできた人間とそうでない人間で問題に対する取り組み方がまるで違う。
- 609 名前：１３２人目の素数さん [2011/05/21(土) 21:00:32.16 ]
- もしかして学問板ログ消滅後、
情報学板はみんなこっちに流れてきてる？
- 610 名前：１３２人目の素数さん [2011/05/21(土) 21:03:49.00 ]
- >>608
自分は門外漢だけどどう違うのか興味有る
- 611 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:10:48.33 ]
- 「応用計算理論を学習する際」の道具として使うのと、基礎論自体を研究するのは全く別だろ
- 612 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:31:02.69 ]
- 新井さん自身が基礎論的な立場じゃなくて、
ロジックは今や基礎論を離れて数学の一分野だって立場の人。
だから竹内の基本予想について、
当時竹内さんが基礎論的立場から言っていた
「予想の解決方法は～であるべき」という言葉に反発する文章を書いている。
ただ最近は逆数学など基礎論的な動機が残っている分野も盛ん。
- 613 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:33:04.38 ]
- 「応用計算理論」ってのが何を意味しているかよくわからんが、
逆数学と計算量理論(特にP=NP周辺)はほとんど不可分になってきている。
- 614 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:48:27.70 ]
- ＞それでは基本予想の解とはどのようなものであるべきか ?
＞残念ながら竹内自身はこのことに殆ど触れていない。
＞ひとは訝しく思うかもしれない：ここで言う 「構成的」 とはいかなる謂か ?
＞数学的に正確に定義されているか ?例えばある形式的理論Tで形式化できることが
＞「構成的」であるための必要十分条件となるTがあるのか ?
＞これに答えて曰く：基本予想のような grand program において、
＞その開始以前にこのようなことを問うことは単なる怯儒というべきである。
＞何が構成的か或いは得られた証明が構成的か否かは、証明 が得られてから
＞吟味すればよいし、 その価値は得られた洞察から判断するほうが生産的である。
こういうの読むと単純に数学として追求するというのとも違う気がするけどね
- 615 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 23:08:08.45 ]
- 整数論で例えれば
類体論の証明ができてから「代数的証明」を求めればいいようなものか。
- 616 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:00:45.29 ]
- >>614
そこをどういうふうに読んだの? 俺は、
< 「構成的」でなくてもいいからまずは証明すればいいじゃないか。
< 証明が得られれば、当然そこから生まれる知見があるはずで、
< 得られる前からこうでないといけないと言っても仕方がない。
と読んだ。最初ちょっとわかりにくいと思ったが。
確か同僚の渕野昌さんも新井さんの立場をそう説明していたはず。
もっと>>612のように直截的に書いてたと思った。
- 617 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:08:57.29 ]
- Girardやら高橋やらPrawitzやらの結果に関しては
こういう証明方法ではいけない、みたいなことを書いてるので
新井先生の立場は>>612とはちょっと違うはず
- 618 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:11:17.37 ]
- >>617
それはどんな分野でもあることでは?
- 619 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 02:57:23.57 ]
- >>617
> Girardやら高橋やらPrawitzやらの結果に関しては
> こういう証明方法ではいけない、みたいなことを書いてるので
> 新井先生の立場は>>612とはちょっと違うはず
竹内の基本予想に対するGirardや高橋の証明は数学の証明としては正しいが
竹内の言うところの有限の立場じゃない。
新井がそれらの方法ではいけないと書いていたということは
>>612の主張とは逆に新井は竹内なんかと同様に
証明論でもGentzen流の無矛盾性証明のような還元的証明論を信奉するってことで
ガチガチの哲学っぽい基礎論屋ってことじゃないか。
Girardや高橋の証明方法が良くないって主張するってことは
基本予想の価値を解析の無矛盾性を与えるって点に置いてるって事だからね。
そういう目的というか価値観ならば確かに有限の立場で証明しないと意味がなくなる。
逆に竹内の基本予想を単に２階論理でのカット消去可能性という純粋に数理論理学的な命題と考える人ならば
Girardや高橋の超越的な（つまり集合論を用いた）証明に文句を言う筋合いはない。
- 620 名前：１３２人目の素数さん [2011/05/24(火) 00:21:56.53 ]
- 松本先生の復刊数理論理学について質問なんですが
p29で述語論理の推論規則として
R1(ModusPonens)の他にR2、R3を付け加えていますが
そうする代わりに論理的公理を増やすことで
推論規則を1種類(R1のみ)のままにしておくことも
可能なんですよね？
- 621 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 00:48:35.20 ]
- >>620
一般化規則 φ->ψ implies φ->∀xψ は公理で置き換えることはできない。
- 622 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 10:07:43.78 ]
- お返事ありがとうございました
もう少し考えてみます
- 623 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 21:40:09.21 ]
- >>622
こういうときは、同等になるはずの論理の体系、
例えばNKの規則が導けるか考えてみるといいよ。
- 624 名前：長文失礼 mailto:sage [2011/05/25(水) 23:25:03.91 ]
- 以前から思っていたのですが、東京大学数理科学研究科准教授の
北田均さんってかなりヤバい（というかいわゆるトンデモ）ですよね？
先日生協書籍部に行った折に彼の「ゲーデル不完全性発見への道」を
ちょっと読んでみたのですけど、本の後半に間違ったことが
堂々と書いてあります（具体的には11．5以降）。数学的に間違った
偽の定理を証明するだけならまだ良いのですが、それを根拠に独自の
「哲学的」な帰結を引き出しています。一応Ahlforsの訳書などの
マトモな本も出している出版社なのに酷いものです。
- 625 名前：長文失礼 mailto:sage [2011/05/25(水) 23:25:50.96 ]
- 以前も「フーリエ解析の話」を見た時に感じたのですが、読むのが
かなり大変なはずのFefermanの論文を引用なんかしているので、
技術的に高度な間違いをされているのかも知れないと思って深入りせず放っていました。
ところが先日出た本には「Fefermanによると ω_{1}^{CK} ＞ ω^(ω^(ω^2))である」
などと頓珍漢なことが書いてあります。こんな（定義を分かっていれば）
自明なことを書くのにFefermanの名前をわざわざ引くのは異様なことです。
おそらく彼はChurch-Kleene順序数ω_{1}^{CK}の定義を御存じないのでしょう。
計算可能性理論の基礎的なことについて知っている感じもしません。
そもそも順序数の冪の定義もご存じ無いかもしれません。
- 626 名前：長文失礼 mailto:sage [2011/05/25(水) 23:26:09.87 ]
- 天下の東京大学数理科学研究院なのに、間違いを指摘してくれる同僚は
居なかったんでしょうか。今の彼のような人が東大数理で基礎論専攻を名乗っている限り、
「ロジックは哲学がかったトンデモに近い奴の集まりだ」と（特に東大の人に）
思われるのも仕方ないと思います。日本の数学研究の中枢にある大学の人が
「ロジック専攻の人」でまず思い浮かべるのが彼なのですから。
日本の数学者に東大卒の方が占める割合はきわめて大きいと思います。
アマチュア数学愛好家の個人ブログが間違っているのとは話が違います。
これは非常に憂慮すべき不幸なことですから、他大のロジック専攻の方も
東大数理に抗議するなり東大の方に知らせるなりした方がいいと思います。
今後きちんと間違いを指摘した書評が「数学」「数学セミナー」などの
雑誌に掲載されるのを期待しています。
- 627 名前：１３２人目の素数さん mailto:sage [2011/05/25(水) 23:26:24.53 ]
- 以下具体的にどこが間違っているのか書きます。両方とも同じ間違いですので
図書館にあった「フーリエ解析の話 第22章 数学は矛盾しているか？」に即して書きます。
21章までは量子論の観測問題っぽい話で内容上まったく独立していて、
331頁～340頁の高々10頁ですのでお暇な方は図書館などで借りて読んでみて下さい。
自分で買うのはお金が勿体無いかも知れません。
北田さんは御理解されていない可能性も高いのですが、まずω_{1}^{CK}は定義上、
ωの上の再帰的（計算可能）な整列順序の順序型の最小上界となります。
従って整列順序ω_{1}^{CK}自体は算術の述語を用いてω上に定義することができません。
- 628 名前：長文失礼 mailto:sage [2011/05/26(木) 00:17:03.38 ]
- S_α:「形式的集合論」Sのsubsystemとしての自然数論、
R_α：S_αのロッサー文（ゲーデル文を取ったって同じことですが）とします。
S_αの公理にR_αまたはその否定を付け加えた理論をS_(α+1)として、
「以下同様に」S_αを全ての順序数に対して定義してあります。
ところが論理式は可算個しかないのだから矛盾する。
基礎論のほうでは付け加える公理としてConsis_αを考えることが多く、
このような命題を公理として付加する場合基礎論のほうでは上述のプロセスが
Church-Kleene順序数と呼ばれる可算の順序数で終わるような制限条件が考えられている、
だそうです。なぜω_{1}^{CK}が上限なのか理解されていません。
不完全性定理の前提として理論S_αが満たすべき条件も理解されていない可能性も高いと思います。
- 629 名前：長文失礼 mailto:sage [2011/05/26(木) 00:19:47.54 ]
- その後、順序数の増加列α_nを用いて
ω_{1}^{CK} = ∪_{n=0}^{∞} α_n と表し、∃n [q~(γ)≦r∧γ＜α_n] を
確かめればよいから、「与えられた式A_γがS_{ω_{1}^CK}の公理か否か」は
n についての帰納法により有限回の操作で再帰的に決定できる、と書いてあります。
∃n …… という式を確かめるために帰納法をどう用いるつもりなのでしょうか。
n と α_n の対応は再帰的ではありませんから、∃n γ＜(α_n)∧……を
自然数論の論理式としてあらわすことも、確かめるプログラムを書くこともできません。
{α_n} が超越的に与えられていることをお判りでないのだと思います。
この後S_αの拡大はα=ω_{1}^{CK}で「ストップ」し、完全となるはずなのに
不完全性定理からこれは不完全であるから矛盾する、などと書かれています。
「ストップ」とはどういうことを想定しているかは分かりません。
- 630 名前：長文失礼 mailto:sage [2011/05/26(木) 00:20:01.46 ]
- 数学を勉強していると、相矛盾する二命題を「証明」できた気になってしまうことは
意外と良くあることです。でもそれが何十年も前から研究されている理論ならば、
その理論が矛盾している可能性より先に、自分の理解が間違っている可能性を強く考えるのが
常識的な態度ではないでしょうか。「よって数学は矛盾している」のような結論を
出してしまうのは、角の三等分家の類と同じ思考回路であると言わざるを得ません。
後はちょっとどこから突っ込めば良いか分からないので以下御説を全て引用します。
- 631 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 00:21:37.80 ]
- (pp.339-340)
このようにメタのレベルにおいても集合論が成り立つと仮定し集合論的論理を
対象理論である形式的集合論自身に適用しようとすると矛盾が生ずる。
ヒルベルトのプログラムでは有限の立場に立ち、メタのレベルでは有限回の操作しか許さないとし、
その上で対象世界では有限を超えた無限の存在を扱おうとする。こうする上では
以上述べたような矛盾は生じないが、対象世界が無矛盾と仮定すると不完全になる。
さらにこの無矛盾性自体が有限の立場では決定不可能となる。しかしこれを逆手に取り、
メタのレベルと同様に対象の世界自体も有限の立場に立つものとすると矛盾は生ぜず、
かつ対象理論は完全になる。正確に言えば対象理論たる集合論において無限公理を仮定しない、
- 632 名前：長文失礼 mailto:sage [2011/05/26(木) 00:21:50.56 ]
- あるいは自然数論においては数学的帰納法を仮定しなければ対象世界とメタの世界は
互いに対称になりかつこの設定において対象世界は完全かつ無矛盾となる。
上記で矛盾が現れたのは対象世界およびメタの世界の両者において
対象に無限公理を措定したためである。すなわち問題が生じたのは「無限」という実体が
対象世界およびメタの世界において存在すると仮定したからであり、「無限」が実体ではなく、
ある「仮想の存在である」とすれば数学は無矛盾かつ完全なまま存在する。
すなわち「数学的実体は計算可能なもののみであり、無限はその計算可能性を探る
補助的手段である」という立場に立てばヒルベルトのテーゼ
「無矛盾性と完全性を数学理論の健全性の証とする」は復活する。
（引用終）
- 633 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 01:40:49.16 ]
- ブログでやれ
- 634 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 08:18:32.04 ]
- チャーチ・クリーネは岩波数学辞典に定義が載ってたね
- 635 名前：１３２人目の素数さん mailto:sage [2011/05/27(金) 22:25:46.95 ]
- よくわからないけど、数学ガール読むより為にならない本ってこと？
- 636 名前：１３２人目の素数さん mailto:sage [2011/05/28(土) 15:27:54.55 ]
- 社会勉強になるかも。
- 637 名前：１３２人目の素数さん mailto:sage [2011/05/30(月) 17:00:59.04 ]
- ガスライティング
- 638 名前：１３２人目の素数さん mailto:sage [2011/06/01(水) 16:30:18.32 ]
- 「数学ガール」とは、部落、在日出身の女の子が差別を克服するために数学を研究する物語。
- 639 名前：１３２人目の素数さん [2011/06/02(木) 20:15:06.08 ]
- すみません、最近集合論を勉強し始めたものですが質問させてください。
集合族{A_x : x in X}があったとして、直積 Π(x in X) A_x (以後単に「ΠA_x」と書きます)
各xについて、それぞれ①A_x={1}のとき、②A_x⊂N(自然数の集合)、③A_xの濃度が可算
(∀A_x≠Φ)⇒(x in X) A_x (以後単に「ΠA_x」と書きます)
各xについて、それぞれ①A_x={1}のとき、②A_x⊂N(自然数の集合)、③A_xの濃度が可算
(∀A_x≠Φ)⇒(ΠA_x ≠ Φ)
が選択公理なしのZFで成立しますか？？
ちなみに私の考えでは①する。②する。③しない。
です。
- 640 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 20:53:54.97 ]
- 質問は質問スレで.
- 641 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 20:58:29.45 ]
- ∀の使い方がおかしい
何を言いたいか半分想像で答えると、>>639の考えの通りでo.k.
- 642 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 21:31:42.98 ]
- 他の分野と比べて質問スレに基礎論の質問してもかえってこないorちんぷんかんぷんな答えが返ってくるからしょうがないっちゃしょうがないんじゃ。。。
- 643 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 21:41:14.33 ]
- 基礎論の質問スレがあったよね。
なぜか基礎論に関係ない高校数学の質問とかが定期的に投げ込まれるっていう伝説のスレが。
- 644 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 00:44:16.80 ]
- >>643
> 基礎論の質問スレがあったよね。
> なぜか基礎論に関係ない高校数学の質問とかが定期的に投げ込まれるっていう伝説のスレが。
「数学基礎論」って数学の専門家以外からは「数学の基礎的な範囲」とか「基礎数学」って思われてるんだろ
あそこは本当に基礎論の質問をするには使い物になってなかったし、以前のサーバークラッシュであのスレは消滅したまま誰も再び立ててないんじゃないの？
ここもそんなにレスが多いわけじゃないから真面目な質問なら許してあげていいと思うが
- 645 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 00:56:22.43 ]
- > あのスレは消滅したまま誰も再び立ててないんじゃないの？
残念だったな、ここがその伝説のスレだ。
前スレが急に変なスレタイを採用して、このスレがそれを継承しちゃったけどね。
see >>2.
- 646 名前：M_SHIRAISHI mailto:eurms@hb,tp1.jp [2011/06/03(金) 05:00:59.00 ]
- www.age.ne.jp/x/eurms/Ronri_Kaikaku.html
- 647 名前：１３２人目の素数さん mailto:euler [2011/06/03(金) 05:16:55.68 ]
- >>646
なっ・・・なんなんだよそれ・・・
|
 |
