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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 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では証明できない命題は存在する。 ところで ＞「解析学がきちんと形式論理のレールに乗るか？」 という発言は 「解析学は、形式論理学で決定可能か？」 という発言と同じだとは普通思わない。 723 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 11:51:17 ] そうでもない。普通の人は > 安心しろ。 > 貴様が知る教養課程程度の解析ならみな形式的に展開できる。 > 貴様が大学の講義をサボったから知らないだけだ（ｗ などと予断に満ちた基地外煽りを入れる前に どういう意味で「解析の形式的展開」と言っているかを 訊ねるものだ。 724 名前：１３２人目の素数さん [2005/10/27(木) 11:58:22 ] >>723 普通の人は、数学を知らない（ｗ ただ尋ねて答えが返ってくると思うのは馬鹿。 煽りは有用な質問技法。 普通の人は、煽られないと考えない。 725 名前：１３２人目の素数さん [2005/10/27(木) 12:06:52 ] 普通の人甲 「ゲーデルの不完全性定理？なにそれ？」 普通の人乙 「ああ、数学の無矛盾性は数学では証明できない、 　とかいうのだろ？なんか奇妙だよな」 普通の人丙 「それは第二だろ？その前に第一があるんだよ。 　数学の中には真だけど証明できない命題がある 　ってやつ。確か「この命題は証明できない」 　とかいう文章が数学の中で作れるんだろ？」 726 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 12:09:10 ] じゃあ煽らせてもらうが、解析の話をしてるのに > 正しくは > 「その理論の中では正しいと考えられるのに > 　形式的に証明できない命題があるんだろうか？」 > > 自然数論を含むような理論であれば当然存在する。 > それがゲーデルの不完全性定理。 なんて話を持ち出しても意味がないだろ。 727 名前：１３２人目の素数さん [2005/10/27(木) 12:29:15 ] >>726 全くだ。ε−δどころかそもそも開集合、閉集合も知らんのに ＞今やっている数学を過不足無く形式化出来るか？ とか尋ねたって無意味だろ。>>700よ（ｗ 728 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 12:48:17 ] ほらほら、せっかく煽ってやったんだからいつもみたいにオウム返し してないで今回くらいはちゃんと考えてみろ。 まあゲーデルしかネタのない無学なお前さんのためにもう少しヒントを くれてやろう。 解析はお前にはまだちょっと難しいらしいから、複素数体でもいいか。 お前は解析にからんで > 「その理論の中では正しいと考えられるのに > 　形式的に証明できない命題があるんだろうか？」 > > 自然数論を含むような理論であれば当然存在する。 > それがゲーデルの不完全性定理。 なんてことを言うが、じゃあ複素数体の理論はお前さんの言うような、 「自然数論を含むような理論」になるのかね？ 729 名前：１３２人目の素数さん [2005/10/27(木) 14:30:17 ] >>728 もしかして 　解析学 ＝実閉体の理論 複素数体の理論 ＝代数的閉体の理論 だと思ってる？ なら、間違いだよ。 expとかlogとかsinとかcosとかtanとか 知らないなら仕方ないけど（ｗ 730 名前：１３２人目の素数さん [2005/10/27(木) 14:36:14 ] 実閉体や代数的閉体の理論には、微分や積分はない（ｗ 731 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 18:47:38 ] あれは勝手に逆数学の研究者が「解析学」とか名前付けちゃってるだけだね もしかしたら例の「完全証明」よりも罪が重いかも >>718 単に公理が弱かったら証明できないよ、ということで、、 要するにQで証明できない命題があったからって誰も大騒ぎしないのと同じこと あれは、PAで証明できない「具体的な」命題を示した、ということが大事なんじゃないかな >>719 逆函数？逆数学じゃないのか、、？ 732 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 18:51:50 ] >>727 なんで俺を何か別の人と混同してないか？ 俺のレスは713=731でその間のレスは俺のじゃないよ まあマニアックな用語は知らないし、そもそもあまり理解していないかもしれないけど 今の話から分かるようなことじゃないかと 733 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 22:07:37 ] >>729 やっぱりちゃんと考えてもその程度か・・・。 734 名前：１３２人目の素数さん mailto:sage [2005/10/27(木) 22:11:10 ] 自分がわからないから「相手は自分以上にわかってない」という 妄想に逃げ込むいつものパターンだな、ドクトルよ。 735 名前：１３２人目の素数さん mailto:sage [2005/10/28(金) 23:42:08 ] >>734 痛いところを突かれるとすぐ妄想とかいうのは 厨房のワンパターンだな。ドクトルよ 736 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 11:57:02 ] なんでsageてるの？ 737 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 16:40:58 ] それはそうと、微積分を持ち込むと自然数論が 自然に入ってしまう気がするがどうか？ 738 名前：１３２人目の素数さん mailto:sage [2005/10/29(土) 22:37:32 ] ってか集合論の使用自体避けられないような いや避けられるのだろうけど、そうすると何か大変 739 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 12:40:58 ] >>737 なぜですか？ 740 名前：１３２人目の素数さん [2005/10/30(日) 15:28:30 ] >>739 周期関数の存在から自然数の性質を 持ち込めるのではないだろうか？ 741 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 17:59:15 ] 数列とか級数を使わずに微積分を展開するの？ じゃあTaylor展開とかも無しか 742 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 18:34:18 ] まず実数をどうやって定義するかだな。 それとも実数なくても微積分できるんだろうか？ 743 名前：１３２人目の素数さん mailto:sage [2005/10/30(日) 19:59:47 ] >>740が言ってるのはそういう話じゃないんじゃない？ 曖昧な言い方してるから俺もはっきりとわからんが。 744 名前：１３２人目の素数さん mailto:sage [2005/10/31(月) 07:31:25 ] >>743 云ってる本人自身曖昧なんじゃないか？ 745 名前：１３２人目の素数さん mailto:sage [2005/10/31(月) 15:02:27 ] まあもうちょっと詳しく言い直してくれることに期待するか 746 名前： [2005/11/03(木) 16:18:15 ] 「数学基礎論」と「数学の哲学」は同じものですか? 747 名前：１３２人目の素数さん [2005/11/03(木) 16:19:40 ] 「数学基礎論」はゴミ。 「数学の哲学」はクズ。 748 名前：746 [2005/11/03(木) 16:29:47 ] >>747 　的確なご回答、ありがとうございます。　 749 名前：１３２人目の素数さん [2005/11/03(木) 17:09:36 ] "Reduction of mathematics to logic" 750 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 02:05:46 ] 基礎論をロジックと同じ意味で使う人もいれば 違う意味で使う人も居るからね でも数学基礎論は哲学じゃないと思う 751 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 12:34:47 ] >>745 要するに分からないんだね。 752 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 13:18:53 ] そう決め付けたら>>740がかわいそうだろ。 753 名前：１３２人目の素数さん mailto:sage [2005/11/04(金) 20:33:58 ] >>740の書いてる意図が分からない、というのがどうかしたか？ そんなに>>740の書いてることを、何の詳しい説明も無しに理解できることが重要なのか？ そもそも元の＞微積分を持ち込むと自然数論が自然に入ってしまう気がする というレスだって曖昧過ぎて是とも非とも言えないような表現なのに 754 名前：１３２人目の素数さん [2005/11/07(月) 15:31:46 ] >>753 わからないならいろいろ考えてみりゃいいじゃん。 要は有理関数しか考えない理論なら完全だとして、 どこまで完全性を維持したまま拡張できるかって ことだろ？ で、740は周期関数があると、その周期をつかって 自然数かどうかの判定をする述語が書けそうなんで 不完全になりそうだと思ってると見た。 755 名前：１３２人目の素数さん [2005/11/08(火) 01:52:32 ] 数学基礎論て大学じゃ習わないんですか？ 756 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 01:54:31 ] 専攻すればいいだけの話だ 757 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 02:33:04 ] 専攻してるヒマはない 758 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 13:45:13 ] >>７５７ 証明してみせろ 759 名前：１３２人目の素数さん [2005/11/08(火) 15:48:07 ] 建前：暇じゃない 本音：面倒くさい 760 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:23:13 ] 専攻って、1つかせいぜい2つかしかできないだろ 暇とかいう問題じゃねえよ、なんで基礎論を習うために 専攻まで変えなきゃなんねえんだ 761 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:25:29 ] ぢゃ独学しろよ 762 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:32:31 ] だから>>756は首吊れってこったな 763 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 16:42:20 ] そもそも基礎論を専攻できる（というより、専攻する ことによって独学以上に何か得られる）大学って そんなにたくさんないんじゃないの。 764 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 17:04:49 ] だから何？ 転学（もしくは海外留学）すればいいだけのこと。馬鹿ぢゃねーの？ 765 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 17:06:08 ] お前アホだろ？ 766 名前：１３２人目の素数さん [2005/11/08(火) 17:19:48 ] >>755 ＞数学基礎論て大学じゃ習わないんですか？ 普通は「大学じゃ教えないんですか？」と書く。 ロジックとかゲーデルの不完全性定理とかは数学科では教えない。 情報科学科とかだと教えてる。まあ、他学科でも聴講できるはずだから それを利用すればいい。別に単位がいらないならモグリでもいいし。 767 名前：１３２人目の素数さん [2005/11/08(火) 17:23:35 ] 情報科学科は大抵、工学部にあるから、論法や真理の基礎を学びたい、 などと思うと思わぬ間違いになるとおもわれるよ。気をつけて！ 768 名前：１３２人目の素数さん [2005/11/08(火) 17:46:13 ] >>767 ＞論法や真理の基礎を学びたい そう思うなら、数学科にいくより工学部にいくほうが妥当。 非標準論理は面白いし役にも立つが数学科の連中はまず 誰も知らないし、そういう研究は「トンデモ」だと思ってる。 769 名前：１３２人目の素数さん [2005/11/08(火) 20:23:39 ] 京大の工学部ではロジックの講義皆無だけど、 どこだったらそういう講義があるの？ 770 名前：１３２人目の素数さん [2005/11/08(火) 20:25:15 ] そんなものは２週間でマスターするシリーズで済ませば？ 771 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:33:05 ] >>769 基礎的なことなら全学共通のでやるんじゃないの？ 772 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:37:02 ] どこってそういう意味じゃないか。 神戸とか筑波にはあったような。でも数学科だったかな。 773 名前：１３２人目の素数さん mailto:sage [2005/11/08(火) 22:47:43 ] 将来基礎論をやりたいから神戸大の数学科に入るとか 絶対やめたほうがいいと思う 阪大とか京大に入って通うべき 774 名前：１３２人目の素数さん mailto:sage [2005/11/09(水) 03:28:10 ] >>769 数理論理学B、火曜日２限（全学共通 ただし、「数学的」ではない 775 名前：VIPPER mailto:sage [2005/11/09(水) 05:24:50 ] ＶＩＰからきますた、数学の天才、ちょっときてくれ(`・ω・´) 開成中の入試過去問題にお手上げ状態┐(´ー｀)┌ 【秀才】 この問題の解き方教えてくれ 【集まれ】 news19.2ch.net/test/read.cgi/news/1131301609/ 776 名前：１３２人目の素数さん mailto:sage [2005/11/09(水) 21:12:53 ] いくつマルチすりゃ気がすむんだ？ 777 名前：１３２人目の素数さん mailto:sage [2005/11/10(木) 22:01:18 ] >>774>>771>>772 教養の講義は本当に初心者向けだから、たいした内容やらないよね。 神戸は確か工学部じゃなかったかな。どんなことやってるんだろう。 778 名前：１３２人目の素数さん [2005/11/14(月) 09:42:55 ] age 779 名前：文系さん [2005/11/24(木) 00:47:48 ] はじめまして、質問スレッドのみなさん。 当方、「ブール代数」について、その名前しか知らないようなど素人ですが、 ブール代数に詳しい方がいらっしゃったら、概要だけでも教えて戴けませんか？ 780 名前：１３２人目の素数さん mailto:sage [2005/11/24(木) 01:23:33 ] >>779 ブール代数は基礎論と無関係とは言い切れないので答えますが‥ 具体的な質問でないと教えようがありません。 概要ならぐぐれば出てきます。 781 名前：１３２人目の素数さん mailto:sage [2005/11/24(木) 01:36:07 ] ja.wikipedia.org/wiki/%E3%83%96%E3%83%BC%E3%83%AB%E4%BB%A3%E6%95%B0 www.google.co.jp/search?hl=ja&q=%E3%83%96%E3%83%BC%E3%83%AB%E4%BB%A3%E6%95%B0&btnG=Google+%E6%A4%9C%E7%B4%A2&lr= ＞概要ならぐぐれば出てきます。 >>771 先生が数学系か計算機系か哲学系かで結構感じが違うかと スマリヤンとかは哲学系って感じでもないけどね まあ将来基礎論の研究したいなら、教養では他分野の先生の授業 聞いといた方がかえって為になるかもしれない ただ、ソクラテスは人間である、式の講義は （もしやってたとしても）下らんのでそういうのは聞かなくて良いと思う 782 名前：１３２人目の素数さん [2005/11/29(火) 16:12:13 ] 指数は次元を現しているのでしょうか？ 2次元、3次元、4次元と・・・ 783 名前：１３２人目の素数さん mailto:sage [2005/11/29(火) 16:34:38 ] 高校数学のｽﾚで聞いてみます。ｽﾚ汚しすいませんでした 784 名前：１３２人目の素数さん [2005/12/07(水) 03:43:08 ] 数学者（基礎論以外専攻）は研究してるときどの程度基礎論のことを考えているものなのですか？ 785 名前：１３２人目の素数さん mailto:sage [2005/12/07(水) 04:42:47 ] ほとんど考えません 786 名前：１３２人目の素数さん mailto:sage [2005/12/07(水) 10:15:37 ] 考えたい人もいますが、考えるだけの専門知識がありません。 （超巡回積とか幾何学に応用できないかなぁ。） 787 名前：１３２人目の素数さん [2005/12/11(日) 20:36:26 ] 神戸大学は、工学部に数学基礎論グループがあるらしい。 でも工学部の学生で、基礎論の研究室に来た人はいなくて、 >773 のいうように京都大学や大阪大学の数学科の学生が通ってくる場合が多い（？）と聞いた。 神戸大学の数学科の方は、あまり勉強には適さない環境という情報もある。 788 名前：１３２人目の素数さん [2005/12/20(火) 16:48:50 ] 基礎論初心者です。 最近、前原「数学基礎論入門」を読み始めたんですが、 いきなりちょっとした疑問を抱きました。 2章の「命題論理」の冒頭（p.13）に、 　(*) Aが証明できればBも証明できる ということを（推論の図式的表現を借りて） 　A 　-- 　B と表す、という内容の記述があるんですが、この 　(*) Aが証明できればBも証明できる っていうのは、 　(*') Aを公理に追加すればBも証明できる（A |- B） と同じことでしょうか？ 789 名前：１３２人目の素数さん mailto:sage [2005/12/20(火) 21:40:02 ] >>788 うん 790 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 01:07:37 ] (*) Aが証明できればBも証明できる と証明と公理の定義から (*') Aを公理に追加すればBも証明できる が導かれる。 その本を読んでないので文脈上どうかと思うが。 791 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 01:23:24 ] 一寸ニュアンス的にまずいような 普通の命題論理又は一階の述語論理では結果的に正しいだろうけど （たとえば論理規則が少なかったり非古典論理だったりして） 演繹定理だとか完全性定理だとかが成り立たなかったりすると、 必ずしも成り立つとも言えないような気がする 792 名前：788 [2005/12/21(水) 19:09:42 ] レスありがとうございます。 「(*')ならば(*)」は自明だと思うんですが、「(*)ならば(*')」は、きちんと示そうとすると どうも微妙な感じでよくわかりません・・・ ちなみに、そもそもの疑問は、 　(*'') （公理から） A→B が証明できる（|- A→B） と 　(*) Aが証明できればBも証明できる が同じことなのか、ということでした。 　(*') Aを公理に追加すればBも証明できる（A |- B）」 と (*'') が同じだ、というのが「演繹定理」ですよね？ 演繹定理の証明は他の本（田中他 「数学基礎論講義」）で読んで納得したんですが、すると結局(*')と(*)が同じなのか ということが疑問になります。 前原「数学基礎論入門」には、(*)と(*'')が同じことだということが明示的には書かれてい ないように思うんですが、にもかかわらず、たとえば p. 20 の「公式2.3」では ¬A→(A→B)の証明として、¬AからA→Bを導く推論図（これはこの本の定義によれば、 「¬Aが証明できればA→Bも証明できる」ことを示す図）が書かれています。 なお、話題にしている体系は、公理系として「ウカシェビッチの公理系」、推論規則として 三段論法（modus ponens）だけをもつ、ごく基本的なものです。 793 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 20:11:47 ] その本を読んでないんだけど、>>788の >  　(*) Aが証明できればBも証明できる >  ということを（推論の図式的表現を借りて） >  　A >  　-- >  　B >  と表す、という内容の記述があるんですが、 という書き方を見るとたぶん (*) はインフォーマルな表現で、これを形式的に書くと A├B になる、 ということのような気がする。 そうじゃないとすれば (*) は (*1) ├A ならば ├B と解釈するのが素直かなと思ったけど、これは A├B と同値ではない。 794 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 21:58:43 ] >>792 2.2 と 2.3 の内容をきちんと理解していないように思える。 >>793 > その本を読んでないんだけど 世の中自然演繹の体系だけではないのだ。 795 名前：１３２人目の素数さん mailto:sage [2005/12/21(水) 23:25:51 ] 古典論理の範囲で考えても、 　├A　が証明できるなら　├∀xAも証明できる が 　├A→∀xA　は必ずしも証明可能でない。 ところで >>792 ＞たとえば p. 20 の「公式2.3」では ＞¬A→(A→B)の証明として、¬AからA→Bを導く推論図（これはこの本の定義によれば、 ＞「¬Aが証明できればA→Bも証明できる」ことを示す図）が書かれています。 のところは演繹定理使ってるだけじゃんか。ちゃんと嫁！！！ 796 名前：791 mailto:sage [2005/12/22(木) 01:43:34 ] (*): |- Aならば |- B (*'):A |- B (*)' ⇒ (*)は |- Aの証明とA |- Bの証明をくっつけるだけだからおｋ (*)⇔（|- Aでない） もしくは （|- B） ） だから(*) ⇒(*)'は、（|- Aでない ⇒ (*)'） かつ （|- B ⇒ (*)' ）と同じ さて、後者の|- B⇒A |- Bの方は明らか （|- Aでない）⇒A |- Bのほうは証明論的な完全性と、 矛盾律が成り立たないといえないと思う 当然ながら⇒は→じゃなくてmetaな意味で使ってます 797 名前：788 [2005/12/22(木) 02:57:20 ] >>793 前原「数学基礎論入門」 p.12 の記述は正確には次のようになってます： （引用始まり） いま、A→Bという論理式が証明できることがすでにわかっているものとす ると、推論規則1（引用者注：modus ponens）により 　　(*) Aが証明できればBも証明できる ということがわかる。われわれは、(*) のような内容を示すのにも、推論の 図式的表現を借りて 　A 　-- 　B と表す。 （引用ここまで） これを忠実に受け取ると、やっぱり 　A 　-- 　B という記号を、この本の著者は 　(*1) ├A ならば ├B の意味で使っていることになると思うんですが・・・ ちなみに普通は 　A 　-- 　B という記号はA├Bと同じ意味で使うんでしょうか？ 798 名前：788 [2005/12/22(木) 03:02:47 ] >>795 公式2.3自体に疑問をもっているわけではなく、演繹定理を使えば、公式2.3が、 この本にかかれているとおりの証明で示せるってことはわかります。 疑問は、 　A 　-- 　B という記号を著者がどういう意味で使ってるのかってことです。 799 名前：788 [2005/12/22(木) 03:08:49 ] >>794 ＞2.2 と 2.3 の内容をきちんと理解していないように思える。 一応読んで理解したつもりなんですが、不十分なのかもしれません・・・ 2.2 と 2.3をきちんと理解したら、 >>792 のような疑問は抱かないはずってことですか？ >>788 や >>792 のような疑問は的外れでしょうか？ 800 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 03:27:33 ] その左のp.12に 　ある論理式が証明できる(provable)というのは，その論理式がある推論の結 （以下省略 と書いてあるからそっちも充分注意しないといけないと思うけど、 「(*') Aを公理に追加すればBも証明できる」というような状況を 考えているわけではないと思う ├ A ならば├ B ということを自然演繹っぽく書いてるけど 実際上は証明の途中にAが出てきてそのさらに下にBが出てくるような状況を「想定」しているのかと （(*)' から(*)はすぐにいえるからこれは別にかまわない この逆に関しては、この本ではあまり気にする必要は無い） p13の一番下の、 一般に，論理式A_1，A_2，…，A_nの全てが証明できれば （以下省略 のほうは(*')の方の意味にしか解釈できないしね この表記法は多少筆者のオリジナルじゃないかな？知らんけど 801 名前：788 [2005/12/22(木) 15:12:22 ] >>800 > 　ある論理式が証明できる(provable)というのは，その論理式がある推論の結 > （以下省略 > > と書いてあるからそっちも充分注意しないといけないと思うけど、 これは「証明できる」のごく一般的な定義じゃないですか？ 「充分注意しないと」というのは具体的にはどういうことでしょうか？ > 「(*') Aを公理に追加すればBも証明できる」というような状況を > 考えているわけではないと思う （途中省略） > p13の一番下の、 > 一般に，論理式A_1，A_2，…，A_nの全てが証明できれば > （以下省略 > のほうは(*')の方の意味にしか解釈できないしね 　A 　-- 　B は、「(*')というような状況を考えているわけではない」のに 　A_1，A_2，…，A_n 　--------------- B は、「(*')の方の意味にしか解釈できない」んですか？ どういうことでしょう？ 802 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 17:40:55 ] 2.4 から後の証明で、「仮定 … のもとで」と書いてあったら、 A -- は B 「仮定 … のもとで A が証明可能」ならば「仮定 … のもとで B が証明可能」 と読む。 803 名前：788 [2005/12/22(木) 19:12:26 ] >>802 それは、2.2 と 2.3 に、演繹定理に相当する内容が書かれているからでしょうか？ 2.1には、「(*) Aが証明できればBも証明できる」ということを 　A 　-- 　B と表す、と書いてあるんですが、それはあくまでもインフォーマルな説明であって、 　A 　-- 　B は、実際は A |- B を表しているということですか？ 804 名前：１３２人目の素数さん mailto:sage [2005/12/22(木) 22:00:57 ] 「仮定 C_1, C_2, ... C_n のもとで」と書いてあったら、 A -- は B |- C_1 ->( C_2 -> ... -> (C_n -> A)...) ならば、 |- C_1 ->( C_2 -> ... -> (C_n -> B)...) という意味。 805 名前：793 mailto:sage [2005/12/22(木) 22:17:58 ] 研究室に問題の本があったんで眺めてみた。 確かに用語の使い方がよくわかんない。 とりあえず A├B って記号は使われてないので>>793の > (*) はインフォーマルな表現で、これを形式的に書くと A├B になる、 は撤回しときます。 著者の頭に (*) の数学的定義があるとすれば (*1) なんだろうけど。 >>797 > ちなみに普通は > 　A > 　-- > 　B > という記号はA├Bと同じ意味で使うんでしょうか？ A├B を表す記号としては 　[A] 　 B みたいなのをよく見るような気がする。 普通 -- を使うのは immediate consequence をあらわすときだと思う。 806 名前：788 [2005/12/22(木) 22:52:42 ] >>804 おー、わかりました！ ありがとうございます！！！ やっぱ、2.2 と 2.3 をよく理解してなかったようです。 2.3の最後（p. 20）のに書いてある 「2.1 に述べた推論法則 2.1 - 2.5 も、任意の仮定のもとで成立する」 ってのがキーですね。 たとえば、公式2.3「¬A → (A→B)」の証明に書かれている推論図 　¬A 　----- 　¬B→¬A 　---------- 　A→B は、格段に「仮定」の「¬A→」を付けた 　¬A → ¬A 　---------- 　¬A → (¬B→¬A) 　---------- 　¬A → (A→B) を意味してるってことですね。 807 名前：788 [2005/12/22(木) 23:05:41 ] で、結局、 (1) この本で使われている 　A 　-- 　B という記号の意味は、p.13の定義の言葉どおり 　|- A ならば|- B を意味している。 さらに「仮定 C_1, C_2, ... C_n のもとで」と書いてあったら、 　|- C_1 ->( C_2 -> ... -> (C_n -> A)...) 　ならば、 　|- C_1 ->( C_2 -> ... -> (C_n -> B)...) を意味している。 (2) 　(*) Aが証明できればBも証明できる（├ A ならば├ B） と 　(*') Aを公理に追加すればBも証明できる（A |- B） は同じではなく、「(*') ならば(*)」は簡単に示せるが、 「(*) ならば(*')」は示せるとは限らない。 だが、この本を読む上では「(*) ならば(*')」はとりあえず気にしなくてよい。 ということでおｋでしょうか？ 808 名前：800 mailto:sage [2005/12/23(金) 06:23:27 ] ＞(*')の方の意味にしか解釈できない じゃなくて ＞(*)の方の意味にしか解釈できない でした 書き間違い失礼 809 名前：788 mailto:sage [2005/12/24(土) 06:01:10 ] その後よく考えたら、 　(*) Aが証明できればBも証明できる（├A ならば ├B） と 　(*'') A→B が証明できる（├ A→B） が同値なわけがないこと（「(*) ならば (*'')」が一般には言えな いこと）がわかりました。お騒がせしてすみませんでした。 「(*) ならば (*'')」が一般には言えないことは、たとえば A が自由変数を含む場合なら、>>795 さんが書いているように 　├A　ならば├∀xA だけど、├A→∀xA　とは限らない ことが反例になっているし、 A が自由変数を含まないとした場合でも、不完全性定理から反例を 作れることがわかりました。具体的には、C も ¬C も証明できないような（自由変数を含まない）論理式 C をとって、 A = C、B = ¬C とすれば、A は証明できないから (*) は自明に 成立するにもかかわらず、A → B ≡ ¬C も証明できないから (*'') が成立しません。 レスしてくれたみなさんありがとうございました。勉強になりました。 810 名前：１３２人目の素数さん mailto:sage [2005/12/24(土) 06:10:45 ] ＞A は証明できないから (*) は自明に ＞成立するにもかかわらず 日常言語で矛盾律使うのかあ アクロバティックだなあｗ 811 名前：１３２人目の素数さん [2005/12/29(木) 08:53:56 ] >810 　そうでもない。 　実際の不完全性定理の証明をよく見ると、「自然数論が展開できる ような理論では、Ｃ が証明されても反証されてもその理論が矛盾する、 という性質を持つような自由変数を含まない命題Ｃが構成できる」と いう形で証明されているから。 812 名前：１３２人目の素数さん mailto:sage [2006/01/02(月) 04:47:36 ] 152 813 名前：１３２人目の素数さん [2006/01/29(日) 06:48:43 ] age 814 名前：１３２人目の素数さん mailto:sage [2006/02/05(日) 07:27:48 ] 836 815 名前：１３２人目の素数さん [2006/02/13(月) 23:54:54 ] すみません。流れ流れてここへ来ました。 １＋１＝２　を証明できるって聞きましたが、 なかなか理解できずに苦しんでます。 ノート１冊使うって聞いたんですが。。。 記号論理のルール　（一階述語論理）　と　集合に関する数個の公理 を使うってことは理解してやっているのですが。。。。 816 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 00:04:04 ] ZF かなんかでやるってこと？ それなら大変なのは証明よりも自然数とか足し算とかの定義だね。 817 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 00:10:09 ] ZFでの自然数の定義は真面目に書き下すなら大変だろうなあｗ Peanoの公理系で証明するんだったらノート一枚くらいだよ 誰がノート1冊使うなんて言ったんだろ そりゃ述語論理の勉強とかで使う分含めるなら確かに1枚くらい 使っても全然おかしくないけどさ 818 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 12:41:30 ] >>816 >>817 Principia Mathematica についての有名な話なんだけど。 819 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 15:28:36 ] 有名な話って何が？ >>815だけでPMの話だとは判らなかったんだが 820 名前：１３２人目の素数さん mailto:sage [2006/02/14(火) 22:59:01 ] ＰＭは一階じゃないわな 821 名前：１３２人目の素数さん mailto:sage [2006/02/18(土) 14:06:17 ] 前原昭二先生の「記号論理入門」買ってきました． 822 名前：１３２人目の素数さん [2006/02/19(日) 21:25:47 ] age 823 名前：１３２人目の素数さん [2006/02/23(木) 12:59:14 ] ∃導入則の説明に、 導出される∃ｘAxはAtという式の中にあらわれるｔの１つないしそれ以上をｘで置き換え、その上で∃ｘを頭につけてできる式である ということが書いてあったのですが、 例えば、 Ha∧Raが導出できるときに、∃ｘ（Hｘ∧Ra）が導出できるということですか？ 824 名前：１３２人目の素数さん [2006/02/23(木) 13:02:09 ] >>823 ｗ 825 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 14:09:30 ] >>823 そういうことです。 826 名前：１３２人目の素数さん [2006/02/23(木) 18:36:39 ] ∃除去則 ∃ｘAxとAt→Cが導出できるとき、Cを導出できる、 とあるのですが、 ∃除去則で、 ∃ｘAxとAtと書いているとき、Atというのは、Aｘにあらわれるすべてのｘをｔで置き換えたものということですか？ 例えば、 ∃ｘ（Hｘ∧Rx）と（Ha∧Ra）→Cが導出できるとき、Cを導出できる、というような 827 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 18:44:45 ] >>826 全て 828 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 18:49:00 ] > ∃除去則 > ∃ｘAxとAt→Cが導出できるとき、 At とは書いてないと思うけど。 829 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:12:10 ] A[x/t]とかいうのも同じ意味だよね >>828 ？ 830 名前：828 mailto:sage [2006/02/23(木) 19:34:32 ] t と書いたら変数とは限らないというのが普通だけど。 831 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:36:22 ] ？termで良いんじゃない？ termのときもAtとか書かないかな 832 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 19:41:28 ] eigenvariable condition 833 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:29:35 ] > ∃ｘAxとAt→Cが導出できるとき、Cを導出できる、 は 「∃xAx が導出可能、かつある項 t に対して At→C が導出可能   ならば C が導出可能」 と読めるけど、これに従えば ∃x.x=0 と 1=0⊃1=0 は導出可能だから 1=0 が導出可能 ということになっておかしいんでは？ 834 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:36:38 ] >>826 >∃ｘAx と At→C が導出できるとき、Cを導出できる、 と書いてあるはずがない。t = 1 で Ax が x は 2 で割り切れる C は 1 = 0 を整数の範囲で考える。 A1 は否定が証明できるから、∃ｘAx と At→C は証明できる。 これで、おかしいことがわからなければ、もう止めたほうがよい。 これがわかれば、 「∃ｘAx と Aa → Cが 導出できて、C に a が現れないとき C を導出できる」 ということを理解する努力をする。 835 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 20:47:11 ] 変数の使い方が慣用に反するってことですね ただレスした人が変えたか そもそも著者がそういう文字を使ってるかは不明ですが 836 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 21:05:06 ] Atというのは、項（定項、自由変項）ｔを含む論理式でしょ、 それがだめ、という話をしてるんですか？〜→Cの〜の式に変項が含まれちゃだめ、とか ところで、Aaというのはなんですか？ 837 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 21:15:56 ] a は自由変数記号。 ∃ｘAx という記号の使いかたをしてるから、それを流用しただけ。 つまり ∃ｘAx は Aa に現れる自由変数 a すべてを x で置き換え前に ∃ｘ をつけたって意味。 もっとも ∃ｘAx をどういう意味で書いているか訊いてから答えた方が いいがもう面倒なので、これで終わり。あとは勉強してください。 838 名前：１３２人目の素数さん mailto:sage [2006/02/23(木) 22:20:41 ] （モデルによる）意味論やった方がいいんでない？ 839 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 17:09:37 ] 命題論理とか述語論理の説明で、集合論のタームが出てきますよね。 たとえば真理値は「真」と「偽」を元に持つ集合だ、とか真理関数はその集合からの 一価関数だ、とか。 で、公理的集合論の方を見るともちろん述語論理で形式化している。 これって循環してないですか？記号論理って集合論を用いないと語れないんでしょうか？ それとも単に便宜上関数とか集合って言葉を使ってるだけなんでしょうか。 840 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:12:53 ] 上のは命題論理を形式化するときの話です。 せっかく集合論やら自然数論を形式化しようとしてるのに、 形式化の意味論?で(素朴な)集合論を持ってきたら意味ない気がするんですが。 841 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:14:30 ] x 上のは命題論理を形式化するときの話です。 ○ 上のは命題論理を形式化するときの話でも、です。 842 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 21:27:05 ] >>839 通常、論理の意味論は集合論を前提して書かれる。 でも論理のシンタクスを論じるときは集合論は使ってないから循環はない。 公理的集合論に必要なのはシンタクスだけで意味論は必要ない。 843 名前：１３２人目の素数さん mailto:sage [2006/02/24(金) 22:16:47 ] どっちも厳密化するために形式的に書かれているとするならまあ矛盾してるよね だから無矛盾性を（本当にテツガク的に厳密な意味で） 示したい場合には確かに問題になると思う モデル論とか選択公理とか基数とか使ったりするしね 逆に言うとそういう無矛盾性とかではなくて、 数学の理論の構造を明らかにしたい、という問題意識的には全く問題ないとも言えると思うけどね 片方は研究対象としての「理論」乃至モデル、 片方はそれを研究するための普通の数学の理論と思えば良いんじゃないかな >>842 でも証明論でも大きな基数使うことあるんじゃないのかな ＞公理的集合論に必要なのはシンタクスだけで意味論は必要ない。 これそうなのかな 844 名前：838 mailto:sage [2006/02/24(金) 22:36:24 ] というかさ、どうせ最初に使う形式（推論規則やらなんやら）は無条件で受け入れる以外に 手はないよね。その受け入れる時に、「誰か他人から手取り足取り教えてもらって」 受け入れるのか、それとも．．． ということが言いたかったのだ。 845 名前：839 mailto:sage [2006/02/25(土) 08:43:55 ] なるほど、確かに命題論理の意味論で素朴集合論の用語を使っても別に問題ないわけですね。 >でも論理のシンタクスを論じるときは集合論は使ってないから循環はない。 それがはっきりしてない本や文章があって、たとえば ttp://www.math.h.kyoto-u.ac.jp/〜takasaki/edu/logic/logic6.html でも「論理の形式的体系は公理系（axioms）と呼ばれる論理式の集合 （空の場合もある）と」 というような記述があって、これが混乱してしまうんです。 しかし「論理の形式化」自身は所詮意味論でしか基礎付けがないのだから、ここの用語(空とか)を 公理的集合論のシンタクスではなく、素朴集合論の意味論だと捉えれば問題ないのかな、 という気がしてきました。 846 名前：１３２人目の素数さん [2006/02/26(日) 15:50:03 ] この手の話はミネルヴァの内井の本辺りには丁寧に書かれてそうだな。 哲だが工学部卒だしlogicはかなりまともにやってるから、数学部分も 一部氣にはなるがまとも。でも、哲だけあって、説明は細かい。前に、 ＮＫや完全性定理の説明とか、ヒルベルトプログラムにおける無矛盾 性の意味（無矛盾を示したいのではなく、理念的命題が悪さをしない ことを保証したい）を正確に捉えているところとか、下手な数学科の 学生より理解していると感心したことがある。良かったら参考にして みてくれ。本のタイトルは忘れた。著者は哲は哲なんで、違う本だと 何の参考にもならないから（笑）、くれぐれも中身を見てからにして くれ。それと、説明は細かいが、技術屋が得るものはないレベルの本 ではあるから、そこは承知しておくように。もともと入門書（啓蒙書 ？）だし、それはそういうものだしな。 847 名前：１３２人目の素数さん mailto:sage [2006/02/27(月) 03:43:20 ] >>845 メタレベルの問題、つまり議論の中でのことと外でのことかの違い。 この区別がこの後もいろいろなかたちで使われます。 リンク先のコンピューター関連は、 「はじめてのＣ」を参考書として選び（もっといいほんがあるのに）、 「Ｃシェルプログラミング」を教える（shでのならわかるが）、なんだかセンス悪い。 848 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 11:56:15 ] ｘ＾ｙでｘのｙ乗を表すとして、 「（無理数）＾（無理数）＝（有理数）」 が成立するようなことがあるか、って問題の解答として、 「（ルート２）＾（ルート２）が有理数であればよし、そうでなければ無理数なので （（ルート２）＾（ルート２））＾（ルート２）を考えれば （（ルート２）＾（ルート２））＾（ルート２）＝（ルート２）＾２＝２ で、これが（無理数）＾（無理数）＝（有理数）の例となる。」 ってのは、やっぱり直観主義の人は証明になってないと思うわけ？ だとしたら、やっぱ直観主義ってついていけんな。 849 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 12:26:21 ] >>848 もちろんなってない。 実数が与えられたとき、それが有理数かどうかなんて一般には決定できない。 850 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:17:04 ] >>848 > 「(無理数)＾(無理数)＝(有理数)」 を「(無理数)＾(無理数)＝(整数)」に変更したらこの証明では手も足も出ない。 へぼい証明だということ。 851 名前：GiantLeaves ◆6fN.Sojv5w [2006/03/01(水) 13:21:50 ] ln(2)が無理数かどうかを判定せよ。 ちなみに、e^ln(2)=2. 852 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:25:37 ] >>849 やっぱそうなんだ。直観主義の人ってまだいるんだろうけど、排中律がそんなに嫌いなのかね？ 嫌いだから直観主義やるのか（少しナットク）。でもじゃあ 「（ルート２）＾（ルート２）は有理数であるかそうでないかのどちらかである。」 を本気で疑ってんのかなあ？それはそれで信じられんなあ？ 853 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:30:24 ] 直観主義でも相当いけるらしいぞ。 背理法以外に証明法ないのか？ 854 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 13:37:56 ] > 背理法以外に証明法ないのか？ 世が世ならそれでフィールズ賞。 855 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:08:06 ] >>848 のなら対数使えばたぶん直観主義でもいけるぞ 856 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:09:36 ] >>852 > やっぱそうなんだ。直観主義の人ってまだいるんだろうけど、排中律がそんなに嫌いなのかね？ じゃなくて、「正しい」という言葉の意味を普通の数学者とは違う意味に捉えてる。 857 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 14:48:40 ] >>855 「(無理数)＾(ルート２)＝(有理数)」だったら？ 858 名前：848 mailto:sage [2006/03/01(水) 17:25:49 ] >>856 ＞じゃなくて、「正しい」という言葉の意味を普通の数学者とは違う意味に捉えてる。 ああ、なるほどねぇ。でもじゃあ、直観主義者の「正しさ」の概念って時間の関数 なのかな？あ、クリプキとかいうヤツがなんかうまいセマンティクス考えたんだっけか？ 漏れそれしらないや。そこんとこどうなんだろ？ 　普通に数学やっている人（古典論理主義者って言うのも変だからこう呼んでおく）は 「正しさ」が時間の関数だとは思ってないよね。例えば、今未解決の問題があったとして、 決定不能命題である場合は別にして、そうでない場合はそれが成り立つかそうでないか は今知らないだけで決まってると思ってるよね？ 859 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 17:39:37 ] > 決定不能命題である場合は別にして 決定不能命題であるかどうかも決定不能なので、 そのような場合分けは無意味なのでは？ 860 名前：849=855=856 mailto:sage [2006/03/01(水) 18:42:06 ] >>857 どうだろうね。 x^{√2} が連続関数であることからいえたりするんだろうか。 でも中間値の定理が一般には成り立たないから無理かもしれん。 >>858 直観主義ってのはそもそも数学的な真実は超越的なものではなくて 人間の内にあるものだって考え方じゃなかったっけ。 だからまあ時間にも依存するだろうけど、どっちかというと数学をやってる主体に 依存するというほうが正しいのかなと思う。 今の直観主義者がどう考えるかは知らないけど、もともとの意味からすると。 後半に関しては、まあ >>859 みたいな突っ込みはいろいろできるだろうけど 厳密な話を抜きにすればだいたいそうだろうね。 > 今知らないだけで決まってると思ってる というのが、まさに数学的な真実は人間を超越しているって考えかたなわけだ。 ちなみにこの辺の話あんまり詳しいわけじゃないんで話半分に聞いといて。 構成主義者ではあるけど哲学屋でも直観主義者でもないので。 861 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 19:00:21 ] >>848 本にそう書いてあったろ >>850 それは今の話の流れとは関係ないのでは。。 普通は対数とるなりして証明するけど (√2^√2)^√2はよく直観主義の説明で出てくる例 862 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 19:07:14 ] 排中律云々は飽くまで結果であってそれが最初にあるわけではないでしょ 直観主義でまず大事なのはなぜ彼らが直観主義の立場を取るかだと 思うんだけど、そこらへんの事が書かれてる本ってどういうわけだか非常に少ないんだよね だから普通に論理学の本で直観主義を勉強すると 「なんか世の中には奇特な人が居て排中律を認めないらしいぞ」 とかそういう感想になる そこいらのことがもっと知りたかったから勁草書房かどっかから出てる 数学の哲学の高い本買ったんだけど、まだほとんど読んでないやｗ >>858 直観主義者だって時間の函数だとは思ってないんじゃないかな まあAxiom of Choiceが「正しい」公理だと見做されるかどうかは結構 時代によって違ったりしてると思うけどね 863 名前：848 mailto:sage [2006/03/01(水) 23:24:45 ] 自分のとこ読むと少し挑戦的な口調も入ってるのに、冷静にレス返されたらこっちも冷静になっち まったい。（つーか漏れのガキさ加減が浮き上がっちまった。） ＞> 今知らないだけで決まってると思ってる ＞というのが、まさに数学的な真実は人間を超越しているって考えかたなわけだ。 フムフム、前よりはなんか許容できそうな気持ちになってきたなあ。なるほど、そういう考えかたねぇ。 まあ、そういわれても漏れはやはり排中律ビシバシを変える気はないけど、でもそういう人もいても おかしくはないか、って感じね。 >>862 ＞そこいらのことがもっと知りたかったから勁草書房かどっかから出てる 漏れもそこいら辺知りたいなあ。ここら辺詳しい人２ちゃんにいないのかなあ。天下の２ちゃん！ そういう人いてくれ！ スマソ ＞>>858 ＞直観主義者だって時間の函数だとは思ってないんじゃないかな 言われてみりゃあそうか。つまり 「（ルート２）＾（ルート２）は有理数であるかそうでないかのどちらかである。」 が正しいかどうかは今は知らないが決まってはいるはずだ、と思ってるかもしれないって事か。 （例が悪いから（ルート２）＾（ルート２）が有理数かどうか周知の事かもしれないけど言いたい 事わかるよね。） 864 名前：850 mailto:sage [2006/03/01(水) 23:30:35 ] >>861 排中律に基づく証明が非構成的であることを反映しているのだと思うが。 865 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 23:38:02 ] wikiに以前直観主義の項目があったと思ったんだが なくなってるね 何でだろ 866 名前：１３２人目の素数さん mailto:sage [2006/03/01(水) 23:40:09 ] >>864 「へぼい」と「非構成的」は同義じゃないでしょう 方法の汎用性と構成的かどうかは寧ろ片方を立てれば もう一方が立たない関係になってる場合の方が多いと思いますよ 867 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 07:54:56 ] >>866 同義とはどこにも書いていないけど。 この証明を構成的にしようとする方向に、 汎用的な定理(Gelfond-Schneider)がありませんか？ 868 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 16:15:25 ] >>867 866とは違う者だけど、>>848の証明が非構成的である理由としては >>850はずれてる、って事を言いたいんじゃないのかな866は。 「>>850は理由になってるの？」っていう。 それに(無理数)^(無理数)=(有理数)の例を挙げるだけだったら、 (√2)^(log_{2}(9))=3で構成主義的に問題無い訳だし。 でも今問題になってるのはあくまで>>848の証明でしょ。 別証は取りあえず置いといて。 869 名前：１３２人目の素数さん [2006/03/02(木) 18:52:50 ] 　　　　　　　　　　　　　　　　　＿＿＿ 　　　　　　　180　　　　　　　ノ7.5-6　　 　　X　＝　----　　　×　　　-----　　　　　　 　　　　　　　　2　　　　　　　　7.5-6 解き方と答え教えて 870 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 21:54:59 ] いつまでもこういうのが絶えないのう..... >>869 ネタじゃなかったら勘違いなのです。 スレタイとは裏腹に基礎数学のスレッドではないのですよ。 質問スレにでも逝かれるがよろしいかと思います。 次は【数理論理】 とか 【Logic】とかつけた方がいいかも 871 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 22:34:36 ] >>865 「数学的直観主義」だね。 ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E7%9A%84%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9 ↓ぐぐって見つけた文章 www.ritsumei.ac.jp/se/~tjst/doc/announce/am96.html ＞トポス理論の構築を通して 構成的議論の本当の意味は、 ＞種々の数学的定式化に依存しない数学的真理を与えるという点にある、 ＞ということを明らかになったのである。 なんかすごい事言ってるような気がするけど、全然分からない… もうちょっと具体的にはどういう事なの？ 872 名前：856 mailto:sage [2006/03/02(木) 23:19:11 ] >>871 なんとなく「いろんな概念が人間の直感に合った形で素直に書けるんですよ」 みたいなことを言いたいんじゃないかなという感じがする。 具体的にどんなものを意識してるのか、それがトポスとどう関係するのかはよ くわからない。というか知らないといったほうが正しいか。 あとそれとは直接関係ないんだけど、 その文章読んでると直観主義・構成主義・排中律の否定の三つを 全部一緒にしてるような印象で気になった。 個人的にはどれも別物だと思ってるので。 873 名前：１３２人目の素数さん mailto:sage [2006/03/02(木) 23:46:25 ] 直観主義が赤のリンクになってるから 無くなっちゃったのかと思った 本来は転送されるべきですね >>871 あれだ、所謂辻下さんのページだ 874 名前：１３２人目の素数さん [2006/03/03(金) 04:42:39 ] 集合論の質問はここでいいのでしょうか？簡単すぎる質問で恐縮ですが、べき集合とは何か、と{φ}と{{φ}}の違いは何か、一応本で読んで知ってるのですが、感覚的に掴めず、ぴんときません。どなたか分かるまで根気よく説明して下さる方はいませんか？ 875 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 05:33:09 ] あれ、集合論スレ落ちちゃったんですね うーむ ＞感覚的に掴めず、ぴんときません。 冪集合は兎も角、{φ}と{{φ}}の違いなんて形式的なものであって 感覚的にそうピンとくるようなものでもないと思いますよ 冪集合に関しては、他の数学の分野を勉強するときに 必然的に使うことになるので、そのときに慣れていけばいいんじゃないでしょうか 集合論的には、ある濃度の集合から、さらに濃度の高い集合を作るための 一般的な規則、とか言うことになるんでしょうけどそういう説明するのも何か違う気がしますし 876 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 05:44:19 ] >>874 ものごとをすべて感覚的に掴めるという錯覚にある人の質問。 100までの数に関することでも、感覚的にわからないことはいくらでも ある。論理的に追えるかどうかが、感覚ができる決め手。 大体、{φ}と{{φ}} が異なる集合であることの証明ができないのでは ないかと推測するが、、、。 877 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 06:02:08 ] ＞大体、{φ}と{{φ}} が異なる集合であることの証明ができないのでは ＞ないかと推測するが、、、。 証明が出来ないってのは、感覚的に分かってない人には証明出来ない、ということ？ 878 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 10:17:24 ] 説明できるような感覚なんてちょっとしかないよたぶん。ある程度経験つまなきゃ感覚もつかめない ってところもあるよ。少ない経験や知識だけで感覚を持とうとしても、無理が出るだけだよ。 もちろん何か説明してくれる人がいる時は聞けばいいだろうけど、自分でも先へ進んでみないと。 879 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 14:41:20 ] 集合論なぜなにスレッド science4.2ch.net/test/read.cgi/math/1064299337/ 昨日の圧縮の時点でレス数985だったからdat落ちさせられたみたい。 880 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:16:58 ] >>872-873 871だけど、う〜ん…あんまり本気にしない方がいいのかな。 本気にしたところで層意味論なんて俺には無理だけど。 881 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:21:05 ] 980過ぎたら埋め立てるのがマナーですぜ 882 名前：１３２人目の素数さん mailto:sage [2006/03/03(金) 23:28:55 ] ＞sheaf semantics ちょっとびびったｗ なんかカッコいいなｗ 883 名前：874 [2006/03/04(土) 07:52:05 ] >>875->>879 皆様、レスありがとうございます。 ＞{φ}と{{φ}}の違いなんて形式的なもの そうですか。ではこれはこのまま意味など追求せず、ざっくり覚えれば良いってことですね。 ＞冪集合に関しては、他の数学の分野を勉強するときに必然的に使うことになるので、そのときに慣れていけばいいんじゃないでしょうか 実は数学専攻ではないのです。冪集合って何故必要なんでしょう？ってところから分からないのです、、、。 ＞集合論なぜなにスレッド どなたか集合論に詳しい方が第二弾を立てて下されば良いのですが、、、。 884 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 08:16:27 ] >>883 感覚的には φ：箱がない、　{φ}：空箱、　{{φ}}：箱の中に空箱 まあ、イメージは個人の好き好きだから、ご自由に 冪集合(公理)がないと、集合の部分集合を集めて新しく集合を作ることが 一般にはできなくなって、すごく困ります 885 名前：１３２人目の素数さん [2006/03/04(土) 08:26:14 ] ＞実は数学専攻ではないのです。冪集合って何故必要なんでしょう？ってところから分からないのです、、、。 冪集合を考えることが本質的に必要になるのと自覚するのは位相とか測度論とかを勉強するときだろう。 ある集合 Ｘ が与えられたとき、Ｘ の元に関する性質だけを議論しているときは冪集合という概念は自覚する必要が無いが、Ｘ の部分集合に関する性質を議論するようになると、冪集合という概念をどうしても意識する必要が出てくる。 886 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 08:44:29 ] 「三角形の集合」と言ったら R^2 の冪集合の部分集合だし 平面図形を回転させてできる回転体は R^3 の冪集合の部分集合の和集合なわけだから、 冪集合ってのは普段から使われてる。 簡単すぎるから無自覚に使ってるだけで。 887 名前：886 mailto:sage [2006/03/04(土) 08:47:55 ] もちろん、無自覚に使うのと、意識して使うのとは全然違うから、 >>885 に反論してるわけではないです。 888 名前：874 [2006/03/04(土) 08:54:40 ] >>884 空集合での例ですね？非常に分かりやすい説明ですね。では空集合でないものは、 a：箱に入ってないa {a}：箱に入ったa {{a}}：箱に入った箱に入ったa っていう感じでいいのかな？ ＞集合の部分集合を集めて新しく集合を作ることが 一般にはできなくなって、すごく困ります 集合の部分集合を集めて新しく集合を作るのは何のためですか？ >>885 以前は、元は単数の要素で、元が複数に集まったものが部分集合なのだと思い込んでました。 でも部分集合のなかに要素がひとつしかなくても、{}の中に入ってればそれは元でなくて部分集合なんですよね。 ひとつきりの要素が元になれたり集合になれたりするのは何故ですか？操作する人が勝手にどちらかに決めているだけの話なのですか？ 889 名前：874 [2006/03/04(土) 09:00:57 ] >>886 ＞「三角形の集合」と言ったら R^2 の冪集合の部分集合だし ＞平面図形を回転させてできる回転体は R^3 の冪集合の部分集合の和集合 そうなのですか？何故そうなるのかもっと詳しく教えて下されば嬉しいです。 890 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 09:35:19 ] φ={ } だから φ：空箱、　{φ}={{ }}：箱の中に空箱、　{{φ}}={{{ }}}：箱の中の箱の中の空箱 とするべきだった >>889 三角形は R^2 の部分集合、R^2 の冪集合は R^2 の部分集合を全部集めた集合 だから、三角形の集合は R^2 の冪集合の部分集合 しばらく自分で考えてみてください 891 名前：874 [2006/03/04(土) 09:51:44 ] >>890 ＞φ={ } そうか！空集合だけが集合と言いながら{ }がついていないのはそのせいなのですね。 ＞しばらく自分で考えてみてください お陰で良く分かりました。Ｒってのが何なのか分からなかった(今も分かりませんが）ので、何のことかさっぱりでした。 892 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 19:08:37 ] Rは実数全体の集合のことですよ >>888 数学全体の中で考えたときに、集合論が何のためにあるのか、 というと代数なり解析なり他の分野の数学を展開するのに充分な基礎を与える、 という役割が一番大事だと思います で、冪集合を認めないと実数や複素数全体（と基数が同じ）集合の存在が 一般に言えず、したがって例えばRからRへの函数全体、などの概念が 実は矛盾概念かもしれない、と言った不安があるわけです 893 名前：874 [2006/03/04(土) 20:23:38 ] >>892 Ｒは実数全体の集合なのかなとも思ったのですが、何故三角形がそれの^2で回転体が^3なのか分からなかったので確信が持てませんでした。 しかし、三角形は平面だからＲのｘ軸*Ｒのｙ軸で^2、 回転体は立体だからＲのｘ軸*Ｒのｙ軸*Ｒのｚ軸で^3、 ということなのですね？ そうすると、平面体の全集合は^2の冪集合を構成し、立体の全集合は^3の冪集合を構成する、 ということなのですね？ 894 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 22:45:57 ] A^2というのは(a1,a2)といったAの要素の二つの組です A^3とかA^nとかも同様です（集合論の教科書に書いてありますが） だから大体そのとおりです ＞そうすると、平面体の全集合は^2の冪集合を構成し、立体の全集合は^3の冪集合を構成する、 ＞ということなのですね？ ここら辺がよくはっきりしないですが、多分「平面体の全集合」で平面R^2の部分集合の全体のことを 「立体の全集合」でR^3の部分集合の全体のことを指しておられるのかな、と 895 名前：１３２人目の素数さん mailto:sage [2006/03/04(土) 22:48:37 ] つーか素朴集合論なんてのは拘泥しないで本を読み進んで 後から読み直す方が早いし理解も深いと思うんだ 896 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 00:15:45 ] >>895 俺もその意見にかなり賛成だが、まあべき集合は重要な概念だし、 一度じっくり考えてみることもそれなりに意味はあるんじゃないの。 説明に対する>>874の理解具合を見るに、べき集合は>>874にとって ほどよい課題だったと思う。ただ素朴集合論の一つ一つの細かいテクニックに こだわりすぎるのははっきり無駄だろうね。 897 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 00:30:42 ] 正直なところなぜ必要なのでしょうかと言われても 数学やらない人には必要ない気もするけどねｗ 898 名前：874 [2006/03/05(日) 04:35:22 ] >>894 よく分かりました。どうもありがとうございました。 皆様のお陰で冪集合に関してはこれですっきりしたような気がします。 次の質問は、カントールの対角線論法なのですが、 あの論法の素晴らしさがどうも分かりません。 なんだかトリックのような狐に摘まれたような気分を味わってしまうのです。 なにかとんでもなく勘違いしているのか、単に理解不足なのか、、、？ 899 名前：１３２人目の素数さん mailto:sage [2006/03/05(日) 09:23:00 ] 狐に抓まれた感じがして正常だと思いますよ 900 名前：１３２人目の素数さん [2006/03/05(日) 15:09:57 ] 　{ a_1 , a_2 , a_3 , … } という数列を与えると、その数列を“使って”、その数列に現れるどの値とも異なる値を構成してみせる、という論法が、いかにも「後だしジャンケン」だからでしょう。 　もし、あらかじめ用意していたストックの中からどの a_n とも違う値を「ほらよ」といって出して見せるならズルくない、というわけでしょうが、 これだって、「ほらよ」と見せる値というのは実際に数列を見せてもらってからでないと指定することができないのだから、結局はズルイ・ズルくない、というのは所詮先入観に過ぎないわけだ。 　とここまで書いて、反論を待つことにしよう。 901 名前：874 [2006/03/05(日) 19:55:26 ] >>899 正常だと言っていただけて嬉しいような、さてではどうしよう、といった不安のような。 >>900 後だしジャンケンというか、あれだと斜めであろうが一つ飛ばしだろうが、 いくらでも簡単に違う値を作れるわけじゃないですか。 でそれを出して見せてるだけなのに、"強力な論法"と絶賛されているのは いったい何故？、と思うのです。 902 名前：１３２人目の素数さん [2006/03/06(月) 16:53:51 ] なんだ結局単発質問スレか 903 名前：１３２人目の素数さん [2006/03/07(火) 01:57:15 ] ゲーデルの原論文（独語） Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme をネット上で読みたいんですが見つけられる人います？ 904 名前：１３２人目の素数さん [2006/03/07(火) 14:17:58 ] 駄スレ保守 905 名前：１３２人目の素数さん mailto:sage [2006/03/08(水) 06:46:56 ] > 後だしジャンケンというか、あれだと斜めであろうが一つ飛ばしだろうが、 > いくらでも簡単に違う値を作れるわけじゃないですか。 > でそれを出して見せてるだけなのに、"強力な論法"と絶賛されているのは > いったい何故？、と思うのです。 どんな馬鹿でも簡単に違う値を作れる必勝ルーチンが 強力でなくて何が強力なんですか 906 名前：874 [2006/03/08(水) 19:13:18 ] ううむ、、、やはり単にそういうことなのでしたか、、、。 素人には見えないが実は数学的に凄いものが隠されているのでは などと勘ぐっていました、、、。 皆様、これまでのご回答ありがとうございました。 また後日、新しい質問を持って再臨します。 907 名前：１３２人目の素数さん mailto:sage [2006/03/08(水) 19:34:06 ] >>906 自己言及の論理と計算 www.kurims.kyoto-u.ac.jp/~hassei/selfref.pdf こういうのとはまるで違うけど、 対角線論法はArzela-Ascoliの定理を始めとする解析の命題の証明でもよく使う。 大雑把に言えば∀∃を∃∀に入れ替えたい時とか。 ＞ただ素朴集合論の一つ一つの細かいテクニックに ＞こだわりすぎるのははっきり無駄だろうね。 908 名前：１３２人目の素数さん [2006/03/10(金) 07:42:10 ] 質問です。(基礎論の記号がつかえないのでわかりづらい文章になってしまいましたが…) ＡがＭ、mにおいてみたされるはＭ　m∽Ａで表すことにします。 またｎ＝ｎ’(i)はi番目のところ以外が同じことを表していることにします 次の定理を今証明したい 「n＝m(j)　ｎｊ＝ｔ[m]ならばＭ　ｎ∽Ａ(aj)⇔Ｍ　m∽Ａ(ｔ)」 この証明で分からない部分 Ａ(aj)に含まれる論理記号の数Ｌについて帰納法でときます。 Ｌは0より大きいときで左側の記号が∀のときでＡ(aj)＝∀xＣ(aj,x)とおいたとき Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば �@Ｍ　ｎ∽∀xＣ(aj,x) ⇔∀n'＝n(i)；Ｍ　ｎ∽Ｃ(aj,ai) �AＭ　m∽∀xＣ(ｔ、ｘ) ⇔∀m'＝m(i)；Ｍ　m'∽Ｃ(t、ai) �@�A両方成立 分からない部分は �@ではaiはＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っているという設定になりますが(定義)これでは�Aにおいてｔがその最小の番号をふくんでいるときにそのaiをとることはできないんじゃないか？ というところです。 これを悩みつづけて死にそうです。誰かお願いします。 909 名前：908 [2006/03/10(金) 07:45:15 ] >>907の補足 松本和夫さんの「数理論理学」のｐ39の部分です。 910 名前：908 [2006/03/10(金) 07:46:04 ] 間違えました>>908の補足です 911 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 08:31:28 ] >>908 > Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば > �@ではaiはＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っているという設定になりますが(定義) > これでは�Aにおいてｔがその最小の番号をふくんでいるときにそのaiをとることはできないんじゃないか？ 含んでないって書いてるじゃん、自分で。 912 名前：908 [2006/03/10(金) 08:40:34 ] >>911お返事誠にありがとうございます。 言い方を少し間違えてしまいました。 �@におけるＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っている自由変数と �AにおけるＣ(ｔ、x)に含まれない自由変数のうちで最小の番号をもっている自由変数とが一致すると断定できないはずなのにこの証明では断定しているところがわからないのです。 913 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 08:47:51 ] >>912 1, 2 についてそれぞれ別々に i をとるって話ならそうなるけど、 >  Ｃ(aｊ、x)およびｔに含まれない自由変数aiをとれば ここであらかじめ i をひとつとって固定して、 その i について 1, 2 が成立ってことではないの？ 914 名前：908 [2006/03/10(金) 08:54:29 ] お返事ありがとうございます。 その可能性はゼロです。 なぜならＣ(aj、ｘ)に表れない自由変数のうちで最小の番号を持っている自由変数はＣ(aj、ｘ)に依存して一つだけ確定しますし Ｃ(ｔ、x)に含まれない自由変数のうちで最小の番号をもっている自由変数も同様にＣ(ｔ、x)に依存して一つだけ確定するからです。 それらが一致することが謎なのです。 915 名前：908 [2006/03/10(金) 09:01:16 ] 補足 Ｍはフレームです。 ｔは項です m、nは点列です。 916 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:09:27 ] >>914 それらが一致すると書いてある？だとすればその本が間違ってそう。 けど、素直に >>908 の証明を読むと >>913 のようにしかとれないし、 それで証明としては正しいような気がする。 # 自由変数云々って計算機上で扱わない限りそんなにこだわるところではないような 917 名前：908 [2006/03/10(金) 09:19:01 ] ＞＞916お返事ありがとうございます。一致するとは書いてありませんが、定義の通り解釈すれば一致するということと同じであるように受け取れます。 もし自由変数の番号付け替え可能ならば話は別です。しかしその可能性は薄い気がします。 Ｍ　m∽∀ｘＡ(xｊ)の定義は松本さんの本によると「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai) ただしaiはＡ(xｊ)に表れない自由変数のうちで最小の番号を持ったものとする」 書いてあります。 918 名前：908 [2006/03/10(金) 09:37:53 ] 実はもうひとつ質問があります。 その本の中に出てくるのですが一意写像とは何でしょうか？ 質問ばかりで誠にすいません。 919 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:38:06 ] >>917 > Ｍ　m∽∀ｘＡ(xｊ)の定義は松本さんの本によると「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai) > ただしaiはＡ(xｊ)に表れない自由変数のうちで最小の番号を持ったものとする」 ちょっと考えなきゃいけないけどこの定義でも >>913 の解釈で大丈夫だと思う。 補題として 「m,n を A(xj) に現れるどの自由変数 ak に対しても mk=nk となるものとする。 　このとき mi=nj であれば 　Ｍ　m∽Ａ(ai) ⇔ Ｍ　n∽Ａ(aj) 」 みたいなのがあればいいかな。(細かいところは修正がいるかも) これを暗黙のうちに使ってるのでは？ 920 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 09:45:13 ] >>918 ttp://www.tanimura.org/v1/?title_id=21987&mode=d これによると一価関数のことらしいけど、それで話通じる？ ぐぐったら二件しかヒットしなかったからほとんど使われない言葉なのかも。 921 名前：908 [2006/03/10(金) 09:47:50 ] >>920はい、それで大丈夫です。ありがとうございます。 今から>>919の文章考えたいので少し(いや、かなり)時間ください。 922 名前：908 [2006/03/10(金) 10:04:11 ] >>919すいません。mi＝nｊの条件はどうやれば出てくるでしょうか？ ｎｊ＝ｔ[m]なのですが… 馬鹿で本当にすいません。 923 名前：908 [2006/03/10(金) 10:15:13 ] お騒がせしました。遂にわかりました。 皆さんありがとうございました。 >>919の補題はｎｊ＝ｔ[m]でも成立するのですね？ そうとしか考えられないし、そうであるとすればすべての合点がいきます。 ＞＞919さんには本当に心から感謝します。 これでもうこの問題の苦悩は完全に解かれました。 誠にありがとうございました。 924 名前：908 [2006/03/10(金) 10:30:21 ] すいません。やっぱりよく考えてみたらわかってませんでした。 ていうか＞＞919の補題普通に考えてｎｊとajのところｔにおきかえたら証明すべき定理になりますね そうとう僕は馬鹿ですね。 925 名前：１３２人目の素数さん mailto:sage [2006/03/10(金) 11:11:59 ] えーと、 >>919 でいいたかったことはむしろ ∀ の場合の ∽ の定義 「m＝n(i)をみたす任意のnに対してＭ　n∽Ａ(ai)」 で i の最小性を条件から外してもいいんじゃないかっていうようなことです。 あんまり書き方よくなかったか。 つまり 　A(xj) で自由でない番号最小の ai と、 m＝n(i) をみたす任意のnに対して Ｍ　n∽Ａ(ai) ⇔ A(xj) で自由でないある aj があって、 m＝n(j) をみたす任意のnに対して Ｍ　n∽Ａ(aj) が成り立つんじゃないかと。 そうすればもともと問題だった番号の最小性は気にしなくていいことがわかる。 で、 → は明らかなんだけど ← を示すのに >>919 みたいなことがいる。 926 名前：908 [2006/03/10(金) 12:19:09 ] わかりました。 今度こそ完全に。 本当に＞＞925さんありがとうございました。返事おくれてすいません。 927 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 17:22:10 ] 自然数x, yについての関係y=2^xを言語(0, S, +, *)で表現するのって、 やっぱりゲーデル数でコーディングしてβ関数とかを用意しないと無理？ 指数関数くらい簡単なものだったらゲーデル数を持ち出さなくても何とかならない？ 928 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:42:38 ] >>927 無理なんじゃないかなあ 昔だいぶ考えたけど、結局のところ列のコーディングをつかわないと 原始帰納が書けないからどうにもならんような。 「∃x.y=2^x」なら書けたけどそのへんで限界を感じた。 929 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:44:27 ] ＞∃x.y=2^x それけっこうすごいな 930 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 21:57:36 ] >>928 やっぱ原始再帰法とガチンコ勝負になっちゃうか。 「∃x.y=2^x」は俺も考えた。 「y≠0は2以外の素因数を持たない」って関係だからこれは何とかなるけど、 そこから「x個の素因数を持つ」ってのが書けなくてアウト。 931 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 22:01:29 ] あ、そうかｗ 932 名前：１３２人目の素数さん mailto:sage [2006/03/14(火) 22:25:35 ] Matiyasevich-Robinson-Davis-Putnam の定理を使えば coding はいらないことになるかな。 933 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 04:54:07 ] 質問させて下さい。 競馬で �@必ず的中率25％になる �A１レース〜６レースまで毎回参加 �B当たればそのあとのレースはしない �@�Aの条件の時(的中しても１〜６レース全てやる)と、 �@〜�Bの条件の時、 １レース目の的中回数、的中率 ２レース目の的中回数、的中率 ３レース目の的中回数、的中率 ４レース目の的中回数、的中率 ５レース目の的中回数、的中率 ６レース目の的中回数、的中率 全て外れる回数、確率 これらはいつかは同じような回数、確率になりますか？ 934 名前：１３２人目の素数さん [2006/03/15(水) 05:43:33 ] age 935 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 06:51:04 ] >>933 条件に追加で １〜６レースまでに１度当たる確率が75％ ってのを加えさせて下さい。 936 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 08:49:43 ] >>935 よく考えたらこれがあると矛盾するんでなしにしてください。 937 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 08:54:17 ] ここは証明論とかモデル論とか不完全性定理のスレなので。。 他をあたって下さい 分からない問題はここに書いてね２３４ science4.2ch.net/test/read.cgi/math/1141432182/ 938 名前：１３２人目の素数さん [2006/03/15(水) 09:06:01 ] >>937 いってみます。 誘導ありがとうございます。 939 名前：中川秀泰 [2006/03/15(水) 11:26:17 ] イッテ見なさい 940 名前：１３２人目の素数さん mailto:sage [2006/03/15(水) 15:07:40 ] >>932 や、指数関数という簡単なものでさえ、+と*だけで書くには コーディングとかその定理とかの大道具が必要になるって事を確認したかった。 コンピュータなんか無い時代に再帰関数とかゲーデル数とかを編み出して、 計算というものをクリアに捉えて、 計算できるものを+と*だけでなんでも表現しちゃおうと考えるなんてマジすげぇ。 941 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 02:05:41 ] 基礎論を知らない人に「基礎論って何ですか？」って聞かれた時に、 簡単な練習問題を幾つか挙げて、それについて考えてもらうことによって 基礎論がどのようなものか理解してもらうとしたら、どんな問題を挙げますか？ なるべく基礎論の魅力がよく表現されているもので、慣れてない人にとってはちょっと難しいが、 ある程度真剣に考えてもらえば殆どの人が回答にたどり着けるような問題をお願いします。 942 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 02:47:44 ] そんな簡単なの無いような 943 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 03:58:39 ] 不完全性定理でいいんじゃないの？ λで書いたやつなら数十行で書けるし 944 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 04:04:35 ] 誘導付けたらすごい長大なものになるかと 945 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 04:53:40 ] 無矛盾性に目をつぶれば20行で出来るんだけどね 946 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 05:54:50 ] 演繹定理なんかどうだろう。 947 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:45:30 ] 初学者です。質問いきます。 形式的体系が無矛盾、というときの形式的体系って、なんか、形式的体系として必須の推論規則とか、あるんですかね？ なんかあたりまえのことらしく、本の最初のほうにすら書かれてないんですが 例えば、 ¬(s0+s0=s0+s0)とs0+s0=ss0を公理として置くとして、これは明白に無矛盾でないんですが、推論規則がなきゃ、s0+s0=ssoは出てこないので、無矛盾か？いや、そんなはずはない、と悶絶しております というか、公理図式だけを置いた形式的体系、論理式をいくつか公理としておいただけの形式的体系なんてあるのか？というところでつまづいてます 948 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:46:33 ] すいませんagemasu 949 名前：１３２人目の素数さん [2006/03/16(木) 15:47:13 ] すいませんagemasu 950 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:48:19 ] すいませんsagemasu 951 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 15:51:59 ] >>947 読んでいる本の書名は？ 952 名前：１３２人目の素数さん [2006/03/16(木) 16:16:44 ] いや、本の問題というか、 どの本も、まず、公理、推論規則、があって形式的体系、 ないし、推論規則だけ置いた自然演繹、ということで始まっていて、 というか、まず、無矛盾である、例えば、一階述語論理の公理系があって、それに固有公理を加えた形式的体系が無矛盾であるとか、無矛盾でない、ということを言ってるんですかね？ 例えば、集めたい論理式の範囲がs0+s0=ss0とs0+s0=s0+s0だけで、s0+s0=ss0とs0+s0=s0+s0だけを、公理としておいて、形式的体系だ、とか言うことはナンセンス、ですかね？ 953 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:25:29 ] > 一階述語論理の公理系があって、それに固有公理を加えた形式的体系が > 無矛盾であるとか、無矛盾でない、ということを言ってるんですかね？ どの本にもそういうことは書いてあるはずなので、間違った読み方をして いるのだと思うが。 954 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:27:10 ] >>952 数論始めるときは一階の述語論理の推論規則と公理は前提にするのが、 普通のやり方と思うが。 「無矛盾」の意味は矛盾式が決して導かれないということだから、 公理に矛盾式が含まれず、推論規則が存在しなければ、無矛盾なのは自明では？ 955 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 16:48:23 ] >>941 基礎論は知らないけど数学は知ってるって人が対象なら、 >>545にあるようなモデル理論の応用を見せるとか。 Hilbertの零点定理は代数閉体の理論の量化記号消去と同値 (正規化定理を使わない)ってのは、代数やってる人には結構面白いかも。 ただ「基礎論がどのようなものか理解してもらう」というのとは違うか。 956 名前：１３２人目の素数さん mailto:sage [2006/03/16(木) 18:47:09 ] ナンセンスというか、べつにそういう「形式的体系」を定義しても いいけど、意味が無いよ、ということだけでは 957 名前：１３２人目の素数さん mailto:sage [2006/03/23(木) 23:53:59 ] 非古典論理上で「純粋数学」をしてる人ってどのくらいいるんですか？ ここでは取りあえず、何か形式的体系の(メタでなくオブジェクトの)定理群の持つ 驚異的な美しさや意外な関係や面白さを味わう事を「純粋数学」とし、 一階古典論理上のZFC(or BG)での「純粋数学」を「古典純粋数学」と言う事にします。 メタとオブジェクトの区別なんて相対的なものだけど、 そこら辺は感覚で(最もオブジェクト寄りとか)。 大分数学を曲解・矮小化してますけど、議論の簡易化のためという事で。 いわゆる代数・幾何・解析は「古典純粋数学」で、 大半の純粋数学者は「古典純粋数学」をやってると言えます。 一方直観主義論理+構成的集合論(or 圏論)という組み合わせも研究されているようですが、 その内容は「純粋数学」っぽくなく、メタ数学やら哲学やら計算機といった 話題ばかりが目に付きます(ネットで検索してみただけですが)。 その他のなんちゃら論理・なんちゃら集合論もどうもそんな感じです。 「古典純粋数学」とパラレルに「非古典純粋数学」が研究されててもいい気がします。 Euclid幾何とパラレルに非Euclid幾何があるように。 958 名前：１３２人目の素数さん [2006/03/24(金) 15:32:27 ] age 959 名前：１３２人目の素数さん mailto:sage [2006/03/24(金) 23:31:32 ] >>957 >>237 を参照 960 名前：１３２人目の素数さん [2006/03/25(土) 14:32:26 ] 紀元前２６０００年に大亜細亜日本帝国が誕生した。西はウラル山脈から 東は日本列島まで、南はオーストラリアまで征服した。これが日本の原型である。 961 名前：１３２人目の素数さん [2006/03/25(土) 14:41:13 ] 1+1=2になるのはどうしてですか？教えて下さい 962 名前：１３２人目の素数さん [2006/03/25(土) 14:54:17 ] 突然の質問ですが、 AD//BCの台形ABCDにおいて、AB=6,BC=13,CD=5,AD=8のときcosＢを求めよ。 この問題解ける方いませんか？ 963 名前：１３２人目の素数さん [2006/03/25(土) 15:19:30 ] スレ違い 964 名前：GiantLeaves ◆6fN.Sojv5w [2006/03/25(土) 15:50:59 ] talk:>>962 いる。それが何か？ 965 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 18:07:21 ] 真である命題全体の集合Aを考えた場合 証明不可能な問題はAに含まれるの？ 966 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 18:43:53 ] >>965 証明不可能な命題の集合と言う事？ それなら一般には含みも含まれもしない 次スレ立てるときは「基礎論」という名前付けると スレ違いの質問が多いから別の名前付けましょうか 数理論理学とかFoundation Of Mathematics とか いずれにしても一寸ニュアンスが違うのが気になるけど 967 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 19:38:30 ] 「メタ数学スレッド」とか？それもちょっと違うのかな。 最初に注意書きでもあればテンプレ嫁で済ましてもいいかもしれない。 968 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 20:01:37 ] >>966 直観主義でなければ排中律を認める 排中律を認めるならば全ての命題は真か偽かのいずれかである よって{真である命題全体の集合}に含みも含まれもしない命題は存在しない ゆえに直観主義以外においては証明不可能な命題は命題ではない というトンデモ理論を見た事がある 969 名前：１３２人目の素数さん mailto:sage [2006/03/25(土) 23:50:12 ] >>967 テンプレきちんと読む奴がそれほど居るか、疑問だけどね >>968 ＞{真である命題全体の集合}に含みも含まれもしない命題は存在しない {.........}にそれ自身φもその否定¬φも含まれない命題は存在しない、 ということだろうかｗ まあ真と証明可能の違いも、真と恒真の違いも考慮されてないから どちらにせよ駄目だろうけどｗ 970 名前：965じゃないけど mailto:sage [2006/03/26(日) 00:52:28 ] >>966 どうもよく分からないんですが、決定不能な命題は真ではないのでは。 ならば決定不能な命題は「真である命題全体の集合」には含まれないのでは。 「真である命題」とは当然「真であると決定できる命題」のことでしょ？ 違うんですか？ 971 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 09:49:29 ] >>969 > テンプレきちんと読む奴がそれほど居るか、疑問だけどね まあ、読めと言い捨てるためにテンプレを書いとくという考え方もあるかと。 972 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 12:15:55 ] その集合はZF？ZFC？ 973 名前：１３２人目の素数さん [2006/03/26(日) 17:57:18 ] 【ロボットは人間にはなれない】の証明はどこで読めますか？ 974 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 22:02:05 ] 「真である命題全体の集合」は公理的集合論では扱えないという事？ よくわからん 975 名前：１３２人目の素数さん mailto:sage [2006/03/26(日) 22:17:20 ] 現存関連スレ ・数学板 数理論理学やりたいのになんで哲学科なんだよ！ 非古典論理について語るスレ ゲーデル不完全性定理 ・哲学板 【必然】様相論理 Vol K【可能】 論理学学習スレッド バカでも分かる論理学 数学の哲学 (Philosophy of Mathematics) 「数理論理学やりたい〜」スレの(スレタイはともかく)実際の使われ方は割とこのスレに近く、 このスレの次スレとして使えなくもなさそうな気もします。 新スレを立て、スレタイを変更するなら、 「数理論理学・数学基礎論スレ」と併記する辺りが無難かなと思います。 >>959 ありがとうございます。 どのようなモチベーションで研究されているのかもう少し調べてみます。 976 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 18:26:50 ] 一年百六十五日。 977 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 20:26:02 ] 証明不可能な命題ってのは{真である命題全体の集合}に入るか {真である命題全体の集合}^cに入るのかが判らない命題 978 名前：１３２人目の素数さん mailto:sage [2006/03/27(月) 22:01:42 ] {真である命題全体の集合} って 真である命題全体の集合 のことか 真である命題全体の集合の集合 のことかどっち？ 「・・・の集合」て言葉と中括弧を重ねられると 「の中止を取り止める」みたいでわかりにくいんだけど 979 名前：１３２人目の素数さん mailto:sage [2006/03/29(水) 21:51:26 ] >>977は正しいの？？？？ ホントに？ 980 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 06:02:55 ] >>970よりは>>977のほうがまし 981 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 14:43:16 ] 素人のおいらの理解 真である命題全部⊃証明可能な命題全部 偽である命題全部⊃反証可能な命題全部 真であり、かつ偽であるという命題はない 真であるのに「証明可能な命題全部」に含まれない、という命題がある 偽であるのに「反証可能な命題全部」に含まれない、という命題もある 982 名前：１３２人目の素数さん mailto:sage [2006/03/30(木) 23:13:52 ] 真であるとか真でないとか言う言い分を公理と証明以外のものに もとめるという感覚が理解できません。 証明できないけど真だっていうのは、たとえばどういうこと？ 983 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 00:06:29 ] >>982 >素人のおいらの理解 984 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 00:49:50 ] いや答えになってないし 985 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:27:59 ] 「証明可能」というときは公理系（理論）を固定して 「その理論において証明可能」というように相対化しないと 正しい理解にはならないよ 「文Aを証明する公理形が存在する」という意味で 「Aは証明可能」というのなら任意の文が「証明可能」になっちゃうし、 「文Aを証明する無矛盾な公理形が存在する」という意味でも 1階論理で反証されない任意の文が「証明可能」になっちゃう 986 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:34:45 ] 「真」の概念もそう 「任意の構造について真」とか 「自然数の構造Nについて真」とか 「ペアノ算術の任意のモデルについて真」とか 何についての真理のことを言っているのか常に自覚しないと駄目 987 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 14:49:41 ] ペアノ算術など、一定の条件を満たす無矛盾な公理系Tでは、 Aも¬Aも証明できない（算術の言語の）文Aが存在する これが（第一）不完全性定理 すると、例えば自然数の構造Nは、ペアノ算術のモデルだけども、 「Nで真の文」と「Nで真でない文、すなわちNで偽の文」は 算術の言語の文すべての集合を2分割するので、 ・AがNで真　（なのにTで証明できない） ・¬AがNで真　（なのにTで証明できない） のどちらかが成り立つ もちろんTと異なる体系T’では、証明できる文、できない文が Tと異なってくる 例えばTに公理としてAを加えた体系T’を考えれば Tで証明できなかったAが自明に証明できてしまう それでもまた新たに、T’で証明も反証もできない文Bがでてくる （T’が不完全性定理の条件を満たしていれば） 988 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 17:10:48 ] せっかくそういう説明しても>>982のようなやつには理解できないと思うよ。つーーーか 理解を拒否される気がする。 989 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 17:33:33 ] そういうもんかな ゲーデル文のアイデアを「感覚的」な（半分嘘の）説明で 説明したほうがいいのかもしれないけど 自分で半分嘘と思いつつ書くってのはどうも抵抗が でもやってみる 文Gを、「Gは証明可能でない」と定義する Gが証明可能だと仮定すると、Gの述べることは真だから、Gは証明可能でなく、仮定と矛盾 従ってGは証明可能でない、ゆえにGは真である というか>>982は、 「真でも偽でもない文が存在する」 という立場にコミットしてることを自覚してるのかな （「真」の意味にもよるだろうけど） 990 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 20:06:05 ] >>989 言ってることはおおむねは分かってるつもりですよ。 つまりその「Gは証明可能でない」にあたる命題が、どのように 公理系を選んでも、自然数の体系を含む公理系である限り 体系内にできてしまうって話しでしょ？ ＞「真でも偽でもない文が存在する」 ＞という立場にコミットしてることを自覚してるのかな そうですね。そうなってしまいますね。 （これをやると直観主義へ行ってしまうんですかね） これはこれで変な主張だなとは思います。だから 私は何かを主張したいというよりも、単純にわからないんで とまどってるんですよね。 ただ、排中律を無批判に認めるべきでない（「排中律を認めるべきではない」 ではない）という直観主義の立場もそれなりに理解はできる。 （ただ、無力ではないかという批判には反論できませんが） たとえば、真でも偽でもない文の存在を認めると、背理法が使えない 場合がでてくるわけですが、数学のすべてが壊れるわけではないし、 背理法を使わない証明がない場合で、背理法を使うのがあやしいような場合は 構成的に証明できるようになるまでの暫定措置だとも考えられる。 （まあ、それなら排中律を事実上認めているわけですが） それに、あと、単に「真」を「肯定証明可能」と同義にするか しないかの言葉の問題にすぎない気もしてきました。 991 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 21:44:45 ] ある一つの（固定された）モデルにおいて、真でも偽でもないような文は無い （つまり命題の真や偽は何故かは知らないがどちらかに決まっている） と信じてそう仮定するのが普通のsemanticsだと思います ある体系（論理の推論規則と公理と数学の公理）で証明可能、 というときに「ある体系」を意識するのが重要なのと同じで、 どの「モデル」で真か、というのが重要です そして全てのモデルで真である、というのを恒真と言います 自然数論や集合論だと分かりにくいので、仮に たとえば有限群論の公理系が与えられたと考えましょうか ∀a∃b a･b = b･a = e とかが公理です（有限性をどう公理にするのか知りませんがｗ） このとき、群の位数は偶数である、はモデルによって真になったり 偽になったりします 一方で群の位数を(p^n)q、qはpの倍数でなく、 pは素数としたときに、位数p^nの部分群が存在する、は恒真です 992 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 21:52:33 ] 直観主義にもKripke semanticsとかあるらしいんですが 勉強してないからしらないや 可能世界意味論とか言うらしいですが さて、たとえば自然数論で言うと、第一不完全性定理の主張は PAが無矛盾（つまり、証明できない文が存在する）なら （まあ、我々は、自然数が矛盾概念であるかもしれないなどとは 考えないので、そうだと強く確信している訳ですが）、 通常我々が言うところの「自然数」をモデルにとったときは 「真」であるはずの文で、しかもPAから証明できない文が存在する、というのが まあある程度正確な第一不完全性定理の主張です 993 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 22:20:18 ] ヒルベルト論理体系に基づく公理系自体が不完全なんだからその上にある自然数の公理が不完全でも仕方ないだろ 994 名前：１３２人目の素数さん mailto:sage [2006/03/31(金) 23:16:20 ] >>991 ＞ある一つの（固定された）モデルにおいて、真でも偽でもないような文は無い ＞（つまり命題の真や偽は何故かは知らないがどちらかに決まっている） ＞と信じてそう仮定するのが普通のsemanticsだと思います つまり、それ自体が公理なんですよね？ 995 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 17:28:39 ] >>993 古典論理の一階述語論理自体は、 あれ以外のもの（証明能力があれより強いもの）は考えられないので 論理体系が「悪い」んじゃなくて、やっぱ自然数論の「せい」なんじゃないですかね >994 まあそうですね 実際に何らかの方法で真偽が確定するわけじゃありません 僕も最初に勉強したときには結構違和感持ちました あの種の研究を最初に始めたのはTarsikiとからしいです 996 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 18:26:50 ] 一年百七十日。 997 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 19:26:16 ] >>995 自然数数論云々はあくまでゲーデルが最初に自然数論を用いて不完全性を照明したという 歴史的背景によるものであって、チャーチとかは自然数論に持ち込まずに不完全性を証明してる罠 998 名前：下妻物語 [2006/03/32(土) 21:05:34 ] 　 　　　 |　 ｲ ／／＼＼　.ﾄ 　|　　　　 　 　　　 |　|／／　| 　＼ヽl.| 　|　　　　　　　　　 　　　　　ヽ| ﾚ'　　　　　　ﾄ、|　|　　　　　　　　 　　　　　　|/　 　 Ｙ　 　　ヽ |/　　　　　　　　　 　　　　　　||丶＿人＿_ノ　| |　　　　　　　　　　 　　　　　　||　 |　 　 　 | 　| .|　　　　　 　　　　　　||　.|.__＿＿_|.　|,..i　　　　　 　 　　　　　|　|.　　 　　|　|　　　　　　 　 　　　　　|　|.　　 　　|　| 　　 　　　　　　　　 　 　　　　　(　⊃ 　　　(　⊃　　 栄えあるATがピンチです。助けて下さい。 AT最強！！ hobby7.2ch.net/test/read.cgi/bike/1142693513/ 999 名前：１３２人目の素数さん mailto:sage [2006/03/32(土) 21:11:35 ] 999 1000 名前：1000 mailto:sage [2006/03/32(土) 21:11:39 ] 1000 円均一 〜 って、もう　寝よ　っと。 基礎は睡眠にあり〜 ってなんちって てへ 1001 名前：１００１ [Over 1000 Thread] このスレッドは１０００を超えました。 もう書けないので、新しいスレッドを立ててくださいです。。。

---

---

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

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