数学基礎論・数理論理学　その8

1 名前： 忍法帖【Lv=11,xxxPT】 [2011/06/30(木) 12:57:29.95 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その7 kamome.2ch.net/test/read.cgi/math/1289481237/ 809 名前：１３２人目の素数さん mailto:sage [2011/09/02(金) 20:58:40.83 ] >>777 とりマセさんが、不完全性定理と停止問題の関係をtwitterでつぶやいているよ 逆数学的には同値ではないっぽい 810 名前：777 [2011/09/02(金) 23:10:08.07 ] そうみたいですね。 停止問題の方が強いと思ってたんですが、 実際は不完全性定理→停止問題は決定不可能 みたいですね・・・。 あとで証明してみようと思います。 チューリングマシンの停止問題の決定不可能性からRE等への間辺りが 自分の問題意識だったみたいです。 811 名前：１３２人目の素数さん mailto:sage [2011/09/02(金) 23:50:14.56 ] ほんとに>>777=>>810？ 812 名前：769 mailto:sage [2011/09/03(土) 00:02:14.35 ] 失礼>>769だった。 813 名前：１３２人目の素数さん mailto:sage [2011/09/03(土) 06:02:01.19 ] >806 無矛盾ということを書こうと思えば、カットがあろうとなかろうと、 無限個ある証明を対象にするのだから、当然なことだ。コード化する とき数値的表現可能性に関する部分が、原始帰納的述語で書くことが 簡単に思い浮かぶ範囲、例えば、有限な対象領域なら問題ない。 このようなことを、簡単だ、常識だといっているのではないでしょうか？ これを難しいというなら、一般に形式化すること自体難しいといっている のと変わらないと思いますが、、、。 814 名前：１３２人目の素数さん mailto:sage [2011/09/03(土) 17:02:48.58 ] 自然数論で述語論理の無矛盾性を証明するのに、 「カット除去なんかより1点構造での解釈を考えた方がはるかに簡単」派と 「いやカット除去と1点構造での解釈を考えるのは同じくらい面倒」派の議論が発端だったのだから、 後者は結局のところ「一般に形式化すること自体難しい」と言いたいのでは？ 俺はそんなことより、1点構造での解釈は、意味論というほどのものでもない、 という前者派の一部の主張を詳しく知りたいのが。 815 名前：１３２人目の素数さん mailto:sage [2011/09/03(土) 17:44:25.25 ] AFはアメリカ留学中初めて体験した。 816 名前：１３２人目の素数さん mailto:sage [2011/09/03(土) 19:54:35.46 ] >>782 超限帰納法が重要になる議論を、余帰納法に置き換えてもほぼ同様にできる、 というのはその手の業界ではよく知られた話。 FAが∈に関する帰納法を許し、AFAが余帰納法を許す公理だと考えれば至極当然のこと。 むしろ余帰納法ではダメだという例をきちんと示すほうが大発見。 よくFA派の人が「この論法はFAを本質的に使うからAFAにすると困る」みたいなことを言ってるけど、 本当に余帰納法に置換えてやろうと試してみたのかよ、と突っ込みたくなる。 817 名前：１３２人目の素数さん mailto:sage [2011/09/04(日) 00:00:50.55 ] 停止問題を持つ形式体系は全て不完全である。 818 名前：１３２人目の素数さん mailto:sage [2011/09/04(日) 00:26:21.20 ] >>809 とりマセ氏は 　「停止問題が決定不可能である」ということを知っていても「ACA_0 は RCA_0 より真に強い」ということしか導けません とか 　「ゲーデルの不完全性定理」を知っていれば「WKL_0 は RCA_0 より真に強い」ということを導ける とか言っているので、>>777の言うのとは少し違うんじゃ？ >>777のは、 　「停止問題が決定不可能である」は ACA_0 と RCA_0 上同値 とか 　「ゲーデルの不完全性定理」は WKL_0 と RCA_0 上同値 とかそういう話でしょ。いやその同値が正しいのか知らないんだけど。 819 名前：１３２人目の素数さん mailto:sage [2011/09/04(日) 06:06:38.32 ] >816 AFA で何が出来るのかよく知らないで AFA を批判する人がいるってことだね。 別に AFA に限った話じゃないような。 820 名前：あんでぃ mailto:sage [2011/09/05(月) 16:25:15.68 ] [T4RM] Tokyo 4units Re Money game [T4RM] 821 名前：769 mailto:sage [2011/09/05(月) 20:29:49.73 ] 田中の数学基礎論講義の PartA最初のページの問１、 「ある形式体系Tで論理式∃xA(x)が証明できても A(t)が証明できるような項tが存在するとは限らない。 そのような体系Tと論理式∃xA(x)の例をあげよ。」 の解答お願いします。 822 名前：１３２人目の素数さん mailto:sage [2011/09/05(月) 21:11:31.34 ] それだけだとZFCのφとか{φ}とかωとか2^ωとかω1とか 無数にtrivialな例があるんだけど、 本当はHerbrandの定理とかの話とはちょっとズレるんだよね 823 名前：１３２人目の素数さん [2011/09/05(月) 21:18:29.14 ] >>822 その下に 「上の問題ができないと、ヘンキンの定数記号を用いた 完全性定理の証明は何をやっているのかわからないと思う」 とありました。 私は形式体系に関数がなければ良いだけと思うんですが。 824 名前：１３２人目の素数さん mailto:sage [2011/09/06(火) 01:23:30.41 ] その本では定数(constant)記号は関数記号の一種として扱ってるのかな？ 825 名前：１３２人目の素数さん [2011/09/06(火) 07:17:21.03 ] アリティー0の関数を定数としていますね。 項の定義は、 変数記号と、変数記号を引数に持つ関数記号ですね。 826 名前：１３２人目の素数さん [2011/09/06(火) 18:44:59.57 ] 完全性定理の後に答え載ってました（爆 A(x)≡(x＝0∧σ)∨(x＝1∧¬σ) でしたね（＾＾； 827 名前：１３２人目の素数さん mailto:sage [2011/09/06(火) 20:05:44.34 ] あくまで答の一例だからね 828 名前：１３２人目の素数さん mailto:sage [2011/09/06(火) 22:52:24.56 ] >826 σか¬σが証明可能なセンテンスならダメじゃないか。 829 名前：１３２人目の素数さん [2011/09/06(火) 23:14:54.22 ] >>828 σと独立な形式体系という条件を忘れてました。 良くわかりましたね（＾＾； 830 名前：１３２人目の素数さん [2011/09/07(水) 08:35:29.09 ] >829 σ と 独立な形式体系という2つの組の例をあげないと答えにならないのでは、、、。 そのような例をあげることができる人には、(x＝0∧σ)∨(x＝1∧¬σ) もわかる からヒントになっているのかな？　 831 名前：１３２人目の素数さん [2011/09/07(水) 18:33:20.47 ] >>830 私はよくわかりませんでした。 算術の公理系Tは σを証明も反証もできない、さらに0と1を定数として持つ。 A(x)←→(x＝0∧σ)∨(x＝1∧¬σ) とおくと T　|―　A(0)∨A(1) だそうですが、なぜこれが証明できるのか不明ですね。 832 名前：１３２人目の素数さん mailto:sage [2011/09/07(水) 20:10:23.14 ] トートロジーだろうが 833 名前：１３２人目の素数さん mailto:sage [2011/09/07(水) 20:47:08.82 ] σがどんな式だろうが σ∨¬σは証明できる 834 名前：１３２人目の素数さん [2011/09/07(水) 21:12:05.30 ] つまり、 T　|―　A(0)∨A(1) でA(0)は¬A(1)だとでも言うのでしょうか？ 835 名前：１３２人目の素数さん mailto:sage [2011/09/07(水) 21:15:43.39 ] >831 独立命題というと難しいものしか思い浮かべられないかもしれません。 しかし、公理系が弱ければ弱いほど、独立命題は増えるわけです。 ですから、形式体系として述語論理そのものを選んでもよいのですが、 算術の体系 T をとりましょう。そして、それに P(x) という述語を付け加えた 体系 T_P を考えます。すると、∃x P(x) は述語 P の解釈により、正しい場合も 間違っている場合もあります。つまり独立命題です。 836 名前：１３２人目の素数さん mailto:sage [2011/09/07(水) 21:33:27.84 ] ZFのスコーレム化ZF^skは ∀x∃yφ(x,y)から∀xφ(x,f(x))が導ける訳なので ZFCと実質的に同じものですよね？ 837 名前：１３２人目の素数さん mailto:sage [2011/09/08(木) 03:50:40.45 ] >>835 その本では等号に関する公理は素の述語論理に含まれている？ というか独立な「文」でないといけないの？ 自由変数が現れている論理式は演繹関係の対象外？ 838 名前：１３２人目の素数さん mailto:sage [2011/09/08(木) 20:33:59.52 ] 正確に言うと擬トートロジー(quasi-tautology)だな 839 名前：１３２人目の素数さん mailto:sage [2011/09/08(木) 21:26:47.12 ] A(0)∨A(1)は述語論理の規則のみで証明できる。 >>834は不完全性定理について書いた本じゃなくて 述語論理のみについて丁寧に書いた本を一冊読んだ方が良いかもしれない。 840 名前：１３２人目の素数さん mailto:sage [2011/09/08(木) 21:27:26.58 ] >>836 その通りです。 ZFにスコーレム関数を付け加えると 選択公理が証明できます。 841 名前：１３２人目の素数さん [2011/09/08(木) 22:00:46.95 ] >>839 述語論理の本も並行して読んでるんですが この論理式がどうしても公理から出せないんですよね・・・。 842 名前：１３２人目の素数さん mailto:sage [2011/09/08(木) 22:28:55.15 ] (0=0)∧(1=1)∧(σ∨¬σ) ------------------------ ((0=0)∧(1=1)∧σ) ∨ ((0=0)∧(1=1)∧¬σ) --------------------------------------- (0=0∧σ)∨(1=1∧¬σ) ----------------------------------------------- (0＝0∧σ)∨(0＝1∧¬σ)∨(1＝0∧σ)∨(1＝1∧¬σ) これすなわち A(0)∨A(1) 843 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 06:18:52.76 ] 等号公理は使っているわな 844 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 07:04:58.76 ] >843 ＝ という記号を使って、等号公理を使わないのなら ＝ という記号 を使わないのが当然。 845 名前：１３２人目の素数さん [2011/09/09(金) 08:03:03.80 ] わしの本では ｘ＝ｘと ｘ＝ｙ→A（ｘ）→A（ｙ）は公理あり 846 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 15:27:06.29 ] >>844 当然といえば当然なんだが、>>834も当然分かっているのかと 847 名前：834 [2011/09/09(金) 19:01:47.87 ] ウシュカヴィッツの公理系とかいうのが使われてますね。 |―A　⇒　|―A∧A の証明もままならないですね（＾＾； 848 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 22:03:06.85 ] >>846 確かに、いわれるとおりですね。きっとわかっていないでしょう。 849 名前：834 [2011/09/09(金) 22:24:12.19 ] （＾＾； （＾＾； （＾＾； （＾＾； （＾＾； 850 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 22:29:38.40 ] なんかみんな　ｘ＝ｘ　のことを「等号公理(equality axiom)」って言ってるみたいだけど、それは ｘ＝ｙ→A（ｘ）→A（ｙ）　のことだよ。 ｘ＝ｘのほうは「同一性公理(identity axiom)」な。 851 名前：834 [2011/09/09(金) 22:40:28.77 ] すいませんが 日本の本でヒルベルト流の推論体系に 詳しいのがあったら教えてもらえませんか。 852 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 22:42:13.44 ] おっと、専ブラの仕様で 名前欄になぜか834と 別の人のレス番が出てしまった。 853 名前：１３２人目の素数さん mailto:sage [2011/09/09(金) 23:19:59.01 ] （　´_ゝ`）ﾌｰﾝ 854 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 03:51:58.56 ] 本人登場か 855 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 05:44:18.79 ] >>850 両方あわせて「等号公理」と呼ぶ流儀も標準的かと 856 名前：１３２人目の素数さん [2011/09/10(土) 07:44:18.11 ] T |― A　かつ　T |― B　⇒　T |― A∧B ウシュカヴィッツの公理系で証明よろ。 857 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 08:31:26.08 ] >>855 そうなのか？「等号に関する公理」と呼んで総称するならわかるが。 >>856 ぐぐっても何にも出てこん。解説よろ。 858 名前：１３２人目の素数さん [2011/09/10(土) 09:00:00.06 ] >>857 ウシュカヴィッツの公理は、 P1.x→(y→x) P2.(x→(y→z))→((x→y)→(x→z)) P3.(¬x→¬y)→(y→x) にMPを追加したものですね。>>856はたった今自己解決しましたが。 補題として、|― x→xが出る。 |― A、|― B　と仮定する。 P2から、((A→¬B)→(A→¬B))→(((A→¬B)→A)→((A→¬B)→¬B)) 補題から、(A→¬B)→(A→¬B) よってMPによって、((A→¬B)→A)→((A→¬B)→¬B)-----�@。 一方P1から、A→((A→¬B)→A) だが、仮定より、(A→¬B)→A-----�A。 そして�@と�AについてMPを使えば、(A→¬B)→¬B。 P3を使って対偶をとると、B→¬(A→¬B) だが、 仮定によって¬(A→¬B)。 ¬(A→¬B)≡¬(¬A∨¬B)≡(A∧B) よって　|― A∧B。（＾＾； 859 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 09:10:14.50 ] いつの間にか練習問題レベルの話題になっているが、もともとは>>821が最初だったよな。 それに応えて>>822がHerbrandの定理のことにちょっと言及してるけど、実は何の関連が あるのかさっぱりだった。 Herbrandの定理とどう繋がるのか誰か教えてくれない？ 860 名前：１３２人目の素数さん [2011/09/10(土) 09:24:16.99 ] >>821の言語では定数(項)として0,1をもち、 T |― ∃xA(x)　⇒　T |― A(0)∨A(1)　が成り立つ。 エルブランの定理は上記を一般化して、 言語Lの理論Tで、T |― ∃xA(x)　ならば、 Lの有限個の項t0,t1,...,tnについて、 T |― A(t0)∨A(t1)∨...∨A(tn)。 このとき必ず T |― A(t) (項tが1個だけ)となる保証はない。 そのため、完全性定理の証明でヘンキン定数を わざわざ付け加える必要があるということが言いたかったのでは？ 861 名前：859 mailto:sage [2011/09/10(土) 09:34:09.72 ] >>860 おお、Herbrandの定理とかConsistencyTheorem(Hilbert-Ackermann)とか 何を言わんとしているのか良くわからなかったんだけど、少し見えてきた。 ありがとうございます。 862 名前：１３２人目の素数さん [2011/09/10(土) 11:33:43.67 ] >>842 (0=0∧σ)∨(1=1∧¬σ) ----------------------------------------------- (0＝0∧σ)∨(0＝1∧¬σ)∨(1＝0∧σ)∨(1＝1∧¬σ) これの詳細よろ（＾＾； 863 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 18:10:34.74 ] >>862 直接 A ------- M∨A が認められてる体系なら A∨B ------------- A∨M∨N∨B は明らかだけど、あんたの体系ではどうなのさ？ 864 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 19:14:46.04 ] >>857 www.cs.toronto.edu/~sacook/csc2429h.02/notes/page25.ps 865 名前：１３２人目の素数さん [2011/09/10(土) 19:45:08.66 ] >>863 そうでしたね（＾＾； 866 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 19:46:03.28 ] >>840 嘘付け スコーレム閉包とっても元の体系の保存的拡大にしかならん 867 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 20:30:52.56 ] >ZFにスコーレム関数を付け加えると をどう解釈するかですな。 スコーレム化のことなのか、公理図式にスコーレム関数が現れる論理式を許すのか。 868 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 20:46:42.43 ] >>866 前原のイプシロン定理のことをいっているのなら，それは公理のない場合だけ． ＺＦなら当然，選択公理が導かれる．それについて間違った論文もすでに 有名なジャーナルから出版されている， 869 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 21:31:14.95 ] その間違った論文の書誌情報ｋｗｓｋ 870 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 22:21:58.66 ] ZFのスコーレム化では、スコーレム関数は分出公理や置換公理の論理式には現れてはいけないわけだが どうやって（スコーレム関数なしの言語で形式化された）選択公理を導くのか説明キボンヌ >>836の >∀x∃yφ(x,y)から∀xφ(x,f(x))が導ける訳なので っていうfは、集合としてこのｆのグラフは定義できないんじゃね？ (適当な集合サイズの定義域に限定しても。) {<x,y>｜y＝f(x)}ってスコーレム化前の言語では定義不可能だから 分出公理の適用外だと思うんだけど。 871 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 22:37:47.84 ] >>868は「当然」と言っているけど確かにどう当然なのか分からんな 872 名前：１３２人目の素数さん mailto:sage [2011/09/10(土) 23:53:14.71 ] 868はもう寝ちまったのか それともいま焦って本をひっくりかえしているのか 873 名前：１３２人目の素数さん mailto:sage [2011/09/11(日) 00:21:38.14 ] 非論理的公理のない体系をスコーレム化しても意味ないような。 874 名前：１３２人目の素数さん mailto:sage [2011/09/11(日) 00:48:12.49 ] >>868は>>867を読んでから書いているはずだから そんな単純な間違いはしていないと思うのだが、、、 875 名前：１３２人目の素数さん mailto:sage [2011/09/11(日) 22:39:39.50 ] 結局 ZF^{sk} は ZFC を含むの？ 876 名前：１３２人目の素数さん mailto:sage [2011/09/11(日) 23:51:35.20 ] 868は直前の>>867を読んでも理解できずにそのまんまの間違いをしたんだろ かいわいそだからこれ以上追及すんなや 877 名前：１３２人目の素数さん mailto:sage [2011/09/12(月) 06:52:44.07 ] 870に書いてある分出公理の論理式に、新たな論理式を加えなければ保存 となることはよく知られている。だから「前原のイプシロン定理」に 触れているんじゃないでしょうか？ 878 名前：１３２人目の素数さん mailto:sage [2011/09/12(月) 15:31:05.42 ] じゃあ>>868は>>866に対して「前原のイプシロン定理」を持ち出して何を言いたかった？ 879 名前：１３２人目の素数さん mailto:sage [2011/09/13(火) 00:51:41.52 ] >>877 分出公理だけが問題か？置換公理に加えても保存性は崩れない？ 880 名前：１３２人目の素数さん mailto:sage [2011/09/13(火) 03:07:08.26 ] 868のいう間違った論文って868が間違ってるとおもってるってだけじゃね？ 881 名前：１３２人目の素数さん mailto:sage [2011/09/13(火) 07:23:27.63 ] >>878 plato.stanford.edu/entries/epsilon-calculus/ に Hilbert の Second epsilon theorem: Suppose Γ ∪ {A} is a set of formulae not involving the epsilon symbol. If A is derivable from Γ in the epsilon calculus, then A is derivable from Γ in predicate logic. というのがあります。 Maehara showed how to prove the second epsilon theorem using cut elimination, and then strengthened the theorem to include the schema of extensionality, in って書いてあります。ですからそのことではないでしょうか？ 間違った論文のことはわかりませんが、、、。>>878 plato.stanford.edu/entries/epsilon-calculus/ に Hilbert の Second epsilon theorem: Suppose Γ ∪ {A} is a set of formulae not involving the epsilon symbol. If A is derivable from Γ in the epsilon calculus, then A is derivable from Γ in predicate logic. というのがあります。 Maehara showed how to prove the second epsilon theorem using cut elimination, and then strengthened the theorem to include the schema of extensionality, in って書いてあります。ですからそのことではないでしょうか？ 間違った論文のことはわかりませんが、、、。 >>879 置換公理というのが何をさしているのかわかりませんが、Zermelo の公理系で 分出公理を置換公理で置き換えたのが ZFC だから、その場合の置換公理は、他 の公理も使えば分出公理より強いので、何をいっているのかわかりません。 そうでないのなら、上記の URL で調べてみては、、、。 882 名前：１３２人目の素数さん mailto:sage [2011/09/13(火) 13:44:44.06 ] >>881 あのね、置換公理の標準的な定式化には二つあってね。 強置換公理と呼ばれる方は分出公理を導くので「Zermelo集合論で分出公理を置換公理で置き換えたのが ZF」と言える。 もう一つの定式化では分出公理を導かないので「Zermelo集合論に置換公理を加えたのが ZF」となる。 >>879の書き方を見て、後者の意味だと読み取れないかな？ 置換公理の定式化を一つしか知らないようだと、スタンフォードの事典なんて読むのはまだ早いと思うよ。 883 名前：１３２人目の素数さん mailto:sage [2011/09/14(水) 02:38:54.17 ] 痴漢公理 884 名前：１３２人目の素数さん mailto:sage [2011/09/15(木) 04:07:41.45 ] 結局、痴漢公理にだけスコーレム関数の出現を許した場合、ZFの保存拡大になるの？ 885 名前：１３２人目の素数さん mailto:sage [2011/09/15(木) 05:27:34.10 ] それより間違った論文というのを見てみたい 886 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 01:38:22.04 ] 数学木曽論を学ぶのにお勧めの大学はどこでしょう？ 高校数学の論理と集合って単元にはまってしまいまして。 887 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 01:42:55.66 ] 国内なら東北大学か神戸大学では。 sites.google.com/site/sendailogichomepage/ kurt.cla.kobe-u.ac.jp/arai-p.html 888 名前：１３２人目の素数さん [2011/09/16(金) 03:19:38.43 ] 京大文学部には林晋さんがいるね 889 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 03:53:57.69 ] 林さんは既に木曾論なんてやってないだろ 890 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 03:54:35.88 ] じゃあ僕がやるお お勧めの教科書教えてくれお 891 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 05:10:35.00 ] >>886 ＞高校数学の論理と集合って単元にはまってしまいまして それだけで基礎論を大学選びの基準にしてしまうのはどうかと思いますよ。 どこでもいいから数学科に進学して学部の4年間ゆっくり考えるのが良いかと。 数学の基礎体力さえあれば基礎論なんて大学院から始めても遅くないですし。 892 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 11:24:11.17 ] > どこでもいいから いやいやw サイコロ降るわけにもいかないから、基準の一つを得ようとしただけでしょ。 893 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 13:28:10.15 ] どうでもいいが、次にスレ立てるときには「木曽論」でどうかね。 基礎的な数学の質問避けにはいいかもしれん。 894 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 14:09:51.20 ] >>886 数学者は人格に難のある人が多い。 (じっさいこのスレの上の方でとある先生の常識の有無が話題になってた) そして木曽論は研究者の数が少ないので その数少ない研究者に嫌われると他の選択肢がほとんどない。 大学選びというか先生選びは慎重にね。 895 名前：１３２人目の素数さん [2011/09/16(金) 18:22:19.84 ] >>893 その案に1票！ 896 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 18:38:31.42 ] いいね、木曽論をNGWORDにすればいいってことだし。 897 名前：１３２人目の素数さん [2011/09/16(金) 19:59:46.90 ] 木曽よりも木曾のが良いだろう 數樂木曾論 898 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 20:37:54.30 ] 変にスレ名をいじるよりも普通に基礎論はスレ名から排除して数理論理学のスレでいいだろ むしろ実態はそっちの方に近いし 899 名前：１３２人目の素数さん [2011/09/16(金) 21:02:17.99 ] 集合論・数理論理学　その９ はどうだろう？ 数理論理学に含まれるという考えもあるかもしれないが、 集合論スレが全くないので。 數樂木曾論　其之九 も悪くないけど。 900 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 21:35:42.01 ] 集合論だと素朴集合論もあるので数理論理学の範囲外になることもある 901 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 22:00:42.53 ] Silver の特異基数の定理は素朴集合論の範囲なんですか？ 902 名前：１３２人目の素数さん [2011/09/16(金) 22:15:16.10 ] 公理的集合論・数理論理学その９ で良いんじゃないの。 903 名前：１３２人目の素数さん mailto:sage [2011/09/16(金) 22:41:14.83 ] そのへんを日本じゃ数学基礎論て呼んでるんだから、今のままでいいだろ。 904 名前：１３２人目の素数さん [2011/09/16(金) 23:03:06.68 ] それだと数学の基礎と間違えるから。 905 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 03:17:45.21 ] 数学木曾論・数理論理学　その９ に決まり！ 906 名前：１３２人目の素数さん [2011/09/17(土) 06:15:51.69 ] 數學木曾論・數理論理學　其之九 くらいに韜晦した方がいいだろ、素人フィルターになるし。 907 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 08:51:05.23 ] なんという閉鎖的な思考 908 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 17:29:04.91 ] 「数学の基礎的な質問」みたいなのには閉鎖的にしたいけれど、 ロジックに興味のある高校生・専門外の人にはオープンにしたいよね。 玄人には「数理論理学」が好まれているようだけど、 高校生や専門外には「基礎論」の方がまだまだ通用する気がする。 とすると>>905案くらいが妥当かと。 909 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 17:36:28.85 ] どうせ基礎的な質問だったら喜んで嫌みったらしくいじめるくせに。 910 名前：886 mailto:sage [2011/09/17(土) 17:48:25.97 ] 色々とありがとうございました。 911 名前：１３２人目の素数さん [2011/09/17(土) 18:47:09.64 ] それにしてもなぜ木曾なんだか。 802 ：１３２人目の素数さん ：sage ：2011/09/17(土) 16:06:23.55 結局、基礎論にも圏論にも特に意味は無い、ということ？ 803 ：１３２人目の素数さん ：sage ：2011/09/17(土) 18:11:32.37 圏論には意味あると思うけど基礎論は無駄だね 912 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 19:01:55.51 ] 別に起訴でも木祖でもなんでもいいんだが せっかく高校生君>>886が興味持って来てくれたんだし それを記念して木曾でいいじゃないの 913 名前：１３２人目の素数さん [2011/09/17(土) 19:26:02.15 ] スレタイ検索で来る人も多いのだから「基礎論」の方が良い ジャニーズ板はよそ者が来ないようにするために判りにくいスレタイにしていて、スレタイ一覧がカオスになっている 914 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 19:28:27.28 ] 数学者がジャニーズ板とか見るんだw 915 名前：１３２人目の素数さん [2011/09/17(土) 19:49:41.44 ] 俺は数学者でなく 数学マニアだが半角2次元も良く見るよ 916 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 19:49:55.65 ] んじゃまた喜んで嫌みったらしくいじめるか 917 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 22:36:59.00 ] 数学基礎論は英語にしたら？ 数理論理学 Foundations of Mathematics その9 とか。 918 名前：１３２人目の素数さん [2011/09/17(土) 23:10:11.57 ] 英語にすると文字数増えてスレタイが読み難くなるんだよね・・・ シンプルに 數學木曾論・數理邏輯學　那個九 で良いと思うけど。 919 名前：１３２人目の素数さん mailto:sage [2011/09/17(土) 23:57:05.75 ] どこがシンプル？ 920 名前：１３２人目の素数さん [2011/09/18(日) 02:18:38.59 ] >>909に同意 下らん議論が多いなwww 921 名前：M_SHIRAISHI mailto:eurms@hb.tp1.jp [2011/09/23(金) 16:17:45.20 ] あろうことか、20世紀の論理学の標準理論は間違っていたのであった。 しかも、肝腎かなめのところで間違っていたのである。 そこで、論理法則を表わしていると信じられていたものは、悉く、 ニセモノか、 又は、ナンセンスなものである。 www.age.ne.jp/x/eurms/Ronri_Kaikaku.html 922 名前：１３２人目の素数さん mailto:sage [2011/09/23(金) 23:07:10.87 ] もう飽きた 923 名前：１３２人目の素数さん [2011/09/23(金) 23:38:07.24 ] Booleの『論理の数学的分析』面白いな 924 名前：１３２人目の素数さん [2011/09/24(土) 00:03:14.54 ] んなマニアックな本よんどランで 最先端の論文追わんか 925 名前：１３２人目の素数さん mailto:sage [2011/09/24(土) 15:10:54.96 ] いっそ、数学糞論にすれば。 糞好き以外来なくなるｗ 926 名前：１３２人目の素数さん mailto:sage [2011/09/24(土) 15:15:01.86 ] >>886 ＞数学木曽論を学ぶのにお勧めの大学はどこでしょう？ ＞高校数学の論理と集合って単元にはまってしまいまして。 日本の大学の学部では大したことは教えないから どこにいっても大して変わりませんよ。 927 名前：１３２人目の素数さん mailto:sage [2011/09/24(土) 15:16:53.20 ] >>892 ＞基準の一つを得ようとしただけでしょ。 試験の成績で十分でしょう。 東大に入れるほど優秀、ってわけじゃないでしょｗ 928 名前：１３２人目の素数さん mailto:sage [2011/09/24(土) 15:19:09.79 ] >>893 ＞基礎的な数学の質問避け 本気なら、決して「数学基礎論」と書かないことだな。 >>903みたいに ＞そのへんを日本じゃ数学基礎論て呼んでるんだから なんてバカいう奴がいたら、鎮静剤で眠らせろｗ 929 名前：１３２人目の素数さん mailto:sage [2011/09/24(土) 15:21:56.66 ] そもそも、集合論と数理論理学を一緒くたにするのは 整数論と代数幾何学を一緒くたにするくらいセンスがない。 930 名前：↑ mailto:sage [2011/09/25(日) 18:31:11.35 ] 同感！ 931 名前：１３２人目の素数さん mailto:sage [2011/09/25(日) 19:57:40.50 ] 整数論と代数幾何を一緒くたにすると数論幾何になって、それはそれでいい感じなんだけど。 932 名前：１３２人目の素数さん mailto:sage [2011/09/25(日) 21:39:00.02 ] ロジックの日本語は数理論理学じゃないの？ 集合論は英語では明らかに logic に含まれるけど。 933 名前：１３２人目の素数さん mailto:sage [2011/09/25(日) 22:56:54.73 ] naiveとaxiomaticは全く扱いも分野も違う どこで英語をならったのか知らないけど寝言は寝てから言おうね 934 名前：１３２人目の素数さん mailto:sage [2011/09/26(月) 00:01:36.25 ] アメリカでもイギリスでもロジックと言えば 現代的なつまり公理的な集合論は確実に含まれるよ。 935 名前：１３２人目の素数さん mailto:sage [2011/09/26(月) 00:07:18.35 ] そう、だから>>932は「明らかに」舌足らずなんだよ 936 名前：１３２人目の素数さん mailto:sage [2011/09/26(月) 01:04:15.57 ] どうでもいいけど数理論理学はmathematical logicな。 単にlogicって言うのなら学問的には古典論理から現代論理まで含めた論理学一般のことを指す。 937 名前：１３２人目の素数さん [2011/09/26(月) 01:19:55.84 ] >>936 数学を語る文脈で語ってたら単にlogicでいいでしょう。 紛れそうなときだけ使い分ければよい。 938 名前：１３２人目の素数さん [2011/09/26(月) 07:46:41.77 ] 本を読まなくてもスレに書き込めるようにテンプレ作ってみた。 数理論理学入門 ●命題論理 命題論理記号：¬,∧,∨,→,⊥ 原子命題：a,b,c...　※a＝「1+1＝2」,b＝「2は素数」など。 原始命題は命題。a,bが命題のとき¬a,a∧b,a∨b,a→bは命題。 真理値関数V：命題aが真ならf(a)＝1,偽ならf(a)＝0とする。 aが原子命題のときV(a)＝f(a) V(¬a)＝1⇔V(a)＝0 V(a∧b)＝1⇔V(a)＝1かつV(b)＝1 V(a∨b)＝1⇔V(a)＝1またはV(b)＝1 V(a→b)＝1⇔V(a)＝0またはV(b)＝1 Vは一意に存在。トートロジーとは任意のVでV(a)=1となる命題a( |＝ a と書く)。 |＝ a→(b→a) |＝ (a→(b→c))→((a→b)→(a→c)) |＝ (¬b→¬a)→(a→b) 上の3つのトートロジーを公理と呼ぶ、まとめて理論と呼ぶ(集合Tや{a}と書く)。 理論Tのすべての公理を1にする関数Vが命題pを1にすることを T |＝ p と書く。 公理は定理。a→bとaが定理ならbも定理。(MP,三段論法,cut等と呼ぶ) aが定理ならaは証明可能( |― a と書く)。 有名なトートロジー:|＝ ¬a→(a→b),|＝ ¬¬a→a 演繹定理：T∪{a} |― b　⇔　T |― a→b 命題aとbで |― a→b∧b→aならaをbに書換え可能でa≡bと書く。 a→b≡¬a∨b,¬a∨¬b≡¬(a∧b),⊥≡¬(a→a)など。 T |― ⊥ のときTは矛盾すると言う、そうでないなら無矛盾。 T∪{¬a} |― ⊥ ⇔ T |― a 。 命題論理の完全性定理：|＝ a　⇔　|― a 命題論理のコンパクト性定理：理論Tの任意の部分集合Aの命題がトートロジー⇒Tの命題はトートロジー。 939 名前：１３２人目の素数さん mailto:sage [2011/09/26(月) 11:09:53.61 ] コンパクト性で「有限」いらないの？ 940 名前：官軍 mailto:sage [2011/09/26(月) 12:57:19.35 ] >>938 ご苦労様。　でも。全部、ナンセンスか「完全に間違うとる」。(^o^) 941 名前：１３２人目の素数さん mailto:sage [2011/09/26(月) 15:19:41.79 ] 数理論理学じゃ長すぎて言いにくいから数論と呼ぼう！！ 942 名前：１３２人目の素数さん mailto:sage [2011/09/27(火) 13:09:11.16 ] スーロン 943 名前：１３２人目の素数さん mailto:sage [2011/09/28(水) 00:24:49.75 ] しゅごく初歩的な質問ですが、命題論理や述語論理の ¬,∧,∨,→,∀,∃ などといったいろいろな記号は あくまで意味を持たない「ただの記号」なのですか？ 944 名前：↑ mailto:sage [2011/09/28(水) 07:19:19.64 ] んなこたぁない。 945 名前：１３２人目の素数さん [2011/09/28(水) 15:51:14.49 ] Booleの「論理の数学的分析」は翻訳されてるのに「思考の法則」はされてないのは 何故なんだ 翻訳するなら後者の方が良い気がするんだがな 946 名前：M_SHIRAISHI mailto:eurms@hb.tp1.jp [2011/09/28(水) 17:09:06.71 ] >>945 共立出版社で翻訳出版される予定らしい。 # Boole は、下層階級の生まれで、出世する為には、ギリシア語や ラテン語をマスターしなければならないと信じていた。 その為、Booleの書いた本（英語）を読むには、ギリシア語や ラテン語の知識を要する。　(^o^) 947 名前：１３２人目の素数さん [2011/09/28(水) 17:52:38.45 ] ええ？ 948 名前：１３２人目の素数さん mailto:sage [2011/09/28(水) 20:28:15.90 ] 原著を読んだことのある奴ならわかるがそんなこたない。 949 名前：１３２人目の素数さん [2011/09/29(木) 01:05:59.29 ] >>946　ソースは？ 950 名前：１３２人目の素数さん mailto:sage [2011/09/29(木) 12:08:11.95 ] >>943 記号そのものには意味はない。 代わりに机や椅子の記号でも良い。 951 名前：１３２人目の素数さん mailto:sage [2011/09/29(木) 17:11:36.17 ] >>950 ありがとうございました。 952 名前：１３２人目の素数さん [2011/09/29(木) 19:01:35.75 ] 歴史的には形式主義と呼ばれる立場と呼ばれる。 953 名前：１３２人目の素数さん mailto:sage [2011/09/29(木) 22:20:58.69 ] ああ眠い。基地外ばっかりじゃんここ。 954 名前：１３２人目の素数さん [2011/09/29(木) 23:12:45.53 ] ２ちゃんは馬鹿の巣窟。 これ常識。 955 名前：１３２人目の素数さん mailto:sage [2011/09/29(木) 23:48:44.64 ] >>946　共立に確認したら予定は無いと言われたぞ糞が。死ね 956 名前：官軍（中尉）(^o^) mailto:sage [2011/09/30(金) 03:16:11.01 ] >>955 ：１３２人目の素数さん：2011/09/29(木) 23:48:44.64 >>946　共立に確認したら予定は無いと言われたぞ糞が。死ね 講座「数学の歴史」のなかで、ブールの「思考の法則」ものっていた。 ブールの英語はむずかしいんで諦めたのかな。　(^o^)　(^o^)　(^o^) # Dover出版社から、リプリント版がでているよ。 957 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 11:50:07.34 ] リプリント版のことなど既知だ 訳が有るかが問題なんだよ糞コテ死ね 958 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 12:34:01.79 ] 誰だよこんなスレ立てたの 數學木曾論・數理邏輯學　その9 kamome.2ch.net/test/read.cgi/math/1317308295/ 959 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 12:38:00.96 ] クヌース・ベンディックスの完備化アルゴリズムをお勉強したい。 完全な証明求む。 オススメの項書き換え系の教科書は何？ 960 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 16:55:52.48 ] www.math.princeton.edu/~nelson/books/elem.pdf ペアノ算術の矛盾を示したとかいう話らしいんだが、分かる人いる？ 961 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 18:03:40.95 ] >>959 なぜこの板に… "Term Rewriting and All That" www.amazon.co.jp/Term-Rewriting-That-Franz-Baader/dp/0521779200 この板的にはこっちがいいかも。 Gr bner Bases: A Computational Approach to Commutative Algebra www.amazon.com/exec/obidos/ASIN/0387979719/ 962 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 19:37:43.43 ] >>961 二番目のやつ注文しますた。足らん場合一番目行きます。アリ。 963 名前：961 mailto:sage [2011/09/30(金) 20:30:15.82 ] まじでw KB完備化は間接的にしか扱ってないから、 www.risc.jku.at/publications/download/risc_3528/paper_48.pdf とか、KnuthのtAoCPも読んどいてね。 964 名前：１３２人目の素数さん mailto:sage [2011/09/30(金) 21:36:16.54 ] KBもグレブナー基底も互除法のわりと 素直な一般化というか高次元化だよね。 965 名前：１３２人目の素数さん mailto:sage [2011/10/01(土) 10:02:22.15 ] >>960 Taoの反論で終了してる

---

---

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

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