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

1 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 19:22:39 ] 立てます。 232 名前：１３２人目の素数さん mailto:sage [2007/03/26(月) 14:37:28 ] 20世紀の論理学は、あまりゴツくはないような。 どちらかというと読み物風というスタイルな気がする。 233 名前：１３２人目の素数さん mailto:sage [2007/03/26(月) 16:07:18 ] >>232 とはいえ、”４分冊”で思いつくのは>>77だけ。 228にはゴツいんだろう。他にどんな本を読んだか知らないけど 234 名前：１３２人目の素数さん mailto:sage [2007/03/27(火) 10:00:15 ] 「20世紀の論理学」のような内容で、証明もちゃんとのせてくれているような本ってないですか？ もちろんそうすると辞書みたいに分厚くなるだろうし、洋書しかないんでしょうけど、どなたか わかるかた、教えて著。 235 名前：１３２人目の素数さん mailto:sage [2007/03/29(木) 19:00:14 ] 日本語の本なら「数学基礎論入門」とか「入門数学基礎論」とか 236 名前：１３２人目の素数さん mailto:sage [2007/03/30(金) 15:40:47 ] 日本語の本なら「数理論理学」とか「数理論理学」とか「数理論理学」とか 「公理的集合論」とか「公理論的集合論」とか「公理論的集合論」とか 「証明論入門」とか「現代集合論入門」とか 237 名前：１３２人目の素数さん mailto:sage [2007/03/31(土) 01:01:53 ] 数学基礎論入門は2種類以上あるし 数理論理学も4種類上あるみたいだけどね 238 名前：１３２人目の素数さん mailto:sage [2007/03/31(土) 19:45:12 ] 前原昭二のは最近復刊されたらしい。 239 名前：１３２人目の素数さん mailto:sage [2007/03/31(土) 22:16:14 ] 「前原昭二の」って「数学基礎論入門」かな？ それとも「数理論理学」かな。 たぶん復刊されたというから前者だと思うけど 数学基礎論入門は少なくとも数年前には単行本化されてたし 今でも手に入ると思うけどね >>234 「20世紀の論理学」には割ときちんと証明が載ってる気がするけど 240 名前：１３２人目の素数さん mailto:sage [2007/04/01(日) 00:05:13 ] 難波完爾「集合論」の最初の数ページに カテゴリーがどうのこうのとか書いてあるけど 最初読んだときは良く意味が分からなかった。 最近哲学系の本を読んでやっとcategorial grammerとか 型理論とかと関係があるんだろうなあ、と想像がつくようになった。 モダン過ぎて初学者には全然意味が分からないと思うんだけどなあ、あの書き方じゃ。 241 名前：１３２人目の素数さん mailto:sage [2007/04/01(日) 04:32:00 ] >>240 1975年当時はもっとモダンに見えただろうなあ、 難波さんの翻訳した本か何かにそれについての論考があったと思うので、 気が向いたら探してみて。 242 名前：１３２人目の素数さん mailto:sage [2007/04/01(日) 04:59:34 ] Davisの「超準解析」にわざわざ付録として書いたアレとか 数学セミナー増刊「数学基礎論の応用」とか 243 名前：１３２人目の素数さん mailto:sage [2007/04/01(日) 14:22:07 ] このスレの人たちにとっては「超積と超準解析」「圏論の基礎」 「代数幾何学」（ハーツホーン）とかはやっぱりデフォなの？ 244 名前：１３２人目の素数さん mailto:sage [2007/04/02(月) 02:48:49 ] >>241>>242 おお、なんかどうもありがとうございます。 今度図書館に行ったときにでも読んでみます。 245 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 18:42:00 ] 変な質問ですが、{ }が空集合である( ⇔ ∀x[¬(x∈{ })] )ことを用いずに、 「 { }は空集合である または { }は無限集合である 」 を証明することは可能ですか？ 246 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 20:15:13 ] >>245 どういう論理体系でやるのかをはっきりさせないと答えようがないような 247 名前：１３２人目の素数さん mailto:SAGE [2007/04/03(火) 20:19:27 ] えーん、全然知らなかったよ〜 www.technobahn.com/cgi-bin/news/read2?f=200704031617&ref=rss 248 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 20:58:42 ] フィールズ賞を受賞したから著名、みたいな書き方ｗ とか思ってたら連続体仮説を「証明」かｗ 249 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 21:18:42 ] Wikipediaは訃報に関しては仕事が早い。 記事へのリンクがあった www.sfgate.com/cgi-bin/article.cgi?f=/c/a/2007/03/30/BAG8DOUKEG1.DTL www.nytimes.com/2007/04/02/us/02cohen.html?_r=2&oref=slogin&oref=slogin 250 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 21:40:14 ] >>245 { }を特徴付ける公理が何もないなら、ほとんど何も証明できないんでないの？（恒真式なら証明できるけど そんなの意味ないでしょ。） 251 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 23:20:02 ] >>250 空集合の公理は、実は無限下降列の非存在（と他のいくつかの公理）から引き出せる 空集合の存在を認めるのと、無限下降列の存在を認めないのと、どちらがいいのかは哲学 252 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 23:47:44 ] {_}という表現が何を意味してるのか、 どういう風に定義されてるに拠るんじゃないの。 何か{_}に関する性質が前もって与えられてないと証明できるわけ無いじゃん。 定数記号cが∀x¬x∈cを満たすことを cに関する論理式を使わないで証明できるわけが無いのと全く同じで。 naiveな集合論しか知らない人にはそういう見通しが立たないのかもしれないけど。 253 名前：１３２人目の素数さん mailto:sage [2007/04/03(火) 23:56:54 ] フィールズ章を受賞したから著名、ってのは必ずしも間違ってないんじゃないの。 特にロジックの非専門家や一般人にとってはね。 連続体仮説を解決じゃなくて証明とか書いてるのは 記者がわかってないんだろうなあ。 連続体仮説はZFCから証明出来ないことを証明した、と書けば良いのに。 254 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 00:29:20 ] その前のパラグラフではちゃんと独立であることを証明と書いてるのが余計に謎だｗ 255 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 00:44:00 ] こんな顔になってたんだなあ 256 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 07:44:07 ] >>250>>251>>252 やっぱりそうですよね。ありがとうございます。 もう1つ質問があるのですが(また変な質問ですが)、f,g：{1,2,3}→{1,2}を f(1)＝1,f(2)＝2,f(3)＝1 g(x)＝1 (x∈{1,2,3}が奇数のとき),2 (x∈{1,2,3}が偶数のとき) と定義するとき、 (1)「f(1)＝1である」ことを使わずに「f(1)＝1または1＝2」を示すことは可能でしょうか？ (2)「g(1)＝1である」ことを使わずに「g(1)＝1または1＝2」を示すことは可能でしょうか？ 257 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 09:43:41 ] fとgの定義は使って良いの？ だとしたら〜を使わずに、というのは意味不明なんだけど。 何が言いたいの？ 258 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 10:20:04 ] トンデモのにほいがしてきた。 259 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 10:31:25 ] そういえば、コーエンの伝記ってどんなんだっけと思って 久しぶりに「アメリカの数学者たち」を部屋の奥から掘り出した俺 260 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 17:04:13 ] >>257 うーん、何と説明したらいいんだろう… と考えていたら、自分でも質問の意味が分からなくなってきました。 >>256は取り下げます。 261 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 18:25:20 ] ひとつ言えることは、>>256は今の勉強法は即刻とりやめて ちゃんとした先生にちゃんとした授業で教えを受けること。 まだ大学に行ける年齢でないならそれまで我慢すること。 262 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 18:41:55 ] >>256はどの辺がどういう感じに基礎論に関係してくるんだ? 263 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 22:21:23 ] P.コーエンの連続体仮説論文の原書持ってるよ それだけだけどｗ 264 名前：１３２人目の素数さん mailto:sage [2007/04/04(水) 22:57:45 ] 全ページスキャンしてZIPでくれ 265 名前：１３２人目の素数さん mailto:sage [2007/04/05(木) 09:29:53 ] >>263 全頁和訳してdvi/ps/pdfでくれ 266 名前：１３２人目の素数さん mailto:sage [2007/04/05(木) 10:57:23 ] 論文？モノグラフとかじゃなくて？ 267 名前：１３２人目の素数さん [2007/04/05(木) 15:22:43 ] >>245 >{ }が空集合である･･･ことを用いずに、 >「 { }は空集合である または { }は無限集合である 」 >を証明することは可能ですか？ { }が無限集合である可能性なんてあるのか？（ｗ 268 名前：１３２人目の素数さん mailto:sage [2007/04/05(木) 23:46:02 ] >>264-266 持ってるのこれの昔の版↓だよ Set Theory and the Continuum Hypothesis (Paperback) たぶん国会図書館や大学図書館で閲覧可能でしょう 269 名前：１３２人目の素数さん mailto:sage [2007/04/05(木) 23:52:15 ] やっぱGoedelが査読した原論文じゃなくて本じゃん。 国会図書館には洋書の専門書ってあまり無い気がするよ。 大学図書館にはあるだろうけど（原論文もあるだろう）。 訳書のほうは国会図書館にもあるだろうね。 270 名前：１３２人目の素数さん mailto:sage [2007/04/06(金) 02:35:25 ] 糞スレ 271 名前：１３２人目の素数さん mailto:sage [2007/04/07(土) 18:30:53 ] Goedelってだれ？ 272 名前：１３２人目の素数さん mailto:sage [2007/04/07(土) 21:00:25 ] >>271 ja.wikipedia.org/wiki/%C3%96 273 名前：１３２人目の素数さん mailto:sage [2007/04/12(木) 21:02:31 ] 「連続体仮説」が Amazon で4500円だ。 古本屋で 8000円出して買った私は少し悲しい・・ 274 名前：１３２人目の素数さん mailto:sage [2007/04/15(日) 15:11:44 ] そのうち、文庫本になるか再版されるから、買い直せば平均単価がさがるよ。 275 名前：１３２人目の素数さん mailto:sage [2007/04/15(日) 17:44:08 ] されるか？望み薄いと思うけどなー 276 名前：１３２人目の素数さん mailto:sage [2007/04/24(火) 15:22:12 ] 古本屋で売ってAmazonで買い直せば少しは救われるかも 277 名前：１３２人目の素数さん mailto:sage [2007/05/06(日) 21:57:22 ] しばらくぶりに復刊とか新刊ないかな。 278 名前：１３２人目の素数さん mailto:sage [2007/05/11(金) 11:09:01 ] 明倫館にカナモリが出てますな >巨大基数の集合論 販売価格　：　\8,000 > >著者名　：　カナモリ，A．著　淵野昌訳 >出版社　：　シュプリンガー・フェアラーク東京 >発行年度　：　1998年 279 名前：１３２人目の素数さん mailto:sage [2007/05/11(金) 17:12:06 ] >>278 むむ、今確認したらもう無くなってる 漏れの書き込みは役にたったんだろうか？？ 280 名前：１３２人目の素数さん mailto:sage [2007/05/11(金) 19:38:19 ] もう無くなったのか。 欲しかった……。 281 名前：１３２人目の素数さん mailto:sage [2007/05/11(金) 23:18:15 ] >>279 ありがとう 282 名前：１３２人目の素数さん mailto:sage [2007/05/12(土) 08:36:33 ] >>281 もしかして買った人？　なら、書いて良かった　ノ （自分の分のときも結構探したので・・） 283 名前：281 mailto:sage [2007/05/12(土) 10:23:37 ] >>282 ＞もしかして買った人？ そうです。もう半分あきらめていたところでした。本当にありがとうございました。 284 名前：１３２人目の素数さん mailto:sage [2007/05/26(土) 21:08:10 ] だからホントに勉強したいなら洋書で買えと。 285 名前：１３２人目の素数さん [2007/05/26(土) 22:18:56 ] そこまで真面目に勉強する気はないけど、ちょっと興味があるみたいな 286 名前：１３２人目の素数さん mailto:sage [2007/05/28(月) 18:21:14 ] 選択公理を使わずに、ボレル非可測なルベーグ可測集合は作れるのでしょうか？ ボレル非可測なルベーグ可測集合の例を ttp://www-an.acs.i.kyoto-u.ac.jp/~kigami/analysis1-9.pdf で読んだのですが、ルベーグ非可測集合を使って構成しています。しかし、 ルベーグ非可測集合を作るには選択公理が必須だと聞いたことがあります。 287 名前：１３２人目の素数さん mailto:sage [2007/05/31(木) 01:49:37 ] ド素人の質問で申し訳ありませんが… Fermatの最終定理って解決しましたよね。 でもあれっていわゆる集合論の枠組みの中での証明な訳ですよね。 ってことは、コツコツ計算していったら ある日Fermatの最終定理の反例が見つかる (系として集合論が無矛盾でないことが分かる)という可能性は 残っている訳なんですか？ 288 名前：１３２人目の素数さん mailto:sage [2007/05/31(木) 04:04:07 ] > いわゆる集合論の枠組みの中での証明 って何？ 先生がいいと言うまで廊下に立ってなさい。 289 名前：１３２人目の素数さん mailto:sage [2007/05/31(木) 19:57:04 ] ここで質問する人って、ホントに素人かキ印ばっかだね 290 名前：１３２人目の素数さん mailto:sage [2007/05/31(木) 21:02:00 ] >>287 まあ残ってますけど、でもZFより弱い枠組みで証明できるはずですよ。 初等整数論の定理はZFCから証明できる場合は選択公理を使わないで証明できる、 とか、どうやらそういう種類の定理があるようで。（数学セミナー増刊号に載ってた） >>289 まあネットだし2chだし。 291 名前：１３２人目の素数さん [2007/05/31(木) 21:13:12 ] 先日本屋にシグルイの新刊を買いに行ったら、レジ前に「お薦めライトノベル」コーナーが特設されていたのね。 でも、んなもんに興味のない俺は、特に気にすることもなく目当てのものを探して、レジで並んでた。 次は俺の会計だな、と思ってたら後ろから怒号が飛んできて、近くにいた人が一斉にそっちに向いたわけ。 一瞬、誰もしゃべらない状態になって、店内に流れるBGMがよく聞こえたよ。 みんなの視線の先には、それはもう絵に描いたようなｷﾓｦﾀがいた。 ｷﾓｦﾀが店員に文句を言ってるんだろうなってのは状況的にすぐに分かった。 周りの注目も気にせずにそのｷﾓｦﾀはフーフー言いながら手に持った単行本らしきものを店員に向けて 「なんでゼロの使い魔がお薦めコーナーにあるのに、涼宮ハルヒの憂鬱は置いてないんだよ！」と。 涼宮ハルヒの憂鬱と、ゼロの使い魔。名前は知っていたよ。あのキモいアニメ。 あのｷﾓｦﾀが持っていたのは多分、ハルヒかゼロの使い魔のラノベだったんだと思う。 店員らしき男の人が申し訳ありません申し訳ありませんって謝ってたけど、ｷﾓｦﾀはその店員に向かって 何度も、「なぜ涼宮ハルヒを置かないんや。廃れるやろがっ！！」って同じ質問を何回も繰り返してる。 そんで最後には店長を呼べと。 店長が来てからはもう凄かったよ。 お前らは商売をする気があるのか、ただ売れてるものを売ってるだけだ、本当の本の価値を分かっていない・・・と。 みんなドン引き。それでもｷﾓｦﾀのラノベ講義は続く。 会計が回ってきた俺が店員に小さく「大変ですね」と言ったら、困った笑顔を作って 「はは・・お騒がせしてすみません」だって。 会計が終わってしばらくしてからｷﾓｦﾀの演説は終わった。俺は帰っても良かったんだが、『めったに見られるもんじゃねえ！』 と思ってずっと横で見物してた。てか見物人が結構いたよ。 最終的に、そのお薦めライトノベルコーナーに涼宮ハルヒを置くことでｷﾓｦﾀは納得したみたいで、文句を言うだけ言って 何も買わずに悠々と店を出て行った。 残った店内で小学生っぽい男の子が「すげー！あれが生オタクだよ！きめえええええええ！」と友達らしき子とキャイキャイ 292 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 00:28:41 ] 一行目を丸ごと検索にかけるとコピペかどうか分かるなｗ 293 名前：287 mailto:sage [2007/06/01(金) 00:52:14 ] >>290 ご回答ありがとうございます。 ところでZFより弱い枠組みって例えばどんなものなんでしょうか。 294 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 04:28:43 ] www.salvastyle.com/images/collect/brueghel_blind00.jpg 295 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 11:00:14 ] ＞「なんでゼロの使い魔がお薦めコーナーにあるのに、 ＞　涼宮ハルヒの憂鬱は置いてないんだよ！」 ハルヒよりハヒル、という人は大人（ｗ 296 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 11:13:12 ] で、さすがの私も、近所のレンタルビデオ屋で 「なんで、"憂鬱"はあるのに、"消失"は置いてないの？」 とツッコム勇気はない。 もちろん、ハルヒではなくハヒルである。 297 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 11:20:44 ] >>293 Peano算術とか。 まあ表現力が弱いとか、片方がもう片方で解釈可能という意味の弱さね。 集合論ならKPなんていう体系はZFCより弱いはず。 298 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 11:28:57 ] ところで私の知り合いは 「涼宮ハルヒの父親はおそらく京大卒のサラリーマン。 　住所は阪神甲子園近く。 　で、御多分にもれず父親は猛烈なトラキチで、 　娘はそんな父親をアフォだと蔑んでいる。」 と推測しているが、こういう些細なことにこだわるのが真のヲタクだろう。 299 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 13:53:45 ] 枠組みとか気にするより岩波文庫の不完全性定理の 読めるところだけでも読んでおけ 300 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 13:58:18 ] それより数学やれ 猪狩さんの実解析入門 301 名前：１３２人目の素数さん [2007/06/01(金) 15:06:38 ] >>300 別のスレのネタ持ち込むなよ 302 名前：１３２人目の素数さん mailto:sage [2007/06/01(金) 17:31:32 ] いやいや本質を突いたレスだと思うぞｗ ある日反例が見つかるかもとか 下手に説明すりゃどんどん妄想を膨らませるばかりだ 303 名前：１３２人目の素数さん [2007/06/06(水) 10:44:40 ] 不完全性定理に用いる不動点定理を眺めているのですが、内容が込み入っていて、どこか眉唾物の雰囲気を漂わせているのですが、 どこが決定的に怪しいのか、もしくは怪しくないのかわかりません 304 名前：１３２人目の素数さん mailto:sage [2007/06/06(水) 15:51:18 ] 君の心理描写はいらん 305 名前：１３２人目の素数さん mailto:sage [2007/06/07(木) 10:13:19 ] 不動点定理ってことはきちんと整理された現代的な本で勉強してるはずだから 分かりやすいはずなんだけどなあ。 あと第一不完全性定理のほうはrecursively enumerableとかそういう概念を使って 不動点定理を使わずに証明する方法もあるよ。 306 名前：１３２人目の素数さん mailto:sage [2007/06/07(木) 11:39:06 ] >>305 ＞どこか眉唾物の雰囲気を漂わせている まあ、気持ちはわかるよ。 不動点定理で出てくる項の意味を取ろうとしても 操作が完結しなくてできないっていうんでしょ？ でも、それを言われても困るんだよね。 307 名前：１３２人目の素数さん mailto:sage [2007/06/07(木) 16:41:51 ] >>303 ちなみに何ていう本読んでんの？ 308 名前：１３２人目の素数さん [2007/06/10(日) 12:32:59 ] >>286 ZFからは証明できない。 309 名前：１３２人目の素数さん [2007/06/10(日) 12:44:22 ] あっそ 310 名前：１３２人目の素数さん mailto:sage [2007/06/10(日) 12:46:53 ] ZFからは証明できない事を証明できない事を証明できない事を示せ 311 名前：１３２人目の素数さん mailto:sage [2007/06/10(日) 14:46:19 ] ZFからは証明できない事を証明できるならば、 ZFからは証明できない事を証明できない事を証明できない事を証明できる 312 名前：１３２人目の素数さん mailto:sage [2007/06/10(日) 15:01:00 ] □¬□→□¬□¬□¬□ 313 名前：１３２人目の素数さん mailto:sage [2007/06/10(日) 15:02:56 ] p→□◇p 314 名前：１３２人目の素数さん mailto:sage [2007/06/11(月) 21:11:58 ] ボレルとルベーグが一致しない理由ってなんだっけ？ 315 名前：１３２人目の素数さん mailto:sage [2007/06/11(月) 21:37:30 ] 掘られたくなかったからだろう…… 316 名前：１３２人目の素数さん [2007/06/12(火) 01:54:12 ] 数学基礎論って将来性ある？ 317 名前：１３２人目の素数さん mailto:sage [2007/06/13(水) 11:32:05 ] これ以上分野として痩せ細ることはないだろうから 昨今のGoedelプチブームなどと考え合わせても、 あとは発展するだけじゃないかな。 318 名前：１３２人目の素数さん mailto:sage [2007/06/25(月) 14:14:56 ] 998 319 名前：１３２人目の素数さん mailto:sage [2007/07/15(日) 08:03:42 ] >>317 日本での最後の輝きにならないようお互いがんばろう。 320 名前：１３２人目の素数さん mailto:sage [2007/07/15(日) 22:56:42 ] フレーゲ、ラッセルの論理主義とヒルベルトの形式主義との違いが 今一つ分かりません。どなたかご教示ください。 321 名前：１３２人目の素数さん mailto:sage [2007/07/16(月) 02:27:59 ] >>320 ちゃんとした返事はこの後わかっている人に書いてもらうとして 論理主義は集合も数もとにかく数学的対象は論理法則から全て導けるという考えから始まったもの 形式主義は数学に非構成的手法を取り入れる正当性を証明を言わば図形とか機械語の列のような無意味な形として眺めることで構文的組み合わせ的に処理し(無矛盾性証明等)示すことでそのような手法を自由に使う数学を認めようという考え 前者はタイプ理論とか今も活きているし哲学よりの論理学者は最近も新しい結果を出している 後者の公理主義の部分は数学者の標準として活きている 322 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 01:42:11 ] 関連して 集合を定義するときに既に定義されている集合しか使ってはいけないとき集合の定義は可術的、そうでないような定義を非可術的という 論理主義は可術的集合のみ扱い、形式主義は非可術的集合も扱う 323 名前：辰宮鵺星守影踏丸 mailto:sage [2007/07/19(木) 10:52:22 ] 「可術」じゃなくて「可述」的のほうが良いんじゃないかしら。 predicativeの訳語で、predicateが叙述する、断定する、基礎を置くのような意味だから。 田中尚夫の「公理的集合論」でも「確かさを求めて」でもそうなっている。 因みにFregeとRusselの論理主義は結構違う。 FregeとRusselの論理主義について知りたかったら 「言語哲学大全　�T」や「ラッセルのパラドクス―世界を読み換える哲学」などを読むのが良い。 「フレーゲ哲学の最新像」なんていう本もある。 Hilbertの形式主義に関しては記号論理学の入門書を読むのが一番早いと思う。 324 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 11:22:10 ] >>323 すまん。いいもなにも完全な誤変換。訂正サンクス。 325 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 21:11:01 ] すいませんが、非可述的に定義された集合の簡単な例を教えていただけませんか。 326 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 21:51:11 ] 実数の上限とか 327 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 22:05:28 ] 上界をもつ集合の、という意味ね 328 名前：325 mailto:sage [2007/07/19(木) 23:35:54 ] なんか勘違いしてたみたいですいません。非可述的というのを 「aを定義するのに、定義されるべきaの情報を使用している」みたいなもんだと 思っていたら、調べてみると、例えば上限では「集合Sの上限aがa∈Sを満たす」 こともある（Sに最大値がある場合）わけですが、その場合、集合S全体を使って 定義されたaはSよりも型が上になるから、そもそもa∈Sと言うことを考えること ができなくなってしまう、というのがラッセルの困ったところなんでしたっけか？ でも 「aを定義するのに、定義されるべきaの情報を使用している」みたいな話ありま せんでしたっけ？ 329 名前：１３２人目の素数さん mailto:sage [2007/07/19(木) 23:44:24 ] >>328 上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？ 330 名前：１３２人目の素数さん mailto:sage [2007/07/20(金) 10:14:58 ] >>329 ＞上限が定義されていないと上限は定義できないからそんな例になってるんじゃない？ え？そうでしたっけ？aがSの上限であると言うのは、 ∀x(x∈S→a≦x)∧∀b(∀x(x∈S→b≦x)→a≦b) で表せますけど、どこら辺が「上限が定義されていないと上限は定義できない」のか教えたいただけませんか。 というか、むしろ実数の連続性が関係するのかな。 331 名前：辰宮鵺星守影踏丸 mailto:sage [2007/07/20(金) 10:39:15 ] TV局の編集でそういうテツガクっぽいこと言ってるところだけ 取られちゃったんじゃないの？多分。 332 名前：辰宮鵺星守影踏丸 mailto:sage [2007/07/20(金) 10:39:57 ] ごめんなさい、誤爆です 333 名前：辰宮鵺星守影踏丸 mailto:sage [2007/07/20(金) 13:06:45 ] 何らかの対象を、それ自身を含む集合を用いて定義することを、 非可述的に定義すると言います。 論理主義というと良く名前が出てくるのはFrege、Russel、Ramsey、Weylなどですが、 可述性がどうのということを言い出したのは多分Weylです。 彼は、著書の「連続体」(1918 因みにDoverから\2,000くらいで英訳が手に入ります）で 　自分の属するclassを用いることによってしか定義できないような実体は存在しない。 と述べて一種の悪循環原理について述べています。 この原理を採用すると、「一般の」実数の有界集合が必ず上限を持つことを保障出来ません。 従って集合論を元に解析学を展開すると、かなり早い段階で躓いてしまいます。 一方、RusselがPrincipia Mathematica (1910-1913. 2nd edn, 1925-1927)で 展開した型理論 type theory というのは、 型 0 の対象から初めて、型（及び階）の低い対象から順に、 既に定義した対象のみを使って次の対象を定義していく、ということをして Russelの逆理を初めとする各種逆理を防ごうという壮大なプログラムです。 が、実際にPrincipia Mathematicaを通読した人は 実はほとんど居ないんじゃないのとか言われてます。 多分この二つを混同されてるんじゃないかと。 因みに現在ではFefermanらが、Dedekindの連続性の公理を少し変更して 可述的な型理論の体系Wを定義したりし、さらに自然科学に応用されているような 数学のほとんどはWのなかで展開できることを示したりしています。 Fefermanは哲学よりの研究者ではありませんが、可述性という概念も未だに研究されているということらしいです。 >>325 たとえば自らを含まない【或いは. 含む】ような集合すべての集合、とか。 334 名前：330 mailto:sage [2007/07/20(金) 20:47:28 ] >>333 ありがとうございます。 335 名前：１３２人目の素数さん mailto:sage [2007/07/21(土) 07:31:44 ] 可述性がどうのということを言い出したのは1905年あたりのことでなかったかなあ。 336 名前：１３２人目の素数さん mailto:sage [2007/07/22(日) 05:00:57 ] Les mathematiques et la logique Revue de metaphysique et de morale,14(1906)294-317 Poincare 337 名前：１３２人目の素数さん mailto:sage [2007/07/24(火) 22:25:19 ] 定義可能性と計算可能性っておんなじですか? 338 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 09:25:38 ] 違うと思います。 339 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 09:29:14 ] 定義できるけど計算できない実数ってなんですか? 340 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 09:38:48 ] Chaitin数（Ω数）とか。 www.nikkei-bookdirect.com/science/page/magazine/0606/omega.html まあそんなことしなくても、たとえば Peano算術だとかZF集合論だとかの公理系とG¨del numberingを 適当に定義した上で、x∈[0,1]を、無限10進小数で、小数第n桁目が nが論理式のコードでないとき0、 証明可能な論理式のコードであるとき1、 反証可能な論理式のコードであるとき2、 証明も反証も出来ない論理式のコードであるとき3と定義すれば このxは計算可能にはならないはずです。 341 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 10:08:00 ] なるほど。そう言われればあたりまえでした。 計算できないやつを実数化すればいいですね 話は変わりますがチューリングマシンにサイコロをつければ 計算能力は上がるんでしょうか? 342 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 11:05:35 ] >>341 計算できるかできないかなら変わらない。 さいころの目が固定されているなら、単純に全ての場合を模倣できる。 （１がでて１が出た場合、１がでて２が出た場合、、、６がでて６が出た場合） なお、計算量で違いがあるかないかはわからない、 違いのあるなしが証明できれば、賞金付きのP=NP?問題。 343 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 17:27:09 ] サイコロ振ってもでたらめな意味の無い数しか出てこないからね。 適当に振ったらなぜか何か意味がある目が出てくると仮定すれば オラクルとして使えることになるから変わるけど。 344 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 20:03:00 ] >>341 >>342 なるほど。出た目によって幅優先で探索すればよいので 計算可能性には影響しないのですね。 そしてサイコロTMで多項式時間で解ける問題が NPに含まれてるのは明らかと。 ではサイコロの出目が無限にある場合はどうなんでしょうか? 例えばポアソン分布にしたがうとか。 345 名前：１３２人目の素数さん mailto:sage [2007/07/25(水) 21:44:22 ] 違う 346 名前：１３２人目の素数さん mailto:sage [2007/07/26(木) 11:43:51 ] >>344 NDTMのDTMによるシミュレーションにexpのコストがかかるかどうかが問題になってるの、 ついでに言うと、P=NP?問題はオラクルでは決着はつかない。 連続分布のほうは知らない。 347 名前：１３２人目の素数さん mailto:sage [2007/07/26(木) 22:23:38 ] [1 0 0 1 1 0 1] [0 1 0 1 0 1 1] [0 0 1 0 1 1 1] 348 名前：１３２人目の素数さん mailto:sage [2007/07/27(金) 10:51:57 ] やっとゲーデルと20世紀の論理学シリーズが全部完結したねー まだ四巻買ってないけど。 349 名前：１３２人目の素数さん mailto:sage [2007/07/27(金) 18:54:53 ] 中身どうなの？ 350 名前：１３２人目の素数さん [2007/07/31(火) 11:40:51 ] 自然数上の足し算のみの体系は構文論的完全で、その定理の集合は決定可能、その補集合も決定可能、 定理の集合の任意のモデルは補集合の要素を真にしないので、濃度がNと同じなら、真にする論理式の範囲が異なることがない、 すなわち、範疇的である、と思うのですが、正しいでしょうか？ご教授お願いします。 351 名前：１３２人目の素数さん mailto:sage [2007/08/01(水) 11:44:53 ] >>350 いいんじゃない？ でも、その体系だと、「２は平方数ではない」が記述できないと思うよ。 352 名前：１３２人目の素数さん [2007/08/02(木) 00:23:51 ] 大学一年の頃、竹内の証明論の（日本語の）本を読んでいた．Cut-elimination の定理の意味というか、 「なんでそんなことを証明したいのか」がわからなくなって放り出した． あれから十年以上経つけど、この板にお住まいのすごい人たちに、cut-elimination の意味を 教えて欲しいです． 353 名前：１３２人目の素数さん [2007/08/02(木) 00:33:44 ] 微分の増減表を書くとき、矢印の向きとか±とかをどうやって決めてるのかわかりません 354 名前：１３２人目の素数さん mailto:sage [2007/08/02(木) 00:56:44 ] >>353 僕はそのことが基礎論とどう関係があるのかわかりません。 355 名前：１３２人目の素数さん mailto:sage [2007/08/02(木) 01:59:58 ] >>352 cut-elimination → 算術の無矛盾性 356 名前：１３２人目の素数さん mailto:sage [2007/08/02(木) 13:41:23 ] 超準モデルがあるから ω-categorical ではない。 357 名前：１３２人目の素数さん mailto:sage [2007/08/02(木) 21:15:11 ] ＞Cut-elimination 証明可能なＳｅｑｕｅｎｔが、それに含まれる論理式の部分論理式だけを使って証明できるってだけでも 「へぇー、すごいなあ。」と思ったものだが。 358 名前：１３２人目の素数さん [2007/08/03(金) 01:52:04 ] >>357 自分のは、「わざわざややこしいCut規則を導入しておいて、それを除去して 喜んでいる」みたいな印象を受けていました．『Cut 規則がないと、色々な 証明図が長くなりすぎる傾向があるから Cut 規則を導入しておくけど、 証明体系の性質についての議論をするときに、Cut が技術的な障害になる ので、Cut なしの証明図に書き換えてよい事を示しておく(※)』のかなあ、とか 考えましたが、独りで本を読んでいて誰にも相談できなかったので、 消化不良感だけ残りました． やっぱり※という理解は間違ってますかね？ 359 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 06:27:38 ] >>358 その理解でもいいと思います。 あとは、LKから構造規則を抜いて部分構造論理を作ったり、 □の規則を加えて様相論理を作ったりしますが、 その時にcut除去定理が成り立ったり成り立たなかったりします。 そのたびにcutを追加したり外したりするのは厄介だし本質的ではないので、 とりあえずいつもcutを入れておく、というのも１つの理由だと思います。 とりあえず入れておいて、cut除去定理が成り立つか否か、という話にしたほうが、 見通しがよくなります。 あとは、cut規則は論理学でいう三段論法に近い感じなので、 論理学の中で重要な三段論法を外せる、という意味合いもあると思います。 Aと¬Aから空シークエントを導出させて無矛盾性の証明もできたりします。 360 名前：１３２人目の素数さん [2007/08/03(金) 09:09:01 ] 助けてください！ 0.238X+9.85√X = 6000 この解き方を教えてください！お願いします。 361 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 09:14:27 ] >>360 数学基礎論と何の関係が？ 362 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 09:14:35 ] >>360 >>8 363 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 11:58:04 ] Cut除去定理ってCutなしの証明図は具体的には得られないんじゃないの？ そういう記号的な操作がどうのこうのということではなくて、算術の無矛盾性とか さらには数学そのものの無矛盾性とか、そういう雲の上の獲物たちを狙うための道具じゃないのコレって。 364 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 12:36:06 ] >>363 具体的に得る方法を与える証明もあるよ 365 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 14:55:31 ] >>364 cut除去についていうと、確かにcutは除去できるし それによって無矛盾性は証明できるけど、 「確かに除去できる」と主張するための帰納法は、 元の体系からは証明できない。 366 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 15:24:35 ] >>359 「わざわざ導入」でいいの？あくまで、 通常の証明では三段論法はあたりまえのように使うので、形式化した推論・証明を考える際も、三段論法を表現できないとダメ。 だけどLKタイプの体系では、カット以外の推論では（単純に）三段論法を扱えないので、カットを導入する必要がある。 だだカット消去定理が成り立つので、結果的にはカットは導入しなくても証明できる論理式に違いは無いことが分かる。 では？ 367 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 16:37:07 ] >>366 LKって別に普通の証明を記述するための体系ではないよ。 またcutを除去すると証明は甚だ重複の多い読みにくいものになる。 cutの除去はあくまで無矛盾性証明のためのプロセス。 こういうことはロジシャンには常識なんだが、一般人はまず知らない 368 名前：352=358 [2007/08/03(金) 21:13:54 ] >>359, >>363 やはりcut-eliminationは技術的な詳細であって、それを使って 何をするかという事のほうが、少なくとも初学者にとっては大事だったみたいですね． 久しぶりに証明論の本を取り出して眺めてしまいました．15年前に２ちゃんがあったら 、独りで悩まずにすんだろうにな〜． 369 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 21:20:21 ] >>367 ＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。 え？cutを除去したら、無駄のない証明になるんでないの？ 370 名前：１３２人目の素数さん mailto:sage [2007/08/03(金) 22:35:42 ] 無駄がないからといって読みやすいとは限らないよ 371 名前：１３２人目の素数さん [2007/08/04(土) 06:32:14 ] 数学の本の証明で“○○の定理により”と書いてあるところすべてに、 その○○の定理の証明が書いてあったらたまらない。 372 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 09:04:48 ] というか無駄にページ数がかさんで詐欺 373 名前：369 mailto:sage [2007/08/04(土) 09:18:31 ] 何かお互いに言ってることがかみ合ってない気がする。cutのある、完全な証明図と、その証明図からcutを 取り除いた証明図を見比べたら、後者の方が無駄のない証明図になっていると思うんだけど。 >>371が言ってるのはそれとは別でしょ。 374 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 09:24:05 ] 定理の適用は cut ではないと？ 375 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 13:17:38 ] 「無駄の無い」という言葉では曖昧だからもっと明確に表現したほうがよいかと。 ＞またcutを除去すると証明は甚だ重複の多い読みにくいものになる。 というのは、 （実際の数学の証明をLKで書き出すようなことは 現実的にはほとんど無いが、仮に書くとしたら） cutありならまだ何とか読める証明も、cut無しなら重複が多くて読めたものじゃなくなる、 ということでしょ、たぶん。 376 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 13:19:54 ] 定理の適用は cut だろ。 cutless の証明は, 定理を適用しない, ものすごい冗長な証明になっているということだが。 377 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 13:29:05 ] 除去されるんだから忌避される理由でもあるのでせうか cut 378 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 14:29:05 ] >>369 >cutを除去したら、無駄のない証明になるんでないの？ 間違い。曖昧なのではなく明確に間違い。 379 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 14:30:45 ] >>373 君、実際にcut除去したことないだろ。 だからそういう全くのウソを平気で喋れるんだ。 手を動かせないなら口も動かすな。 380 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 16:40:14 ] cut なしの証明については、Girard の本の前書きに少し書いてある． 381 名前：１３２人目の素数さん mailto:sage [2007/08/04(土) 21:45:09 ] cutとか、その意味での三段論法とか言うのは 要するに議論のモジュール化ということだよね。 なんか陳腐な言い方になっちゃうけど。 382 名前：369 mailto:sage [2007/08/05(日) 12:58:02 ] 直観主義論理で、Sequent　Ａ⊃Ｂ⇒¬Ｂ⊃¬Ａの証明のＢに¬¬Ａを採用 すれば、三重否定からの二重否定の除去　⇒¬¬¬Ａ⊃¬Ａが得られると 聞いて素直にSequentで証明したことがある。 　　　Ａ⇒Ａ　　　　　　　　 −−−−−−−−−　　　 ¬Ａ，Ａ⇒　　　　　　　　　　　　　　　　Ａ，Ａ⊃¬¬Ａ⇒¬¬Ａ −−−−−−−−−　　　−−−−−−−−−−−−−−−−−−− 　　　Ａ⇒¬¬Ａ　　　　　　　　¬¬¬Ａ，Ａ⊃¬¬Ａ⇒¬Ａ −−−−−−−−−　　　−−−−−−−−−−−−−−−−−−− 　　　　⇒Ａ⊃¬¬Ａ　　　　　　　　　　　　Ａ⊃¬¬Ａ⇒¬¬¬Ａ⊃¬Ａ −−−−−−−−−−−−−−−−−−−−−−−−−−−−−− 　　　　　　　　　　　⇒¬¬¬Ａ⊃¬Ａ でもそれをCut除去定理の証明の方法でCutを除去していったらすごく簡単 になってびっくりしたんだよね。 　　　　　　Ａ⇒Ａ −−−−−−−−−−−−− 　　¬Ａ，Ａ⇒ −−−−−−−−−−−−− 　　　　　　Ａ⇒¬¬Ａ −−−−−−−−−−−−− ¬¬¬Ａ，Ａ⇒ −−−−−−−−−−−−− 　　¬¬¬Ａ⇒¬Ａ −−−−−−−−−−−−− 　　　　　　　⇒¬¬¬Ａ⊃¬Ａ 私が言いたかったのは具体的に言うとこういうこと。 383 名前：１３２人目の素数さん mailto:sage [2007/08/05(日) 15:48:06 ] >>382 リテラル１個しかないような命題論理の証明１つだけで 「どんな証明もカット除去すれば簡単になるっ！」 と断言されてもなあ。全然論理的じゃないし。 384 名前：369 mailto:sage [2007/08/05(日) 16:30:30 ] >>383 うーむ。それはそうだなあ。しかし、今まで自分が実際にcutを除去したときはいつも簡単になったので そう信じていた。それなら、今まで実際にcutを除去したことある人で、cutを除去したら証明が冗長に なった例を知っている人は教えてくれないかな。というか、そういう例を探してると次第に「cut除去する と証明って簡単になるんだな」と思えてくると思うのだが。 385 名前：１３２人目の素数さん mailto:sage [2007/08/05(日) 17:46:08 ] 計算量の理論に近い人ならいろいろ知っていると思う． cut を除去すると証明の長さが指数関数的に増大する例がありそう． 386 名前：１３２人目の素数さん mailto:sage [2007/08/05(日) 19:52:07 ] >>382 ＡＡにしかみえない 387 名前：１３２人目の素数さん mailto:sage [2007/08/05(日) 20:42:51 ] >>384 命題論理の簡単な証明なら cut 使うまでもないからなあ。 算術での例がこれの appendix にある ttp://www.seitoku.ac.jp/~ikedak/arai.pdf 詳細は追っかけてないけど証明のサイズが論理式の double exponential になるのかな 388 名前：１３２人目の素数さん mailto:sage [2007/08/06(月) 09:06:50 ] >>384 George Boolosの論文 "Don't eliminate cut" を読め。そういえばこれも算術での例。 389 名前：１３２人目の素数さん mailto:sage [2007/08/06(月) 14:17:46 ] >>387 算術の例というわけではないでしょ． 390 名前：１３２人目の素数さん mailto:sage [2007/08/06(月) 14:35:10 ] >>389 算術っていってるのは、自然数論のこと。 勿論、公理まで含めて記述すれば述語論理の命題になるからＯＫ 391 名前：１３２人目の素数さん mailto:sage [2007/08/06(月) 14:45:01 ] > 公理まで含めて記述すれば はじめからそう記述しているよね。 392 名前：１３２人目の素数さん mailto:sage [2007/08/08(水) 01:39:02 ] A sequent calculus without cut-elimination is like a car without engine Jean-Yves Girard 393 名前：１３２人目の素数さん mailto:sage [2007/08/08(水) 10:59:50 ] >>392 ＞A sequent calculus without cut-elimination cut除去なしのsequent計算がエンジンのない車のようだと言ってるの？ 394 名前：１３２人目の素数さん mailto:sage [2007/08/08(水) 11:19:20 ] まあ、cut抜きだと証明図を作るときに 基本的に分解していけばいいので アホでも出来る。 cutを使って簡潔な証明を書くには魔力が必要（ｗ 395 名前：１３２人目の素数さん mailto:sage [2007/08/15(水) 00:03:49 ] 下手な分解はタマネギの無限皮むき（ｗ 396 名前：１３２人目の素数さん [2007/08/16(木) 00:31:37 ] 場違いかもしれないんですが、 −×−＝＋ になるのはどうしてなんでしょうか？ 397 名前：１３２人目の素数さん [2007/08/16(木) 00:38:12 ] 「かもしれない」ではなく完全に場違いです。 398 名前：１３２人目の素数さん mailto:sage [2007/08/18(土) 09:47:47 ] >>395 うまくいく場合は、上手下手に関係なく剥ける。 399 名前：１３２人目の素数さん mailto:sage [2007/08/19(日) 12:52:01 ] >>398 うまくいくシーケントかどうか計算できない。 400 名前：１３２人目の素数さん mailto:sage [2007/08/20(月) 07:36:08 ] >>399 事前の計算は不必要。 うまくいく場合には、方法論に依存しないといっただけ。 もちろん、これは手数を度外視している。 手数をケチるには、オツムを使う必要がある。 401 名前：１３２人目の素数さん mailto:sage [2007/08/24(金) 15:24:36 ] 一般には cut を含む証明図 P に、cut を含まない 証明図 f(P) を対応させる関数 f は、原始帰納的でつか？ 402 名前：１３２人目の素数さん mailto:sage [2007/08/24(金) 15:30:37 ] >>401 P と f(P) が同じ命題の証明って条件は当然付くんだよね 考えたことないが、原始帰納では厳しいんじゃないか？ 403 名前：１３２人目の素数さん mailto:sage [2007/08/24(金) 17:05:49 ] >>402 レスありがとうございます。 はい。同じ命題の証明図です。 帰納的な事は、すぐにわかるのですよ。 （二重帰納法を使いますが） 原始帰納的なことの証明を与えようとして、うまくいかなかったので。 やはり厳しいと予想されますか。 404 名前：１３２人目の素数さん mailto:sage [2007/08/25(土) 01:20:38 ] 一階の述語論理の cut 除去ならば，原始帰納的。 通常の帰納法で証明できることは Gentzen の自然数論の無矛盾性の論文に ちょろっと書いてある． Girard の本では二重帰納法による証明の評価をまじめにやって、原始帰納的な 上限を与えている． 405 名前：１３２人目の素数さん mailto:sage [2007/08/25(土) 20:07:06 ] >>404 ありがとうございます！ 406 名前：１３２人目の素数さん [2007/08/26(日) 12:10:54 ] (1) 大学で集合の講義をしなければならなくなった。 (2) 入門としての集合の講義なのでそんなことを授業で話す必要は 　　まるでないのだけど、教える以上は知っておかなければならないだろうと 　　ZF 等の公理論的なものや歴史を勉強しようと思った。 (3) とりあえず岩波基礎数学の集合と位相を読み、また歴史関係の本を読む。 　　学生時代、そういうことは勉強しなかったこともあり、とても面白い。 (4) ところがその後いろいろと詰めて考えみると「命題」というものが 　　良くわかってないことが判明。 (5) しょうがないので基礎論の教科書を読み出し、見事にはまる。 というわけで現在本業(微分方程式)そっちのけ状態w 質問ですが、 (a) 現在の数学基礎論は多岐にわたるそうですが、現在の研究の進展状況を 　　解説したもの (所謂 survey) はないですか？ (b) 数学基礎論ではどういう学会・研究集会があるんですか？ 　　日本数学会ではあまり活動してないようなんだけど・・・。 知り合いに基礎論関係の人がいません。教えてくださいませ。 407 名前：１３２人目の素数さん [2007/08/26(日) 12:44:31 ] >>406 僕も日本数学会の基礎論分科会に属していますが、 入会以来、なしのつぶて。 研究集会など、何の連絡もありません。 408 名前：406 mailto:sage [2007/08/26(日) 12:55:02 ] >>407 どもども。 僕は分科会は関数方程式論にしか入ってませんが、ここは分科会の人が頑張って メーリングリストで研究集会の連絡をしたり、り欧文論文雑誌などを作ったりなど、 それなりには活動はしてますね。 数学会の基礎論の分科会はあまり活動してないのかな。 日本にも基礎論の人が結構いるみたいだから、どこかで活動はしてるんだと 思ったんだけど、どこで頑張ってるのかなぁ。参加しやすそうな研究集会とかに ぶらりと言って顔を出してみたかったんだけど。 409 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 14:14:30 ] 基礎論の人は和気藹々と群れたりしないんだよね 専攻柄数学観を強固に持っている人が多いし、そこを侵されるのを極端に嫌う傾向が強い。 410 名前：γ ◆WqqSMT0LS6 mailto:sage [2007/08/26(日) 16:51:43 ] test 411 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 17:20:40 ] >>406 ＞「命題」というものが良くわかってないことが判明。 具体的に、命題の何がどう分からないのでしょうか？ ところで、本当に公理的集合論についての講義が学生に必要だと お考えならば、貴方が勉強するよりも、集合論の研究者に講義を 任せるほうがよろしいかと思いますが、いかがでしょうか？ 412 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 17:22:14 ] >>409 部外者は知りもしないで口からデマカセのウソばかりいうね。 413 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 20:42:23 ] >>406 今から本屋に行って 「ゲーデルと２０世紀の論理学」を買ってきて読む →数学基礎論サマーセミナー2007に参加する。 9/4から三日間の間静岡で行われます。8/31が締切なのでお早めに。 集合論に関する比較的入門的な内容の講義をするようです。（forcingとかBoole値モデルとか） 私は基礎論の専門家じゃないですけど、 基礎論の専門家が居る大学では、 それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。 414 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 22:45:28 ] >>413 正しくは、数学基礎論サマースクール、だね。 415 名前：１３２人目の素数さん mailto:sage [2007/08/26(日) 22:56:21 ] >>411 ちょっと書き方がわるかったようですね。 「入門としての集合の講義」というのは一年生の数学の入門としての講義です。 所謂、素朴な集合論のことですね。 ただ、ある程度しっかり話そうとするとこのテーマで話す場合 excuse を 並べることになりますね。そこをいかに話すかが、先生の腕の見せ所となるかと 思いますが、しかし知らないことを話すわけにはいかない。 あーだ、こーだと下手な考えをするまえに、現時点で数学では集合はどのように 理解されてるかをまず知っておこう、というのが勉強を始めた動機です。 > 具体的に、命題の何がどう分からないのでしょうか？ 集合論で使う命題の定義がわからなくなったんですよ。 > ところで、本当に公理的集合論についての講義が学生に必要だと > お考えならば、 普通の数学科の入門としての講義では必要ないと思ってますよ。 私自身も自分の研究では今まで（そして、おそらく今後も）なしで済ませていて、 それで困ったことがありませんから。 > 集合論の研究者に講義を任せるほうがよろしいかと思いますが、いかがでしょうか？ 特論などで本当に講義をしてもらうのであれば、そのほうがいいでしょうね。 というより、そうすべきでしょうね。 416 名前：406=415 [2007/08/26(日) 23:06:41 ] >>413 どうも、どうも。四巻からなる本ですね。 サマースクールですか。 まともに出張の日と重なってしまいました。 しかし、そういう活動はされてるんですね。いいですね。 > 基礎論の専門家が居る大学では、 > それぞれの大学で盛んな分野の研究集会をやったりしてるみたいですよ。 なるほど。いろいろ探してみたら、比較的近くの大学で基礎論の研究グループが あるみたいです。とりあえずはそこをホームページをウォッチしてみますね。 どうもありがとうございました。 417 名前：（´・ω・`） mailto:あげ [2007/08/27(月) 00:05:15 ] 基礎論って今時、若い人でやる人いるんだろうか・・・・ 418 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 00:56:10 ] 数年前から独学で始めたんですが、３０代ももう終わりじゃ、若くないですか？w 419 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 01:09:59 ] 何事も学び始めるのに遅すぎることはない ただ独学は危険 420 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 11:32:14 ] >>415 いえ、書き方は悪くありません。 「入門としての集合の講義」だということは分かっていましたから 公理的集合論のことなど言い訳としても考慮する必要がないだろう という意味で書きました。 さて >> 具体的に、命題の何がどう分からないのでしょうか？ >集合論で使う命題の定義がわからなくなったんですよ。 集合論のどこで使う命題でしょう？ 内包的記法で使う場合のことでしょうか？ それなら｛ｘ｜Ｐ（ｘ）｝と書かずに、すでに集合と分かっているａについて ｛ｘ∈ａ｜Ｐ（ｘ）｝と書いておけばラッセルパラドックスはおきません。 421 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 11:46:33 ] 420で述べたことは、岩波基礎数学の「集合と位相」の冒頭にも書いてあります。 422 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 12:15:54 ] でもそういう解決法はいかにも場当たり的で、 どうして{x; φ(x)}がclassであってもsetではないのかが 学生には十分納得できないと思うけどね。 423 名前：１３２人目の素数さん [2007/08/27(月) 12:19:46 ] >>420 > 公理的集合論のことなど言い訳としても考慮する必要 私、何か言い訳けしましたっけ？ >集合論のどこで使う命題でしょう？ 至るところで使う命題のことですよ。 失礼ですが、命題とは何かここで定義してみていただけますか？ >ラッセルパラドックスはおきません。 そうですね。だから？ 424 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 14:44:00 ] >>423 >私、何か言い訳けしましたっけ？ これから、学生に対してするんでしょう？ excuseを並べるといったじゃないですか。 >>集合論のどこで使う命題でしょう？ >至るところで使う命題のことですよ。 うーん、普通の数学では気にならないのに なぜ、集合論だと問題になるんでしょう。 メタ数学の話をするわけじゃないんでしょ？ >>ラッセルパラドックスはおきません。 >そうですね。だから？ ラッセルパラドックスが気になってるんだろうと 見当つけたんですが、もっと手前でつまづいてるんですか？ 425 名前：１３２人目の素数さん [2007/08/27(月) 14:49:16 ] >>423 さんは、「命題の定義」がわからない ・・と言うようなことをおっしゃったので、 恐らくは、論理式の定義で、躓いているのではないですか？ 426 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 14:50:39 ] >そういう解決法はいかにも場当たり的で 文句ならツェルメロにいってくれよｗ >どうして{x; φ(x)}がclassであってもsetではないのか 古典論理や直観主義論理で考える限りにおいては、 上記のようなsetでないclassはどうしても存在せざるを得ない。 427 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 15:03:16 ] >どうして{x; φ(x)}がclassであってもsetではないのか それこそ、集合論を BG 式に定式化して、 学生に説明する必要があると思う。 428 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 15:39:49 ] >>427 方式の問題ではないんだな。 集合であろうがなかろうが、ＶとＶ→２の間に 一対一対応なんかつけられないんだから。 429 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 19:51:37 ] 煽り屋さん、いなくなりましたか？ 430 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 19:58:14 ] 誰が誰を指して言ってるのかによるな 431 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 20:09:33 ] >>411は当然の疑問 >>415はまだ曖昧 >>420はちょっとピントがずれてるけど煽りではない >>423は煽り 432 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 20:15:08 ] とりあえず、{ X:文字列 | X ∈ {命題} } を日常語に近い高級言語でかきなおしてくれ。 433 名前：１３２人目の素数さん [2007/08/27(月) 20:26:22 ] >>432 要求の意味がわからない。 434 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 20:43:01 ] >>406,415さんは、集合論をやり始めたときは命題がわからなかったけど、>>406を書いた時点では もう解決してるんだよ。そこんとこわかってやれよ。 だから、>>411はかなりトンチンカン。というか、相手を見下した感じがして失礼だと思う。 そもそも>>406の(2)を読めよ。公理的集合論を講義で教えるつもりはないと書いてある。そして、 なぜ、それでも公理的集合論について調べたくなったかも書いてある。 ．．．つーか ちゃんとレス嫁。 435 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 20:46:58 ] >>434 同意 436 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 21:03:13 ] >>433 ある文字列が命題であるとは？ 437 名前：433 mailto:sage [2007/08/27(月) 21:12:27 ] >>436 あー、そういうことね。 確か、文字列の長さに関する帰納法で定義するんじゃなかったかな？ ここに定義を書くのは、めんどくさいけど。 で、日常語に近い高級言語って、何ですか？ 438 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 21:19:18 ] >>426 Zermeloはきちんと正当化のための論文を書いて居るし 現代の数学の哲学の研究者もiterative concept of setなんてことに対して 深く考えたりしているよ setでないclassが存在せざるを得ない、というのは古典論理や直観主義論理からの 論理的帰結でも何でもないんですけどね。 439 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 21:38:36 ] >>437 たとえばプログラミングで 機械が読むためのアセンブリは低級言語、 人が読むためのCなんかは高級言語。 命題の定義を、論理式などではなく、普通の数学の 日常的な言葉で言ってみろ という話。 440 名前：406, 415, 423 mailto:sage [2007/08/27(月) 21:45:10 ] どもども。私のせいでちょっと荒れ模様になってしまったようですね。 申し分けないことです。>>411 あたりで怪しいなとは思ったのですが、 中途半端に相手にしたのが間違いだったようですね。 すいません。 もう私は相手にしないことにします。 そうそう、もう集合の授業は無事終わってますからね。大部昔の話です。 それでは、私の書き込みはこれで終わりにします。 441 名前：441 mailto:sage [2007/08/27(月) 21:55:42 ] √(411) = 21 世紀 442 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 22:49:27 ] > そうそう、もう集合の授業は無事終わってますからね。大部昔の話です。 あーそういう話だったのね。納得した。 >>406 の「はまる」ってのを「さっぱりわからん」って意味にとっちゃって、 (a)(b) とつながんなくておかしいなあって思ってた。 >>411 とは別人ですが、同じ勘違いをしたんじゃないでしょうか。 443 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 23:19:04 ] どうかんがえても、「マイブーム来ちゃった」って意味以外 取りようがなかったと思う。 444 名前：１３２人目の素数さん mailto:sage [2007/08/27(月) 23:44:54 ] まあ分かってみればそうなんだけど、不思議なもんで一度勘違いしちゃうと そっちの解釈で頑張って理解しようとしてしまうんですよ。 445 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 01:17:37 ] 俺も「さっぱりわからん」の意味だと思ってた。 446 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 02:01:52 ] マイブーム来ちゃったから研究集会とか紹介してくれ って流れだろ、常識的に考えて。 447 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 02:13:36 ] ・「命題」が良く分かってないことに気づき、「しょうがないので」基礎論の本を読み出す。 ・専門は微分方程式。 ・本業(微分方程式)そっちのけ状態。 この3つからは、「さっぱり分からん」の流れもまた「常識的」だろ。しかし、後半の(a)(b)とは 繋がらない。で、なぜ繋がらないのか考えようとしても、>>444のような思考のスパイラルに陥る (このスパイラルもまた、常識的に考えてよくあること)。 すなわち、「さっぱり分からん」と解釈して首をひねる人が出るのも、常識的に考えて普通。 448 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 02:15:28 ] >>447 そんなことより、結局「命題」を定義できる奴は此処には折らんの？ 449 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 07:37:25 ] >>434 ＞>>406,415さんは、集合論をやり始めたときは命題がわからなかったけど、 ＞>>406を書いた時点ではもう解決してるんだよ。 ウソでしょ。 >>435 ＞同意 自作自演でしょ。 450 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 07:39:06 ] >>432 ＞{ X:文字列 | X ∈ {命題} } 間違い。"X ∈ {命題}"なんて書き方はない。 顔洗って出直せ。 451 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 07:45:40 ] ＞Zermeloはきちんと正当化のための論文を書いて居る 後からいくら言い訳したって、場当たり的でなくなるわけでもない ＞現代の数学の哲学の研究者も ＞iterative concept of setなんてこと ＞に対して深く考えたりしているよ Boolosの反復的集合観が、classの存在を否定するわけでもない 452 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 08:05:20 ] 場当たり的なのは或る面では集合論自体の性格から来ることだけど、 定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか 必要な公理を統一性もなくただ要請していくようなやり方よりは幾分かはマシだよ。 あくまでいくらかは、だけどね。 ＞Boolosの反復的集合観が、classの存在を否定するわけでもない そりゃ当たり前で、だいたい>>422に書いてあるのは、 classが必ずしも集合とは言えない、ということだけで classが存在しないなんてことは誰も言っていない。 classが存在すると考えても新たな矛盾は起きない、それだけ。 453 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 08:11:54 ] >>406氏と同様の状況に陥った人のページ www.math.h.kyoto-u.ac.jp/~takasaki/edu/logic/ ただしコチラは集合ではなく論理が中心だが。 454 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 08:17:17 ] ＞だいたい>>422に書いてあるのは、 ＞classが必ずしも集合とは言えない、ということだけで ＞classが存在しないなんてことは誰も言っていない。 >>426に書いてあるのも、集合でないclassがあるのは 通常の論理では致し方ない、ということだけだが。 少なくとも対角線論法によって矛盾を導き出せるならば そうならざるを得ない。 455 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 08:19:52 ] ＞場当たり的なのは或る面では集合論自体の性格から来ることだけど、 ＞定式化の仕方を変えることで、少なくとも和集合公理だとか対公理だとか ＞必要な公理を統一性もなくただ要請していくようなやり方よりは ＞幾分かはマシだよ。あくまでいくらかは、だけどね。 その言い分、まるで今井弘一の複ベクトルの正当化と同じだな。 456 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 11:05:17 ] いや私はZermeloが1930年に書いた論文とか Boolosとかが書いたiterationに関する論文のことを言ってるんだけど。 定式化の方法が変わるだけで論理的には既存のZFCと全く同値なんだから 数学的には別に何も問題ない。 複ベクトルってのは知らないけど何か似たようなものなのかな。 Russelのantinomyから論理的にいえるのは、 ∃y.∀z.(z∈y⇔φ(z))という式のφに¬z∈zという論理式を入れると 矛盾しますよ、というだけで、じゃあどういう論理式を排除するべきか、 という判断にはあまり合理的な根拠がない。 Cantorは、¬z∈zを代入するとyが「絶対無限多数」になってしまうから いけないんだとか考えていたけど、そうではなくて¬z∈zという論理式は 型に関するルールが守られていないからだめなのだ、という考えもあり得るし、 またそれと別に、φに否定記号が入っているような論理式を認めないようにしよう、 という定式化の仕方もありうる。 en.wikipedia.org/wiki/Positive_set_theory 実際この集合論でもZFCや、ZFCより強いMorse-Kelleyの集合論を 解釈できる能力を持っているわけで、CantorｙやZermeloの案が採用されたのは 歴史的経緯に過ぎないよ。 457 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 12:02:39 ] いや私は「和集合公理だとか対公理だとか」を 「必要な公理を統一性もなくただ要請していく」 としか認識できない点が、ｉ＾２＝１なる元ｉ を添加する複素数体の構成の仕方をアドホック なものとして嫌う、能登の御隠居と全く同じ 感覚だと述べたまで。 458 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 12:12:35 ] ＞Russelのantinomyから論理的にいえるのは、 ＞∃y.∀z.(z∈y⇔φ(z))という式のφに¬z∈zという論理式を入れると ＞矛盾しますよ、というだけで、じゃあどういう論理式を排除するべきか、 ＞という判断にはあまり合理的な根拠がない。 そもそも、「φに入る論理式を排除する」という 判断それ自体に全く論理的な根拠がない。 459 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 12:17:11 ] ＞Cantorは、¬z∈zを代入すると ＞yが「絶対無限多数」になってしまうから ＞いけないんだとか考えていたけど、 それ以前に、濃度の違い云々というのが 対角線論法の成立から出てきているわけで そもそもその対角線論法自体が成り立たない ような論理を考えるという方策もある。 460 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 12:24:15 ] ＞･･･そうではなくて¬z∈zという論理式は ＞型に関するルールが守られていないからだめなのだ、 ＞という考えもあり得るし、またそれと別に、 ＞φに否定記号が入っているような論理式を認めないようにしよう、 ＞という定式化の仕方もありうる。 ＞en.wikipedia.org/wiki/Positive_set_theory ＞実際この集合論でもZFCや、ZFCより強いMorse-Kelleyの集合論を ＞解釈できる能力を持っているわけで、CantorやZermeloの案が ＞採用されたのは歴史的経緯に過ぎないよ。 そもそも古典論理が採用されたのも歴史的経緯に過ぎない。 461 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:15:57 ] レベルの高いお話の途中すいません。最近次のような述語論理に出会いました。 公理系 F,G,Hは任意の論理式。xは任意の変数。tは任意の項として、 公理 (1)　F→(G→F) (2)　(F→(G→H))→((F→G)→(F→H)) (3)　((¬F)→(¬G))→(G→F) (4)　(∀x(F→G))→((∀xF)→(∀xG)) (5)　F→∀xF　ただし、変数xはFの中に現れない (6)　¬∀x¬(x=t)　ただし、変数xはtの中に現れない (7)　x=t→(P[x]→P[t/x])　P[x]は原子論理式 （P[t/x]は、P[x]にあるどれか1つのxに項tを代入したもの） 推論規則 (8)　FとF→GからGを導く (9)　Fから∀xFを導く 以上です。これは「変数の自由出現に項を代入する」という表記法がないので 技術的に有利なのだそうです。しかし、以上の公理と推論規則から (10)　∀x(x=x) や (11)　Fの中に自由なxがないとき、(∀x(F→G))→(F→∀xG) を導くにはどうすればいいのでしょう？ぐぐってもそれらしいのが 見つからず、また、自分の頭ではわからず困っています。 どなたか教えていただけないでしょうか。あるいはweb上で証明してある ところがあるなら教えていただけないでしょうか。 462 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:26:20 ] >>461 （１０）はexistential instantiation ruleから （１１）はdeduction theoremから導く 463 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:37:51 ] >>457 でも実際Zermeloが最初に集合論の公理的取り扱いに関する論文を 発表したころは誰も見向きもしなかった。 なぜなら少なくとも当時の数学者には、Zermeloの公理系が ただ「必要な公理を統一性もなくただ要請していく」ように見えたからね。 >>458に対しては 矛盾する命題が導かれるんだから論理的根拠はあるでしょ。 少なくともreductio ad absurdumが成り立つ限りにおいては。 古典論理が採用されたのが歴史的経緯に過ぎないという意見は 一般に認められたものでもないと思うけどね。 464 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:45:19 ] >>463 ＞Zermeloの公理系がただ ＞「必要な公理を統一性もなくただ要請していく」 ＞ように見えた のは「当時の数学者」ではなく君だろう。 それとも君はその当時の数学者だったのか？ 465 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:48:28 ] ＞＞どういう論理式を排除するべきか、 ＞＞という判断にはあまり合理的な根拠がない。 ＞そもそも、「φに入る論理式を排除する」という ＞判断それ自体に全く論理的な根拠がない。 ＞矛盾する命題が導かれるんだから論理的根拠はあるでしょ。 ないよ。φに入れる論理式のせいだと決め付ける論理的根拠はない。 実際、φに入れる論理式を制限せずに解決できる。 場当たり的というなら、φのせいだというのも場当たり的 場当たり対場当たりなら引き分け。 466 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 14:57:45 ] ＞少なくともreductio ad absurdumが成り立つ限りにおいては。 矛盾が導けなければ背理法が認められても意味がないｗ ＞古典論理が採用されたのが歴史的経緯に過ぎないという意見は ＞一般に認められたものでもないと思うけどね。 実際には、昨今の論理の研究は、君の思い込みが 正しくないことを示しつつある。 467 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 15:07:45 ] www.math.s.chiba-u.ac.jp/~komori/jyugyou/suuriron.pdf 468 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 15:19:54 ] ＞レベルの高いお話の途中すいません。 もっともレベルの低い話ですいません。命題論理です。 公理 (1)　F→(G→F) (2)　(F→(G→H))→((F→G)→(F→H)) 推論規則 　FとF→GからGを導く ここで、以下の命題はどうやって証明できるんでしょう？ (a)　(A→(B→C))→(B→(A→C)) (b)　(A→(A→B))→(A→B) 469 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 15:22:28 ] >>464 いや当時の数学史に関して普通によく言われることなんだけど。 私の個人的意見ではないですよ。 >>465>>466>>467 古典論理もしくは直感主義論理のような背理法が使える論理を 前提に話をしてるんだけどね。 部分構造論理くらい知ってるけど、そんなの研究してるのは 大抵計算機関係の人だと思ってたけどね。 部分構造論理だとか矛盾許容論理を使って 集合論だとか解析だとかをやろうなんて話はほとんど聞いたことがない。 「昨今の論理の研究は古典論理が採用されたのは 歴史的経緯に過ぎないことを示しつつある」なんて大嘘もいい所。 大多数の数学者は古典論理は自然に受け入れた。 なぜならそれまで自分たちが使っていた論理を自然に形式化したものだったから。 470 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 15:24:09 ] >>468 (1)と(2)から証明の複雑さに関する帰納法で 演繹定理というものが導けるからそれを使えばいい。 教科書には大抵載ってます。 471 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 15:25:55 ] ×直感 ○直観 472 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:02:51 ] >>469 ＞古典論理もしくは直感主義論理のような ＞背理法が使える論理を前提に話をしてるんだけどね。 直観主義論理では、背理法は無条件には使えないよ。 ＞部分構造論理くらい知ってるけど、そんなの研究してるのは ＞大抵計算機関係の人だと思ってたけどね。 んなこたぁない。 ＞部分構造論理だとか矛盾許容論理を使って ＞集合論だとか解析だとかをやろうなんて話は ＞ほとんど聞いたことがない。 Grisinが聞いたら嘆くだろうな。 「縁無き衆生は度し難し」 とかいって。 473 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:08:05 ] ＞大多数の数学者は古典論理は自然に受け入れた。 ＞なぜならそれまで自分たちが使っていた論理を ＞自然に形式化したものだったから。 ふーん。 じゃ聞くけど ・１２０円持ってる ・１２０円でコーラが買える ・１２０円でお茶が買える 古典論理だと、ここから ・コーラもお茶も手に入る が導けるけど、こんなこといったら コドモにもバカにされるぞｗ 474 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:20:16 ] ちゃちゃいれるのはいいとしても、何故そんなに挑発的に書く必要がある？ 度量の狭さを自ら露呈することもないだろ 475 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:30:17 ] >>474 単に経済活動においては古典論理が成り立たないことの例を示したまで。 マルクスがこれを知っていたら、弁証法の代わりに部分構造論理を 口にしたかどうかは定かではないが。 476 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:33:41 ] 煽りたいだけの奴はほっとけ 477 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:35:53 ] まあこういうのが得意な人なんだよ 478 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 16:49:34 ] >>476-477 常識でガチガチに固まってるから 簡単に煽られて炎上するんだよ。 479 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 17:09:32 ] >>468 演繹定理使えば？ 480 名前：461 mailto:sage [2007/08/28(火) 17:10:08 ] >>462さっそくのレスありがとうございます。おかげで(11)は解決しました。（気が ついてみると、(11)はとても簡単でした。お騒がせしました。） 　ところが(10)がまだわかりません。どうか、もう少しヒントなりいただけないでしょうか。 それから、証明したい論理式の型を1つ忘れていました。 (12)　∀xF→F[t/x] （F[t/x]はFにある自由なxの全てに項tを代入したもの。ただし、代入可能な場合に限る） これもなかなかわかりません。どうかお助けください。 481 名前：461 mailto:sage [2007/08/28(火) 17:12:06 ] あ、ちなみに>>468は私ではありません。それともそのくらい示せるかどうか試しているのでしょうか？ >>468くらいならできますが．．．。 482 名前：468 mailto:sage [2007/08/28(火) 17:29:47 ] 演繹定理ですか･･･なかなか難しいですね。 いまのところ(a)について 公理２によって(A→(B→C))から((A→B)→(A→C)) 公理１によってBと((A→B)→(A→C))から(A→C) は示せましたが･･･ で、(b）のほうは、 公理２によって(A→(A→B))から((A→A)→(A→B)) で、(A→A)が導ければ(A→B)は導けるのだが･･･ ということで、追加問題 (c)　(A→A) 483 名前：461 mailto:sage [2007/08/28(火) 21:08:46 ] >>468は本当に疑問だったんですね。私も質問ばかりでは申し訳ないので、今回は 私が>>482の(c)に答えることにします。（ので、誰か私の疑問についてもどうかお願い します。） はっきりいえば、演繹定理証明しちゃえば>>468さんの(a),(b)はいずれも明らかで すよ。早く何かの入門書で演繹定理を学ばれることを強く勧めます。 では>>482の(c) (i)公理(1)より　A→(A→A) (ii)公理(1)より　A→((A→A)→A) (iii)公理(2)で、F,HとしてA、GとしてA→Aをとると 　　　　(A→((A→A)→A))→((A→(A→A))→(A→A)) (iv)(ii)と(iii)より　(A→(A→A))→(A→A) (v)(i)と(iv)より(A→A) っていうか、公理(2)は仮定Fのもとでの、「GとG→HからHを導くこと」 になってること、見えてます？そうすれば演繹定理なんて簡単なんだけど。 484 名前：484 mailto:sage [2007/08/28(火) 22:16:43 ] 4=8-4 485 名前：１３２人目の素数さん mailto:sage [2007/08/28(火) 23:10:48 ] >>480 (10)はごめんなさい、勘違い ちょっとやり直してくる 486 名前：１３２人目の素数さん mailto:sage [2007/08/29(水) 00:11:08 ] >>461-462 閉じてない論理式に対しては演繹定理成り立ってないような気がします。 (11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。 487 名前：461 mailto:sage [2007/08/29(水) 09:09:51 ] >>486 ＞閉じてない論理式に対しては演繹定理成り立ってないような気がします。 generalization（>>461の推論規則(9)）が無条件で行われるので当然ではないで しょうか。そもそも私が最初に(11)が証明できないと早合点してしまったのも それが原因です。 ＞(11) の証明では命題論理レベルの話に落ちるので結局問題ありませんけど、一応。 ええ、ですから私も>>480で(11)に関しては証明できたと申し上げました。 488 名前：468 mailto:sage [2007/08/29(水) 09:26:08 ] >演繹定理証明しちゃえば>>468さんの(a),(b)はいずれも明らかですよ。 戸田山氏の「論理学をつくる」に書いてありました。 これで勉強します_(_o_)_ 489 名前：461 mailto:sage [2007/08/29(水) 13:07:56 ] だめもとと思ってぐぐってみたら、 Kalish, D. and R. Montague. On Tarski's Formalization of predicate logic with identity, Arec. f. Math. Logik und Grundl. vol. 7(1964). p.81-101 をネット上で見つけることができました。>>461の(10)に関しては最初の方 （p.85のLEMMA 2.）で証明されていました。後は>>480の(12)のみです。 こっちはできるかどうかわかりませんが、がんばります。また、お分かりの方 いましたら、ご教示いただけるとたすかります。では。 （ある程度昔の論文ならネット上で誰でも閲覧できる、何てふうにならないか なあ。） 490 名前：461 mailto:sage [2007/08/29(水) 13:10:19 ] >>489訂正 （誤）Arec.→（正）Arch. 491 名前：１３２人目の素数さん mailto:sage [2007/08/29(水) 15:27:19 ] これが俗に言うMontague&Kalish型なんですか、なるほど 492 名前：１３２人目の素数さん mailto:sage [2007/08/29(水) 16:42:03 ] >>489 > をネット上で見つけることができました。>>461の(10)に関しては最初の方 > （p.85のLEMMA 2.）で証明されていました。 これの概要教えて 493 名前：１３２人目の素数さん mailto:sage [2007/08/29(水) 17:01:39 ] >>489 ならんな。泥棒猫め 494 名前：461 mailto:sage [2007/08/29(水) 17:07:50 ] >>492 を、興味を持ってくれた人がいるんですね。では概略を。命題論理関係の式変形 は省きます。 (i)公理(7)より　y=x→(y=x→x=x) (ii)(i)より　y=x→x=x (iii)(ii)より　¬x=x→¬y=x (iv)推論規則(9)より　∀y(¬x=x→¬y=x) (v)公理(4)より　∀y¬x=x→∀y¬y=x (vi)(v)の対偶を取って　¬∀y¬y=x→¬∀y¬x=x (vii)公理(6)より　¬∀y¬y=x (viii)(vi)(vii)より　¬∀y¬x=x (ix)公理(5)より　¬x=x→∀y¬x=x (x)(ix)の対偶を取って　¬∀y¬x=x→x=x (xi)(viii)(x)より　x=x (xii)推論規則(9)より　∀x(x=x) 495 名前：461 mailto:sage [2007/08/29(水) 17:09:04 ] >>493 ネット上で普通に読めるのに？ 496 名前：１３２人目の素数さん mailto:sage [2007/08/29(水) 17:10:13 ] 煽りに反応するなよ 497 名前：497 mailto:sage [2007/08/29(水) 22:40:28 ] √(49)=7 498 名前：１３２人目の素数さん mailto:sage [2007/08/30(木) 07:41:37 ] 泥棒は盗むばかり 499 名前：１３２人目の素数さん mailto:sage [2007/09/02(日) 16:02:31 ] 集合論ってさ、演習やらないとわかってこないもんかな？ それとも教科書読むだけでわかってくる？ 500 名前：１３２人目の素数さん mailto:sage [2007/09/02(日) 22:46:41 ] どんな分野も、自明でない例を一つ二つ考えた上で その例で内容をなぞりつつ文献を読まないと 表面的な理解にすらも行き着かずに終わるだろうね。 501 名前：１３２人目の素数さん mailto:sage [2007/09/03(月) 18:17:18 ] 集合論をテーマにしたエロゲーをつくりたい タイトルは「プリクリ オルタネイティヴ」 502 名前：１３２人目の素数さん mailto:sage [2007/09/04(火) 10:22:13 ] ﾜﾛﾀ 503 名前：１３２人目の素数さん mailto:sage [2007/09/22(土) 01:11:45 ] >>499 結局集合算はドリルしないとだめじゃね？ 504 名前：１３２人目の素数さん mailto:sage [2007/09/25(火) 20:21:09 ] 俺のドリルが天を衝く 505 名前：１３２人目の素数さん mailto:sage [2007/09/25(火) 21:51:22 ] >>504 んーまあ、何をやりたいかによるんだよ。 1+1やるのに毎回毎回ペアノ算術したりλ計算する奴はあんまりいないよね？ までも一回は集合のジャングルで遭難しておいた方がいいとは思うけどね。 進めなくなって娑婆に出てこれなくなるかもだがｗ。 506 名前：１３２人目の素数さん [2007/09/28(金) 00:24:21 ] 初心者ですみません。集合論の外延の公理は論理学で示せるのでしょうか。 507 名前：１３２人目の素数さん mailto:sage [2007/09/28(金) 00:28:56 ] >>506 へ? 508 名前：１３２人目の素数さん mailto:sage [2007/09/28(金) 03:23:07 ] >>506 高階論理、４階以上ならでてくる。 509 名前：１３２人目の素数さん mailto:sage [2007/10/01(月) 11:41:28 ] >>508 M_SHIRAISHI降臨？ 510 名前：１３２人目の素数さん mailto:sage [2007/10/01(月) 20:29:24 ] 地下１階の論理ってあるんですか？ 511 名前：１３２人目の素数さん mailto:sage [2007/10/01(月) 20:30:26 ] そこは立ち入り禁止だから 512 名前：１３２人目の素数さん mailto:sage [2007/10/01(月) 22:10:10 ] 霊界の論理 513 名前：１３２人目の素数さん mailto:sage [2007/10/03(水) 04:53:03 ] >>509 普通にtype理論を扱った教科書にはでてくるだろう。 なお、 "M_SHIRAISHI"はNGワード 514 名前：１３２人目の素数さん mailto:sage [2007/10/04(木) 12:02:08 ] >>513 君が見た本の書名と証明が書かれたページ数を記載すればいい。 515 名前：１３２人目の素数さん mailto:sage [2007/10/04(木) 16:54:56 ] それくらい自分で探せよ 516 名前：１３２人目の素数さん mailto:sage [2007/10/05(金) 09:51:02 ] >>515 そもそも 「普通にtype理論を扱った教科書」 なんて知らん 517 名前：１３２人目の素数さん mailto:sage [2007/10/06(土) 01:07:22 ] それは探す努力を全くしてないんじゃないだろうか 518 名前：１３２人目の素数さん mailto:sage [2007/10/06(土) 03:23:09 ] G,Takeui:Proof Theory だとP197以下、 P,Andrews 小川訳:数理論理学とタイプ理論　だとP161以下。 519 名前：１３２人目の素数さん mailto:sage [2007/10/06(土) 04:50:16 ] 読むのメンドクセーから証明ここに書けや、ウジムシ 520 名前：１３２人目の素数さん mailto:age [2007/10/06(土) 19:15:28 ] すみません、{ω,ω^ω,ω^(ω^ω),ω^(ω^(ω^ω)),…}のいずれよりも 大きい最小の順序数は何と書き表すのでしょうか？ 521 名前：１３２人目の素数さん mailto:sage [2007/10/06(土) 19:16:30 ] 数理論理学と論理学ってどう違うの？ 522 名前：１３２人目の素数さん mailto:sage [2007/10/06(土) 19:19:38 ] さーなー どこかのスレに書いてあったんじゃねーの 523 名前：１３２人目の素数さん [2007/10/06(土) 22:33:03 ] 雨宮の定理って何ですか？ 524 名前：１３２人目の素数さん [2007/10/07(日) 03:30:04 ] >>520が人の顔に見える 525 名前：１３２人目の素数さん mailto:sage [2007/10/07(日) 14:44:21 ] >>518 おおっ、先週「数理論理学とタイプ理論」買ってた俺、大勝利！！ 526 名前：１３２人目の素数さん [2007/10/07(日) 16:42:46 ] 直観主義をわかりよく解説した日本語の本ありますか？ 教えてください。 527 名前：１３２人目の素数さん mailto:sage [2007/10/07(日) 19:18:49 ] >>520 ε_0 528 名前：１３２人目の素数さん mailto:sage [2007/10/07(日) 21:55:16 ] >>527 ありがとうございます！ ではε_1はε_0,ε_0^ω,ε_0^(ω^ω),ε_0^(ω^(ω^ω)),…ですか？ 529 名前：１３２人目の素数さん mailto:sage [2007/10/08(月) 02:18:32 ] ω^(ε_0+1),ω^(ω^(ε_0+1)),...

---

---

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

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