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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 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 > やっぱそうなんだ。直観主義の人ってまだいるんだろうけど、排中律がそんなに嫌いなのかね？ じゃなくて、「正しい」という言葉の意味を普通の数学者とは違う意味に捉えてる。

---

---

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

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