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

1 名前：１３２人目の素数さん mailto:sage [2007/02/04(日) 19:22:39 ] 立てます。 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