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

1 名前：1 [04/10/13 18:26:50] 数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。 ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。 さて、私の質問ですが、 『論理学をつくる』という本の、一階述語論理の公理系の例のところに、 公理として、　∀ξ（ξ=ζ）　　　ξ、ζは個体変項をあらわす図式文字 というものがあがっていました。 公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。 どなたか、わかる方、お教えください。 357 名前：１３２人目の素数さん [2005/04/28(木) 21:26:03 ] 高校の数学の教科書を見ていると、ＡとＢの掛け算を Ａ×Ｂ と書かずに Ａ・Ｂ と書かれてるのですが、「×」と「・」は同じ意味と考えて良いのでしょうか？ また、なぜ二種類の書き方があるのでしょうか？ ご存知の方教えて下さい。お願いいたします。 358 名前：１３２人目の素数さん mailto:sage [2005/04/28(木) 21:57:21 ] >>353 野矢「論理学」の該当部分を眺めてみました。 この本では Pr(x) の定義を与えていないので、証明できるわけがないですね。 この箇所まで読んだ時点では、想像をたくましくしても無駄です。 「数学基礎論講義」なり、前原「数学基礎論入門」を読むことをお薦めします。 359 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 05:17:45 ] 田中さんて人が書いてる本をもう一冊かりてきて読んでたら、なんか解決しました。 >>357 スレ違いです。 数学基礎論は「数学の基礎」ではありません。 とのことです。 数学基礎論的に言えば、 算術の言語の語彙としてのそれなら、混乱が避けられているかぎり、 ×や・に替わって、＄でも￥でも好きなものを使ってかまわないと思います。 360 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 10:19:19 ] 「数学の基礎をめぐる論争」　(^-^;) 361 名前：１３２人目の素数さん [2005/04/29(金) 12:08:52 ] 数学基礎論は数学の基礎だよ. しかし基礎の数学ではない. 362 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 12:19:57 ] まあそれは言い方の問題じゃないですか？ ただ、初等数学とはあまり関係のない、 数学の一分野であることは確かですね。 数学基礎論とは何か、と言うとまた 難しい問題になりますけど 363 名前：１３２人目の素数さん [2005/04/29(金) 12:55:06 ] 「数学基礎論は時代の関数」と言ったの誰だっけ？ 364 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 12:59:06 ] Atiyah たしか厳密性は時代の函数 365 名前：１３２人目の素数さん [2005/04/29(金) 13:58:52 ] 物理のコンセプトを用いている数学者達に対する 厳密性云々というのは、数学基礎論とは別カテゴリー？ 366 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:01:25 ] 小数第2位を四捨五入すると　2.55　は2.6になるのでしょうか？それとも3ですか？ 367 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:06:59 ] >>366 >>310 368 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 14:09:33 ] >>367 すみませんでした。 369 名前：べーた　LVβ5　402 403 407 410 [2005/04/29(金) 15:03:34 ] >>368 いいですよ 370 名前：１３２人目の素数さん mailto:sage [2005/04/29(金) 15:05:30 ] 荒らすな 371 名前：べーた　LVβ5　402 403 407 410 [2005/04/29(金) 15:06:36 ] >>370 そうですよ！ 372 名前：１３２人目の素数さん [2005/05/01(日) 00:49:06 ] ＞365 微妙です。 373 名前：１３２人目の素数さん [2005/05/03(火) 19:26:23 ] ラッセル、ノイマン、コーエン、後世に残したインパクトの大きさでは 誰が一番？ 374 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 22:49:20 ] 基礎論ならラッセル，集合論ならコーエン， 経済学とか解析学とかならノイマン． 他分野の人間を比較するのは， 極端なことを言えばアインシュタインとトロツキーは どちらが強い影響を及ぼしたか，とかと同じくらい意味が無いような 375 名前：１３２人目の素数さん [2005/05/03(火) 23:04:50 ] ＞374 恐縮です。 ノイマン、コーエンも数学基礎論に貢献した人物かと思っていました。 376 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 23:33:52 ] ノイマンもいくらか仕事はしてるけど， 基礎論に関する限り，それほど大きな仕事はしてないような （弱い算術の無矛盾性の証明とかだったような． ほかは不勉強で知らない．） たしかにforcing知ってれば再帰函数論とかで有利みたいですけど 基礎論は必ずしも集合論を知らなくても出来ますし， ACは十分自然な公理であって，ACの独立性など あまり重要ではない，という人も居ます． また，ノイマンの階層論理も，ロジックプロパーな人は よく使うみたいですから，どっちがインパクトが大きいとも言えないかと． 377 名前：１３２人目の素数さん [2005/05/03(火) 23:46:20 ] ＞376 なるほど。 ご教示いただき感謝します。 378 名前：１３２人目の素数さん mailto:sage [2005/05/03(火) 23:52:53 ] あ，ごめん ノイマンの階層論理じゃなくてラッセルの階層論理です． 訂正 379 名前：１３２人目の素数さん [2005/05/04(水) 00:06:06 ] 幼稚な質問ですが、教えてください dx/dtの読み方・書き順ですが 読み方、dx dt 書き順も分子から dx / dt となるのは、どうしてですか？ おねがいします。 380 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 00:10:52 ] >>379 >>310参照 ◆ わからない問題はここに書いてね １６３ ◆ science3.2ch.net/test/read.cgi/math/1114465980/ にレスします． 381 名前：１３２人目の素数さん [2005/05/04(水) 01:13:22 ] >>376 クラス概念の導入が基礎論にとって大きな仕事でないというならば そうだろうね。 382 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 01:44:46 ] >>381 それならベルナイスも少なくとも同程度に 評価すべき． 383 名前：１３２人目の素数さん mailto:sage [2005/05/04(水) 04:13:34 ] >>382 GBN を GN と書かれてベルナイスの泣きが入ったというエピソードもあったね。 384 名前：１３２人目の素数さん [2005/05/04(水) 18:43:41 ] ∀x(P(x)->Q(x))->(∀xP(x)->∀xQ(x)) ∃x(P(x)->Q(x))->(∃xP(x)->∃xQ(x)) これは二つとも成立しますよね？ 385 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 08:06:13 ] ＞384 ２番目の式は、Ｐ が１箇所だけ真、Ｑ が全部偽な場合を考えてみるべし 386 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 08:12:51 ] 1箇所Pを偽にしとくのも忘れずにねー 387 名前：１３２人目の素数さん [2005/05/05(木) 12:35:21 ] 不完全性定理の一般向け啓蒙書としては、「ゲーデル・エッシャー・バッハ」 が傑作？ 388 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 14:20:38 ] あれって不完全性定理に関してそこまで 書かれているわけじゃないような というか，不完全性定理スレが荒らされていてびっくり 389 名前：１３２人目の素数さん mailto:sage [2005/05/05(木) 15:48:53 ] >>385-386 わかりました。ありがとうございます。 390 名前：１３２人目の素数さん [2005/05/09(月) 15:14:12 ] 誰か教えてください。 本に、次のように書いてあるのですが、よくわかりません。 原始式から命題結合記号と有界量化記号∀ｘ＜ｔ、∃ｘ＜ｔだけを使って作られる論理式を有界な（bounded)論理式と呼ぶ。 ここで∀ｘ＜ｔは∀ｘ（ｘ＜ｔ→・・・）、∃ｘ＜ｔは∃ｘ（ｘ＜ｔ∧・・・）の省略形で、ｔはｘを含まない項とする。 はじめ、普通の量化子∀ｘになんらかの制限を課したものかな、くらいに思ってたのですが、上の説明文の２行目の意味がよくわからなくて、こんがらがってます。 （「∀ｘ＜ｔは∀ｘ（ｘ＜ｔ→・・・）の省略形で」というのがよくわかんないんですが、 ∀ｘ＜ｔ（普通の論理式の形をしたもの）と表記されている論理式が、∀ｘ（ｘ＜ｔ→・・・）（ふつうの論理式の形をしたもの）ということでは、おそらく、ないはずで、 ということは、別のことを言ってるはずなんですが、その内容がいまひとつよくわからない・・） 391 名前：１３２人目の素数さん mailto:sage [2005/05/09(月) 15:37:33 ] 例えば ∀x＜t ( Fx ∨ Gx ) は ∀x ( x＜t → ( Fx ∨ Gx )) の省略形 392 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 00:09:33 ] ありがとうございました。わかりました。 にしても、何故略記？とか、考えてるんですが、 なんか意味があるんでしょうね 393 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 05:52:58 ] ∀x(x<t→P(x)) は、「全てのxについて、xがtより小さいならばP(x)が成り立つ」 ∀x<t(P(x)) は、「tより小さい全てのxについてP(x)が成り立つ」 と読み下せるけど、両者は同じ意味になる。 394 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 12:48:53 ] >>392 何を悩んでるのかがよくわからん。 なぜ ∀x＜t を、基礎的な量化子ではなくて略記法という ことにするのか、ってこと？ ∀x を使って同じ意味の表現を与えられるんだったら 基礎的な記号の数を増やす意味があまりない。 というかこの場合はかえって有害。 ∀x＜t を言語に含まれる無定義の記号ということすると、 「引数をとる量化子」なんて新しいカテゴリを導入しなくては ならなくなるし、完全性やらのメタ証明でチェックする項目が 1個無意味に増える。 一方、理論の中じゃなくてメタのレベルで略記してるだけ、 ってことにすればメタ定理の証明では無視できる。 古典論理の文脈では、∀x＜t だけじゃなく、∃x と ∀x の 一方を他方で定義した略記法として処理することも多い。 395 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 14:56:25 ] 例題みたいなのの内容を眺めている最中なんですが、 ド･モルガンの法則は使えるんですね、これ ¬（∃y＜ｘ¬Pｙｎ） で ∀ｙ＜ｘPｙｎ みたいなかんじで、 略記したものなんだろうけど、扱いは、なんか基礎的な量化子っぽいですね。 ¬（∃y＜ｘ¬Pｙｎ） ¬（∃y（ｙ＜ｘ∧¬Pｙｎ） ∀y（¬（ｙ＜ｘ）∨Pyn） ∀y（ｙ＜ｘ→Pyn） ∀ｙ＜ｘPｙｎ か 396 名前：１３２人目の素数さん mailto:sage [2005/05/10(火) 15:02:19 ] ついでに質問させてください。 自分が、この有界量化記号∀ｘ＜ｔ、∃ｘ＜ｔというのに不案内なのも関係しているんだと思いますが、 ある関係Aはロビンソン算術に不等号を加えた公理系において、∃ｘ（θ1ｘｚ∧∃ｙ＜ｘθ2ｙｚ）・・・�@によって表現される。 というときの、�@がでてくる脈絡がよくわかりません。 Aが成り立たない、の出発点になるところの ¬∃ｘθ1xｎ∧∃ｙθ2ｙｎ・・・�A これは文意が読み取り易いんですが、 それに対応する、 Aが成り立つ、の出発点になるところの ∃ｘ（θ1ｘｚ∧∃ｙ＜ｘθ2ｙｚ）・・・�@ というのが、なんでこういうことになってんのかが、よくわかりません。 〜より小さい、というのが、どこから出てきて、なんで必要なんだろう、ということがわかりません。 397 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 09:43:13 ] >>392 例えば、このような表記は日常的な推論を記号化する場合などに便利。 日常で「すべて」とか考える場合に、その世の中にあるありとあらゆるもの全てを 想定して考える場合はまれでしょ？なんらかの範囲のなかで「すべて」を 考えている場合が多いはず。 あらかじめたくさんの種類の量化子を導入するタイプの論理は、 many-sorted logic とよばれる。ぐぐってみ。 >>393 の言う通り、一般の一階述語論理の中では解消可能とされるが、 いろいろ面白い性質があるらしいぞ。 398 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 12:08:29 ] >>396 数論の場合は、有界の量化子が成り立つかどうかは 必ず有限の時間で判定がつくでしょ。 有界でなければそうとは限らない。 後々、その述語の判定のしやすさを扱うときに、 量化子が有界かどうかは重要になってくるよ。 399 名前：１３２人目の素数さん [2005/05/11(水) 12:46:29 ] ここ数日間、本を読んでてよくわからなくなった部分周辺を見回していますが、 ∀x<t >>393 のような意味で用いられてるみたいですね ここにくるまで、そういう表現が特に必要がなくて、で、いまだに、どうして、こういう表現が必要なんだろう、というところで、ぐるぐる混乱しています。 >>396のはなかったことにして、 ロッサーの可証述語というものについて、誰か教えてください。 Pr'（ｘ）≡∃ｙ（Prov(y,x)∧¬∃ｚ＜ｙDispr(z,x)) Pr'（φのゲーデル数の数項）で、意味は、 「ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも¬φの証明ではない」ということらしいですが、 なんで、〜より小さなもの、ということを言わなければいけないのか、がわかりません。 「ある論理式φの証明があって、ある¬φの証明は無い」ではだめなのでしょうが、その理由がよくわかりません。 400 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 12:56:08 ] >>398 レスついてんの気が付きませんでした・ とすると、ロッサーの可証述語というやつも、そういうことからの要請なんですかね 401 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 14:01:23 ] > ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも¬φの証明ではない それは読み間違いです。 402 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 14:12:11 ] >>400 > とすると、ロッサーの可証述語というやつも、そういうことからの要請なんですかね ええと、それは、ちょっと関係なくて、 ゲーデル文を改良するためのトリックです。 403 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 16:24:20 ] Pr'（ｘ）≡∃ｙ（Prov(y,x)∧¬∃ｚ＜ｙDispr(z,x)) これだけを見ると、よく文意がわからないんですよね ∃ｙが全体にかかってて、で、∃ｚ＜ｙってのは、例のごとくなんかの省略なわけで、ｙが縛られているのかどうかもよくわかんねえし（有界量化子ってなんだよ、という上の質問もここらへんの関係から） ということは、コレ自体がなんかの目的で作られたというよりは、なんかを変形して流れ着いたのが、これなんじゃないか、というように勘ぐってたら、 今、『数学基礎論講義』という本を読んでるんですが、 ＞Pr'（ｘ）≡∃ｙ（Prov(y,x)∧¬∃ｚ＜ｙDispr(z,x)) の意味は、 ＞「φの証明ｙがあって、ｙよりゲーデル数が小さなものはどれも¬φの証明ではない」 とあって、 ふ〜ん、そうなんだ、と、よくわかんないまま、そのまま引用したのが >>399 の書きこみです。 >>402 もうひとこと、さらなる書きこみ、ﾏｯﾃﾏｽ 404 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 18:53:57 ] >>403 ごめん、読みはそれであってますわ。 詳しくは nl.ijs.si/~damjan/Rosser.html でも読んでね。 405 名前：１３２人目の素数さん mailto:age [2005/05/11(水) 21:43:11 ] 集合α1,i⊇0,を命題論理における複雑さi以上の論理式集合全体の集合と定義し、 A={a0,a1,a2,…}と定義する。 このとき∩Aは命題論理におけるどんな論理式全体の集合になるか分かる人います？？ 406 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 21:47:02 ] いない。バイバイ 407 名前：１３２人目の素数さん mailto:age [2005/05/11(水) 23:33:11 ] >>405 |│　／ |￣＼ |− ﾟ ）─ |＿／ |∧　＼ |−ﾟ） |∧∧ | ﾟ−ﾟ）　ｿｰ |⊂/ 【解説＆解答随時受付中】 408 名前：１３２人目の素数さん mailto:sage [2005/05/11(水) 23:36:02 ] いないっつってんだろ。かえれ無礼者 409 名前：１３２人目の素数さん mailto:sage [2005/05/12(木) 00:39:11 ] >>405 空集合じゃないの？ 410 名前：１３２人目の素数さん [2005/05/12(木) 01:34:28 ] 内積ベクトル空間の任意のベクトルaに対してa0=0になることを証明せよ。この当たり前の事をどう証明していいかわかんないんです、、、お願いします 411 名前：１３２人目の素数さん mailto:sage [2005/05/12(木) 01:43:58 ] マルチさん乙！ 412 名前：１３２人目の素数さん [2005/05/13(金) 20:07:30 ] 数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い数学嫌い 413 名前：１３２人目の素数さん [2005/05/15(日) 17:04:14 ] >>399 ＞ロッサーの可証述語というものについて、誰か教えてください。 教えてやってもよいが、いくら払う？ ＞「ある論理式φの証明ｙがあって、ｙよりゲーデル数が小さなものは ＞どれも¬φの証明ではない」ということらしいですが ＞なんで、〜より小さなもの、ということを ＞言わなければいけないのか、がわかりません。 わからん、とすればそこだろうな ＞「ある論理式φの証明があって、ある¬φの証明は無い」 ＞ではだめなのでしょうが、その理由がよくわかりません。 その文章ではダメだな。せめて 「ある論理式φの証明があって、どれも¬φの証明では無い」 くらいにいわんと。 414 名前：１３２人目の素数さん [2005/05/15(日) 17:17:44 ] >>413 しかし 「ある論理式φの証明があって、どれも¬φの証明では無い」 を論理式でかくと、∃ｙProv(y,x)∧¬∃ｚDispr(z,x) となってしまって、zはyと何のかかわりもなくなる。 ∃ｙ(Prov(y,x)∧¬∃ｚ((ｚ＜ｙ)∧Dispr(z,x))　 だとｚはｙに依存する。 415 名前：１３２人目の素数さん [2005/05/15(日) 17:42:32 ] >>414 ｙを具体的に与えたとき Prov(y,x)∧¬∃ｚ((ｚ＜ｙ)∧Dispr(z,x)) を判定する述語はつくれるが、zがyと独立だった場合 ¬∃ｚDispr(z,x) （つまり∀ｚ¬Dispr(z,x)）を 判定するのは無理。 416 名前：１３２人目の素数さん [2005/05/15(日) 18:56:06 ] 解析接続てなんですか？ 417 名前：GreatFixer ◆ASWqyCy.nQ [2005/05/15(日) 18:59:41 ] Re:>>416 正則関数の定義域を広げること。 418 名前：１３２人目の素数さん [2005/05/16(月) 13:05:23 ] 可証性述語を表現するとされる論理式を、ちょっと強くしたんだろうな、 くらいで通り過ぎようと思っていましたが、なんか教えてもらえそうなので、もう少しくらいついてみます。 >>413 >>414 >>415 ∃ｙProv(y,x)∧¬∃ｚDispr(z,x) 「ある論理式φの証明があって、どれも¬φの証明では無い」では、ｚがｙと関係付けられていないので、まずい、 〜より小さい、というのは、ｚをｙと関係付ける一つの方法だ、 というように読めるのですが、 それが、 ・〜より小さい、という表現を用いている ・「ある論理式φの証明があって、どれも¬φの証明では無い」 ではだめ ということの理由ですか 419 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 14:46:36 ] >>418 つーか、>>414ぬきに、>>415で"ｙより小さい"という 限定を行って計算可能になったからＯＫなのでは？ 420 名前：１３２人目の素数さん mailto:age [2005/05/16(月) 21:22:37 ] >>409 詳細キボンヌ　ハァハァ 421 名前：１３２人目の素数さん mailto:sage [2005/05/16(月) 23:51:08 ] >>418 T を PA を含む帰納的な理論、Prov(y,x) を T の標準的な可証性述語、 P が T の証明図、A が T の論理式のとき、g(P), g(A) をそれぞれ P, A のゲーデル数を表す数字とする。 このとき、ゲーデルの第一不完全性定理は次の表現可能性と対角化補題 から導くことができる。 P が論理式 A の T での証明図 ⇔ Prov(g(P),g(A)) が T で証明可能. 一方、Prov'(y,x) ≡ Prov(y,x)∧¬∃z＜y Dispr(z,x) とおくと、 T が無矛盾という仮定の下で、次が成立する。 ロッサーの不完全性定理は、これよりゲーデルの第一不完全性定理と 同様の方法で証明できる。 P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能 ところが、Prov*(y,x) ≡ Prov(y,x)∧¬∃z Dispr(z,x) とおくと、 T が無矛盾という仮定があったとしても、 「P が論理式 A の T での証明図」と「Prov*(g(P),g(A)) が T で証明可能」 との同等性が証明できない。 422 名前：１３２人目の素数さん [2005/05/17(火) 12:07:17 ] ありがとうございます。 ＞Prov(y,x)∧¬∃z＜y Dispr(z,x) とおくと、・・ ＞Prov(y,x)∧¬∃z Dispr(z,x) とおくと、・・ というくだりで、ずいぶんと、わかんない部分が補完されてきたような気がします。 ところで、 標準的な可証性述語もロッサーの可証性述語も 扱ってる関係は ＞P が論理式 A の T での証明図 であるのに、 それを表現するとされる論理式は、 標準的な可証性述語　　∃ｙProv(y,x） ロッサーの可証性述語　　∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ））　 で異なってるわけで、 これは、ただ単に、必要な条件を無矛盾である、にするための工夫ということですか はじめ、標準的な可証性述語の∃ｙProv(y,x）だけ、見てたときには、扱う関係のメタ的な情報を表したものなのかな、くらいに思ってましたが、 ロッサーの可証性述語の∃ｙ（Prov(y,x）∧∀ｚ＜ｙ¬Disp(y,ｚ））の場合は、扱ってる関係（P が論理式 A の T での証明図）とは、あんまり（全部は）関係ありませんよね 423 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 13:17:32 ] >>420 直感的には x≦yの→a_x∪a_y＝a_y なので ∪Ａ＝(...((((a0∪a1)∪a2∪)a3∪)a4∪)...a∞)＝a∞ 論理式は有限である必要があるので複雑さも有限 複雑さが∞のa∞という論理式は存在しない。 厳密な解はｼﾗﾈ。 424 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:35:47 ] 恐らく分かる人にはレベルが低すぎなのかもしれませんがご教授ください。 計算式も書いてもらえると嬉しいです。m(_ _)m 例題 チョコレートAには30％のホワイトチョコが含まれている。 チョコレートBには１０％のホワイトチョコが含まれている。 両方のチョコを使わなくてはならない。 以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは いくつ用意しなければいけないが？ 425 名前：>424 [2005/05/17(火) 22:37:23 ] 少し訂正です。 以上のことから。150Kgのホワイトチョコを集めるためにはチョコレートAとチョコレートBは 何キロずつ用意しなければいけないが？ 式 426 名前：１３２人目の素数さん mailto:sage [2005/05/17(火) 22:39:19 ] >>424の問題のどこらへんが、数学の基礎をゆるがすんだろう。 427 名前：１３２人目の素数さん mailto:age [2005/05/17(火) 23:07:54 ] R^2はR^3の部分空間ではないことを説明して、＊と比較せよ。 ＊…平面ベクトル全体からなる集合は自然に空間ベクトルの全体からなる線形空間の部分空間と見ることができる。 （;TωT） ナゼR^2がR^3の部分空間でないのか？？昨日からずっとモヤっとしています。誰か処方箋をキボンヌ。 428 名前：１３２人目の素数さん mailto:sage [2005/05/18(水) 00:09:00 ] マルチすんなよ 429 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:13:35 ] >>422 ＞扱ってる関係 なんかこの言い方がキモチ悪いのだが、それはさておき･･･ ＞標準的な可証性述語だけ、見てたときには、 ＞扱う関係のメタ的な情報を表したものなのかな、 ＞くらいに思ってましたが、 メタ的な情報って何だい？ ぶっちゃけていえば、 「命題も証明も数字であらわして、 　後者が前者の証明であることを 　算術だけで言い表したもの」 だな。数字＝ビット列、算術＝プログラムと思えばいい。 430 名前：１３２人目の素数さん mailto:sage [2005/05/19(木) 10:19:12 ] >>422 ＞ロッサーの可証性述語の場合は、扱ってる関係とは、 ＞あんまり（全部は）関係ありませんよね なにいってんのかわかんねぇぞ！ これもぶっちゃけていえば、 「単にシンタクスチェックをするだけではなく 　与えられた証明よりも小さな証明の中に 　与えられた命題の否定の証明がないことを 　チェックするもの」 ということだな。 ここで、「与えられた証明よりも小さな証明」と 上限を設けてるのがミソ。これがないと、 チェックする証明が無限になってしまう。 それではプログラムが終了するとは限らない。 （実際、終了しない） 431 名前：１３２人目の素数さん mailto:age [2005/05/19(木) 23:12:57 ] >>405 >>409 詳しくヨロ♪ 432 名前：１３２人目の素数さん [2005/05/19(木) 23:23:47 ] p,qが命題変数のとき p∧q この選言標準形と連言標準形を求めよ。 すごいレベル低いと思いますが選言標準のほうがわかりません。どうやって求めるのでしょうか？ 433 名前：１３２人目の素数さん [2005/05/19(木) 23:38:55 ] あ。解決しました　お恥ずかしい 434 名前：１３２人目の素数さん [2005/05/20(金) 14:03:53 ] >>421 でそのロッサーの不完全性定理ってどんなものなんでしょう？結論はどうなっているの？それから 　　P が論理式 A の T での証明図 ⇔ Prov'(g(P),g(A)) が T で証明可能 はどう証明すればいいんでしょう。 きっと⇒が本質的なんですよね。それで¬Dispr(1,g(A)), ... ¬Dispr(g(P) -1, g(A)), Prov(g(P), g(A))の証明を作ればいいんでしょうか。 このDispr(p,g(A)) は Dispr(MP(p,q),g(A)) ≡ Prov(p,g(A⇒B))∧Dispr(q,g(B)) のように具体的なpについて原始帰納的に定義されているの？でもそれだと∃z<y(Dispr(z,x))は定義できない。。。 435 名前：１３２人目の素数さん [2005/05/20(金) 17:50:26 ] ちっともわかってませんでした。証明木の全ての箇所が正しいように。。。 Dispr(p,x) ≡ ∃d(DTH_SENTENCE(p,d,x) ∧∀d'<d,y,z(DTH_SENTENCE(p,d'+1,y) ∧DTH_SENTENCE(p,d',z) ∧DTH_SUBPROOF(p,d',q) ⊃ Prov(q,IMP(y,z))) ∧∀y(DTH_SENTENCE(p,0,y)⊃ IS_AXIOM(INVERSE(y)) 436 名前：１３２人目の素数さん [2005/05/20(金) 21:52:36 ] 証明: pの大きさに関する帰納法 PROOF(p)がPROP(a)の証明である(PROP(a)が公理) → 示すことはない。 PROOF(p)がPROP(a)の証明である(PROP(a)は公理でない) → あるbがあってpの部分木であるfst(p)とsnd(p)がそれぞれPROP(b)⊃PROP(a)とPROP(b)の証明である。 → ∀q<fst(p)(¬Dispr(q,impl(b,a)))と∀q<snd(p)(¬Dispr(q,b))の証明がある。(帰納法の仮定) → ¬Dispr(0,impl(b,a)),..¬Dispr(fst(p)-1,IMPLIES(b,a))と¬Dispr(0,b),..¬Dispr(snd(p)-1,b)のそれぞれの証明がある。 → ... → ¬Dispr(1,a),..¬Dispr(p-1,a)の証明がある。 → ∀q<p(¬Dispr(q,impl(b,a)))の証明。 という感じになると思います。 で何でq<pがついてるかですがひとつには帰納法のベースケースが作れることと思う。つまりpが葉ならばなにひとつ¬Disprを示せていなくてよいわけです。 PROP(a)が公理だとしても∀q¬Dispr(q,a)の証明を作ることはT内での無矛盾性の証明だと思う。 437 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 22:23:05 ] 集合Xから集合Yへの写像fが全射となる条件って量化記号でどう表現できますか？ 438 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:24 ] ∀y(y∈Y → ∃x∈X(f(x)=y)) 439 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:26:58 ] ∀y∃x (x∈X∧y∈Y∧f(x)=y) 440 名前：１３２人目の素数さん mailto:sage [2005/05/23(月) 22:36:10 ] 下が成り立ってたらすごいことになるな 441 名前：１３２人目の素数さん mailto:age [2005/05/23(月) 23:06:11 ] >>438-440 えーーーと…、で結局答えはあるのでしょうか？ 442 名前：１３２人目の素数さん [2005/05/24(火) 00:02:29 ] >>439 すごいかはともかく。こっちはどんなyも必ずYに入っている。かつfは全射といってる。 443 名前：１３２人目の素数さん [2005/05/24(火) 00:07:30 ] ∀y∈Y∃x∈X(f(x)=y) は ∀y(y∈Y → ∃x(x∈X ∧ f(x)=y)) の省略。 444 名前：１３２人目の素数さん [2005/05/24(火) 14:24:40 ] 完全性証明 T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である よって Tで証明可能である　なら　Tで真である は何故言えるんですか？ T∪{¬φ}で証明可能である　なら　T∪{¬φ}で真である は、分かるんですが 445 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 18:07:55 ] 基礎論ムズイ 446 名前：１３２人目の素数さん mailto:sage [2005/05/24(火) 23:24:52 ] 基礎論ズームイン 447 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:13:14 ] 命題論理の範囲だと、古典論理でAが証明可能なとき、 直観主義でも¬¬Aが証明可能になることは比較的簡単に言えるのは 皆さんご存知かと思いますが、述語論理の範囲では似たようなことは 言えないのでしょうか？ご存知の方おられましたら何とぞご教示ください。 448 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 00:32:02 ] >>447 Glivenko の定理の拡張の話ですね。 "Glivenko theorem" "predicate logic" で検索するといろいろ出てくるようです。 449 名前：１３２人目の素数さん [2005/05/25(水) 00:52:17 ] >>444 「Tで証明可能である　なら　Tで真である」のことは健全性といいますよ。 450 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 01:25:53 ] > T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である > よって > Tで証明可能である　なら　Tで真である こんなことが書いてあるはずがない。 「(φが) T で真であるなら T で証明可能である」 でしょ。 451 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 02:10:15 ] 基礎論の学部授業がある大学ってありますか？ 452 名前：１３２人目の素数さん [2005/05/25(水) 02:13:40 ] >>449 健全性は公理を真とするベースステップからはじめて証明の大きさの帰納法で簡単にでてくる。 453 名前：447 mailto:sage [2005/05/25(水) 09:04:59 ] >>448 早速情報ありがとうございます。ぐぐってみます。 454 名前：１３２人目の素数さん [2005/05/25(水) 12:59:32 ] >>450 そう、それ、ミスった、 健全性の逆の方向 完全性証明 T∪{¬φ}は無矛盾である　なら　T∪{¬φ}は充足可能である よって >「(φが) T で真であるなら T で証明可能である」 は何故言えるんですか？ でした、 455 名前：１３２人目の素数さん mailto:sage [2005/05/25(水) 16:12:50 ] >>454 対偶考えろ。 456 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 00:14:00 ] 解決しますた。お騒がせしました。 457 名前：１３２人目の素数さん mailto:sage [2005/05/26(木) 04:36:47 ] >>451 京大では「計算機科学」っていう3回生向けの講義でそれっぽいことやってた。

---

---

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

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