数学基礎論の質問スレッド

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 622 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 18:54:03 ] 強さは同じ 数学基礎論入門に、片方で導ける論理式はもう一方で示せることの証明も載ってる （まあこんなの読まなくても大体証明のやり方は見当付くと思うけど） 623 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 21:55:25 ] >Aを仮定し、その仮定のもとでBが導かれる ”普通の一階述語論理の公理系”に公理として論理式「A」を加えると、論理式「B」の証明が作れる >（Aという仮定なしに）A→Bを導くことができる ”普通の一階述語論理の公理系”にて、論理式「A→B」の証明が作れる 624 名前：１３２人目の素数さん mailto:sage [2005/09/19(月) 23:32:44 ] 自明でないのは演繹定理だけだな。 証明図の高さに関する帰納法で証明。 625 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 03:01:09 ] 演繹定理なしだと、証明問題がやたらムズイねｗｗｗ 626 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 13:18:13 ] >>619 ＞その分野の人は数学といえば集合論とか基礎論のことだとか思ってたりするｗ マジレスすると、まだそのあたりまでしか総括できていないだけ。 627 名前：１３２人目の素数さん mailto:sage [2005/09/20(火) 18:58:10 ] まだっていうか、数論幾何とか微分位相幾何学とか複素多様体論とか、 そもそも哲学の人は総括するつもりないでしょ まあ無くて構わないけど 628 名前：１３２人目の素数さん mailto:sage [2005/09/21(水) 11:47:03 ] レスくれた方、 ありがとうございました。 629 名前：１３２人目の素数さん [2005/09/21(水) 21:05:40 ] （例えば、）ロビンソン算術の公理系でのある論理式の証明を考えるときに、 根性が足らんくて、この論理式は、私には、証明可能できない、というのではなくて、 この論理式は証明可能でない、というのは、どうやって言ってるんですか？ ∀ｘ（0＋ｘ＝ｘ）はロビンソン算術の公理系で証明可能でない、というのを本で見たんですが、 630 名前：１３２人目の素数さん mailto:age [2005/09/21(水) 22:57:12 ] たとえばそれが成り立たないモデルを作るとか 『数の体系と超準モデル』の五章に問題として載ってるみたいですよ 本で見た、というのがこの本のことだったら済みません 631 名前：１３２人目の素数さん mailto:sage [2005/09/22(木) 21:36:13 ] いえ、いえ、どうもです。 とりあえず、図書館逝って借りて読んでみます。 632 名前：１３２人目の素数さん mailto:age [2005/09/23(金) 00:21:11 ] pp.116の問題1ね 問題1 次のことを証明せよ(1).........（略） (3) Qで∀ｘ（0＋ｘ＝ｘ）は証明できない 巻末に答えが載ってます 633 名前：１３２人目の素数さん [2005/09/29(木) 15:40:59 ] 295 ：１３２人目の素数さん ：2005/09/29(木) 11:58:46 夫馬です。 黒木先生。この基礎論・計算科学屋を叩いて下さい。 「完全証明」という専門用語を使い、「今まで数学 的に完全な証明がなかった！」というように素人に 思い込ませる。コケオドシをやっています。ポモ的 です。やっつけて下さいな。 ＞フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの ＞数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大 ＞工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との ＞約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り ＞などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が ＞完成。中村教授らは「完全証明したのは世界初」としている。 www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html 634 名前：１３２人目の素数さん [2005/09/29(木) 15:41:58 ] 302 ：１３２人目の素数さん ：2005/09/29(木) 15:16:20 >>301 ポモ的なのに叩かないのは、そういう理由だったんだね！ 土建屋＝宇沢＝長谷川＝黒木 ← 隠れポモ野郎 禿藁＝Ｕ健爾 ← 隠れポモ野郎 あほ鴨＝中村 ← 隠れポモ野郎 303 ：１３２人目の素数さん ：2005/09/29(木) 15:26:53 >>302 >>295 こいつらって、結局 ポモと同じでしょ。 ＞そして、別の場所で、極端なことを言っているのではないかと非難された場合には、 ＞3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。 www.math.tohoku.ac.jp/~kuroki/FN/relativism.html 635 名前：１３２人目の素数さん [2005/10/04(火) 21:26:07 ] 構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である、ってのは、 自然数上の足し算のみの体系は構文論的に完全で、モデル（Ｎ,＋,s,0）によって充足されてて、 証明可能でない論理式を加えたものは充足可能でないから、証明可能である論理式の範囲とモデル（Ｎ,＋,s,0）のもとで真である論理式との範囲が一致して、 で、モデル（Ｎ,＋,s,0）のもとで真である論理式の範囲を定義できる、ということですか？ 636 名前：１３２人目の素数さん [2005/10/05(水) 18:26:58 ] 358 ：今年のＡＡを振り返る ：04/12/29 09:28:40 　↓無職の引き篭もりのキモヲタの精神障害者フマ 　　　　　　　　〜∞ 　　 　／⌒⌒￣￣￣＼　〜∞ 　　／　　　　　　　　　　 ＼　　　〜〜〜〜〜 　　|　　　　　＿___丿ﾉﾉ.＿_|　　つ〜ん 　　|　　　 ／Ｕ　 .＿）　 .＿）　　　　ﾌﾟｩ〜ん 　　|　　　| 　 　　　　　 　 （　　　　〜〜〜 　　|　ノ（６ 　 ∵　（　。。） ）　　＿＿＿＿＿＿＿ 　　 　　　　　Ｕ　 　　) ３ .ﾉ　 /　＿＿＿＿＿＿__ ／ 　＼ ヽ ,,_　 Ｕ　 ___,,ノ　　/　/ 　　　 　＼,,＿__＿＿_,ノ ＼/　/　　＿＿＿＿＿ 　　　　　　 　　　　　　　 　./　/　　/| ..　 　　　　　　　　　　　　./　/　　./ .| 　　「殺人的ブスいないかなぁ？僕ちゃんブス大好き☆」 637 名前：１３２人目の素数さん [2005/10/05(水) 21:47:41 ] 質問の仕方がなんかまずかったみたいです（ｺﾞﾒﾝﾅｻｲ 率直に聞きます 構造（Ｎ,＋,s,0）で真である論理式の集合が算術的に定義できる集合である って、どういうことか、何方か教えていただけないでしょうか 638 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 22:32:50 ] >>637 真である論理式すべてといったら、算術的に定義できないに決まっている のではないでしょうか？ それとも、ある部分集合というなら、空集合は算術的に定義できますね。 何を訊いているんですかね。 639 名前：１３２人目の素数さん [2005/10/05(水) 23:10:06 ] 『数学基礎論講義』という本を読んでいるのですが、 構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、 とありまして、 ・構造で真である論理式の集合を算術的に定義する、というのはどういうことか、 ・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、 ・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、 について、よくわからないでいる、という次第です 640 名前：１３２人目の素数さん mailto:sage [2005/10/05(水) 23:19:32 ] >>637 算術的に定義できる、の定義が知りたいんじゃないの？ >>639 ゲーデル数でも考えて自然数の部分集合として考えているんじゃないのかな？ しらんけど 641 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 01:44:26 ] ってかそんな言い回しが未定義で使われてるわけないと思うのだが。 論理式のゲーデル数を入力とするある算術的な手続きによって 全ての論理式の真偽が決定可能である、といった感じかなあ。 642 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 02:54:04 ] いや、あの本は未定義で使われてたかと こういう定理もあるよ、というコメントの部分に書かれてた 何の定理だっけ 643 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 04:21:55 ] >>642 ＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 ゲーデルの定理と同じことだけど名前は知らん。 ＞構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できる集合、 プレスバーガー(Presburger)の定理 644 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 06:01:00 ] > ＞構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できない集合、 > ゲーデルの定理と同じことだけど 不完全性よりは弱くね？ 645 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 09:12:34 ] Tarskiの定理だっけ？ 646 名前：１３２人目の素数さん [2005/10/06(木) 10:56:46 ] ありがとうございました。 あと、 『数学基礎論講義』で、 構造（Ｎ,＋,・,s,0）で真である論理式の集合を公理とする理論は完全であるが、具体的には、なにがこの理論の公理なのかがわからないので、このままでは使えない。 ある理論が数学として妥当であるためには、その公理の集合が再帰的であること、が最低限要請される。 という部分があって、 理論の固有の公理の集合は再帰的である必要がある。 ということかな？とも思ったんですが、 r.e.公理化可能という言葉もあるし、理論の固有の公理の集合はr.eであればよかったんじゃなかったっけ？ と、ちょっと、よくわからないでいます。 647 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 11:59:15 ] >>646 r.e.では不便。 公理でないときの判定ができないから。 r.e.の意味を理解していれば自然に分かる筈 理解してないなら分からないだろうが。 648 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:11:55 ] ＞・構造で真である論理式の集合を算術的に定義する、 ＞というのはどういうことか、 つまり構造で真である論理式のゲーデル数の集合が、 算術的性質によって記述できること。 649 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:19:06 ] ＞・なぜ、構造（Ｎ,＋,s,0）で真である論理式の集合は算術的に定義できるか、 プレスバーガーの証明を読め。 ちなみにこの結果は、ゲーデルの不完全性定理の直前に出された。 650 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 12:23:10 ] ＞・なぜ、構造（Ｎ,＋,・,s,0）で真である論理式の集合は算術的に定義できないか、 "ゲーデル・エッシャー・バッハ"を読め。 651 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 13:49:23 ] お前は出てくんな 652 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 14:29:14 ] >>651 お前こそ消えろ 653 名前：１３２人目の素数さん [2005/10/06(木) 14:43:30 ] 132個目の素数は何ですか？ 654 名前：１３２人目の素数さん mailto:sage [2005/10/06(木) 15:03:05 ] >>653 743（ななしさん＝名無しさん） 655 名前：１３２人目の素数さん [2005/10/07(金) 13:22:15 ] 文の真偽判定ってのは、 それ自体に関してアルゴリズムとか形式的な検証があるのか、 それとも、 文の証明可能かどうかのアルゴリズムとか形式的な検証があって、 意味論的な完全性とかを間にかまして、それを言ってる内容なんでしょうか？ 意味論的な内容を形式的に定義する、というくだりが不思議でしょうがないのですが 656 名前：１３２人目の素数さん mailto:sage [2005/10/07(金) 17:59:38 ] >>655 ＞形式的な検証 ああ、まちがってる。 657 名前：１３２人目の素数さん mailto:sage [2005/10/07(金) 18:00:28 ] 形式的な定義と、検証は無関係。 関係づけるからまちがう 658 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 00:10:43 ] ＞文の真偽判定 何の話？文脈が無いと分からない どうも論理式の真理値の定義の話してるみたいだけど あれは、論理式の真理値を定める定義というよりは 　ある論理式がある真である、偽である、という「性質」は明らかに以下の性質を満たす 　〜以下略 って感じの"定義"だと思ったほうがいいかも 659 名前：１３２人目の素数さん [2005/10/08(土) 01:53:48 ] >論理式のゲーデル数を入力とするある算術的な手続きによって >全ての論理式の真偽が決定可能である、といった感じかなあ。 とあったので、 論理式のゲーデル数を入力したときに、ある構造で真であるなら１を出力して停止、 真でないなら０を出力して停止するような機械が作れるのかな、と、 違うんですかね？ 論理式のゲーデル数を入力したときに、ある公理系で証明可能なら１を出力して停止、 証明可能でないなら０を出力して停止するような機械が作れて、 その公理系の定理の集合が再帰的なので、・・・ で、 こっから、 そのような公理系なら、（その構造における論理式の真偽は）決定可能である、とこうくるわけですが、 なんで、定理の集合が再帰的であることから、（その構造における命題の真偽が）決定可能であるのかが、わかんないんですね 660 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 02:18:47 ] 再帰的ってのは計算可能って言葉に置き換えて見ると分かりやすいよ 実際そういう（少なくとも再帰的→"計算可能"はなりたつような）定義になってるでしょ とrecursion theoryは苦手なんだけど、答えてみるテスト ってか一冊キチンとした本読んだほうが早いような まあちょっとした入門書でも 661 名前：１３２人目の素数さん [2005/10/08(土) 03:03:46 ] 基礎論専攻してる学者で有名な人っているか？ すごいマージナルな印象なんだけど 662 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 03:44:23 ] 居るんじゃない？ まあその辺は「有名」の定義付けによるとしか言いようが無いが Shelahとかは有名かと 663 名前：１３２人目の素数さん mailto:sage [2005/10/08(土) 10:17:14 ] Shelahの専攻は集合論であって"基礎論"ではない 664 名前：１３２人目の素数さん mailto:sage [2005/10/09(日) 01:39:30 ] でも、それを言い出すと”基礎論”で有名な人はいないのでは？ 665 名前：１３２人目の素数さん [2005/10/09(日) 04:44:57 ] だよね。基礎論って自分の専攻の傍ら趣味でやるもんでしょう。 666 名前：１３２人目の素数さん mailto:sage [2005/10/09(日) 20:40:04 ] モデル論は"基礎論"に入らないの？ じゃあ"基礎論"やってる人って例えばどんな人なんだろ 667 名前：１３２人目の素数さん mailto:sage [2005/10/10(月) 17:18:24 ] 667 668 名前：１３２人目の素数さん mailto:sage [2005/10/11(火) 03:19:37 ] 基礎論古典四科目（証明論モデル論集合論帰納関数論）は数学になりました。 669 名前：１３２人目の素数さん mailto:sage [2005/10/11(火) 08:48:29 ] 「Shelahスゲェ!」とかいう集合論ヲタは掃いて捨てるほどいるが 「Girardスゲェ!」とかいうリニアロジックヲタはまずいないな。 リニアロジックはやっぱりすげぇ。 contractionがなくなっただけで、 ロジックが意味的にちっとも ロジックぽくなくなってるところが すげぇ。 リニアロジック知っちまうと 論理主義とか直観主義とかいうのは 実は本質からズレてる議論なんじゃ ないのかと思うね。マジで。 670 名前：１３２人目の素数さん [2005/10/12(水) 18:59:24 ] 基礎論なのかどうなのか分からないのですが、質問です。 超準解析って、現在、普通の数学にどのくらい応用されているのでしょうか 671 名前：１３２人目の素数さん mailto:sage [2005/10/12(水) 19:07:04 ] 詳しくは知らん。又聞きだけど。 数十年前には超準解析によって初めて証明された定理もあったのだが、 その後通常の解析学者によって残らず普通に証明されてしまったため、 超準解析はあまりありがたみがないような位置づけになってしまった。 というのが現状じゃなかったっけかな。 672 名前：１３２人目の素数さん [2005/10/12(水) 19:13:26 ] 応用は解析分野がほとんどなんでしょうか？ 673 名前：１３２人目の素数さん [2005/10/12(水) 20:07:47 ] 偏微分が簡単になるってくらいだけど。。。ソフトがあるからいらねー 674 名前：１３２人目の素数さん mailto:sage [2005/10/12(水) 23:26:44 ] 超準解析で証明できることは普通の解析で証明できるからね ただ、論理的に簡単かつ明晰になるので、 新しい定理や証明を発見するときには役に立つ、って感じだったような あとよくFeynman経路積分と超準解析との関係がどうだとか 確率論がどうだとかそこそこあるような 675 名前：１３２人目の素数さん [2005/10/20(木) 00:07:40 ] 超巡回積を勉強したてなので教えてほしいのですが、 例えば、超連続とかって、どういう定義になるのでしょう？ 超冪による超準モデルの中ででもかまいません。 (別な板にも書きましたがあっさりスルーされてしまったので。) 676 名前：１３２人目の素数さん mailto:sage [2005/10/20(木) 12:55:46 ] 定義なら教科書に書いてあるだろ。 ってかマルチは嫌われるよ。 677 名前：１３２人目の素数さん [2005/10/20(木) 19:39:52 ] >>676 どんな教科書ですか？具体的にお願いします。 678 名前：１３２人目の素数さん [2005/10/20(木) 22:01:29 ] age 679 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 08:02:35 ] >>677 逆に聞くが ＞超巡回積を勉強したてなので 何で勉強したの？ 680 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 09:35:49 ] はい、すいません。 東京図書。「超冪と超巡回積」です。斉藤先生の。 681 名前：１３２人目の素数さん mailto:sage [2005/10/21(金) 13:55:16 ] ま、国語を勉強する方が先だろ。君の場合。 682 名前：675 [2005/10/22(土) 00:30:56 ] 結構真剣な質問なんですが。 >>676と>>681は別人でしょうか？ >>681は結局知らないのですか。 誰か知っている人いたら、>>675教えてください。 683 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 00:35:07 ] 真剣なときは誤字脱字は禁物とおもわれ。 684 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 00:57:39 ] 十二指腸の壁面に純化した胃石がたまるという疾患についての本 「腸壁と腸純化胃石」なら漏れも読みますた。 685 名前：１３２人目の素数さん [2005/10/22(土) 01:10:28 ] では「超冪と超準解析」です。 脱字はないと思いますが。 686 名前：１３２人目の素数さん [2005/10/22(土) 16:02:09 ] 結局、反応はあっても良い教科書知っている人はいないのでしょうか？ （教科書に書いてあると言われても。どんな本にあるのだか・・・。） 687 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 18:33:37 ] ヒント：その程度の質問で他人に頼るな！！ 　自分でいろいろ乱読しろ！！ 　狂ったように数学を楽しむこと！！！ 688 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 19:25:17 ] > 超巡回積を勉強したてなので教えてほしいのですが、 教科書は Ming Mei 著 Lectures on the Hypercyclic Products がいいでしょうな 689 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:16:53 ] >>688 ありがとうございます。 図書館の検索をしてみたのですが見つかりませんでした。 シュプリンガーか何かシリーズものでしょうか？ 690 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:43:03 ] もちろん民明書房刊 691 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:45:44 ] ていうか「シュプリンガー」って単語を知ってるんなら シュプリンガーの超準解析本くらいはチェックしたんだろうな？ 692 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 20:57:05 ] もしかしたらと思ったけど・・・。 693 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:00:22 ] ようするに、ここには何も知らないのに、 教科書嫁とかいう人しかいないという事ですか。 694 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:08:53 ] ったく、しゃあねえな Lectures on the Hyper... まではあってるよ SpringerのGTMだ 695 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 21:54:25 ] どうも。 >>687のとおり他人に頼るという態度がいけないのかもしれませんね。 簡単に他人を信用するなということが改めてよく分かりました。 実際にＧＴＭを探してから返答させてもらいます。 696 名前：１３２人目の素数さん mailto:sage [2005/10/22(土) 22:31:07 ] LNMにも超準解析関連の本があるね RobinsonのはElsevierの Studies in logic and the foundations of mathematicsシリーズか 697 名前：１３２人目の素数さん [2005/10/25(火) 16:30:47 ] >何も知らないのに、教科書嫁とかいう人しかいない というか、正確には、 「教科書の題名は馬に食わせるほど知ってるが、 　肝心の中身は１ページだってまともに読めず 　そのくせ、神保町の明倫館あたりでもっとも 　らしい顔して古びた数学書のページ繰って 　喜んでる数学ヲタ」 しかいない。 698 名前：１３２人目の素数さん [2005/10/25(火) 16:35:33 ] 人は先ず歴史・発展史を愛し次に人とその著作を愛し最後に本同士の引用関係を愛する。 699 名前：１３２人目の素数さん mailto:sage [2005/10/25(火) 16:44:16 ] >>693, >>697のような書き込みは単に煽ってるだけだと思っていたが なるほどそうかもしれないと感じつつある。 特定のスレにしか識者がいないような気がする 700 名前：１３２人目の素数さん mailto:age [2005/10/26(水) 00:11:15 ] 無限小解析（ってか超準解析）って言語とかモデルとか 数理論理を援用しまくるけど、 今の解析学が、きちんと形式論理のレールに乗るか？ 今やっている数学を過不足無く形式化出来るか？ という問題がありうると思うんだけどどうよ？ 以前ジョルダンスレで妙に問題になってたのを思い出したんだけど 701 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:13:15 ] そんな大げさなことじゃないだろう。 日本語でデービスの超準解析の訳本があって、後は、何に応用するかだから 論文にあたるってことだろ？ そんなの識者じゃなくってもわかんじゃないの？本があんまりないんだから。 702 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:29:32 ] >>700 たとえば、竹内 two applicasions of logic to mathmatics とかにあるけど、 集合族を何度もとっていくと大変だなあ。 703 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 00:52:56 ] 識者ってどのレベルの事言ってるのかな 学部以上の知識を持った人はかなり少ないはず 基礎論とか大学でやらないから猶更 704 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 01:06:15 ] >>700 19 世紀末の問題意識だね。 705 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 01:10:26 ] そうか？ ヒルベルトのテーゼとかって結構重視する人も居るけど まあ主流の考えはそうだろうね 706 名前：１３２人目の素数さん [2005/10/26(水) 07:47:19 ] >>700 ＞今の解析学が、きちんと形式論理のレールに乗るか？ 安心しろ。 貴様が知る教養課程程度の解析ならみな形式的に展開できる。 貴様が大学の講義をサボったから知らないだけだ（ｗ 707 名前：１３２人目の素数さん [2005/10/26(水) 07:50:45 ] ＞学部以上の知識を持った人はかなり少ないはず つーか、ε−δすら理解できない奴ばかりだが。 708 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 07:57:16 ] と2ch基礎論関連スレ最強の名物識者がおっしゃっております 709 名前：１３２人目の素数さん [2005/10/26(水) 10:21:30 ] 基礎論とε−δ論法との関係が・・・ っと、基礎付け繋がりかorz 710 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 10:49:41 ] ちょっとﾜﾛｽw 711 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 15:53:14 ] ＞ 基礎論とε−δ論法との関係が・・・ 基礎論抜きで、 「解析学のイロハのイがわかってない」 というもっとも根本的な侮蔑。 712 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 15:58:42 ] 要するにただの煽りですな 713 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 19:58:26 ] >>706 俺（じゃなくて他人の書いてたことそのままだけどなｗ）が言ってるのは、 形式的に「展開出来るか」、じゃなくて「本当に展開出来ているか」ということ ま、確かめようがないけどね 集合論を定義して代数系を定義して位相空間を定義して、実数体を定義して（りゃ ってやれば そら集合論の言語に略記法を加えるだけで一応は形式的に展開できるだろうさ 714 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 22:36:33 ] >>704 ＞>>700 ＞19 世紀末の問題意識だね。 >>706 >>700 ＞＞今の解析学が、きちんと形式論理のレールに乗るか？ ＞ ＞安心しろ。 ＞貴様が知る教養課程程度の解析ならみな形式的に展開できる。 ＞貴様が大学の講義をサボったから知らないだけだ（ｗ 昔どこかでParis Harringtonの定理という言葉を見かけたことがあります。 fnite Ramsey theoremの拡張で、「自然で数学的に興味のあるstatement」（？）、 なのだがtrue but not provable in PAだというのです。私は詳しくないので わからないのですが、それでも今の解析学がきちんと形式論理のレールに乗るか どうかほとんど明らかなのでしょうか？ 　これは反語で述べているのではなく純粋に疑問なのです。どなたかくわしくて説明 してくださる人いましたら、お教えいただけないでしょうか？ （そもそもfnite Ramsey theoremも知らないでこんなこと言うのはDQNなんでしょうか。） 715 名前：１３２人目の素数さん mailto:sage [2005/10/26(水) 23:18:52 ] >>714 > それでも今の解析学がきちんと形式論理のレールに乗るか > どうかほとんど明らかなのでしょうか？ 「それでも」の前後の文が逆接の関係にないのだけど。 なぜそう思うのかがわからない。 716 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 00:33:23 ] レスありがとうございます。私がアホ杉で申し訳ありません。 >>715 ＞「それでも」の前後の文が逆接の関係にないのだけど。 ＞なぜそう思うのかがわからない。 実はとても短絡的な（アホな）思考なのです。ゲーデルの不完全性定理の 証明のときに出てくる決定不能命題というのは何というか 「自分自身が証明できない」みたいなトリッキーな命題なもんですから、 「ああ、そこまで表現できるほど理論が豊かならそうなっちゃうわけね」 みたいに漠然と思っていたのです。そこから短絡的に「じゃあ、普通の数学理論を やってる分にはそんな決定不能命題に出会ったりしないな、たぶん。」などど思って いたら、Paris Harringtonの定理とか言うのが出てきて、 ＞「自然で数学的に興味のあるstatement」（？）、なのだがtrue but not provable in PAだ なんて言うもんですから、急に先ほどの自信がなくなってしまって 「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに形式的には 決定不能になってる命題がでてきたりしちゃうんだろうか」 と思ってしまったわけです。 こんなアホですけど、どうか見捨てないでくださいまし。 717 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 00:56:14 ] 「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに 形式的には決定不能になってる命題がでてきたりしちゃうんだろうか」 ? 決定不能命題は定理ではない。 Paris Harringtonの定理はZF上の定理であって、PA上の定理ではないというだけのこと。 718 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 01:41:09 ] 　あ、なるほど。違う意味なのにどちらにも「定理」という言葉を使ってしまっていました。 すいませんでした。 　「Paris Harringtonの定理」と呼ばれているものは、ZF上では定理になっているのなら 素朴な自然数論（標準のモデル？）においては真になるはずですよね。それなのにPA上 では形式的な証明を与えることはできないわけですよね。（PA上では定理ではないので すから。） 　だとするなら、解析学においても素朴に考えれば真なのに、形式的には証明できない 有用な命題があるのではないか、という疑問がわいてきます。しかし>>704 >>706による と、その疑問は払拭されるらしい．．．。簡単なのか？どうなのか？ このように、「Paris Harringtonの定理」と呼ばれているものから、「解析学がきちんと 形式論理のレールに乗るか？」の疑問へいたったのです。 やっぱ、どこか勘違いしてるのかなあ。 719 名前：１３２人目の素数さん [2005/10/27(木) 11:26:34 ] >>714 いっておくが、解析学のステートメントの真偽が決定可能となるような 解析学の形式的理論が存在するとは、いっていないぞ。 あくまで、大学の教養で習うような解析学をカバーする形式的理論が 存在するといったまで。詳しくは逆関数というキーワードで検索すべし 720 名前：１３２人目の素数さん [2005/10/27(木) 11:29:42 ] ＞「やっぱ普通の数学理論やっててもその理論の中で有用な定理なのに ＞　形式的には決定不能になってる命題がでてきたりしちゃうんだろうか」 正しくは 「その理論の中では正しいと考えられるのに 　形式的に証明できない命題があるんだろうか？」 自然数論を含むような理論であれば当然存在する。 それがゲーデルの不完全性定理。 721 名前：１３２人目の素数さん [2005/10/27(木) 11:32:30 ] ＞自然数論を含むような理論 自然数論ではなくて？ 722 名前：１３２人目の素数さん [2005/10/27(木) 11:34:42 ] ぶっちゃけていえば、真と考えられるが ZFCでは証明できない命題は存在する。 ところで ＞「解析学がきちんと形式論理のレールに乗るか？」 という発言は 「解析学は、形式論理学で決定可能か？」 という発言と同じだとは普通思わない。

---

---

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

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