数学基礎論・数理論理学のスレッド　その7

1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その6 kamome.2ch.net/test/read.cgi/math/1265884076/ 368 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 08:02:56.58 ] 有限の立場ってのは有限公理化可能ってことだとするなら、 ZFCやMKは有限でないが、NGBは有限。 排中律を公理にするかは１階述語論理での話で、 むしろ背理法なしで無矛盾な集合論を展開できるかということ。 答えはYes。 369 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 08:14:46.30 ] こりゃまた斬新な答えだ 370 名前：１３２人目の素数さん [2011/02/23(水) 10:13:34.91 ] 有限の立場は人の数だけあるとは言うが… 371 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 12:09:40.31 ] 少ない脳味噌を如何に活用するかってことなんですね。 372 名前：368 mailto:sage [2011/02/23(水) 19:56:25.65 ] >>369>>371 文句があるなら論破してみろ。 373 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 20:04:38.06 ] どこから手をつけろと言うんだｗ 374 名前：368 mailto:sage [2011/02/23(水) 20:22:42.56 ] >>373 言い訳乙＾＾ 375 名前：368 mailto:sage [2011/02/23(水) 21:10:09.87 ] 全員まとめてかかってこい！ ジャクソンとショーアのlow basic theoremより recursive degreeを下げることで不完全性定理は成り立たないようにできる！ 376 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 21:15:08.73 ] basicってことはadvancedとかもあるの？ 377 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 21:27:56.54 ] 結局、有限の立場で背理法はOKなの？ 378 名前：368 mailto:sage [2011/02/23(水) 22:13:03.52 ] >>376 basicってのは日本語では恐らく基底とか基数に該当するので基本とかではないです。 379 名前：368 mailto:sage [2011/02/23(水) 22:19:23.25 ] >>377 有限の立場の立場を明確にせよ 380 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 22:21:36.12 ] Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist. 381 名前：368 mailto:sage [2011/02/23(水) 22:59:50.96 ] >>377 述語の数を増やせばできます。 382 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 23:43:01.36 ] >>378 いやlow basis theoremのはずなのにスペル間違ってたから きっと内容分かってないんだろなと思ってからかっただけだよ というかジャクソンってもしかしてJockuschのことじゃないだろうな？ 383 名前：１３２人目の素数さん mailto:sage [2011/02/23(水) 23:52:38.94 ] >>367 ヒルベルト達の言う有限の立場で示せる命題と言うのは、 或る特定の自然数に対する命題（Δ0式）とか、 或いは変数 x を使って x に対して成り立つ命題を証明することで 「任意の x に対して〜〜」を示す、とか、つまりかなり直截的に証明できるものなので、 ∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、 そういう凝った証明は出て来ないんじゃないかと思います。 従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、 背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。 だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。 384 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:02:15.70 ] 訂正 ∀x P(x)を仮定して背理法によって∃x ¬P(x)を示すとか 385 名前：368 mailto:sage [2011/02/24(木) 00:14:58.16 ] >>384 ∃x ¬P(x)は∀x P(x)の略記じゃないんですか？ 386 名前：368 mailto:sage [2011/02/24(木) 00:21:42.85 ] >>382 ああそうだよ、内容なんてわかってないよ。 俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、 最近shoenfieldを読み始めたばかりだよ。 low basis theorem　についてはある人のブログで知ったんだよ、問題あるか？ 387 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:26:29.37 ] 議論・喧嘩してるわけでもないのに、なんで名前固定してんのこの人 388 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:26:46.53 ] 仮に∀x P(x)を仮定して〜〜みたいな議論がそもそも無いので ¬∀x〜〜という論理式がそもそも出て来ない。 だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。 あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。 389 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 00:28:01.31 ] くあんてぃふぁいあふりー 390 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 16:44:00.27 ] 素人でこの方面興味持つ奴は概ね基地外 391 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 20:11:19.86 ] >>387 話の展開をわかりやすくするためだろ。 392 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 20:28:22.40 ] というかロジックの場合、他分野では優秀な数学者が 往々にしてトンデモだったりするから困る 393 名前：１３２人目の素数さん mailto:sage [2011/02/24(木) 21:04:17.78 ] >>392 www 本当杉て困る。 394 名前：368 mailto:sage [2011/02/24(木) 22:45:14.87 ] まともに勉強していないからに決まっている。 395 名前：368 mailto:sage [2011/02/24(木) 23:12:50.35 ] 集合論研究者でさえ 論理学をやったことない人がいる。 396 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 12:41:58.62 ] いまどき素朴集合論のみで食ってる研究者なぞおらんわ 寝言は寝てから言え 397 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 12:44:27.44 ] いや、普通の数学の専門家は可算濃度と連続濃度の算法しか分からんのが結構いる。 398 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 13:40:21.63 ] >>397の「いや」へ >>395-396の流れを読め。 399 名前：368 mailto:sage [2011/02/25(金) 19:53:26.53 ] >>396 公理的集合論やモデル理論の研究者で ロジックをやったことがないといのは 結構あるぞ。 400 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 20:18:53.14 ] いやモデル理論はロジックの一部だし。 あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。 非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。 401 名前：368 mailto:sage [2011/02/25(金) 22:19:27.88 ] 知識あれば良いけど、 キューネンとかウッディンとかの本読んでるけど、 論理学のテキストまったく読んだことない人間でも 読めると思うけど？ 実際に自分が読めてる。 論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。 実際に直感的に明らかな論理学の結果しか使わないし。 何だかんだで代数、位相、測度、基数の方がメインな道具に見える。 402 名前：１３２人目の素数さん mailto:sage [2011/02/25(金) 23:35:13.21 ] Woodinって何読んでんの 403 名前：368 mailto:sage [2011/02/25(金) 23:57:02.29 ] The Axiom of determinacy, forcing axiom, and the non-stationary ideal 404 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 01:20:35.00 ] >>399 > 公理的集合論(略)の研究者で 実際に何やってる人? 組合せ論的な構成可能集合の研究とか? 405 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:35:27.99 ] 基礎論を勉強し始めたど素人ですが、どなたか教えてください。 前原「数学基礎論入門」で、「等号の基本性質」の節の冒頭にある、 次の記述意味が分かりません。 >sとtがn階の対象式である場合には、s=tは、 >∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) >という論理式の略記法であった。 ここで、_{n+1}により下付き文字をあらわしました。 この定義ですと、t∈ξ_{n+1}でかつ、¬(s∈ξ_{n+1})となるξ_{n+1}が 存在した場合でも、論理式s=tが成立し得るというふうにとれます。 その意味で正しいのでしょうか？ 普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、 思えるんですが。 406 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:42:08.97 ] ξ_{n+1} の前に ∀ があるので、適切な内包公理の下で、 ∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から ∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。 ちょっと読み進めばそのことが書いてあるはず。 407 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:43:42.25 ] >>405 "集合" ξ_{n+1} の補集合を考えれば、 s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K. 408 名前：１３２人目の素数さん mailto:sage [2011/02/27(日) 21:53:53.94 ] >>406 >>407 ありがとうございます。 ちゃんとした理屈があることが分かり、安心しました。 内包公理や補集合をヒントに理解してみます。 409 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 15:09:48.69 ] 知ったかぶりのバカが集まるすれですね 何の役にもたたないのにｗ 410 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 16:30:05.36 ] 自己紹介ご苦労 411 名前：368 mailto:sage [2011/03/03(木) 21:57:25.77 ] >>404 点集合トポロジーだったかなんだったか。 >>409 俺もそうだけど、別にいいじゃん知ったか。 知ったかでも博士とれちゃう国あるんだよ、世界には＾＾ 412 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 22:08:12.18 ] だったら無駄に名乗らないでください 邪魔なんで 413 名前：368 mailto:sage [2011/03/03(木) 22:34:23.08 ] >>412 こんな俺でも ここじゃちょっとは役に立つと思って助言してる。 なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる 人間みるとつい助けたくなっちゃう。 414 名前：１３２人目の素数さん mailto:sage [2011/03/03(木) 22:55:43.28 ] >>413 じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？ 415 名前：368 mailto:sage [2011/03/03(木) 23:09:52.65 ] >>414 pcfはJechに載ってるだろう。 予備知識などいらん！ 416 名前：368 [2011/03/05(土) 23:12:13.84 ] 志賀の無限からの光芒って面白いね。 知らなかった定理が結構ある。 417 名前：１３２人目の素数さん mailto:sage [2011/03/06(日) 06:14:59.41 ] 証明抜きが多かった記憶 418 名前：368 [2011/03/07(月) 21:37:05.07 ] >>417 まぁ本来啓蒙書なんで。 その割には証明がある丁寧な本程度と考えた方が。 419 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 18:44:12.04 ] 東北大学のサイト落ちてますねえ。 まあ仕方ないかな。 420 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 18:46:10.16 ] 被災地域の大学生、教員でアボーンした人どれだけ居るのやら。 421 名前：１３２人目の素数さん mailto:sage [2011/03/16(水) 19:09:28.70 ] 田中一之さん、東北大学だよね。心配ですねえ。 422 名前：１３２人目の素数さん mailto:sage [2011/03/17(木) 13:19:17.80 ] 今東北にロジックの学生どれくらいいるの？ 423 名前：１３２人目の素数さん mailto:sage [2011/03/17(木) 13:24:44.90 ] 学徒動員。福島原発に突入せよ。 424 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:11:10.98 ] 質問です。 命題論理のごく初歩的なところをやっているんですが、 replacement theoremとstrong replacement theoremの違いがわかりません。 wff Aを何回か含むwffをC[A]とし、C[A]の中のいくつかのAをwff Bで置き換えた結果をC[B]とする。このとき、 replacement theorem：AとBが論理的同値ならばC[A]とC[B]も論理的同値 strong replacement theorem：(A←→B)→(C[A]←→C[B])はトートロジー なぜ、後者のほうが「強い」のでしょうか？ 425 名前：368 [2011/03/18(金) 22:19:34.59 ] strong replacement theorem なんて初めて聞いた。 426 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:22:50.44 ] それはお前が無知なだけ 427 名前：368 [2011/03/18(金) 22:45:13.30 ] >>426 そんなら425をサクッと説明しちゃってくださいよ。 428 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:50:59.58 ] なにこの糞数字コテ 429 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 22:56:57.07 ] 「A→Bが証明可能」　⇒　「Aが証明可能⇒Bが証明可能」 だけど、逆は一般には成り立たないことに なぞらえてるのでは？ 430 名前：１３２人目の素数さん mailto:sage [2011/03/18(金) 23:05:57.04 ] だって、replacement theoremとstrong replacement theoremは同値じゃん。 なんでstrongなのかわからん 431 名前：１３２人目の素数さん [2011/03/19(土) 00:31:55.49 ] そういうときは wff、置換、論理的同値、トートロジー の定義を書いてみよう。 書いているうちにわかる場合が多いよ。 432 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 00:33:29.97 ] なにその万能な回答 433 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 00:44:12.36 ] 万能文化猫娘 434 名前：431 [2011/03/19(土) 00:50:10.47 ] え、割と有効なやり方だと思うんだけど 435 名前：368 [2011/03/19(土) 08:09:26.45 ] まぁ確かに定義を書くことで 頭が整理されるってことは結構あると思う。 436 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 09:44:19.26 ] strong replacement theoremというのは一般的な呼び方じゃないと思う。 別の名前が付いている訳でもないけど。 AならばBというのとA→Bはトートロジーだというのでは 後者の方が強い気はするよね。 トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。 437 名前：１３２人目の素数さん [2011/03/19(土) 11:07:58.09 ] ジェフリー『形式論理学』の決定可能、決定不可能のくだりで 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？ それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか どなたか、お教えください よろしくおねがいします 438 名前：368 [2011/03/19(土) 11:58:48.45 ] >>437 > ジェフリー『形式論理学』の決定可能、決定不可能のくだりで > 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？ > それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか > どなたか、お教えください > よろしくおねがいします 言葉の定義とかも書かないとわからないと思いますよ。 普通の数理論理学のテキストにない用語が多いですから。 439 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 12:00:34.25 ] なにこの糞数字コテ 440 名前：368 [2011/03/19(土) 12:07:59.68 ] >>437 > ジェフリー『形式論理学』の決定可能、決定不可能のくだりで > 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？ > それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか > どなたか、お教えください > よろしくおねがいします 付値は命題への真偽値の与え方と考えてよろしいでしょうか？ それから「自由な表れ」とはなんでしょうか？ 441 名前：368 [2011/03/19(土) 12:09:39.27 ] >>439 > なにこの糞数字コテ どうも！ 442 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 12:34:39.61 ] >>436詳しく頼む 443 名前：368 mailto:sage [2011/03/19(土) 13:42:36.35 ] strong replacement theoremでググったらこのスレが一番だったW 444 名前：368 mailto:sage [2011/03/19(土) 13:58:43.76 ] >>442 strong replacement theorem から replacement theorem が証明できる。逆は一般に成り立たないね。 fを付値とすれば strong replacement theorem より (A←→B)→(C[A]←→C[B])がトートロジーだから、 f((A←→B)→(C[A]←→C[B]))＝Т 一般に f(⊥→X)＝f(⊥)→f(X)＝Т f(X→Т)＝f(X)→f(Т)＝Т が成り立つから、 f(A←→B)＝⊥ ∨ f(C[A]←→C[B])＝Т replacement theorem の仮定から、 A と B は論理的同値なので、 f(A)＝(B)＝Т ∨ f(A)＝(B)＝⊥ このとき f(A←→B)＝f(A)←→f(B)＝Т であるので、 f(C[A]←→C[B])＝f(C[A])←→f(C[B])＝Т よって、 f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥ なので C[A] と C[B] は論理的同値。 445 名前：368 mailto:sage [2011/03/19(土) 14:09:13.52 ] 下から2行目訂正 誤：f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥ 正：f(C[A])＝f(C[B])＝Т ∨ f(C[A])＝f(C[B])＝⊥ 446 名前：368 mailto:sage [2011/03/19(土) 14:17:43.26 ] 訂正：逆も成り立ちますね。 447 名前：424 mailto:sage [2011/03/19(土) 14:23:56.03 ] 逆も普通に成り立ちますよね？ なんでstrongなのか・・・ ちなみに戸田山和久の『論理学をつくる』ってテキストです 448 名前：368 mailto:sage [2011/03/19(土) 14:26:13.99 ] strong replacement theorem は、 C[A] と C[B] が論理的同値ならば、 A と B が論理的同値でない場合でも成り立つので、明らかに強いですね。 449 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:41:00.37 ] それはreplacement theoremもおなじじゃないの？ 450 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:41:41.10 ] んなら>>446の逆も成り立ちますってどういうことなの 451 名前：368 mailto:sage [2011/03/19(土) 14:44:01.60 ] 論理学をつくるが出典か。 それじゃあ深い意味はなく、 使いやすい程度の直感的な命名の可能性が高い。 452 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:45:21.50 ] そんじゃ、どっちがstrongもなく、同値な定理と考えてＯＫ？ 453 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:46:54.49 ] ちなみに、地の文にも「より強い置き換えの定理」とはっきり書かれています 454 名前：368 mailto:sage [2011/03/19(土) 14:48:57.61 ] >>450 私の間違えですね。訂正します。 ： A→B　　B ------------ A ： のとき、A→BはAよりも強いと言いますから、 同値の場合は強いとは言わないかもしれないですね。 455 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:52:51.44 ] >>454そこを詳しく！ 456 名前：368 mailto:sage [2011/03/19(土) 14:56:16.92 ] 多分戸田の言いたいことは、 strong replacement theorem は replacement theorem と同値だが、 C[A] と C[B] が論理的同値 という別の命題があった場合、 strong replacement theorem は 「A と B が論理的同値でない」 場合にも成り立ちますが、 このとき replacement theorem が成立している必要はないという意味で、 「強い」と命名したんじゃないんでしょうか。 ですから>>454でいうような定義での「強い」ではないですね。 まぁその本読んだことないんで知りませんが。 457 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 14:59:31.77 ] replacement theoremも、AとBが論理的に同値でない場合も成り立ちますよね？ 458 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 15:03:58.55 ] 結局、俺には>>429がなぜ正しいのかわからない 459 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 15:09:35.95 ] 規制で書き込めなかった… >>424 証明するために、内包公理が必要かどうか。 >>430 「同値」の階層を混同している。 「論理式が同値」と「命題が同値」は全く異なる概念。 「A←→Bならば、その時に限って、A≡B」が証明できるというだけ。 ←→、≡は共に略記だけど、常識の範囲だから定義は略。 完全性定理をきちんと理解するには、この辺の区別は重要。 460 名前：１３２人目の素数さん [2011/03/19(土) 15:11:11.86 ] >付値は命題への真偽値の与え方と考えてよろしいでしょうか？ よいです。 ＝が自由な表れでないと言っているのは、∀ｘ（ｘ＝ｘ）のような公理があるために、＝を他の述語と置き換えることは必ずしも自由でないということを言っています 461 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 15:11:24.83 ] 初学者向けと謳っているのにそのあたりの解説がないのは不親切だなぁ 462 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 15:12:31.06 ] ごめん、>>429がなぜなのか、もう少し説明してもらえないだろうか 463 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 15:16:38.80 ] 付置はvaluationの訳語。 valuation function: wff→truth value 464 名前：１３２人目の素数さん [2011/03/19(土) 20:46:20.72 ] すみません、初学者なのですが、質問させてください。 ∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) が成立しないんじゃないかと思います。 反例として、 箱が二個(箱１、箱２)と玉が一個だけの世界を考えて、 Ｐ(ｘ)、Ｑ(ｘ)がともに、玉が箱ｘに入っているという命題を表すものとします。 このとき、各ｘに対してｙ＝ｘと考えてやれば「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))」は真になりますよね。 ところがｙ＝１のときはｘ＝２を、ｙ＝２のときはｘ＝１の場合を考えてやればいずれも「Ｐ(ｘ)→Ｑ(ｙ)」が成立しないため、「∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))」が偽になりますよね？？ と考えたのですが、間違いがあれば教えてくださいｍ(＿　＿)ｍ 465 名前：368 mailto:sage [2011/03/19(土) 20:58:24.75 ] >>462 散歩ついでに読んでみたけど 71ページの辺りの文脈読んでなんとなく推測。 replacement theorem は A←→B がトートロジーならば C[A]←→C[B] もトートロジーと書ける。 |= C ⇔ C はトートロジー　　　-----------（１） （１）の書き方に従えば、 |= A←→B ⇒ |= C[A]←→C[B] 　　　-----------（２） また、 strong replacement theorem は、 |= (A←→B)→(C[A]←→C[B])　　　-----------（３） （３）からCuttingによって（２）が証明できるが逆は成り立たない。 だからstrongと読んでいるのではないだろうか？ >>459の言うとおりだとしても、 置き換えの定理が出てくるこの時点で、内包公理どころか 集合論の気配は一切ない。 本来のstrong replacement theoremの意味はどうだから知らないが、 少なくともこの本を読んでも、 「強い」が内包公理の要不要に依存しているようには思えない。 466 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 21:15:27.00 ] >>429に関して、独立で説明してもらえないだろうか。 >>429は一般に言えることなの？ 467 名前：368 mailto:sage [2011/03/19(土) 22:19:40.96 ] >>466 定理１　T，A |= B ⇔ T |= A→B のTを空集合とすれば、 A |= B ⇔ |= A→B 定理２（Cutting）　T |= A 、A, K |= B ⇒ T, K |= B のような定理で、TとKを空集合とすれば、 |= A 、A |= B ⇒ |= B となり、replacement theorem が証明される。 |=という記号はこの本の定義（2重ターンスタイルとか書かれてた）に従ったが、 上の定理１と２が常に成り立つかは恐らく証明体系に依存する。 >>429はこの|=のことを証明を表す記号として言っているのでは？ 468 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 22:38:17.87 ] 初学者の俺には何言ってるかわからない・・・ もうちょっとわかりやすくたのむ・・・ strongとそうでないのは、結局、どっちからどっちをも証明できると考えておいてＯＫ？

---

---

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

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