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

1 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 19:22:39 ] 立てます。 2 名前：にょにょ ◆yxpks8XH5Y mailto:sage [2007/02/04(日) 19:24:46 ] 　今だ！2ｹﾞｯﾄｫｵ ￣￣￣￣￣∨￣￣￣　　　　　　　(´´ 　　　　 ∧∧　　　)　　　　　　(´⌒(´ 　　⊂（ﾟДﾟ⊂⌒｀つ≡≡≡(´⌒;;;≡≡≡ 　　　　　　 ￣￣　 (´⌒(´⌒;; 　　　　　　ｽﾞｻﾞｰｰｰｰｰｯ 3 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 19:59:49 ] 前スレ>>999 濃度の比較可能定理⇔AC 4 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 20:07:54 ] いいことを教えてやろう。 こんなスレを立ててくれたんだからな。 スペイン語で数字の「５」のことを「Cinco」って言うんだ。 OK、あぁ、わかってる。 お前のことだからとりあえずチンコを連想しただろ？ 読み方をカタカナで表すとシンコって感じなんだが、 まぁ、今はそんなことどうだっていいんだ。 いいか、よく聞け。 これからは２ゲットの時代じゃなく、５に Cinco って書くことが流行る。 そう、５に合わせてただ Cinco とだけ書くんだ。 読み方のわからない厨房はチンコを連想するだろ？ まさにそれが狙いなんだ。 頭のいいお前には「５」ってことがわかるが、厨房には「チンコ」だ。 わかるか？それがお前と厨房の差なんだ。 これからはそうやって５をゲットすることでお前のすごさを見せ付けてほしい。 ↓さぁ！ 5 名前：にょにょ ◆yxpks8XH5Y mailto:sage [2007/02/04(日) 20:10:51 ] ちんこ 6 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 20:11:10 ] いつつ 7 名前：１３２人目の素数さん [2007/02/04(日) 20:38:56 ] べつに基礎論って言うけど基礎でもなんでもないくせに 8 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 22:51:30 ] とりあえず前スレから 116 名前：１３２人目の素数さん[sage] 投稿日：2006/05/12(金) 12:15:28 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野で、 非古典論理、証明論、構成的数学、モデル論や意味論、集合論、計算論 などの分野群の総称です （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです） 応用、ないし交流のある分野は、計算機科学の諸分野や、 代数幾何（Hrushovskらiによる研究）などを含み、多岐にわたります （cf. 数学セミナー98年6月号、「数学基礎論の学び方」） ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります 他のスレで御質問なさるようにお願いします 9 名前：１３２人目の素数さん mailto:sage [2007/02/05(月) 00:14:12 ] >>8 前スレ958で修正されてたバージョンの方が良かったのでは 10 名前：にょにょ ◆yxpks8XH5Y mailto:sage [2007/02/05(月) 11:05:36 ] >>7は多分ツンデレ 11 名前：１３２人目の素数さん mailto:sage [2007/02/05(月) 21:03:22 ] 前スレ 数学基礎論の質問スレッド　その２ science5.2ch.net/test/read.cgi/math/1143943264/ 数学基礎論の質問スレッド science4.2ch.net/test/read.cgi/math/1097659610/ 12 名前：１３２人目の素数さん mailto:sage [2007/02/07(水) 21:55:43 ] 建築物基礎論 13 名前：（　^ω^） mailto:（　^ω^） [2007/02/08(木) 23:35:00 ] PrawitzのNatural Deduction買ってきたお（　^ω^） これから読むお（　^ω^） 14 名前：１３２人目の素数さん mailto:sage [2007/02/09(金) 00:13:51 ] >>13 一緒に読も 15 名前：１３２人目の素数さん mailto:sage [2007/02/11(日) 10:08:24 ] 「数学基礎論」は誰が命名したの？ 16 名前：１３２人目の素数さん mailto:sage [2007/02/11(日) 23:15:54 ] 数学建築家が 17 名前：１３２人目の素数さん mailto:sage [2007/02/12(月) 06:46:40 ] 英語だと「数学基礎論」じゃなくてFoundations of mathematics。 独語ではGrundlagen der Mathematikで、同名のHilbertとBernaysによる著書が 1939年に出版されていて、日本語の抄訳がSpringerから「数学の基礎」の題名で出ている。 いつ誰が分野名として「Grundlagen der Mathematik」という言葉を使ったのが最初か、 誰が「数学基礎論」と命名したのかはちょっと謎。 上のHilbert/Bernaysが起源となっている可能性も高いと思うけど、 きちんと調べて見ないと自信持って答えられないんじゃないかな。 「キソロン」みたいな語感は日本に特有だと思う。 英語名だともっと「数学の基礎（付け）」って感じじゃないかな。 分野名としても使われてる言葉だとは思うけど。 18 名前：１３２人目の素数さん mailto:sage [2007/02/14(水) 14:54:09 ] 「現代思想」臨時増刊の渕野先生の記事ﾜﾛﾀ 19 名前：１３２人目の素数さん mailto:sage [2007/02/15(木) 09:56:48 ] 基礎論と位相幾何ってあんまり接点ないですかね？ 20 名前：１３２人目の素数さん [2007/02/15(木) 10:57:46 ] あるよ。基本群とか。 21 名前：１３２人目の素数さん mailto:sage [2007/02/15(木) 11:17:52 ] >>20 具体的に論文とかありますかね 22 名前：１３２人目の素数さん [2007/02/15(木) 19:44:42 ] 今出せないけどいくらでもあるから探してみたら？ 23 名前：１３２人目の素数さん [2007/02/15(木) 20:37:16 ] 四次元多様体が位相同型で分類不可能であることの証明にそれっぽいことを使っていたかも。 24 名前：１３２人目の素数さん mailto:sage [2007/02/15(木) 20:41:42 ] あまり接点はないよ 25 名前：１３２人目の素数さん mailto:sage [2007/02/15(木) 21:27:58 ] >>22-24 ありがとうございます。さがしてみます 26 名前：１３２人目の素数さん mailto:sage [2007/02/15(木) 21:49:05 ] どちらかというとトポロジーそのものよりも組み合わせ群論とか幾何学的群論とかで関係するといった感じかな。 27 名前：１３２人目の素数さん mailto:sage [2007/02/16(金) 18:09:56 ] Jech って何て読むんですか？ 28 名前：１３２人目の素数さん mailto:sage [2007/02/16(金) 21:14:36 ] いえっく？ 29 名前：１３２人目の素数さん [2007/02/17(土) 20:42:04 ] いぇっち　でしょ！！ 30 名前：１３２人目の素数さん [2007/02/18(日) 10:15:45 ] 定義式の質問です。 ある物体oに曜日の設定を１つしたい場合 week(o) = {mon, tue, wen, thu, fri, sat, sun} とすると７つとも設定すると言う意味でしょうか？ ∨などを曜日の略記の間に挟んだりしなければならないのですか？ 宜しくお願いします。 31 名前：１３２人目の素数さん [2007/02/18(日) 10:41:01 ] 何だそりゃ 32 名前：１３２人目の素数さん [2007/02/18(日) 10:53:01 ] >>31 week関数に曜日を設定する定義式の書き方です。 weekは・・・ああー自決しました。頭悪かったです。 失礼しました。 33 名前：１３２人目の素数さん mailto:sage [2007/02/18(日) 11:09:43 ] (^ω^；) 34 名前：１３２人目の素数さん mailto:sage [2007/02/18(日) 15:59:05 ] 基礎論のスレで基礎論と全然無関係の質問して あげくに首つったか腹掻っ捌いたか知らんが自決とは…… 何、いまどきの日本人ってこんなに低レベルなんだっけ？ 35 名前：１３２人目の素数さん [2007/02/18(日) 18:03:58 ] 基礎論で、ゲーデル達の完全性／不完全性定理以降、それに匹敵するくらい 重要かつ興味深い結果って何か出てるんですか？ 36 名前：１３２人目の素数さん [2007/02/18(日) 19:58:28 ] 人によって興味とか違うからなあ 37 名前：１３２人目の素数さん mailto:sage [2007/02/18(日) 20:21:06 ] むしろ不完全性定理が大して興味深くない 38 名前：１３２人目の素数さん mailto:sage [2007/02/18(日) 22:42:45 ] >>35 Lowenheim-Skolemの定理（実数論の可算モデルを作ったり出来る）とか、 証明論ならcut除去定理とか、集合論を含めるならCohenのforcingとか。 それにプログラミングが好きならCurry-Howardとかも興味深いだろうし さらに人によっては自然数論とか「解析」の無矛盾性証明が興味深くて重要かもしれないし。 >>36>>37にだいたい同意。 不完全性定理のインパクトの強さは人による。 完全性定理に匹敵する結果が無いって事はないんじゃないかなあ。 39 名前：１３２人目の素数さん mailto:sage [2007/02/18(日) 23:06:53 ] 巨大集合にかんする話や計算可能実数とか順序極小理論とか計算量に関する話とか。 証明論だと巨大基数類似可算順序数を利用した数学の無矛盾性プログラムなんてのもある。 40 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 00:17:52 ] >>35が予想あるいは期待していた答は「ない」であったという方に 病院にいる花京院の魂を賭けるぜ 41 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 00:46:32 ] パッと見で>>40に花右京メイド隊と書かれているように空目しました。 42 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 03:49:01 ] >>38 人によって違うのはそうだけど、基礎論に与えた影響という意味で重要性を測るとしたら、 不完全性定理に比べたら、cut除去定理とか自然数論の無矛盾性とかかなり見劣りするように思う。 43 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 08:10:36 ] 「どんな命題も真か偽かどちらかなんだから証明か反証ができるはず」と素朴に思ってる人には不完全性定理は驚異的。 だけど「証明や反証できるのはラッキーな場合だけで、いつもそんなにうまくいくはずがない」と思ってる人とか、更には「そもそも命題が真か偽かどちらかだという考えがおかしい。」という直観主義者にとっては不完全性定理なんて「ふうん。当たり前じゃん」で終わり。 44 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 09:39:39 ] 「当たり前じゃん」と思う問題でも、「そんなことどうやって証明すんだよ」っていう類のものであれば、 やっぱり感嘆の対象になるでしょう。不完全性定理はそういう結果だと思う。 あんな証明方法思いつくところがすごい。 45 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 11:08:44 ] 公理系の強弱を測るモノサシができたのはよかった 46 名前：１３２人目の素数さん mailto:sage [2007/02/19(月) 13:30:31 ] ＞「証明や反証できるのはラッキーな場合だけで、いつもそんなにうまくいくはずがない」 こういう常識的感覚を生んだのが不完全性定理だから ちょっとアレだけどね。 >>42 それは証明論の基礎論での位置をどのくらい重要だと評価するかの問題が大きいと思う 47 名前：１３２人目の素数さん [2007/02/20(火) 05:12:46 ] 突然ですが、記号論理学でいう“話の世界”と確率でいう“場合”は同じだと思いませんか？ 48 名前：１３２人目の素数さん [2007/02/20(火) 05:39:29 ] どうしても解けなくて困ってます。 abcde-fghi=33333 abcdefghiは1から9までのいずれかの数字が入り。同じ数字は使えない。 よろしくお願いします 49 名前：１３２人目の素数さん mailto:sage [2007/02/20(火) 06:10:01 ] 基礎 質問 というキーワードが含まれているからだなｗ 50 名前：１３２人目の素数さん [2007/02/20(火) 07:33:44 ] abcde-fghi=33333=3 mod 10 =33 mod 100 =333 mod 1000 =3333 mod 10000 =33333 mod 100000 51 名前：１３２人目の素数さん mailto:sage [2007/02/20(火) 14:00:00 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 52 名前：１３２人目の素数さん mailto:sage [2007/02/21(水) 09:18:33 ] blog.livedoor.jp/dankogai/archives/50764943.html ＞ヒルベルトの「幾何学基礎論」は、そのまま中学の教科書に使えるのではないかというぐらい平易で、 ＞「本物に教えてもらう」快感を「ふつうの人」でも存分に味わうことができる。 ↑こういうことを言う人のブログが日本で9番目に多く読まれてるらしいです（・・ 53 名前：１３２人目の素数さん mailto:sage [2007/02/21(水) 09:29:33 ] そう書いておけばamazonのアフィリエイト収入が期待できるからだろう 54 名前：１３２人目の素数さん mailto:sage [2007/02/21(水) 10:23:16 ] ああdankogaiかｗ おとなしくスクリプトでも書いてりゃいいのに 55 名前：１３２人目の素数さん mailto:sage [2007/02/21(水) 10:31:18 ] Azriel Levy のBasic Set Theory ではどのような内容のことが 扱われているのでしょうか。amazon.comのページを見る限り、 Boole代数、無限組み合わせ論や巨大基数について触れられてるのは分かるのですけど、 例えば強制法などについては載っているのでしょうか。 友隣社やマテマティカなどにも置いてないようで、ちょっと内容が分からないのでご存知の方いらっしゃったら教えて下さい。 56 名前：ビギナー [2007/02/21(水) 23:59:00 ] ビギナーです。 「数学の楽しみ」２００６秋「ゲーデルと現代ロジック」で、p.47脚注13に、 「矛盾する命題が一つ証明できれば、それからすべての命題が証明されてしま うので、体系が無矛盾であることは、ある命題がその体系から証明できない ことと同値である」との記述があります。 「ある命題」には、「体系が無矛盾であること」も含まれるのでしょうか。 そうであれば、第二不完全性定理から、（初等数論の体系を含む）公理系は、 自身の無矛盾性を証明できないので、そのことは、体系が無矛盾であることと 同値であるということになり、結局、体系が無矛盾であることを示していると なりそうなのですが、どこが間違っているのでしょうか。 57 名前：１３２人目の素数さん mailto:sage [2007/02/22(木) 00:20:06 ] 第二不完全性定理から、（初等数論の体系を含む）公理系は、 「無矛盾ならば」自身の無矛盾性を証明できないので、 が正しい。 58 名前：１３２人目の素数さん mailto:sage [2007/02/22(木) 00:56:32 ] あと「体系が無矛盾であること」をその体系で表現できるか、という問題もありますね。 例えていえば微分積分の理論が無矛盾であることを微分方程式や級数なんかを使って 命題で表現しろというわけですからtrivialからは程遠いでしょう？ その条件が「（初等数論の体系を含む）」となってるわけですが。 あと無矛盾性は、具体的に証明のどこで使ってるんですか？と言われると きちんと勉強してないと答えるのが難しいね。 59 名前：１３２人目の素数さん mailto:sage [2007/02/22(木) 01:37:46 ] > 「矛盾する命題が一つ証明できれば、それからすべての命題が証明されてしま > うので、体系が無矛盾であることは、ある命題がその体系から証明できない > ことと同値である」との記述があります。 これの意味はおｋ？なにか誤解してそうなんだけど 60 名前：１３２人目の素数さん [2007/02/22(木) 09:13:05 ] >>55 modelの話は扱わないという方針。 だから、forcingも出てこない。 61 名前：55 mailto:sage [2007/02/22(木) 17:47:56 ] うーん、強制法載ってないんですか… 強制法の載っている教科書はやっぱり高いなあ… 62 名前：１３２人目の素数さん mailto:sage [2007/02/22(木) 17:54:21 ] 強制法なしで巨大基数の話してるのか・・・ 63 名前：１３２人目の素数さん [2007/02/22(木) 23:21:11 ] 有理数と複素数の中間体である代数的閉体のうちで、 その存在証明に真に選択公理を必要とするものがありますか？ 64 名前：１３２人目の素数さん mailto:sage [2007/02/26(月) 09:52:56 ] 日本語の教科書で強制法について詳しく書いてあるのってありますか？ 65 名前：１３２人目の素数さん mailto:sage [2007/02/26(月) 10:47:22 ] 強制法って何よ 66 名前：１３２人目の素数さん mailto:sage [2007/02/26(月) 10:54:13 ] フォーシング 67 名前：１３２人目の素数さん [2007/02/26(月) 11:12:12 ] 定理を強制列車に乗せること（ｗ 68 名前：１３２人目の素数さん [2007/02/26(月) 11:13:34 ] >>64 洋書嫁。最近の和書は絶版か品切ればかり。 69 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 16:40:52 ] >>35 ＞基礎論で、ゲーデル達の完全性／不完全性定理以降、 ＞それに匹敵するくらい重要かつ興味深い結果って ＞何か出てるんですか？ コーエンのフォーシングと、これを用いた選択公理・連続体仮説の独立性 70 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 16:45:21 ] >>38 ＞Lowenheim-Skolemの定理とか これ、ゲーデルの完全性/不完全性定理より古いんじゃなかった？ ＞Curry-Howardとか これも、結構古い。もともとはCurryがλ計算と 論理との関連を研究していて見つけたもの。 71 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 16:56:35 ] 基本的なところを読みたいなあ〜と思ったりする日々 「数学と論理」に挙がってるこの本っておすすめですか？ Stephen G. Simpson : Subsystems of second order arithmetic Springer 1991 72 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 16:58:20 ] >>58 ＞「体系が無矛盾であること」をその体系で表現できるか 残念ながらできません。 73 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 18:34:55 ] >>71 それは二階算術の部分体系を用いて、代数・解析・幾何などをやろうっていう本なので、 基礎論の基本的な勉強をしたいというときに使う本ではないぞ 74 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 18:48:51 ] >>73 あらら、逆数学というのを勉強したら、数学基礎論で使う証明の形式の 枠組みが（弱い体系限定かもしれませんが）きちんと理解できるのかと 思ってたんですが、必ずしもそういう印象ではないのですか？ 75 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 20:15:15 ] 逆数学にしろ何にしろ、そういう応用分野は、 まず基礎論で使う基本的な枠組みは理解してから取り組むものだと思う というか、そういう類の本は、 読者が基礎論のそれなりの知識を既に持ってることを前提として書いてあるもんだが 76 名前：１３２人目の素数さん mailto:sage [2007/02/27(火) 20:35:43 ] このチグハグっぷりはなんとしたことだ 77 名前：１３２人目の素数さん mailto:sage [2007/02/28(水) 12:12:24 ] とりあえず、あと１０日もしたら 「ゲーデルと２０世紀の論理学」の３巻が出ることになってて それに「逆数学と２階算術」の章があるみたいだぞ 78 名前：１３２人目の素数さん mailto:sage [2007/02/28(水) 13:01:49 ] 数理論理学 (数学基礎論) とはどんな学問かという話が出たときに、 自分の意見を言ってみたら、逆数学はその定義に当てはまらなかった。 79 名前：１３２人目の素数さん mailto:sage [2007/02/28(水) 19:20:36 ] 逆数学が数学であるとしても数学でないとしても矛盾が出た。どうしよう。 80 名前：１３２人目の素数さん mailto:sage [2007/03/01(木) 01:51:09 ] 逆数学が存在しないことの証明だね。 81 名前：１３２人目の素数さん [2007/03/02(金) 05:19:55 ] 近傍について質問です。 Vがxの近傍というのは、x∈U⊂Vを満たす開集合Uが存在するということですけど、Vの開核が存在すればそれはUになりえるので、必然的にVは近傍になっちゃうと思うのですがどうなんですか？ 82 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 05:27:31 ] ○・←x 83 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 06:18:30 ] 有限の立場ってのがいまいちよくわかりません ご教授お願いします。。。。。。 84 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 09:09:29 ] >>81 >>51 science6.2ch.net/test/read.cgi/math/1149259755/330 にちょっとレスしました 85 名前：１３２人目の素数さん [2007/03/02(金) 21:05:00 ] すいません、よろしくおねがいします LKでψが証明可能である⇒入力¬ψに対してタブローが停止する はどうやって証明したらよいのでしょうか 86 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 21:16:00 ] >>85 完全性定理を使えば自明 87 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 21:41:56 ] いや、それで完全性定理を説明しようと思っているのですが 88 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 23:23:07 ] >>85 林晋の数理論理学（コロナ社）にのっていたと思う。証明長いからここじゃ無理。 89 名前：１３２人目の素数さん mailto:sage [2007/03/02(金) 23:24:00 ] このスレで質問していいか不安ですがお願いします。 廣瀬健の「帰納的関数」（共立出版）に次のように有りました。 （＊）「1変数の原始帰納的関数はすべて1変数の関数のみで構成できる」 上記の本には証明の概略しか載っていないため、（しかもその概略がよくわか らない）どうしても示せないのです。どなたかご教示いただけないでしょうか？ （＊）をもう少し詳しく記述します。 初期関数として （１）s(x)=x+1（後者関数） （２）L(x)（定義後述） （３）R(x)（定義後述） （４）0(x)=0（常に0をとる定数関数） 以上の初期関数から初めて、 （５）2つの関数f(x),g(x)からJ(f(x),g(x))を作る。（J(x,y)の定義は後述） （６）2つの関数f(x),g(x)からf(g(x))を作る。 （７）2つの関数f(x),g(x)から次のようにh(x)を作る。 　　　　h(0):=f(0),　　h(x+1):=g(h(x)) を有限回繰り返し適用するだけで、1変数の原始帰納的関数をすべてつくる ことができる。 J,L,Rの定義（というか、単なる説明というか） J(x,y):=(x+y)(x+y+1)/2+x L,Rはz=J(x,y)⇔「L(z)=x∧R(z)=y」となるような関数 例えばL(z)+R(z)やL(z)・R(z)なんかはどうやって作るんでしょう？ どなたか偉い方お願いします。 90 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 00:05:24 ] >>89 昔全く同じところで悩んだ記憶があるよ J をうまく使えばできるはず 91 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 02:37:10 ] Robinson の結果だったような気がする。 92 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 07:44:05 ] >>83 私も良く知らないんですが、（Hilbertの）「有限の立場」は大雑把に言って 「有限の具体的図形に関する具体的な性質、具体的な操作、および具体的な推論のみを許す立場」 のことみたいです。ということで、良いんじゃないかな。多分。 参照文献 Web上の文章では、以下で引用する ・Hilbert's Program (Stanford Encyclopedia of Philosophy) ttp://plato.stanford.edu/entries/hilbert-program/ が一番詳しく纏まっていると感じました。 ・ヒルベルト・プログラムとは - はてなダイアリー ttp://d.hatena.ne.jp/keyword/%A5%D2%A5%EB%A5%D9%A5%EB%A5%C8%A1%A6%A5%D7%A5%ED%A5%B0%A5%E9%A5%E0 は数学の哲学専攻の大学院生の方が書かれたようです。（慶應大かどこか？） ・Hilbert's program - Wikipedia, the free encyclopedia ttp://en.wikipedia.org/wiki/Hilbert%27s_program Wikipediaの記事 ・数学基礎論三つの神話 ttp://www.shayashi.jp/HistorySociology/HistoryOfFOM/myth.html 終わりのほうに有限の立場に関するGoedelの認識がどうだったかが載っています。 ・自然演繹の正規化定理に基づく算術の無矛盾性証明 ttp://research.nii.ac.jp/~terui/mita03.pdf ぐぐって出て来たので一部ちょっとだけ参考にさせて貰いました。 ・Hilbert's Program members.at.infoseek.co.jp/nbz/ref/hprogram.html 逆数学がHilbertのプログラムの部分的実現となっているという喧伝。 93 名前：その壱 mailto:sage [2007/03/03(土) 07:46:16 ] ・有限の立場（独; finiten Standpunkt/英; finitistic standpoint)とは何であったか Stanford 哲学百科事典 のHilbertのプログラムの記事から必要そうなところだけごく一部引用。 文献番号省略。finitary standpointとfinitist point of view、 有限の立場と有限主義はほぼ同義語として使われているような感じです。 1.　Hilbeltのプログラムの歴史的発展 1.3　有限主義と無矛盾性証明の探求 Hilbertによると、内容的な算術という「具体的記号に関する純粋に直観的な基礎にのみ依拠する」 特別な数学の分野があり、その対象は「全ての思考に先立って直観的に直接経験として存在する」、 「それらの対象の存在、それらの差異、それらの並びは （それらの対象自身と同じように）何か別のものに還元できない」 これらは記号列は意味を持たず、つまり抽象的な対象を表さず、然しながら演算を受け （例えば連結され）比較される。これらの性質や関係の知識は直観的で論理的推論を介さない。 Hilbertによると、このようにして展開された内容的な算術は確実であり、 内容的数論の命題には論理的な構造がないのであるから、いかなる矛盾も起きない。 3.　形式主義、還元主義、道具主義 理念的な手法によって証明される実在的命題が「正しい」こと、 つまり有限の計算によって直接的に確かめられることが求められる。 これをSmorynskiが、実在的数学に理念的数学を付け加えて保存拡大になること、 と言い換えていることが4.　HilbertのプログラムとGoedelの不完全性定理に述べられている。 94 名前：その弐 mailto:sage [2007/03/03(土) 07:46:51 ] 2. 有限の立場（この項目が本題なんだけど長いので箇条書きで） この方法論的な立場は、数学的思考を「全ての思考に先立ち直観的に直接経験として存在」 するような対象、またそのような対象に関する抽象的概念の導入を必要とせず、特に、 完結した無限の総体に訴えることをしないような、演算と推論の方法に制限することより成っている。 2.1　有限的な対象と有限主義者の認識論 ・Hilbertが数項（numeral、数字とも訳す）をどれくらい正確に理解していたか？ Bernaysの提示した最も円熟した有限主義においては、有限主義の対象は 繰り返しの過程によって再帰的に生成される形式的な対象として特徴付けられる。 ・有限主義における対象の認識論的な意義についてどう考えていたか？ ・当時までの学者達のHilbert及びBernaysへの影響。 2.2　有限的に意味のある命題と有限的な推論 ・特性函数が再帰的に、典型的には原始再帰法によって定義されるような関係は受け入れられる。 ・このような関係から論理積∧、論理和∨、否定¬、限定量化によって出来た命題。 「任意のnに対してn+1=1+nとなる」のような数項に関する一般的事実を述べる命題は 問題のある有限的命題である。「どうしたって全ての数について試すわけにはいかない。」 有限的な一般命題は無限な連言∧_{x} φ(x)としてではなく、 「ただ、一つ数項が任意に与えられたときに何かを主張するような仮言的判断φ(x)として」 理解されねばならない。 このように一般的有限的命題に問題があるとしても、この種の命題は特に重要である。 95 名前：その参 mailto:sage [2007/03/03(土) 07:47:30 ] 2.3　有限的な操作と有限的な証明 ・どのような演算、どのような原理が有限の立場で許されるのか、という問題は決定的に重要である。 Hilbertは一般的な説明を与えず、ただ許容される内容的算術の演算と推論方法の例を与えただけ。 Hilbertは直観的な思考は「再帰法と有限主義的に存在する総体に対する直観的帰納法」を含むと述べて 累乗法（冪）を例に挙げ、Bernaysは累乗法が如何にして数項に関する有限的演算と理解されるかを述べた。 ・彼らが述べたことによれば原始再帰法により定義された演算と、 （仮言的）帰納法による証明が許されることになる。 ・これらは原始再帰法による函数定義と量化記号なしの論理式の上の帰納法を認める 原始再帰算術（primitive recursive arithmetic; PRA）として形式化できる。 ・しかしHilbertもBernaysも原始再帰法「しか」有限的だと見做されないと主張したわけではないし、 実際彼らは原始再帰的でない方法を用いて、表面的には有限的な無矛盾性証明を既に1923年に得ている。 （ε計算を使うらしいから「数学の基礎」に載ってるやつか？） 96 名前：その四 mailto:sage [2007/03/03(土) 07:48:00 ] ・どんな演算が有限的だと見做される「べき」であるか。 Parsons(1998)は有限主義の直観との関係を重視。 ・有限的とみなせるのは、せいぜいが加法と乗法から限定再帰法（bounded recursion）で得られた算術的演算。 ・累乗法と一般再帰法は許容されるものではない。 Tait(1981)は有限主義は原始再帰的な推論と一致するという主張を広く受け入れられるしかたで強力に擁護。 ・直観により表現されるという点を有限主義の特徴づけとは考えず、 有限主義的推論を「全てのnon-trivialな数学的推論に前提される最小限度の推論」と考える。 ・有限的な演算と手法を分析して有限列の形の数の概念に潜在的なものであるとした。 また別の、興味深いが哲学的に詳細な正当化を与えるわけではない有限的証明の分析が Kreisel(1960)により提案され、有限的な函数とはPAで全域的であると証明できる函数であるとされた。 またKreisel(1970)は「可視化出来る」という事に商店をあてた別の分析を与え、やはり有限的に 証明可能であるということとPAで証明可能であるということは実は同等である、という結論を導いた。 ・Primitive recursive arithmetic - Wikipedia, the free encyclopedia en.wikipedia.org/wiki/Primitive_recursive_arithmetic 97 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 08:59:57 ] >>92 有限の立場が 「有限の具体的図形に関する具体的な性質云々」 は全然違うと思うけど……。 　 98 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 09:11:06 ] >>96 PAはPRAかな >>97 神話としてはいいんじゃない？現代的な解釈はともかく 99 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 09:18:06 ] 原文ではPAになってるね 100 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 10:38:18 ] 聞いててもはや「数学」という感じがしないのは気のせい･･･？ 101 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 15:41:10 ] うん 102 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 17:51:09 ] 書いた本人ですがそもそも数学の話じゃないと思いますよ。 基礎論での「直観」などというのはKant的な意味合いが大きいみたいです。 そもそも有限の立場での絶対的な無矛盾性の証明は実現不可能なんだから 体系を限定することに昔ほど大きな重要性はないんのではないでしょうか。 >>98 Hilbertたちはどう考えていたか、というあくまで「Hilbert（学派）の有限の立場」の話なので。 最後の項には竹内外史の仕事だとか逆数学だとかも書いてありましたけど 直接的に関係がないので省略しました。 >>97 でも>>92の照井一成先生のpdfではそういう説明がされてるし、 大雑把に一言で説明するならこういう説明になりそうな気がするのですが どういうところがおかしいですか？ 「図形」というのは証明図のような 「有限個の記号から作られた有限的なもの」程度の意味です。 （↓「ゲーデルの世界」廣瀬健、横田一正より） 　すなわちこの立場は，直観的に確かめられうる対象とそれらに対する 　有限の操作の過程というものに方法を限定したものであった． （↓岩波文庫「不完全性定理」の「内容的な数学」の説明） 　ポイントは、これらの表現が全て有限個の記号から構成された有限的存在であり， 　また，それに関する議論も有限的であるという事実である．内容的な数学とは， 　本質的に有限的な数学なのである．そして，そこには直観的な議論があるだけで， 　過程すべき公理も論理法則もないのである．（中略） 　これが後に有限の立場と呼ばれるようになるものの原型である． 103 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 18:03:03 ] >>83　>>92　>>97　>>102 そもそも 「有限の具体的図形に関する 　具体的な性質、具体的な操作、 　および具体的な推論」 の全体を有限個の文字で記述 しつくすことは不可能。 つまり「有限の立場」は有限ではない。 104 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 18:09:41 ] ？ 誰も許される推論全体が有限だとか全て書き尽くせるだとか そういうことは言ってないけど… finitary「有限個のものに関するような、有限的な」と finite「有限個の」じゃだいぶ意味が違うような 105 名前：１３２人目の素数さん mailto:sage [2007/03/03(土) 18:40:59 ] >>103 有限の立場ってのは、 個々の証明について、必ず具体的な有限の操作で行うってことじゃないのか 106 名前：89 mailto:sage [2007/03/03(土) 23:57:21 ] >>90,91 レスありがとう。 忘れ去られてるっぽいけど、どなたか気が向いた方、ご教示お願いいたします。 >>89 107 名前：１３２人目の素数さん mailto:sage [2007/03/04(日) 10:32:11 ] >>89は要約すると、ゼロ関数C0、後者関数S、L、Rから （1変数関数合成） h(x) := f(g(x)), （1変数原始帰納法） h(0) := f(0) & h(x+1) :=g(h(x)), （2変数から1変数への圧縮）J(f, g)(x) := J(f(x), g(x)) で作られた関数全体が1変数の原始帰納関数全体と等しいことを示せということ。 まず恒等関数idはid(0) := C0(0) & id(x+1) := S(id(x)) でOK。 さて、A := J(L(x), R(y)) を使うと(x1, x2, x3)をA(x1, A(x2, x3))、 (x1, x2, x3, x4)をA(x1, A(x2, A(x3, x4)))みたいな感じで全単射で1変数に圧縮することが出来る。 この(x1,........., xn)が圧縮されたものを[x1,........., xn]と表すことにする。 逆にyをn変数に圧縮されたy :=[x1,........., xk]とみてxiたちへ「解凍」することも出来る。(*) xi = d_{n, i}(y) := L^i(y) if i < n, xn = d_{n, n}(y) := R(L^(n-1)(y)) 原始帰納関数はC_0、S、射影I_{n,i}（1≦i≦n）から （関数合成） h := f(g1,......, gm) （原始帰納法） h(x1,......, xm, 0) := f(x1,......, xm) & h(x1,......, xm, x+1) := g(h(x1,......, xm, t), x1,......, xm ,x) で作られるのでその帰納的定義を模倣emulateするようなf '[x1,.........,xn]を作れば良い。 実際f(x) = f '(d_{1,1})([x])である。 (*) Aや圧縮[ ]自体は>>89では使えないがg1'、g2' が得られていれば J(x1, x2) = J(d_{2,1}, d_{2,2})[x1, x2]は任意の[x1, x2]に対して計算できる！ のでこれを[g1', g2']と書こう。3変数以上のときも同様。解凍のほうは大丈夫。） C_0、後者Sは与えられており射影I_{n, i}' := d_{n, i} （1≦i≦n）ももう作った。 関数合成h := f(g1,......, gm) はh '[x1,........., xm] := f '([g1',......, gm']) で OK。 原始帰納的定義 h(x1,......, xm, 0) := g(x1,......, xm) & h(x1,......, xm, t) := f(h(x1,......, xm, t), x1,......, xm ,t)は h '([x1,......, xm, 0]) = g' ([x1,......, xm]) := g' [d_{n+1, 1}[x1,......, xm, 0], d_{n+1, 2}, ........., d_{n+1, n}[x1,......, xm, 0], ] （[d_{n+1,1},........., d_{n+1, n}]でn+1変数をn変数に直す） & はh '(x1,......, xm, t) := f' [h '[x1, ......, xm, t], x1,......, xm ,t] よってこれで全てemulate出来ている。 108 名前：１３２人目の素数さん mailto:sage [2007/03/04(日) 14:36:51 ] >>107 h'の定義が h(0):=f(0),h(x+1):=g(h(x)) と一致していないような 109 名前：89 mailto:sage [2007/03/04(日) 15:32:07 ] >>107 をを！これから解読しまつっ！thx! 110 名前：89 mailto:sage [2007/03/04(日) 16:29:01 ] >>107 やっぱり原始帰納的定義のところが、どーしてもわかりましぇん。例えばH(z):=L(z)+R(z) なんてどうやって構成すればいいのやら。おばかですみません。もう少しヒントを。 111 名前：１３２人目の素数さん mailto:sage [2007/03/05(月) 02:38:08 ] 有限の立場って、 「証明論等のメタ数学では、自然数論の範囲を超えた方法は使わない」 っていうような感じに捉えてたんだけど。 例えば、cut除去定理を証明する場合に、数学的帰納法は使ってもいいが、 超限帰納法は使っちゃダメ、みたいな。 ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、 まさにこれを実践するためでしょ？ 112 名前：１３２人目の素数さん mailto:sage [2007/03/05(月) 12:47:22 ] >>104 ＞誰も許される推論全体が有限だとか ＞全て書き尽くせるだとか ＞そういうことは言ってないけど… 本来、有限の立場とは、何が推論として許されるかが 有限個の文字数で書き表せ、有限ステップの操作で 検査可能である、という主張。 したがって、>>92のような立場は、有限の立場から逸脱している。 なお、専門家の中にも、この手の誤りをおかす者は少なくない。 113 名前：１３２人目の素数さん mailto:sage [2007/03/05(月) 15:59:01 ] お、専門家の間違いをびしびし指摘してくだいますね さすがドクトル 114 名前：１３２人目の素数さん mailto:sage [2007/03/05(月) 16:02:24 ] 誤りというか宗教論争の気がする・・・ 115 名前：１３２人目の素数さん mailto:sage [2007/03/05(月) 21:26:47 ] その「本来、有限の立場とは〜」の 「本来」ってのはどの文献にそういうことが載ってるの？ Hilbertがどこでそういうことを言ったんですか？ 116 名前：89 mailto:sage [2007/03/06(火) 09:23:24 ] >>89の疑問をいまだに解決できず、悶々としているものです。ところで、 Raphael M. Robinson , Primitive recursive functions, Bull. Amer. Math. Soc., vol.53 (1947), no. 10, pp. 925-942. を一般人が手に入れる方法はないのでしょうか？ arxiv.org/ とかいうところで検索しても出てきませんでした。Daniel E. Severinと言う方の 「Unary Primitive Recursive Functions」を今解読中ですが、どうも私の疑問を解決しては くれなさそうな．．．。（英語も苦手なんで、四苦八苦中） おやさしい方、どうかご教示ください。 117 名前：１３２人目の素数さん [2007/03/06(火) 11:51:40 ] ¬（A→B）→（A∧¬B）の自然演繹の証明方法をどなたかよろしくおねがいします。 ¬（A→B）を仮定して、¬（A→B）からどう動けばよいのか、別に何を仮定したらよいかがわかりません よろしくおねがいします。 118 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 14:22:49 ] ¬A, A |- Bだから¬A |- A→B ¬(A→B), ¬A |- （矛盾） だから ¬(A→B) |- ¬¬A、あとはNKの二重否定除去を使う。 NJでは出来なさそうな気がする。 B |- A→Bだから¬(A→B), B |- （矛盾） だから¬(A→B) |- ¬B、こっちは楽ー 119 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 18:20:14 ] >>115 HilbertはGoedelの不完全性定理の証明の後 表向き「有限の立場」だといいつつ、実際には かつて主張していた「有限の立場」を完全に 否定する論文を書いた。 Goedelはこれをみて 「よくもまあこんなものが書けたものだ」 といったそうだ。 120 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 19:14:51 ] 文献名（論文の表題）を教えて下さい。 Grattan-Guinnessに書いてあるだとか、 Ewaldに載ってただとかそういうのでも構いません。 その不完全性定理後にHilbertによって修正された立脚点のことを 「本来の有限の立場」と言ってるのだとしたら苦しすぎないですか？ Königsbergの会議が1930年7月だから せいぜい30年の年内くらいまでのHilbertの有限主義が「本来の有限の立場」だと思いますが。 121 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 22:30:19 ] >>116 > Raphael M. Robinson , Primitive recursive functions, > Bull. Amer. Math. Soc., vol.53 (1947), no. 10, pp. 925-942. 大学の図書館にならありそうだよ。 webcat.nii.ac.jp/cgi-bin/shsproc?id=AA00578276 122 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 23:30:31 ] >>118 それってシーケント計算じゃない？ 123 名前：１３２人目の素数さん mailto:sage [2007/03/06(火) 23:45:19 ] おお、sequentっぽくなってるｗ 単にNKの公理を一段メタな立場から書いたつもりだったんだけど。 ちょうど今「完全性定理とモデル理論」 のLKのカット除去のとこ読んでたからそれが影響したのかねｗ こんな感じ↓ 　[B]1 ------ A→B,　¬(A→B) ---------------1 　　　　¬B 124 名前：89 mailto:sage [2007/03/07(水) 00:36:42 ] >>121 ありがとう。でも一般人が大学から資料もらえるのかな？（もちろんコピーだけど）電話で聞けばいいのかな？ でもここから大学まで車で片道2時間。日曜日って大学やってないよね？ 125 名前：１３２人目の素数さん mailto:sage [2007/03/07(水) 01:00:14 ] >>124 休日やってるとこもあるよ。 web で簡単な利用案内があると思うから、確認してみては。 あるいは、公立の図書館通じてコピーを送ってもらうとか。 どこでも対応してくれるわけじゃなさそうだけど、運がよければ。 126 名前：１３２人目の素数さん mailto:sage [2007/03/07(水) 05:05:23 ] >>120 >>119はその通り「修正前が本来」と 言ってるように思ったけどな 127 名前：１３２人目の素数さん mailto:sage [2007/03/07(水) 16:42:57 ] >>126 漏れもそう思う。>>119は日本語が読めてない。 北朝鮮に帰れ。 128 名前：１３２人目の素数さん mailto:sage [2007/03/07(水) 17:55:30 ] 修正前の有限の立場が>>112で、それに対して、 修正された有限の立場、もしくは修正後流布した俗説が>>92ってこと？ でも>>119の主張を裏付ける（可能性がある）ものは 具体的にどの論文か良く分からないが 「Hilbertが不完全性定理の発見後に書いたらしいかつての立場を放棄する論文」しかない。 一方でStanford 哲学百科 はHilbertが書いたものだけでも20くらいの文章、本から 翻訳引用して、彼はここではこういっているし別のこれでもこういうことを言っている。 だから当時のHilbertの考えはこういうことなのだろう、というふうに推測している。 そのうち"Grundlagen der Mathematik" 1 & 2以外は全て不完全性定理発見前の文献。 Stanford 哲学百科の記事が正しいのだとしたらそれを大雑把に （Kantに馴染みの薄い現代の日本の読者に対しても意味があるように） 要約したものとしては>>92の説明で間違っているとはいえないような気がするけどなあ。 「有限の立場」の>>112みたいな説明はここ以外で読んだことない。 >>103は「具体的」というものが何を意味するのかわからないから駄目だ、 とか言っているのかもしれないし、曖昧であることは確かで、実際は Hilbertは例えば |、||、||| みたいな棒を並べたものを「具体的図形」の例として提示して たとえば||と|||の連結は|||は||に等しい、というのが2 + 3 = 3 + 2の意味だ、とか言っている。 「具体的」というのがきちんとformalに表現できて、 「有限的にある推論が許されるかどうかが、有限的に確かめられる」為にはそもそも 超数学自体が形式化されないといけないような気もするけど、 「直接経験」だとか「直観により論理を介さず」とか言ってたHilbertが そういうことを考えてたとは思わないけどなあ。 ジャキントの本（田中一之 監訳）読んでからレスしたかったけど、まあとりあえず。 129 名前：１３２人目の素数さん mailto:sage [2007/03/07(水) 17:57:40 ] ×||と|||の連結は|||は||に等しい ○||と|||の連結は|||と||の連結に等しい 連結はconcatenationの訳です 130 名前：１３２人目の素数さん mailto:sage [2007/03/08(木) 16:26:44 ] >>128 ＞でも>>119の主張を裏付ける（可能性がある）ものは 119のいう「不完全性定理証明後の変節論文」は 115の問いの答えではなくて、問い自体の ナンセンスさを指摘するものかと。 ＞「有限の立場」の>>112みたいな説明はここ以外で読んだことない。 いったいどこでどんな説明を読んだの？ 君こそ今までに読んだ文献を全て挙げてごらんよ。 131 名前：１３２人目の素数さん mailto:sage [2007/03/08(木) 16:29:53 ] >>128 ＞「具体的」というのがきちんとformalに表現できて、 ＞「有限的にある推論が許されるかどうかが、有限的に確かめられる」為には ＞そもそも超数学自体が形式化されないといけないような気もするけど、 安易にformalとか形式化とかいってるけど、 君はその意味を説明できるかい？ その説明は112の主張を否定するものかい？ 132 名前：１３２人目の素数さん mailto:sage [2007/03/08(木) 16:32:49 ] さすがドクトル 133 名前：１３２人目の素数さん mailto:sage [2007/03/08(木) 16:49:27 ] マギステルかも 134 名前：128 mailto:sage [2007/03/09(金) 01:09:28 ] >>112と>>119は違う人である可能性も無いでは無いと今思ったのですが 私が特に間違いだと思っているのは>>119ではなくて、>>112の「有限の立場」の説明に関してです。 >>112はHilbertたちの本来の「有限の立場」がこうだ、という主張なのですから、 Hilbertや周りの人たちの書いたり述べたりしたものが根拠に無ければなりません。 その一次資料が何か（或いは、それは何という二次資料を読めば分かるか）を教えてくれ、 という問いはナンセンスではない有意味な質問だと思いますが。 少なくとも「Hilbertはひっきりなしに態度を変えていて一貫していなかったから、 本来の立場と呼べるものなど無いのだ」などの主張は>>112のレスと両立しません。 Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など ある種の具体性を要求しています。 それが有限の文字数で書き表せるかどうかというのは別問題です （いやもちろん、曖昧な説明でも良いなら、Hilbertの著作中に現れる文字数は 明らかに有限なのだからこの条件は自明に満たされることになりますが。。） それに対して ＞何が推論として許されるかが有限個の文字数で書き表せ」 というような、「許される推論の説明に要する文字数」について Hilbeltや周囲の人間が何か要求していたというのは聞いたことがありません。 ＞君こそ今までに読んだ文献を全て挙げてごらんよ。 私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから このスレ以外に>>112のような説明が決して無いことは立証出来ません。 そもそも、今までに読んだ文献を「全て」挙げろ、というのは 幾らなんでも無茶な主張じゃないですか？あなたは出来ますか？ 私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを2ch以外で 「少なくとも一つ」教えてくれ、といっているだけなので、出来て当然だと思いますが。 135 名前：128 mailto:sage [2007/03/09(金) 01:14:54 ] あ、またtypoだ Hilbelt→Hilbert 136 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 11:49:13 ] >>134 ＞>>112はHilbertたちの本来の「有限の立場」がこうだ、 ＞という主張なのですから 112にはHilbertの名前は出てこないよ。 128が勝手に「有限の立場はHilbertが言い出したんだから Hilbertの言葉がなければ根拠にならない」とわめいてるだけ。 しかも128は当のHilbertの論文を理解できていない可能性大。 だから馬鹿にされるんだよ。 137 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 11:53:44 ] >>134 ＞Hilbertは明らかに「直接経験」だとか「直観により論理を介さず」など ＞ある種の具体性を要求しています。 ＞それが有限の文字数で書き表せるかどうかというのは別問題です やっぱり数学が判らずに、言葉だけで勝手な憶測しちゃってるな。 ＞＞何が推論として許されるかが有限個の文字数で書き表せ」 ＞というような、「許される推論の説明に要する文字数」について ＞Hilbeltや周囲の人間が何か要求していたというのは ＞聞いたことがありません。 ほら、君、やっぱりHilbertの論文読めてないよ。 138 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:06:23 ] >>134 ＞私は世の中のHilbelt計画に関する文章を全て読んだわけではありませんから もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。 ＞ そもそも、今までに読んだ文献を「全て」挙げろ、というのは ＞幾らなんでも無茶な主張じゃないですか？ 一つも挙げられないのは、いくらなんでもヒドイんじゃないか？ｗ ＞私は>>112と同趣旨のHilbelt計画の説明が書いてあるものを ＞2ch以外で「少なくとも一つ」教えてくれ、といっているだけなので、 ＞出来て当然だと思いますが。 そもそも112は、Hilbertが言ったとはいっていないのだが。 むしろ、Hilbertが言ってることとは違うというなら、 君がHilbertの言葉を引用すべきであって、112にそれを 求めるのは間違ってる。 139 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:07:50 ] 具体的に指摘しないとトンデモの強がりと区別がつかんぞ 思わせぶりじゃなくちゃんと書いたらどうだ？ 140 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:09:06 ] あっ、>139は>137へのレス 141 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:11:05 ] >>139 なに、泣きわめいてるんだ。この馬鹿ｗ 貴様は三歳のガキか。 142 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:13:30 ] >>140 自分でHilbert読め。馬鹿がｗ 143 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:25:36 ] マツシンみたいな奴だな そういう書き方しかできないのならトンデモ扱いされても仕方ないだろう 最初から具体的に書けばすむことなのになあ 144 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:46:38 ] >>143 ＞最初から具体的に書けばすむことなのになあ ほんとだよ115=128=143君ｗ 自己矛盾はマツシン以下の馬鹿だよｗ 145 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 12:48:20 ] ＞そういう書き方しかできないのならトンデモ扱いされても仕方ないだろう ガキって自分にモノを教えてくれないと、 拗ねて相手をトンデモ呼ばわりするよねｗ 146 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 13:33:02 ] まあ君自身がマツシンレベルと理解できたならおれはどうでもいいや 以後は気をつけな 147 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 14:21:21 ] 哲学屋のにおいがプンプンします 148 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 14:54:24 ] 数学も哲学も生齧りの半可通でしょ 149 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 14:57:03 ] >>146 マツシンマニアってキモイ 150 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 14:58:16 ] >>147 トンデモの便臭を漂わすなよ（ｗ 151 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 15:00:00 ] >>148 君は全然不可通だけどな（ｗ 152 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 15:21:00 ] 基礎論スレッドの質問でいいのかなという気もちょっとだけしますが、 Scott位相とか領域理論について丁寧に書いてある本ありますか？ 読書のスピードからいくと、できれば和書がいいのですが、 無いということであれば洋書でも大丈夫です 153 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 15:47:23 ] >>152 自分で探せ 154 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 16:10:37 ] >>153 おすすめがなければ、こいつに突撃かと思ってるんですけど 高いしごっつそうだし、もう少し何か無いものかと・・ www.amazon.co.jp/Continuous-Lattices-Encyclopedia-Mathematics-Applications/dp/0521803381/ref=sr_1_1/503-7608567-7147966?ie=UTF8&s=english-books&qid=1173424058&sr=1-1 155 名前：128 mailto:sage [2007/03/09(金) 19:32:42 ] >>136>>137 いやHilbertじゃなくてBernaysでもAckermannでもNeumannでも良いですよ。 「有限の立場」というのは彼らGoettingenの公理論者の 主義主張を指す言葉だから彼らがそういう主張をしていた、ということでしょう。 一次文献かせめて二次文献くらいの根拠はあるものだと思いましたが。 もう啓蒙書とかブルーバックスとかでも構いませんけど。 竹内外史なんかは多少違った主張をしますけど、 彼の主張はどちらかというと異端的ですし、歴史的にみて明らかに後発で 彼を持って先行者を「本来の立場」ではなかったとすることは出来ません。 「当のHilbertの論文」とは具体的にどれですか？と言ってるのに それに答えられないで読めてないなあ誤解してるなあばかり連発されても困ります。 Hilbertのどの論文を読めてないのかもわかりません。 その論文には表題は付いてなかったんですか？ >>138 ＞もしかして全く読んでないのか？ｗ。それじゃわかるわけないな。 「全て」と言われているのにニ、三冊だけ挙げても答えになっていないし それだけしか読んでないのか、なんて言って莫迦にする人も居るかもしれませんしね。 「たとえばニ三冊挙げるなら」Stanford哲学百科とか岩波文庫の「不完全性定理」とか （きちんと全部読んでないけど）Heijenoortとかまだ一部しか読んでないけどジャキントとかですけど。 あなたが読まれたHilbert計画に関する文献を全部挙げて下さい。 156 名前：128 mailto:sage [2007/03/09(金) 19:33:28 ] ＞Hilbertが言ってることとは違うというなら、君がHilbertの言葉を引用すべきであって 「全ての思考に先立ち直観的に直接経験として存在」 「どうしたって全ての数について試すわけにはいかない。」だとか 「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか 全部Hilbertたちが書いたものそのままの引用なんですよ。 「許される推論の説明に要する文字数」について Hilbertや周囲の人間が何か要求していたことを示す文献は無いと言っているんですが。 112が「本来の有限の立場」とは違うというなら、 112が「本来の有限の立場」を示す分権を引用するべきだと思いますけど 「本来の有限の立場」と言えばHilbertの周囲の者、 もしくはHilbert自身の立場だとみなすのはごく当たり前かと。 それに>>92にも（Hilbertの）有限の立場だとことわってあります。 >>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、 というのにたいして、それは違う、と言ってるのが>>112でしょ。 で、そういう文献は知られていない、というレスに対して 157 名前：128 mailto:sage [2007/03/09(金) 19:35:05 ] 途中で送信しちゃった。 >>93以降の文献つきの根拠ある主張を簡単に初心者向けに言えば>>92になるんじゃないか、 というのにたいして、それは違う、本来はこうだ、と言ってるのが>>112でしょ。 で、そういう文献は知られていない、というレスに対して、 じゃあ>>112を否定する文献を挙げろ、と求めてるのがレスの流れ。 どうして>>112は根拠を挙げなくて良いんですかね。 158 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 19:40:45 ] まだ相手する気なの？ 基礎論スレの初心者？ 159 名前：128 mailto:sage [2007/03/09(金) 20:30:13 ] どういうことですか？ 160 名前：１３２人目の素数さん mailto:sage [2007/03/09(金) 20:50:49 ] マツシンという奴（か“それと同レベルの奴”）が 基礎論関係のスレには永遠に住み着いていて こいつ（ら）と言い争いになったらスルーが基本。 マツシン（かそれと同レベルの奴）が誤りを認めることは 基本的にありえない。人工無能のように必ずレスを返して いつまでも食い下がっては鸚鵡返しで煽り、はぐらかす。 無理に調伏しようとするとスレがぐだぐだに荒れる。 「お前マツシン並だな」と言われたときに 普通人なら「マツシン並なのはお前のほうだ」と言い返すところを 何故か「お前はマツシン以下だな」と返す、などの習性がある。 161 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 00:22:53 ] >>160 横レスですが、大変勉強になりました。ありがとうございます 162 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 01:01:42 ] 有限の立場って怖いね 163 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 10:54:24 ] >>155 112は誰の名前も出していないよ。 「「有限の立場」はHilbertとその仲間のものだ」 という128こそ一次文献でも二次文献でも啓蒙書でも ブルーバックスでもいいから文献名と引用文で 示せばいいが、ドイツ語どころか漢字も読めないかい？ 164 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 11:06:25 ] >>155 ＞竹内外史なんかは多少違った主張をしますけど、 ＞彼の主張はどちらかというと異端的ですし、 ＞歴史的にみて明らかに後発で ＞彼を持って先行者を「本来の立場」ではなかった ＞とすることは出来ません。 >>92のほうが碍子っぽいけどな。 そういえば>>120でも ＞不完全性定理後にHilbertによって修正された立脚点のことを ＞「本来の有限の立場」と言ってるのだとしたら なんて真逆な誤読してるヤシがいたけど、マジで日本語読めないのか？ 165 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 11:14:02 ] >>155 ＞「たとえばニ三冊挙げるなら」 ＞Stanford哲学百科とか ＞岩波文庫の「不完全性定理」とか ＞（きちんと全部読んでないけど）Heijenoortとか ＞まだ一部しか読んでないけどジャキントとかですけど。 じゃ、それぞれの中で君が読んだという箇所を上げてごらん。 岩波文庫もハイエノールトもジャキントもここにあるから 君が読んだかどうかは確認できるよ。さあ、やってごらん。 166 名前：128 mailto:sage [2007/03/10(土) 11:16:55 ] 「「有限の立場」はHilbertとその仲間のものだ」ってどういう意味ですか？ 誰もHilbertたちの占有物だ、とは言ってませんよ。 「「有限の立場」はHilbertとその仲間の提唱したものだ」と同じ意味にとって良いんですかね。 これくらい基礎論では常識だと思ったんですが。 167 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 11:21:08 ] >>156 ＞「全ての思考に先立ち直観的に直接経験として存在」 ＞「どうしたって全ての数について試すわけにはいかない。」だとか ＞「再帰法と有限主義的に存在する総体に対する直観的帰納法」だとか ＞全部Hilbertたちが書いたものそのままの引用なんですよ。 ふーん、つまらない文章を引用するね。 まず、はじめの文章は何も述べていないに等しい。 次の文章はあまりにも自明で、引用するだけ無駄。 問題は最後の文章で、再帰法や直観的帰納法として どこまで考えているかってこと。 168 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 11:24:55 ] >>156 ＞「許される推論の説明に要する文字数」について ＞Hilbertや周囲の人間が何か要求していたことを ＞示す文献は無いと言っているんですが。 だから無限に書き続けていいというのが 「不完全性定理後に修正された立脚点」 であって、ゲーデルにバカにされたこと なんだがな。 169 名前：128 mailto:sage [2007/03/10(土) 11:45:22 ] >>166の通りに解して良いんですね。じゃあ文献名つきで論拠を。 ＞The consistency proof itself was to be carried out using only what Hilbert called "finitary" methods. ＞On the conceptual side, ＞the finite standpoint and the strategy for a consistency proof were ＞elaborated by Hilbert (1928); Hilbert (1923); Hilbert (1926) and Bernays (1928b); ＞Bernays (1922)</a>; Bernays (1930), ＞of which Hilbert's article "On the infinite"(1926) ＞provides the most detailed elaboration of the finitary standpoint. ・Hilbert, David, 1928 Die Grundlagen der Mathematik", Abhandlungen aus dem Seminar der Hamburgischen Universität, 6: 65-85. ・Hilbert, David, 1923, "Die logischen Grundlagen der Mathematik", Mathematische Annalen, 88: 151-165. Lecture given at the Deutsche Naturforscher-Gesellschaft, September 1922. Reprinted in Hilbert (1935, 178-191). ・Hilbert, David, 1926, "Über das Unendliche", Mathematische Annalen, 95: 161-90. Lecture given Münster, 4 June 1925. ・Bernays, Paul, 1928b, "Zusatz zu Hilberts Vortrag über "Die Grundlagen der Mathematik"", <em>Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg, 6: 88-92. ・Bernays, Paul, 1922</a>, "Über Hilberts Gedanken zur Grundlegung der Arithmetik", Jahresbericht der Deutschen Mathematiker-Vereinigung</em>, 31: 10-19. ・Bernays, Paul, 1930</a>, "Die Philosophie der Mathematik und die Hilbertsche Beweistheorie", Blätter für deutsche Philosophie, 4: 326-67. Reprinted in Bernays (1976, 17-61). plato.stanford.edu/entries/hilbert-program/ これで満足？ 170 名前：128 mailto:sage [2007/03/10(土) 11:59:45 ] >>167 別にその文章で「有限の立場」がどういうものか完璧に分かるって言ってんじゃないですよ。 Hilbertの別の著作から普通に解釈すれば原始再帰算術になるって何十年か昔から言われてるし、 その解釈に対する議論も為されてるじゃないですか。それで何が問題が？ >>92の「有限の立場」の大雑把な説明は上から五番目のpdfから ほぼそのまま取ってきたものですけど、著者はPRAくらい当然知ってて その大雑把な説明を与えているんだと思いますけど。 誰もあれが完璧な説明だなんて思ってないでしょう。 >>112だと超数学のレベルでどんな抽象的でよく訳の分からないidealな対象でも 使って良いことになりますよね。例えば自然数の任意の部分集合とか。 証明が正しいことは有限的に判定できますから。 一方で超数学における推論の説明には普通一般に言われてるよりもきつい条件を貸すことになる。 どんなに具体的でrealで、誰もがよく知っているようなものでも、 よく説明出来ないものは使っちゃいけないことになる。 そんなことHilbertが言っていましたか？ 無限に続けるってのは、多分、何が許される推論か、Hilbertが無限に説明を続けるんじゃなくて 「有限ステップの操作で検査可能である」の方に反するんじゃないですか？ 具体的にどの文献のどこのなんと言う文言か教えてくれるつもりがないようなので確かめようが無いんだけど。 171 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:02:57 ] >>170 ＞>>112だと超数学のレベルでどんな抽象的でよく訳の分からない ＞idealな対象でも使って良いことになりますよね。 112にはそんなことは全く書いてないが。 ＞例えば自然数の任意の部分集合とか。 ＞証明が正しいことは有限的に判定できますから。 やっぱり日本語がまったく読めない人なんだな。 自然数の任意の部分集合全体なんて、 有限個の文字数で書き表わせないが。 ああ「有限個の文字数で書き表わす」と言う場合の 有限個は文字の種類数ではなく、例えば「２００字以内で書け」 という意味の純然たる字数のことである。 172 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:05:15 ] >>170 ＞無限に続けるってのは、多分、何が許される推論か、 ＞Hilbertが無限に説明を続けるんじゃなくて ＞「有限ステップの操作で検査可能である」の方に ＞反するんじゃないですか？ 見苦しい言い訳だな。バカなんじゃないのか？ 173 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:08:02 ] >>169 ＞On the conceptual side, ＞the finite standpoint and the strategy for a consistency proof were ＞elaborated by Hilbert (1928); Hilbert (1923); Hilbert (1926) and Bernays (1928b); ＞Bernays (1922)</a>; Bernays (1930), ＞of which Hilbert's article "On the infinite"(1926) ＞provides the most detailed elaboration of the finitary standpoint. これが「有限の立場」がどういうものか完璧に分かる文章なのかい？ バカなんじゃないのか？ 174 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:18:18 ] >>160 ＞誤りを認めることは基本的にありえない。 ＞人工無能のように必ずレスを返して ＞いつまでも食い下がっては鸚鵡返しで煽り、 ＞はぐらかす。 128だな。二言目には文献とわめき サルでもできる検索の結果をどうだと ばかりにひけらかす。まったく恥かしい。 ＞無理に調伏しようとするとスレがぐだぐだに荒れる。 「調伏」なんて聞いたことがないので、 もしかして朝鮮語かと思って検索したら、 「加持や祈祷を用いて、悪霊や物の怪を屈服させること。」 なんて奇怪な意味の言葉らしい。 やっぱり数学よりも妖怪に詳しいオカシナ奴らしいな。 175 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:27:28 ] >>170 ＞超数学における推論の説明には普通一般に言われてるよりも ＞きつい条件を貸すことになる。 ＞どんなに具体的でrealで、誰もがよく知っているようなものでも、 ＞よく説明出来ないものは使っちゃいけないことになる。 なんかまったく見当違いなことをいってるな。 半可通を笑う四半可通、といったところか。 もちろん、1/2よりも1/4のほうが小さい。 176 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 15:51:10 ] >>170 ＞>>92の「有限の立場」の大雑把な説明は ＞上から五番目のpdfからほぼそのまま ＞取ってきたものですけど、 >>102では「照井一成先生のpdf」と自慢げに名前を出してたがｗ で、しかも、>>92を見ると ＞ぐぐって出て来たので一部ちょっとだけ参考にさせて貰いました。 なんて臆面もなく書いてるね。 上記のpdfを拝見したが、そもそも碍子チックな臭いが プンプンするわけで、92の説明もそういう立場を理解した 上で読まないと間違う。 ０を正当化するのに１、１を正当化するのに２・・・ とつづけていって、１も２も・・・も全部有限だからＯＫ みたいな屁理屈は、体系の強さの順序付けとかいう後から 出てきた御利益を除けば、本来の無矛盾性証明の目的を 全く達成していない点で無意味。 177 名前：１３２人目の素数さん mailto:sage [2007/03/10(土) 16:10:53 ] 碍子もテリーも、ゲンツェンのカット消去の”魔法”に 幻惑されてるように思える。 カット消去は数学的には興味深いが、哲学的な基礎付けの問題を 解決するようなものではない。 岡田光弘氏も現代思想の「ゲーデル」特集号の中で、 ゲーデルの不完全性定理から考えてカット消去は 正しいとしても体系内では証明できないことが 明らかであり、竹内外史は竹内予想を提出する際 この点について”楽観的”だったのではないか と指摘している。 178 名前：128 mailto:sage [2007/03/10(土) 22:05:48 ] >>171 使っていけない、と書いてない以上>>112の条件さえ満たされたら 使って良いと考えるのはごく当然だと思うけど。 ＞自然数の任意の部分集合全体なんて、 ＞有限個の文字数で書き表わせないが。 「書き表せる」ってのは何のことを言ってるんですかね。 一つ変数を用いれば自然数の任意の部分集合なんて いくらでも表記のしようがあると思いますが。 例えば「偶数全体の集合」（七文字）だとか円周率だとかは 有限の文字数で書き表せるの？そうじゃないの？ 「偶数全体」は書き表せないから、「偶数」という概念は使っちゃ駄目ってことなんですか？ >>173 >>163で「有限の立場」がHilbertやその周囲の人物の提唱した立場であることを 示せとか言い出すから根拠を書いたんですが。 本当はこんなこと常識以外の何ものでもないと思うけど。 「有限の立場がHilbertのものだとは言ってない」とやたら強調されてたけど Hilbert以外の誰が提唱したとおっしゃるんですかね。 ＞どうだとばかりにひけらかす。 自分で文献を挙げろと言っておいてそりゃないだろう。自分が何言ったか覚えてないのか？ ＞もちろん、1/2よりも1/4のほうが小さい。 はあ？ 179 名前：１３２人目の素数さん [2007/03/10(土) 22:36:56 ] 定年退職後に数学博士号　大阪大の７１歳男性 www.chunichi.co.jp/flash/2007031001000102.html 180 名前：１３２人目の素数さん [2007/03/11(日) 06:18:40 ] 何々世代まえの人数を出す方程式が知りたいんですがどなたか知っていますか？ 181 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 09:32:45 ] >>180 それと基礎論と何の関係が? 182 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 10:41:10 ] >>112 >>115 >>119 >>120ときてその後いきなりgdgdになりはじめたな 120までは普通の流れなのに なんで文献名が出ないんだ？ 183 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 10:42:01 ] 「質問スレッド」で検索して最初に見つかったスレに突撃する人が どこの板にもいるものだ。「基礎」とか書いてあるしｗ 184 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 13:43:50 ] >>182 文献文献と＊＊の一つ覚えで騒ぐ＊違いか 185 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 13:52:46 ] >>178 128は形式化が全く理解できていない四半可通 186 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 14:21:48 ] 551 187 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 15:15:53 ] 結局>>112の >本来､有限の立場とは、何が推論として許されるかが >有限個の文字数で書き表せ、有限ステップの操作で >検査可能である、という主張。 これって本当なの？ 一連の流れは 「本来」って書いてるぐらいだから有限の立場を唱えていた学者のうちの誰かがそれを唱えてたんでしょ？ それは誰よ？ って質問なんじゃないの？ 188 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 16:41:42 ] >>187 自分の主張を逸脱といわれて逆上し ＊＊の一つ覚えを繰り返す＊違い 189 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 17:03:15 ] >>111 ＞ゲーデルの不完全性定理の証明で原始帰納関数からｼｺｼｺ始めてるのは、 ヒルベルトの弟子であるアッカーマンが実質的に PRA（原始帰納的算術）を有限の立場と考え、 その無矛盾性を「証明」していたから。 （「不完全性定理」岩波文庫ｐ229） ただし上記の文献にもあるように、上の「証明」は 実際には超限帰納法を用いている。 実際、不完全性定理から明らかなように、 PRA自身の無矛盾性はPRAでは証明できない。 190 名前：128 mailto:sage [2007/03/11(日) 21:22:19 ] Derivability ConditionってPRAで証明できましたっけ。 と思ってぐぐったら出来るっぽいですね。 しかし文献を示せというから言われた通り示したら 「どうだとばかりにひけらかす」とか言われてビックリしたよ 何かの罠みたいなもんだったのかなー 自然数の無矛盾性証明なんて別にGentzenに限らず 多くの人が行っていて、何通りもある。 ただ「有限の立場」はHilbertの書きものを素直に読めばPRAとほぼ同一視でき、 全ての証明はPRAを逸脱した立場で行なわれているから Hilbert計画の達成とは見做されない、それだけの話なのにね。 >>112は多分そういうことを知らないんだろうけど、 Gentzenの自然数論の無矛盾性証明を 「有限の立場で認められる無矛盾性証明」から排除するために 「本来の有限の立場」なんてのを後付けでデッチアゲてしまっているんだろう。 それでいて後から主張を翻したHilbertを批判してるんだから御目出度いものだ。 だからHilbert学派がそういうことを述べていたソースを出せ、と言われても 答えられないし、挙句の果てには「有限の立場」はHilbertたちのものじゃない、 などと馬鹿げたことを言い出す。 きっと「本来の有限の立場」なるものは「オレ流・真・有限の立場」な感じで >>112の脳内のなかにしかないんでしょ。 191 名前：128 mailto:sage [2007/03/11(日) 21:29:52 ] しかし結局>>160の言うとおりになってしまったなあ、 素直に>>160の言うことを聞いておけば良かった。 スレ汚し申し訳ない。 192 名前：１３２人目の素数さん mailto:sage [2007/03/11(日) 21:55:03 ] お疲れさん 193 名前：１３２人目の素数さん mailto:sage [2007/03/12(月) 01:15:11 ] 何だよ結局>>111が答えってことかよ 194 名前：１３２人目の素数さん mailto:sage [2007/03/12(月) 08:04:03 ] ＞きっと「本来の有限の立場」なるものは「オレ流・真・有限の立場」な感じで ＞>>112の脳内のなかにしかないんでしょ。 なるほど納得 >>112も始めから「『俺が思うに』有限の立場とは本来こういうものなんだよ！」 て書けばいいのに 195 名前：１３２人目の素数さん mailto:sage [2007/03/12(月) 09:42:11 ] >>190 ＞自然数の無矛盾性証明なんて別にGentzenに限らず ＞多くの人が行っていて、何通りもある。 ＞ただ「有限の立場」はHilbertの書きものを素直に読めば ＞PRAとほぼ同一視でき、全ての証明はPRAを逸脱した立場で ＞行なわれているからHilbert計画の達成とは見做されない、 ＞それだけの話なのにね。 やっぱり肝心なことがわかってないな。 超数学で元の体系より強いものを使ったらダメなんだが。 有限の立場は「内容的な数学」だとかいうのは、 不完全性定理以後では、そういう無茶を押し通すための 強弁に成り下がってしまった。 196 名前：１３２人目の素数さん mailto:sage [2007/03/12(月) 09:50:24 ] >>190 ＞Gentzenの自然数論の無矛盾性証明を ＞「有限の立場で認められる無矛盾性証明」から排除するために ＞「本来の有限の立場」なんてのを後付けでデッチアゲて ＞しまっているんだろう。 Gentzenの「証明」の問題点は、有限の立場とかいう以前に 対象理論では定義してないことを、後だしジャンケンのように 超数学の理論で持ち出していることにある。 「超限帰納法だって定義できるからいいだろう」というかも しれないが、そうやって、後だしジャンケンを無限につづければ いいという発想で、全体をなし崩しに正当化するのは、結局有限の 立場自体を否定するものである。 197 名前：１３２人目の素数さん [2007/03/14(水) 12:12:28 ] なんか重い空気のなかすみません 自然演繹で ∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である （ただし、∃ｘA（ｘ）はaを含んではいけない）、というのは、 例えば、 ∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか ∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから、きっと、ｓ０と０は別物で、ｓ０は入れていいのだ、と勝手な判断をして導出を続けていったら、 いろいろなものがでてきて、ちょっと今、困ってます 198 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 14:19:05 ] >>197 > ∃ｘ（０＋ｘ＝ｘ）から（０＋０＝０）を出してはいけないのはもちろんのこと、（０＋ｓ０＝ｓ０）も（０＋ｓｓ０＝ｓｓ０）も出してはいけません、ということですか これ自体は正しいけど、その前の部分とこのことをあなたがどうやって関係付けたのかわからない > ∃ｘ（０＋ｘ＝ｘ）から（０＋１＝１）は出してよいのだから よくないよ もしかして∃と∀を混同してない？ 199 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 14:22:07 ] 一つ確認 > ∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら ここの a は変数？ 200 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 15:47:09 ] すみません 書き方が良くなかったです 前のはなかったことにして、 定項（数項）０、１、２、・・・があって 関数記号ｓがなし、 関数記号＋があって、 ∃ｘ（０＋ｘ＝ｘ）が導出可能で ０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメですか？ ということでした 201 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 16:21:19 ] >>200 普通の自然演繹の体系ならダメ 202 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 17:27:00 ] 関数記号を含んだ項の扱いかたがいまひとつよくわからないのですが、 例えば、 ＝除去規則 ｓx＝ｓxとx＝０＋xが導出可能であるならばｓ（０＋x）＝ｓxが導出可能である、というような代入のしかたはOKでしょうか 203 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 18:27:17 ] >>202 導出自体は問題ないと思うけど、 1. = の除去規則 2. その規則をどう使ったら sx=sx, x=0+x から s(0+x)=sx が出るのか を正確に書ける？ 204 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 18:52:59 ] そのまま １＝除去規則 A（a）とa＝bが導出可能であるならばA（ｂ）が導出可能である、（A(ｂ）はA（a）のaのところを（全部でなくてよい）ｂにおきかえたもの よって２ としたのではまずいでしょうか 205 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 20:48:03 ] >>204 よさそうだけど一応確認を。 2 で A(a) に対応する論理式と b に対応する項は？ 206 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 23:05:31 ] A(a) に対応するのがsx=sxでb に対応するのが0+xだと思いますが ところで >>201 ∃ｘ（０＋ｘ＝ｘ）が導出可能で ０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ ということなので >>１９７ の、 >（ただし、∃ｘA（ｘ）はaを含んではいけない） は（ただし、∃ｘA（ｘ）はaに含まれる項を含んではいけない のようなことになるのでしょうか 207 名前：１３２人目の素数さん mailto:sage [2007/03/14(水) 23:20:38 ] >>206 どこでおかしくなってるのか分かったような気がする。 あなたの知っている∃除去規則を正確に述べてみてください。 208 名前：１３２人目の素数さん mailto:sage [2007/03/15(木) 20:10:17 ] >>204 等号に関する公理（equality axiom）というのがあります。 教科書などの、この公理に関する記述を参照。 あと∃の除去則（∃-elimination）のところも要復習。 要は>>207さんの言う事を良く聞きましょう、という事で。 209 名前：ご迷惑をおかけしました mailto:sage [2007/03/16(金) 09:14:00 ] ０変数関数記号を定数と呼ぶ ∃ｘA（ｘ）が導出可能で、A（a）を仮定して⊥（矛盾）が導出可能であるなら（A（a)→⊥（矛盾）が導出可能であるなら）⊥が導出可能である （ただし、∃ｘA（ｘ）はaを含んではいけない） aは新しい定数 ∃ｘ（０＋ｘ＝ｘ）が導出可能で ０＋（０＋１）＝（０＋１）を仮定して⊥を導出できれば、⊥を導出可能、という導出はダメ ０＋１は定数ではなくて項だからダメ でした。 210 名前：１３２人目の素数さん mailto:sage [2007/03/16(金) 13:11:05 ] aって新しい"定数"なの？変数じゃないの？まあ、新しい定数を言語に導入してしまうってのもありかもしれんけど。 もしかしてそこらへんにわかってない原因があるんじゃないの？ちなみに ＞０＋１は定数ではなくて項だからダメ これはとてもとんちんかんに感じる。 211 名前：１３２人目の素数さん mailto:sage [2007/03/17(土) 15:52:05 ] なんかいまいち良く分かってないみたいだなあ、、 まあ良いや 212 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 16:38:34 ] 先週買った本、郵便屋さんキター！！ 読むべし、読むべし 　　　　集合の本？　ボコボコにしてやんよ 　 ∧＿∧ 　 (　･ω･)＝つ≡つ 　 (っ　≡つ＝つ 　 /　　　) ﾊﾞﾊﾞﾊﾞﾊﾞ 　( /￣∪ 2ch-news.net/up/up50539.jpg 213 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 17:05:29 ] 古本屋さんか？ よく手に入ったね しかし田中をこれから読むのにカナモリさんも一緒に買うとはなかなか 214 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 20:06:50 ] それは俺も思ったが こういうのは手に入るときに手に入れておこう 215 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 20:08:12 ] というかｸﾞｯｼﾞｮﾌﾞ 216 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 20:51:14 ] つ図書館 217 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 21:31:45 ] まあ英語版の二版は手に入るみたいですけどね （邦訳は初版） KunenとかJechがまだ訳書出てないのに意味無いよね、はっきり言って 218 名前：１３２人目の素数さん mailto:sage [2007/03/19(月) 23:37:08 ] それは言えた 219 名前：１３２人目の素数さん mailto:sage [2007/03/20(火) 16:05:22 ] set theory? 今や時代はsubstructural logicだYO! 220 名前：１３２人目の素数さん mailto:sage [2007/03/20(火) 17:14:11 ] それはさすがにない 221 名前：１３２人目の素数さん mailto:sage [2007/03/21(水) 17:02:09 ] 220は世間知らず 222 名前：１３２人目の素数さん mailto:sage [2007/03/21(水) 21:24:43 ] あほか 223 名前：１３２人目の素数さん mailto:sage [2007/03/21(水) 22:13:46 ] "世間"が構成可能集合でなければ、知らなくてもどうということもない　ノ 224 名前：１３２人目の素数さん [2007/03/22(木) 10:11:39 ] >>223 集合論研究者のいう世間とは、同業者の集まりことらしい 225 名前：１３２人目の素数さん mailto:sage [2007/03/22(木) 12:10:23 ] 烏合の衆 226 名前：KingOfUniverse ◆667la1PjK2 [2007/03/22(木) 12:19:15 ] 人の脳を読む能力を悪用する奴を潰せ。 227 名前：１３２人目の素数さん mailto:sage [2007/03/22(木) 23:17:33 ] 最先端の研究テーマは何ですか？ 228 名前：１３２人目の素数さん mailto:sage [2007/03/23(金) 01:14:07 ] なんか４分冊のごつい本でたね 229 名前：１３２人目の素数さん mailto:sage [2007/03/23(金) 10:59:27 ] >>228 どんな本？ 230 名前：１３２人目の素数さん mailto:さげ [2007/03/23(金) 12:07:46 ] >>228 わしも聞きたい 231 名前：１３２人目の素数さん mailto:sage [2007/03/23(金) 13:40:28 ] >>77のかな？ 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