数学基礎論・数理論理学のスレッド　その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/ 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とそうでないのは、結局、どっちからどっちをも証明できると考えておいてＯＫ？ 469 名前：368 mailto:sage [2011/03/19(土) 22:40:11.88 ] >>464 ∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) が「成立しない」の意味によりますね。 論理式としては成立しますが、これだけでは常に真ではないですね。 最後の方の文章がいまいち理解できませんが、 一応確認しておきたいのですが、 論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、 後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは 分かっていますか？ 470 名前：368 mailto:sage [2011/03/19(土) 22:46:39.88 ] >>468 strong replacement theorem と replacement theorem という定理は、 メタ理論において定理とみなされていて、 メタ理論において必要十分条件（同値）になっています。 しかし形式体系の中で、論理式として取り扱う際には、 strong replacement theorem から replacement theorem への 論理式の変形は可能ですが、逆への変形は不可能なのです。 つまり形式体系の中で strong だと主張しているのです。 471 名前：１３２人目の素数さん mailto:sage [2011/03/19(土) 22:48:50.08 ] >>470 おお、よくわかった。 また質問したいです。よろしければお名前を教えていただけませんか 472 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/19(土) 23:01:35.98 ] >>471 仮に368としておきます。 論理学をつくるをざっと眺めたところ、 無駄に冗長なうえに、 今回の意味論とシンタックスの混同のように、 さまざまな罠が張り巡らされているようなので気を付けてください。 473 名前：464 mailto:sage [2011/03/19(土) 23:04:43.49 ] >>469 ありがとうございます。 すみません、「成立」は述語論理でトートロジーになるという意味です。 僕の読んでいる教科書で、「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」をＮＫで証明せよという課題が載っていて、解答がなかったもので。。。 >論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、 >後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは それは分かっています。 「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」の反例(偽になる場合)があれば教えていただけませんか？ 474 名前：１３２人目の素数さん [2011/03/20(日) 00:09:54.48 ] フレーム(枠組み、構造とも呼ぶ)の領域を整数全体 P,Q ともに1変数述語として、対応する部分集合をそれぞれ整数全体、偶数全体 x,y を異なる変数 とすれば、このフレームはモデルとならない。 475 名前：１３２人目の素数さん mailto:sage [2011/03/20(日) 00:13:56.99 ] 質問し直します 多項関係の述語記号を持ち関数記号を持たない理論は決定不可能とあったのですが、その理論で算術の定理（例えば、任意の数項に関して、数項と0の積と0と数項の積は同一という算術の定理）は真ですか？ というのが聞きたかった内容です >>473 あってると思いますよ ∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))は妥当ではないですから 例えば、任意のドメインの要素がＰに含まれあるドメインの要素がＱに含まれ（∀ｘ∃ｙ(Ｐｘ→Ｑｙ)が真）、あるドメインの要素が¬Ｑに含まれる（∃ｘ∀ｙ(Ｐｘ→Ｑｙ)が偽）世界を考えれば、∀ｘ∃ｙ(Ｐｘ→Ｑｙ)→∃ｘ∀ｙ(Ｐｘ→Ｑｙ)の妥当性の反例になると思います もっとも、教科書が妥当でない式の証明を求めるということはないので、誤植か読み違いが起きてるのでしょう ｘとｙの順序をｙとｘと読み違えたりすることで式の内容はかわってきますよ 476 名前：１３２人目の素数さん mailto:sage [2011/03/20(日) 02:02:42.88 ] a0.twimg.com/profile_images/1279026415/ac_bigger.png 477 名前：464 [2011/03/20(日) 17:46:21.59 ] >>475 ありがとうございます。どうも誤植だった模様です。 正確には∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｙ∀ｘ(Ｐ(ｘ)→Ｑ(ｙ))だったようです。 478 名前：１３２人目の素数さん mailto:sage [2011/03/20(日) 18:21:08.09 ] なんだ、戸田山さんの本か。 戸田じゃなくて戸田山ね。 あの人は（学部の素朴な）集合論の普通の定理に関しても この定理は哲学的には問題があるとか良く分かんないこと書いてた気がする。 ゲーデルと20世紀の論理学の彼が書いた記事は面白かったけどね。 479 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/21(月) 10:54:28.93 ] >>475 「多項関係の述語記号を持ち関数記号を持たない理論は決定不可能」 というのBoolosによって示された定理のことでしょうか。 算術の定理に必要な関数記号を論理学の述語で代用するということは、 数学を二階述語論理で直接展開するということでしょうか。 これが真になるというのは、どのような場合なのでしょうか。 私は知りませんが、興味はありますね！ 480 名前：１３２人目の素数さん mailto:sage [2011/03/22(火) 18:59:09.84 ] >>466 >429は一般に言えることなの？ p を命題変数とする。勝手な論理式 A に対し、 p が証明可能ならば A も証明可能 しかし、p→A は一般にはトートロジーではない。 証明可能の条件をもうちょっと強めると、古典命題論理の範囲では Mints による定理があって、逆にあたることが成立する。 481 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 00:53:46.06 ] >算術の定理に必要な関数記号を論理学の述語で代用するということは、 >数学を二階述語論理で直接展開するということでしょうか。 は、私がそういうことかなと推測した内容で、本が言っている内容かはわかりません 数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない じゃあどうやって？ 述語でやろうというのか？しかし・・ という感じで質問に来ました 482 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:44:06.57 ] 非古典論理の階層（１） Modal logic 　Classical modal logic 　　Regular modal logic 　　Normal modal logic 　Modern modal logic 　　Temporal logic 　　　Propositional dynamic logic 　　　Linear temporal logic 　　　Interval temporal logic 　　　　Graphical interval logic 　　　　Signed interval logic 　　　　Future interval logic 　　　Kinetic logic 　　Dynamic logic 　　　Propositional dynamic logic 　　　Multimodal logic 　　Hennessy-Milner logic 　　Epistemic modal logic 　　Public announcement logic 　　Product update logic 　　Deontic logic 　　　Dyadic deontic logic 　　Imperative logic 483 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:44:42.49 ] 非古典論理の階層（２） Algorithmic logic Branching-time logic 　CTL* 　　Computational tree logic Tense logic Computational verb logic Hybrid logic Quantum logic Many-valued logic 　Fuzzy logic 　　T-norm fuzzy logics 　　　Monoidal t-norm based logic 　　　Product fuzzy logic 　　　Nilpotent minimum logic 　　　Lukasiewicz logic 　　　Godel-Dummett logic 　　　Basic fuzzy logic 　Post logic 　Kleene logic 　Provability logic 　　Interpretability logic 484 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:45:10.90 ] 非古典論理の階層（３） Bayesian logic Probabilistic logic Subjective logic Combinations logic Substructural logic 　Relevant logic 　Linear logic 　　Strict logic 　　Full linear logic 　　Modern Lambek calculus 　　　Non-commutative logic 　　　　Cyclic linear logic 　　　　Pomset logic 　　　　BV 　　　　NEL 　　Bunched logic 　Affine logic 　　Direct logic 　　Full affine logic 485 名前：１３２人目の素数さん mailto:sage [2011/03/23(水) 23:45:50.52 ] 非古典論理の階層（４） Paraconsistent logic 　LP 　FDE Doxastic logic Floyd-Hoare logic Description logic Minimal logic Independence-friendly logic Dependence logic branching quantifier logic Non-monotonic logic 　Default logic Autoepistemic logic Free logic Connexive logic Combinatory logic Categorical logic Q0 Logic Ω-logic Separation logic ： ： 486 名前：１３２人目の素数さん [2011/03/24(木) 00:05:02.46 ] 分岐量化子とか客観論理が好みですね... まぁ私は全て知っていましたけど。 487 名前：１３２人目の素数さん [2011/03/24(木) 00:49:54.63 ] そんなにいっぱいあるんですか… それらを(ある程度)統一した強力な体系とかあるんでしょうか？ 488 名前：１３２人目の素数さん [2011/03/24(木) 07:37:33.20 ] Wikipedia 489 名前：368 ◆jkwVJMjC32 [2011/03/24(木) 08:08:58.26 ] >>481 > 数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない > じゃあどうやって？ > 述語でやろうというのか？しかし・・ > という感じで質問に来ました 述語論理で必ずしも算術をする必要があるのでしょうか？ Boolosの定理は算術の存在を仮定しなくても、成り立つように思えます。 一般的な論理と数学に必要な論理は分離していった歴史がありますから。 490 名前：１３２人目の素数さん [2011/03/24(木) 21:08:48.47 ] Paraconsistent logic 矛盾許容論理... もう何でもありだな。 491 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/24(木) 21:56:46.43 ] 上記リストの中から、 興味のあるものや、詳しく知りたいものがあったら 言ってもらって結構です。 大抵答えられます。 492 名前：１３２人目の素数さん mailto:sage [2011/03/25(金) 16:41:52.80 ] intuitionistic logic がないのは何故だろう? 493 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/25(金) 23:47:24.56 ] >>492 直観主義論理は上記リストから見ると、 ちょっと古いのではないでしょうか。 古典論理から中間論理、直観主義論理、そして超直観主義論理までの 意味論はクリプキが可能世界の導入によって自然に拡張しましたから、 当然、上の非標準論理の基礎にはなっています。 しかし上のリストは恐らく、 様相論理を基本的な枠組みとして取り入れた 論理を紹介する意図があったのではないでしょうか。 いずれにしろ、個人の仕事なのですから 上記リストに抜けがあることは致し方ないでしょう。 それよりも良い検索キーワード集を提供してもらえたことに感謝しましょう。 494 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 18:29:03.87 ] Public announcement logicって名前が面白いな どういうことをやるんだろう？ Taoのblogに載ってたようなcommon knowledge的な話とかかな？ あとInterpretability logic とΩ-logic について宜しく 495 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 19:45:59.19 ] >>493 368の過去レスを見るとそんな偉そうな総括が言える力量とは思えない おそらくハッタリであろう 496 名前：１３２人目の素数さん mailto:sage [2011/03/26(土) 20:33:19.56 ] ロジックの本を読むのは初めてなのに それが日本最高峰の教科書と言っちゃうくらいだからな>>188 497 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/26(土) 22:32:27.30 ] >>496 正確にははじめてではないですね。 知識と信念の論理という本がはじめてですね。 この本で命題論理・述語論理から 様相論理、デフォルト論理やメンタル・スペース理論まで まとめて学習しました。 理解できない部分は論理と計算のしくみという本で補填しました。 またこの本で完全性定理や不完全性定理を学習しました。 498 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/27(日) 08:26:17.10 ] 公開告知の論理PAL（Public announcement logic） 動的認識論理DEL（Dynamic Epistemic Logic）の一種で、 公開告知やプライベートなどの多種の言語伝達に依存して エージェントたちの認識状態が変化するというアイデアによる。 様相論理を基礎にしている。 例 APLにおける文φの意味の公開告知の型がφ！であるとき、 様相演算子を[φ！]、<φ！>と置く。さらに命題ξに対して、 公開告知の後、[φ！]ξが真する。 ξが「K_aχ：エージェントaがχを知っている」で定義されるとき、 公開告知によって[φ！]K_aχが真。 これは公開告知による知識の変化を記述している。 おっしゃられる通り、common knowledge やmutual knowledge への拡張もされています。 また認識論理の代わりに義務論理を選択することで、 指令論理ECL（Eliminative Command Logic）なども作られました。 関連 DEUL (Dynamic Epistemic Upgrade Logic） DDEPL（Dynamic Deontic Epistemic Preference Logic） Arbitrary Public Announcement Logic (APAL) Future Event Logic（FEL） カテゴリ 数理論理学｜計算機科学 499 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/27(日) 09:08:57.64 ] 解釈可能性論理Interpretability logic 証明可能性論理GLを拡張したもので、さまざま種類があります。 算術的に完全なILMやモンターギュの公理を加えた最小論理IL、 持続公理をILに加えたILPなど。 p、q...は束、 ∧、∨、→、⇒は様相論理のオペレータ 定義1 d(p)＝1 d(⊥)＝0 d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1 公理2 略 自分よりも弱い理論の文を自分の中に置き換えて 数学的な性質を比較するという感じでしょうか。 500 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/29(火) 23:09:07.72 ] 解釈可能論理(IL) GL＋述語記号△ 二項様相演算子△を以下のように定義する。 理論Tにおける、A△Bの算術的な実現は TにBの実現を加えたものは、TにAの実現を加えたものを解釈可能である。 つまり、Tの言語の論理式で、 T＋B |― C implies T＋A |― f(C) となるような比較解釈可能関数ｆが存在する。 定義１ 式Aの次数d(A)を次を満たす。 ・d(p)＝1 ・d(⊥)＝0 ・d(A∧B)＝d(A∨B)＝d(A→B)＝d(A⇒B)＝d(A)+d(B)+1 定義２ ILの公理 K:□(p→q)→(□p→□q) L:□(p→p)→□p J1:□(p→q)→(p△q) J2：(p△q)∧(q△r)→(p△r) J3:(p△r)∧(q△r)→((p∨q)△r) J5:(◇p)△p ILの推論規則 MP 501 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/29(火) 23:09:26.37 ] 定義３ ILPの公理 ILの公理に以下の公理を加えたもの P:(p△q)→□((p△q)　(永続公理) 定義４ 論理式Aと論理Lについて、L+Aとは、 L∪{A}を含む論理式の最小の集合で、 様相論理のMP、置換、必然性の3つの規則において閉じている論理。 定義５ IK4とは、 K、J1、J2、J3、J5に、 4：□p→□□p を加えた6つの公理とすべてのトートロジーを含む最小の論理式の集合で、 様相論理のMP、置換、必然性の3つの規則において閉じている論理。 定理１ IK4 ⇔ △-free fragment が様相論理K4となるILの部分論理。 定理２ IK4＋PはILPの部分論理。 定理３ IL＝IK4＋L ILP＝IL＋P＝IK4＋P＋L 定理４ IL、ILPはクリプキ構造で完全。 502 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 19:18:55.66 ] 定義６ Γ_A≡Γ−{A}を論理式の集合、 ◎∈{□,◇,¬}を接頭辞としたとき、 ◎Γ≡{◎A｜A∈Γ} Γ△⊥≡{A△⊥｜A∈Γ} と表現し、推件式は以下のように表現する。 Γ→�� 定義７ 推件式GIK4Pの公理 A→A ⊥→ 503 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 21:24:29.35 ] 定義８ 論理式Aの部分論理式の集合をSub(A) Γ∪∆の各論理式の部分論理式の集合をSub(Γ → ∆)で表す。 定義９ GIK4Pの推論規則。 (T→)Γ→∆：A,Γ→∆　 (→T)Γ→∆：Γ→∆,A　 (cut)Γ→∆,A、A,Π→Λ:Γ,ΠA→ ∆A,Λ　 (∧→i)Ai,Γ→∆：A1∧A2,Γ→∆　 (→∧)Γ→∆,A、Γ→∆,B：Γ→∆,A∧B　 (∨→)A,Γ→∆、B,Γ→∆：A∨B,Γ→∆　 (→∨i)Γ→∆,Ai：Γ→∆,A1∨A2　 (⊃→)Γ→∆,A、B,Γ→∆：A⊃B,Γ→∆　 (→⊃)A,Γ→∆,B：Γ→∆,A⊃B　 (△K4P)A,{B,X1,···,Xn}△⊥,Σ→B,X1,···,Xn、Σ→Y1△B、…、Σ→Yn△B： X1△Y1,···,Xn△Yn,Σ→A△B　 504 名前：368 ◆jkwVJMjC32 mailto:sage [2011/03/30(水) 21:29:12.26 ] 残念ながらこの論理の肝である、 シーケンス計算は、 証明図が奇抜な形をしているため 掲示板に書くことはできませんでした。 505 名前：１３２人目の素数さん [2011/04/03(日) 01:45:35.55 ] N型推論図ってすごい使いにくいような気がする。 これのメリットって何があるの？ 506 名前：論理体系の表現能力 [2011/04/03(日) 12:08:08.76 ] ↑たかい ↑ 様相論理（時相論理・認識論理・信念論理...） ↑ 中間論理 ↑ 超直観主義述語論理 ↑ 超直観主義命題論理 ↑ 直観主義述語論理 ↑ 直観主義命題論理 ↑ 部分構造論理(ランベック計算・線形論理、矛盾許容論理、ウシュカヴィッチ多値論理、ファジー論理、適切論理...) ↑ ↑ひくい 大体こんな関係じゃないでしょうか？>>487 507 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 19:08:36.22 ] 予習が完了しました。 今夜からΩ-論理の説明をはじめましょう。 508 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 20:39:42.43 ] >>491で大抵答えられますって言ってたのは 勉強したら答えられるようになりますって意味だったの？ 勉強したての人間の説明は何が本質的なのか全然分かんないから勘弁してほしい 509 名前：１３２人目の素数さん mailto:sage [2011/04/05(火) 21:28:09.34 ] いえ、「Ω-論理以外」は何でも答えられるという意味である。 上記のリストにΩ-論理はない。 510 名前：１３２人目の素数さん [2011/04/06(水) 10:18:46.30 ] １０は３で割り切れないって言うけど１０人分のケーキを三人に分けることはできるんだが？ hatsukari.2ch.net/test/read.cgi/news/1302019119/l50 511 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 11:09:08.03 ] >>510 凄い発見だな！僕は自分の人生さえ割り切りが付かないぞ！ 512 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 22:33:49.35 ] 仏教論理もこのスレでいいの？ 513 名前：１３２人目の素数さん mailto:sage [2011/04/06(水) 23:42:36.65 ] >>512 現在仏教論理は主流ではないですね。 量化が特殊なので非常に研究が難しい。 イスラエルでマルグリス（超剛性定理で有名な）らにより 研究されているキリスト教的論理学との関連が指摘されています。 キリスト教的論理学の推論規則ではほとんどの仮定が落ちません。 514 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:01:16.27 ] インド論理⊇仏教論理∪易罫 515 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 08:03:17.55 ] 仏教論理は様相論理 516 名前：１３２人目の素数さん mailto:sage [2011/04/07(木) 13:06:25.30 ] 区体論はこのスレでいいんすか？ 517 名前：１３２人目の素数さん mailto:sage [2011/04/08(金) 20:06:05.60 ] >>494 > Taoのblogに載ってたようなcommon knowledge的な話とかかな？ え？ テレンス・タオってロジックにも進出しているの？ 天才に来られると萎縮するわ... 518 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:12:13.38 ] >>505 N型推論図（フレーゲ流）はNKなどの公理を持たない体系で、 仮定を落とすのを記述するのに使われることが多いです。 L型推論図はシーケント計算など仮定がない体系で使われます。 一般的な数学はNKのN型推論図などを用いると表現しやすいです。 シーケント計算のL型推論図は様々な論理式を 証明するのに下から辿れるので使いやすいです。 本によっては → が |― と書かれていたりしてまちまち。 またHKは仮定がないのでL型で書かれることが多いです。 （HKは公理の変形が複雑だが部分構造論理で使われるそうな） それから論理式の左側にtermと呼ばれるものをつけて、 証明の経路を辿れるようにしたものもありますね。 この際、NKの仮定をラムダ項に対応させることが出来、 カリー・ハワード対応と呼ばれることもあります。 仮定の落ちる回数に制限を設ける論理もあったと思います。 519 名前：１３２人目の素数さん mailto:sage [2011/04/09(土) 19:16:06.90 ] ま初歩的な証明論程度の質問ならなんでも 答えられるので何でも聞いて良いですよ。 520 名前：１３２人目の素数さん mailto:sage [2011/04/10(日) 21:52:24.80 ] 実は証明論に公理は不要である。 これを知らないから無駄な努力をしてしまう。 521 名前：１３２人目の素数さん mailto:sage [2011/04/13(水) 23:51:38.10 ] kamome.2ch.net/test/read.cgi/math/1293882228/980 岩波書店5月　『数学基礎論』新井敏康　著 ttp://www.iwanami.co.jp/hensyu/science/next.html 気合入ってるなあ　楽しみ みすずから出たトルケル・フランセーンの本もかなり良いよ。 ロジック専攻というレベルじゃなくて不完全性周りが まさに著者の専門だからかなり細かいことまで徹底的に書いている。 但し著者独自の主張じゃないか、と思うようなことも無いではないけどね。 訳者の田中先生って今どうしてるんだろうか。 今年春に東工大で講演会やるみたいな話あった気がするけどどうなってるのかな。 522 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 07:08:42.36 ] 微積分みたく入門書ばかりがどんどん増えていきますね。 メドベージェフ次数が日本に紹介されるまではまだかかるでしょうね。 523 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 08:18:58.10 ] 　　ま　　た　　お　　前　　か 524 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:12:25.74 ] 日本語の本は入門書のみで十分。 後は英語の世界。 525 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 19:20:30.70 ] >>521 内容は Shoenfield のと同じようなもん？ 526 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 20:55:12.37 ] >>525 Shoenfield は証明論がなかったですよ。 それから計算理論が何を指しているのかが分かりません。 ページ数が気になりますね。 解説を読む限り強制法にも触れてそうですね。 ただメドベージェフ還元まではいかないと思いますね。 527 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:34:06.56 ] 帰納関数論でしょ。 528 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 21:39:51.30 ] 原子帰納関数を導入してから、 ゲーデルが証明したのに近い不完全性定理を導入するってことですか。 算術的階層やペアノ算術までいくShoenfieldよりは進まないということかな。 529 名前：１３２人目の素数さん mailto:sage [2011/04/14(木) 22:15:29.27 ] ペアノ算術やらないわけない。 入門篇で原始帰納関数、基礎編で超限帰納法やるんじゃないだろうか。 530 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 00:58:48.51 ] 集合論をかなりやってから証明論に進む構成だから、 新井先生の専門とかから考えるなら、 再帰的Mahlo順序数とかを使うKP（ZFの断片）に対する順序数解析とかに 触れたりして現代の証明論を紹介したいのかな、とか思ってるんだけど。 PohlersのProof Theory: The First Step into Impredicativity（11章）とか RathjenのThe art of ordinal analysis www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf とかの後半（2.2. Set theories.以降）とか。 新井先生のarxiv.org/abs/1102.0596で言うなら4 Jäger以降の内容。 ちょっと希望的観測過ぎるか。 531 名前：１３２人目の素数さん mailto:sage [2011/04/15(金) 20:27:40.85 ] 順序数解析はやっぱり入れるんじゃないか 532 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 01:08:11.68 ] にわかで申し訳ないんですが、 モデル理論とはどのようなものなんでしょうか ゲーデルあたりの研究成果を元に生まれたとは聞いたんですが 533 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 07:46:53.79 ] 理論のモデルを研究することですね。 534 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 17:24:57.55 ] >>532 タルスキが最初だよ。 ゲーデルと並行して研究されてた。 535 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 22:55:12.90 ] >>533 >>534 なるほど 「モデル」がどういう意味なのか分からなくて困ってましたが 要は意味論のことなんですかね ありがとうございました 536 名前：１３２人目の素数さん mailto:sage [2011/04/16(土) 23:57:38.44 ] 正確には意味論がモデルと等しいわけではないですね。 1階述語論理の意味論は構造と呼ばれており、 この構造である理論のどんな論理式を解釈しても、 真になれば構造が理論のモデルになるとされますね。 つまりある理論を「まともに」解釈できる構造のことですね。 無矛盾な理論はモデルをもつ。 という完全性定理がモデル理論の初期の研究成果です。 それからコンパクト定理とレーベンハイム・スコーレムの定理は どんな本にも載っていますね。 例えば、 可能世界で有名なクリプキ構造は様相論理のモデル、 チューリング・マシンはある計算理論のモデル、 2^ωが型なしラムダ計算のモデルになったりしますね。 ハインティング代数やブール代数などの代数的構造を モデルにすることで、論理学を代数にする手法もあります。 モデル間の同型写像を考えて構造同士の関係・分類もできます。 連続体仮説のZFCからの独立性を証明する強制法のアイデアも 提供しておりますし、モデル自体をZFC上で形式化する研究もあります。 また様々な階数の述語論理を計算の複雑さの階層 （EXPとかPSPACEとかNPとか...）に対応させ、 算術的階層などと組み合わせて現代数学の全体像を浮かび上がらせる 記述計算量理論というものにもアイデアを提供してます。 大雑把にいって証明論に対して存在しているようにも思われます。 537 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 00:03:25.54 ] 訂正： つまりある理論を「まともに」解釈できる構造のことですね。 ↓ つまりある理論を「正当に」解釈できる構造のことですね。 まともでない解釈も存在しますからね。 538 名前：１３２人目の素数さん mailto:sage [2011/04/17(日) 11:25:13.19 ] なるほどなるほど 面白そうですね 丁寧にありがとうございました！ 539 名前：１３２人目の素数さん mailto:sage [2011/04/22(金) 21:46:08.83 ] 上の方で登場したヒルベルトの公理なんですが、 これっていくつ位存在するんですか？ リストみたいなものってありますか？ それから今使われてる公理はなぜ使われるようになったんですか？ 540 名前：１３２人目の素数さん mailto:sage [2011/04/23(土) 08:16:45.01 ] ベクトル空間の基底の取り方みたいなもので無数にあるよ たぶん自分で独自に選んで本書く人も多いんじゃないかな 541 名前：１３２人目の素数さん [2011/04/23(土) 11:40:28.66 ] 自称論理学者（ID:M/m1hILG）がとんでもない論理を展開中 yuzuru.2ch.net/test/read.cgi/edu/1291023518/l50 542 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 00:15:26.75 ] 例えばヒルベルト流命題論理の 含意断片論理（論理記号が'→'だけのもの）で、 大抵の教科書に出てくる公理のように メタ変数が3個で論理記号4個でカッコの付け方が正常な論理式の総数だけでも、 ざっと概算したところ100万個を超えた。 一般の命題論理の¬や∧、∨など5種類ほど加えると数十億に到達するらしい。 公理選択で重要なのは、「独立」を調べること。 MPを推論規則にもつとき、 A→A A→A→A A→A→A→A の3つで上の2つの文は下の文から証明可能なので公理に不要。 「完全性」「健全性」「独立」などの条件が重要で、 定理自動証明機械なども研究された。 歴史的にほとんどの証明体系が意味から出発している。 にもかかわらずそのほとんどが上記条件を満たすのである。 543 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 07:10:00.79 ] 数十億ではなく6億くらいですね。 カッコの付け方が位相みたいに、 シンプルに計算できないので正確ではないですが。 544 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:39:01.16 ] おい、公理系の独立性はたいして重要で無いだろ。 おまいは、命題論理の公理系学んだとき、その独立性チェックしたか？ 多くの教科書同様、完全性と違ってしてないはずだ。 545 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 13:57:23.11 ] 独立でなくてもいいのなら、明らかに無限通りあるからじゃない？ 546 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 20:39:31.01 ] 大抵の教科書に掲載されているHKの公理は、 ある程度意味のあるもの、 例えばLKとの同等性が示せるものだとかに 絞られているわけです。 つまり独立性を示す努力は本の著者というか、 「論理の歴史」が勝手に代替してくれているわけですね。 私が言いたかったヒルベルト流とは推論がMPだけという意味です。 そして独立性の証明は完全性よりはるかに煩雑です。 確かに必須ではありませんが、 無から公理を創造する場合は独立に近くする努力はするべきですね。 547 名前：１３２人目の素数さん [2011/04/24(日) 22:41:45.58 ] 論理学をやる人は高踏趣味があるのかやたら専門用語を散りばめた文章を書く。 少し解りにくいことも解っていて当然なような口ぶりだ。 548 名前：１３２人目の素数さん mailto:sage [2011/04/24(日) 22:53:10.92 ] 分かっている人ほど簡素な文を書く 分かったふりをする人は難解な文を書く 549 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 01:06:51.10 ] >544 重要でなければ強制法とかの技法も要らない気がするけど。 550 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 07:12:08.71 ] いや述語論理の独立性の話だろ Principia Mathemticaの公理なんか 独立じゃないことが数十年後に判ったんだぞ 551 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 11:42:06.24 ] 独立性の証明は難しいことが多い。 しかし証明が必要になることはまず無い。 552 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 16:59:17.12 ] 与えられた体系の中での命題の独立性と、 公理系そのものの独立性の話の話は区別しないと。 前者は気にするのが普通だし、重要な問題であることも多い。 後者はよほど特別なことがない限り、気にすることはない。 553 名前：546 mailto:sage [2011/04/25(月) 20:50:54.18 ] >>547 それは私のレスポンスに関するものでしょうか。 そうであるとしたら具体的どこに高等趣味があるのかを、 該当箇所の引用したうえで述べてください。 >>551 詳しそうなので質問します。 独立の証明の有益な方法はありますか？ それから証明する必要がないとはいえ、 テキスト中のHKは大抵独立だったり完全だったり 無矛盾だったりして、 「子供が安全に遊べるように人為的に作ったアスレチック」で あることが多いとは思いませんか？ >>548>>550>>552 同感です。 554 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:04:40.48 ] 自覚あるんだね 555 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:22:09.77 ] いつぞやこのスレで総スカンを食らったコテの匂いがプンプンする 556 名前：546 mailto:sage [2011/04/25(月) 21:23:12.91 ] >>554 ローマに入ればローマに従えというか、 論理学を語る時だけ独特の文体になることは確かだと思います。 しかし、文章の中に含まれる専門用語は他の数学に比べれば かなり少ないと思いますが？ （まさか専門スレッドでテクニカルターム禁止だというわけでもないだろうし。） それに難解なことなんか言ってないんですよ。 普通に1階述語論理までやっていれば言いたいことは 分かると思うんですが。 557 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:34:54.22 ] それを言うなら郷に入っては郷に従えだ 英語のことわざとごっちゃにするなよ、半可通 558 名前：546 mailto:sage [2011/04/25(月) 21:45:09.44 ] >>557 >郷に入っては郷に従えだ あえてローマに入ればローマに従え といったんですが。 意図的に日常さはんじをちゃめしごとと読んだり、 既出をガイシュツと呼んだりする、 当たり前だのクラッカーみたいなノリで言ったんですよ。 これに関して本気で突っ込むそちらの方が半可通なのでは？ 559 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 21:58:46.82 ] 図星みたいだ 560 名前：１３２人目の素数さん mailto:sage [2011/04/25(月) 23:02:07.21 ] これはみっともない 561 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 00:10:16.55 ] >>558 ばーか 562 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 07:15:02.06 ] どうでもいいことで何を議論してるんだか…… Shoenfieldの第一章の演習問題は独立性を公理それぞれに対して証明しているよね 著者がそういう細かいことにこだわる人だったのかもしれない 563 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:09:34.17 ] >>552 > 与えられた体系の中での命題の独立性と、 > 公理系そのものの独立性の話の話は区別しないと。 前者はどういう意味? ある形式系で命題が形式系の他の公理から独立なら それは公理として認めないと真には成り得ないけど? 後者の「公理系そのものの独立性」って公理系が何対して独立なの? 564 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 11:11:21.23 ] >>562 独立でない公理があるなら、それは公理としては不必要なんだから、 基礎論的な意識の強い学者は当然こだわるわな。 565 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 18:31:40.30 ] >>563 そういう根本的なことから理解出来てないと、ビックリする 566 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:05:38.43 ] いくつかの公理・推論規則と それから証明可能なすべての論理式の集合をS、T、 ある公理または推論規則をA、 S＝T∪{A} としたとき、 TでAが証明できない。⇒SでAは独立。 Aが任意⇒Sは独立。 独立性証明のテクニック⇒3値論理。 567 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:22:28.23 ] おー久しぶりだな「考える人」 正直もう二度と見たくなかったが。 568 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 20:25:18.26 ] 訂正： 誤 Aが任意⇒Sは独立。 正 上記条件プラスAが任意⇒Sは独立。 計算機科学とかでは体系が 独立じゃないと一般的に色々複雑になるらしい。 569 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:04:15.53 ] >>564 集合論のZFとかだと各公理は独立じゃなかったりするでしょ。 独立性が大事かどうかというと、あまり大事じゃない場合も多い。 少なくとも完全性に比べると些事。 >>566 一般的にはAも¬Aも証明できないときに「独立」という気がするけど。 反証可能な場合は普通は含めない。 あとAが任意って何が言いたいのか分からない。 任意の式Aが証明不可能だということはあり得ない。 三値の真偽値の割り当てで証明不可能性が証明できることもあるけど 証明できないことも多いと思う。 570 名前：１３２人目の素数さん mailto:sage [2011/04/26(火) 21:07:16.28 ] >>569 ここはエレキな人が多過ぎて困りますなあw 571 名前：566 mailto:sage [2011/04/26(火) 22:10:07.14 ] >>569 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Aを証明できないことをいう。 さらにその公理系Sの中のすべての公理と推論規則が独立なら 公理系Sは独立。 という主張をうまく書こうとしたところ変な文章になっただけです。 なぜ、「Aも¬Aも証明できないときに「独立」」という定義に しないかといえば、 ¬という記号が公理系で必ずしも定義されているか不明だからです。 （公理的集合論やるなら気にしなくてもいいかもしれませんが。） 例えば¬AがA→⊥のメタ理論的な略記だとしても、 ⊥が公理・推論規則に含まれていないために、 単なる命題変数になっている場合もあるかもしれません。 それから3値論理はそういう方法もありますよ、位に行っただけです。 一般的に独立を証明する巧い手段は知りません。 572 名前：１３２人目の素数さん mailto:sage [2011/04/27(水) 00:21:21.26 ] そういや、公理がそれぞれ独立なZFて誰か考えないのかな？ どうすれば良いのか想像もつかないけど…… 573 名前：１３２人目の素数さん [2011/04/29(金) 08:43:43.06 ] 数理論理学の組み合わせ論的研究の本OR分野を教えてください。 上の論理式の総数みたいなやつです。 574 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 09:47:53.77 ] www.amazon.co.jp/dp/4320122097/ 575 名前：１３２人目の素数さん [2011/04/29(金) 23:10:35.52 ] >>558 ＞意図的に日常さはんじをちゃめしごとと読んだり、 ＞既出をガイシュツと呼んだりする、 ＞当たり前だのクラッカーみたいなノリで言ったんですよ。 若者＝バカモノっていうのはホントだね。 ホルモンが無駄に出てるせいかな？ 576 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:29:08.45 ] >>558が若いのか結構年取ってるのかも分からないし 仮に若かったって若者が皆バカって訳じゃないと思うけどなあ 577 名前：１３２人目の素数さん mailto:sage [2011/04/29(金) 23:44:05.25 ] >>571 それ「独立 independent」じゃなくて普通に「証明不可能 unprovable」で良い話だよね 578 名前：１３２人目の素数さん [2011/04/30(土) 10:50:22.25 ] >>577 大抵の論理学の本に書かれている定義に準拠しているなら、 独立は証明不可能より条件が強いと思います。 独立性は「公理と推論規則に無駄がない」という主張です。 証明不可能は理論の持つ公理と推論規則だけで 特定の論理式の証明図が書けないという主張です。 579 名前：謝罪 mailto:sage [2011/04/30(土) 10:56:05.79 ] >>571 を読み返してみたところ間違っていました。 「ある公理系Sの中の公理（推論規則）Aが「独立」である。」 というのは、その公理系SからAを取り除いた 公理系Tの公理・推論規則とそれから証明可能な式だけで Sで証明可能な式でTでは証明できないものが存在すること。 でした。 580 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 11:18:11.62 ] >>579 謝罪を受理しました。 では続きまして、『賠償』を求めます。 宜しくお願い致します。 581 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 12:13:51.50 ] まぁ独立性って言葉を使うから議論が起こるわけで、 単に公理と推論規則に無駄がないって言えばいいんだと思う。 加えて言うと、独立性はもちろんのこと、 完全性や無矛盾性さえ体系には必要ない。 582 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 16:41:03.73 ] ある公理が公理系に対して独立であるというのは、 公理系に肯定を付け加えても、否定を付け加えても矛盾しないってことです。 無駄がないとかアホか。 583 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 19:01:36.70 ] で結局どの独立がホントの独立なんよ。 584 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 19:56:17.91 ] 多分>>579は現代数理論理学序説(P56)に載っている奴だと思う。 これと>>582は同値だけど、こっちの方が良く見かける。 585 名前：１３２人目の素数さん [2011/04/30(土) 20:34:00.85 ] 否定のない論理体系も考えたいからややこしい言い回しをしてるんでしょ。 意図を明示しないでもってまわった記述をするから高踏的って言われるんだよ。 586 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:05:18.03 ] >>579 揚げ足ですが、 普通公理系って閉論理式の集合だから 推論規則は入らないと思いますよ。 形式体系とか言った方が無難だと思います。 587 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:08:55.34 ] >>577を独立って言っているケースもあるよね。 >>582より弱くなるはずだけど。 588 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:19:28.53 ] 否定のない体系では無矛盾性とかどうなるんだろう... 589 名前：１３２人目の素数さん mailto:sage [2011/04/30(土) 22:21:07.74 ] 現代数理論理学序説みたいに部分構造論理とかBCK論理の話とか、 様相論理みたいにS3とS5は証明できる式が違うとか そういうことをやりたい場合の独立性の話をしてた訳ね ヒルベルト式の述語論理に限って言えば、 ああいう体系の独立性を調べる作業は ただの面倒くさいだけのパズルに過ぎないと思う あと、カット除去定理があるからsequent計算のカット規則は「独立」ではないわけだけど だからといって無駄がある、というような見方が如何に浅薄かというのも 証明論の本によく書いてあると思うけどね カットを使わないと証明の長さが指数関数的に長くなる >>581 無矛盾性は大抵の場合は必要だけどね 590 名前：１３２人目の素数さん mailto:sage [2011/05/01(日) 07:36:51.86 ] >>589 > 現代数理論理学序説みたいに部分構造論理とかBCK論理の話とか、 > 様相論理みたいにS3とS5は証明できる式が違うとか > そういうことをやりたい場合の独立性の話をしてた訳ね この場合の独立性以外ってのは例えばどういったものがあるのでしょうか？ 591 名前：１３２人目の素数さん mailto:sage [2011/05/01(日) 09:26:47.68 ] 例えばShoenfieldの本の演習問題みたいなやつとか。 結果自体の意義としては、独立だと分かったからどうなの？ ということになっちゃうので、あくまで独立性を示すためには 新しい真偽値もどきを定義したりしてこういうことをやるんだよ、 というテクニックの習得のためだけに設けられた演習問題だと思う 592 名前：１３２人目の素数さん [2011/05/01(日) 22:58:39.80 ] BCK論理とか様相論理の各公理系についても、 体系の強さが相対的に比較できれば良いだけ。 ある論理式が証明できるかどうかに着目しているため、 体系自体の独立性が問題になることはない。 また否定のない体系ではすべての論理式が証明可能であるため、 あまり意味のない体系になる、零環やX/=みたいな 数学的に面白みのない構築物になる。 根源まで戻れば論理学も所詮組み合わせ論的構造の産物でしかないし、 意味のない構造が無数に作られる。 こういった主張をするのならばそれは、 「すべての数学はグラフ理論（または数論、2進数）で書きかえられる。」 といった、「数学は記号で書かれている。」といった主張と 同レベルの無意味な議論になってしまう。 もちろん根源はバベルの図書館的宇宙における カオス的情報の広がりへと到達してしまい 人類は自ら数学という精神活動を停止させることになる。 593 名前：１３２人目の素数さん [2011/05/01(日) 23:00:30.52 ] >>592 誤：また否定のない体系ではすべての論理式が証明可能であるため、 正：また否定のない体系ではすべての論理式が定理であるため、 594 名前：１３２人目の素数さん mailto:sage [2011/05/02(月) 01:39:50.54 ] たとえば BCK 論理ではすべての論理式が定理となると 書いていることに気づかないのかなあ。 595 名前：１３２人目の素数さん mailto:sage [2011/05/03(火) 12:31:38.14 ] すいませんが、 ススリン線を加えたZFでも ストリクト・ヴァイハードの定理は成り立つのでしょうか？ 596 名前：１３２人目の素数さん mailto:sage [2011/05/03(火) 22:00:08.65 ] 成り立つよ。 ¬SHならGCHやdiamondを加えたものでも成り立つ。 597 名前：１３２人目の素数さん mailto:sage [2011/05/04(水) 10:43:55.19 ] パタゴニアの庭とかいわれる順序が 入ったErdos Universeに非分岐独立なType構造を定義すれば、 ススリン仮説が無効化されること、 いわゆるパタゴニア予想が去年肯定的に解決された。 598 名前：１３２人目の素数さん mailto:sage [2011/05/05(木) 11:10:17.61 ] ﾊｲﾊｲﾜﾛｽﾜﾛｽ そのハッタリを張る能力を生かして、 数学なんかやってないでSFとかラノベとか書いた方が良いんじゃないか？ 599 名前：考えない人 mailto:sage [2011/05/05(木) 12:27:16.78 ] 公理の独立性がもしも証明されないのだとすれば、 すべての公理系の中に他の公理から 証明されるような公理が存在することになります。 この場合の被証明公理のformulaの変形、 つまりλ-formulaのβ-reductionを考えると、 無駄な関数適応や関数抽象が生じることになって、 エレガントではなくなるのではないでしょうか。 600 名前：１３２人目の素数さん [2011/05/05(木) 14:05:10.25 ] >>598 あんた良く俺が学生時代にSF幻想文学オタだったってわかったな。 やっぱ発想が似てくるものなのか。 601 名前："屁理屈王子" [2011/05/05(木) 22:02:37.49 ] おう、ｵﾂﾑいい>>1-1000 ok "勝てねぇヨゥ？">> ��c.2ch.net/test/-/soc/1297053366/67-�� みんな〜！！？(みんな〜！！？＾＞｀) 602 名前："世界的サディスト" [2011/05/06(金) 19:45:42.26 ] なんだ 《アインシュタイン共》 もう 【【【【【涙目】】】】】 か・・・・・ 603 名前：１３２人目の素数さん mailto:sage [2011/05/19(木) 21:43:03.06 ] 岩波書店　『数学基礎論』新井敏康　著 立ち読みしてたら、文献のところに HinmanのFundamentals of Mathematical Logicは大著だから 本書よりも記述が丁寧とか書いてあって焦った いやいやいや 604 名前：１３２人目の素数さん mailto:sage [2011/05/19(木) 22:54:44.24 ] もう出てるんだ。 amazonもう品切れで、中古が15,250円w >>603 あれ900ページあるもんね。 数式多いとはいえ、日本語500p.と英語900p.だと、 軽く倍以上のヴォリュームになる。 605 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 06:13:37.53 ] >>603 昨日買って読んでるけど、日本語でこれ程の内容が読める日が来て感動してる。これをきっかけに基礎論ブーム来ないかな。 606 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 17:09:24.34 ] >>605 来ない。 「基礎論」なんて勿体つけた哲学っぽい呼び方は時代遅れ、つうか「基礎論」なんていつの時代の呼び方だ。 今や変な色のついてない技術的な側面だけに着目した数理論理学が分野の呼び方としては適切だが （基礎論屋と称する連中のどれだけが実際に数学の基礎付けに本気で関心を持ってるんだよ？） Girardが「math logicは初めて応用分野を得た」と呼んだ応用分野としての理論計算機科学そのものが 今や瀕死の状態だから数理論理学も今となっては流行遅れの分野。 部分的にはモデル論とかで数学の他の分野との交流はあってそういう分野はそれなりに生きてるけど。 607 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 17:34:17.17 ] 別に数学の他の分野が特に流行ってる訳でもないけどね だいたい流行がどうとかで判断するのがおかしい 608 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 20:45:22.25 ] むしろ数理論理学は今でこそ応用計算理論を学習する際の必須科目になってるんだけどな。 これを体系的に学んできた人間とそうでない人間で問題に対する取り組み方がまるで違う。 609 名前：１３２人目の素数さん [2011/05/21(土) 21:00:32.16 ] もしかして学問板ログ消滅後、 情報学板はみんなこっちに流れてきてる？ 610 名前：１３２人目の素数さん [2011/05/21(土) 21:03:49.00 ] >>608 自分は門外漢だけどどう違うのか興味有る 611 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:10:48.33 ] 「応用計算理論を学習する際」の道具として使うのと、基礎論自体を研究するのは全く別だろ 612 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:31:02.69 ] 新井さん自身が基礎論的な立場じゃなくて、 ロジックは今や基礎論を離れて数学の一分野だって立場の人。 だから竹内の基本予想について、 当時竹内さんが基礎論的立場から言っていた 「予想の解決方法は〜であるべき」という言葉に反発する文章を書いている。 ただ最近は逆数学など基礎論的な動機が残っている分野も盛ん。 613 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:33:04.38 ] 「応用計算理論」ってのが何を意味しているかよくわからんが、 逆数学と計算量理論(特にP=NP周辺)はほとんど不可分になってきている。 614 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 21:48:27.70 ] ＞それでは基本予想の解とはどのようなものであるべきか ? ＞残念ながら竹内自身はこのことに殆ど触れていない。 ＞ひとは訝しく思うかもしれない：ここで言う 「構成的」 とはいかなる謂か ? ＞数学的に正確に定義されているか ?例えばある形式的理論Tで形式化できることが ＞「構成的」であるための必要十分条件となるTがあるのか ? ＞これに答えて曰く：基本予想のような grand program において、 ＞その開始以前にこのようなことを問うことは単なる怯儒というべきである。 ＞何が構成的か或いは得られた証明が構成的か否かは、証明 が得られてから ＞吟味すればよいし、 その価値は得られた洞察から判断するほうが生産的である。 こういうの読むと単純に数学として追求するというのとも違う気がするけどね 615 名前：１３２人目の素数さん mailto:sage [2011/05/21(土) 23:08:08.45 ] 整数論で例えれば 類体論の証明ができてから「代数的証明」を求めればいいようなものか。 616 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:00:45.29 ] >>614 そこをどういうふうに読んだの?　俺は、 < 「構成的」でなくてもいいからまずは証明すればいいじゃないか。 < 証明が得られれば、当然そこから生まれる知見があるはずで、 < 得られる前からこうでないといけないと言っても仕方がない。 と読んだ。最初ちょっとわかりにくいと思ったが。 確か同僚の渕野昌さんも新井さんの立場をそう説明していたはず。 もっと>>612のように直截的に書いてたと思った。 617 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:08:57.29 ] Girardやら高橋やらPrawitzやらの結果に関しては こういう証明方法ではいけない、みたいなことを書いてるので 新井先生の立場は>>612とはちょっと違うはず 618 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 01:11:17.37 ] >>617 それはどんな分野でもあることでは? 619 名前：１３２人目の素数さん mailto:sage [2011/05/22(日) 02:57:23.57 ] >>617 > Girardやら高橋やらPrawitzやらの結果に関しては > こういう証明方法ではいけない、みたいなことを書いてるので > 新井先生の立場は>>612とはちょっと違うはず 竹内の基本予想に対するGirardや高橋の証明は数学の証明としては正しいが 竹内の言うところの有限の立場じゃない。 新井がそれらの方法ではいけないと書いていたということは >>612の主張とは逆に新井は竹内なんかと同様に 証明論でもGentzen流の無矛盾性証明のような還元的証明論を信奉するってことで ガチガチの哲学っぽい基礎論屋ってことじゃないか。 Girardや高橋の証明方法が良くないって主張するってことは 基本予想の価値を解析の無矛盾性を与えるって点に置いてるって事だからね。 そういう目的というか価値観ならば確かに有限の立場で証明しないと意味がなくなる。 逆に竹内の基本予想を単に２階論理でのカット消去可能性という純粋に数理論理学的な命題と考える人ならば Girardや高橋の超越的な（つまり集合論を用いた）証明に文句を言う筋合いはない。 620 名前：１３２人目の素数さん [2011/05/24(火) 00:21:56.53 ] 松本先生の復刊数理論理学について質問なんですが p29で述語論理の推論規則として R1(ModusPonens)の他にR2、R3を付け加えていますが そうする代わりに論理的公理を増やすことで 推論規則を1種類(R1のみ)のままにしておくことも 可能なんですよね？ 621 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 00:48:35.20 ] >>620 一般化規則 φ->ψ implies φ->∀xψ は公理で置き換えることはできない。 622 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 10:07:43.78 ] お返事ありがとうございました もう少し考えてみます 623 名前：１３２人目の素数さん mailto:sage [2011/05/24(火) 21:40:09.21 ] >>622 こういうときは、同等になるはずの論理の体系、 例えばNKの規則が導けるか考えてみるといいよ。 624 名前：長文失礼 mailto:sage [2011/05/25(水) 23:25:03.91 ] 以前から思っていたのですが、東京大学数理科学研究科准教授の 北田均さんってかなりヤバい（というかいわゆるトンデモ）ですよね？ 先日生協書籍部に行った折に彼の「ゲーデル不完全性発見への道」を ちょっと読んでみたのですけど、本の後半に間違ったことが 堂々と書いてあります（具体的には11．5以降）。数学的に間違った 偽の定理を証明するだけならまだ良いのですが、それを根拠に独自の 「哲学的」な帰結を引き出しています。一応Ahlforsの訳書などの マトモな本も出している出版社なのに酷いものです。 625 名前：長文失礼 mailto:sage [2011/05/25(水) 23:25:50.96 ] 以前も「フーリエ解析の話」を見た時に感じたのですが、読むのが かなり大変なはずのFefermanの論文を引用なんかしているので、 技術的に高度な間違いをされているのかも知れないと思って深入りせず放っていました。 ところが先日出た本には「Fefermanによると　ω_{1}^{CK} ＞ ω^(ω^(ω^2))である」 などと頓珍漢なことが書いてあります。こんな（定義を分かっていれば） 自明なことを書くのにFefermanの名前をわざわざ引くのは異様なことです。 おそらく彼はChurch-Kleene順序数ω_{1}^{CK}の定義を御存じないのでしょう。 計算可能性理論の基礎的なことについて知っている感じもしません。 そもそも順序数の冪の定義もご存じ無いかもしれません。 626 名前：長文失礼 mailto:sage [2011/05/25(水) 23:26:09.87 ] 天下の東京大学数理科学研究院なのに、間違いを指摘してくれる同僚は 居なかったんでしょうか。今の彼のような人が東大数理で基礎論専攻を名乗っている限り、 「ロジックは哲学がかったトンデモに近い奴の集まりだ」と（特に東大の人に） 思われるのも仕方ないと思います。日本の数学研究の中枢にある大学の人が 「ロジック専攻の人」でまず思い浮かべるのが彼なのですから。 日本の数学者に東大卒の方が占める割合はきわめて大きいと思います。 アマチュア数学愛好家の個人ブログが間違っているのとは話が違います。 これは非常に憂慮すべき不幸なことですから、他大のロジック専攻の方も 東大数理に抗議するなり東大の方に知らせるなりした方がいいと思います。 今後きちんと間違いを指摘した書評が「数学」「数学セミナー」などの 雑誌に掲載されるのを期待しています。 627 名前：１３２人目の素数さん mailto:sage [2011/05/25(水) 23:26:24.53 ] 以下具体的にどこが間違っているのか書きます。両方とも同じ間違いですので 図書館にあった「フーリエ解析の話　第22章 数学は矛盾しているか？」に即して書きます。 21章までは量子論の観測問題っぽい話で内容上まったく独立していて、 331頁〜340頁の高々10頁ですのでお暇な方は図書館などで借りて読んでみて下さい。 自分で買うのはお金が勿体無いかも知れません。 北田さんは御理解されていない可能性も高いのですが、まずω_{1}^{CK}は定義上、 ωの上の再帰的（計算可能）な整列順序の順序型の最小上界となります。 従って整列順序ω_{1}^{CK}自体は算術の述語を用いてω上に定義することができません。 628 名前：長文失礼 mailto:sage [2011/05/26(木) 00:17:03.38 ] S_α:「形式的集合論」Sのsubsystemとしての自然数論、 R_α：S_αのロッサー文（ゲーデル文を取ったって同じことですが）とします。 S_αの公理にR_αまたはその否定を付け加えた理論をS_(α+1)として、 「以下同様に」S_αを全ての順序数に対して定義してあります。 ところが論理式は可算個しかないのだから矛盾する。 基礎論のほうでは付け加える公理としてConsis_αを考えることが多く、 このような命題を公理として付加する場合基礎論のほうでは上述のプロセスが Church-Kleene順序数と呼ばれる可算の順序数で終わるような制限条件が考えられている、 だそうです。なぜω_{1}^{CK}が上限なのか理解されていません。 不完全性定理の前提として理論S_αが満たすべき条件も理解されていない可能性も高いと思います。 629 名前：長文失礼 mailto:sage [2011/05/26(木) 00:19:47.54 ] その後、順序数の増加列α_nを用いて ω_{1}^{CK} = ∪_{n=0}^{∞} α_n と表し、∃n [q~(γ)≦r∧γ＜α_n] を 確かめればよいから、「与えられた式A_γがS_{ω_{1}^CK}の公理か否か」は n についての帰納法により有限回の操作で再帰的に決定できる、と書いてあります。 ∃n …… という式を確かめるために帰納法をどう用いるつもりなのでしょうか。 n と α_n の対応は再帰的ではありませんから、∃n γ＜(α_n)∧……を 自然数論の論理式としてあらわすことも、確かめるプログラムを書くこともできません。 {α_n} が超越的に与えられていることをお判りでないのだと思います。 この後S_αの拡大はα=ω_{1}^{CK}で「ストップ」し、完全となるはずなのに 不完全性定理からこれは不完全であるから矛盾する、などと書かれています。 「ストップ」とはどういうことを想定しているかは分かりません。 630 名前：長文失礼 mailto:sage [2011/05/26(木) 00:20:01.46 ] 数学を勉強していると、相矛盾する二命題を「証明」できた気になってしまうことは 意外と良くあることです。でもそれが何十年も前から研究されている理論ならば、 その理論が矛盾している可能性より先に、自分の理解が間違っている可能性を強く考えるのが 常識的な態度ではないでしょうか。「よって数学は矛盾している」のような結論を 出してしまうのは、角の三等分家の類と同じ思考回路であると言わざるを得ません。 後はちょっとどこから突っ込めば良いか分からないので以下御説を全て引用します。 631 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 00:21:37.80 ] (pp.339-340) このようにメタのレベルにおいても集合論が成り立つと仮定し集合論的論理を 対象理論である形式的集合論自身に適用しようとすると矛盾が生ずる。 ヒルベルトのプログラムでは有限の立場に立ち、メタのレベルでは有限回の操作しか許さないとし、 その上で対象世界では有限を超えた無限の存在を扱おうとする。こうする上では 以上述べたような矛盾は生じないが、対象世界が無矛盾と仮定すると不完全になる。 さらにこの無矛盾性自体が有限の立場では決定不可能となる。しかしこれを逆手に取り、 メタのレベルと同様に対象の世界自体も有限の立場に立つものとすると矛盾は生ぜず、 かつ対象理論は完全になる。正確に言えば対象理論たる集合論において無限公理を仮定しない、 632 名前：長文失礼 mailto:sage [2011/05/26(木) 00:21:50.56 ] あるいは自然数論においては数学的帰納法を仮定しなければ対象世界とメタの世界は 互いに対称になりかつこの設定において対象世界は完全かつ無矛盾となる。 上記で矛盾が現れたのは対象世界およびメタの世界の両者において 対象に無限公理を措定したためである。すなわち問題が生じたのは「無限」という実体が 対象世界およびメタの世界において存在すると仮定したからであり、「無限」が実体ではなく、 ある「仮想の存在である」とすれば数学は無矛盾かつ完全なまま存在する。 すなわち「数学的実体は計算可能なもののみであり、無限はその計算可能性を探る 補助的手段である」という立場に立てばヒルベルトのテーゼ 「無矛盾性と完全性を数学理論の健全性の証とする」は復活する。 （引用終） 633 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 01:40:49.16 ] ブログでやれ 634 名前：１３２人目の素数さん mailto:sage [2011/05/26(木) 08:18:32.04 ] チャーチ・クリーネは岩波数学辞典に定義が載ってたね 635 名前：１３２人目の素数さん mailto:sage [2011/05/27(金) 22:25:46.95 ] よくわからないけど、数学ガール読むより為にならない本ってこと？ 636 名前：１３２人目の素数さん mailto:sage [2011/05/28(土) 15:27:54.55 ] 社会勉強になるかも。 637 名前：１３２人目の素数さん mailto:sage [2011/05/30(月) 17:00:59.04 ] ガスライティング 638 名前：１３２人目の素数さん mailto:sage [2011/06/01(水) 16:30:18.32 ] 「数学ガール」とは、部落、在日出身の女の子が差別を克服するために数学を研究する物語。 639 名前：１３２人目の素数さん [2011/06/02(木) 20:15:06.08 ] すみません、最近集合論を勉強し始めたものですが質問させてください。 集合族{A_x : x in X}があったとして、直積 Π(x in X) A_x　(以後単に「ΠA_x」と書きます) 各xについて、それぞれ�@A_x={1}のとき、�AA_x⊂N(自然数の集合)、�BA_xの濃度が可算 (∀A_x≠Φ)⇒(x in X) A_x　(以後単に「ΠA_x」と書きます) 各xについて、それぞれ�@A_x={1}のとき、�AA_x⊂N(自然数の集合)、�BA_xの濃度が可算 (∀A_x≠Φ)⇒(ΠA_x ≠ Φ) が選択公理なしのZFで成立しますか？？ ちなみに私の考えでは�@する。�Aする。�Bしない。 です。 640 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 20:53:54.97 ] 質問は質問スレで. 641 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 20:58:29.45 ] ∀の使い方がおかしい 何を言いたいか半分想像で答えると、>>639の考えの通りでo.k. 642 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 21:31:42.98 ] 他の分野と比べて質問スレに基礎論の質問してもかえってこないorちんぷんかんぷんな答えが返ってくるからしょうがないっちゃしょうがないんじゃ。。。 643 名前：１３２人目の素数さん mailto:sage [2011/06/02(木) 21:41:14.33 ] 基礎論の質問スレがあったよね。 なぜか基礎論に関係ない高校数学の質問とかが定期的に投げ込まれるっていう伝説のスレが。 644 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 00:44:16.80 ] >>643 > 基礎論の質問スレがあったよね。 > なぜか基礎論に関係ない高校数学の質問とかが定期的に投げ込まれるっていう伝説のスレが。 「数学基礎論」って数学の専門家以外からは「数学の基礎的な範囲」とか「基礎数学」って思われてるんだろ あそこは本当に基礎論の質問をするには使い物になってなかったし、以前のサーバークラッシュであのスレは消滅したまま誰も再び立ててないんじゃないの？ ここもそんなにレスが多いわけじゃないから真面目な質問なら許してあげていいと思うが 645 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 00:56:22.43 ] > あのスレは消滅したまま誰も再び立ててないんじゃないの？ 残念だったな、ここがその伝説のスレだ。 前スレが急に変なスレタイを採用して、このスレがそれを継承しちゃったけどね。 see >>2. 646 名前：M_SHIRAISHI mailto:eurms@hb,tp1.jp [2011/06/03(金) 05:00:59.00 ] www.age.ne.jp/x/eurms/Ronri_Kaikaku.html 647 名前：１３２人目の素数さん mailto:euler [2011/06/03(金) 05:16:55.68 ] >>646 なっ・・・なんなんだよそれ・・・ 648 名前：１３２人目の素数さん [2011/06/03(金) 07:21:08.29 ] �dデモと見える学説に対しては、一般論として、我々は 非常に、慎重でなければならないと思う。 学問の歴史を振り返ってみれば、最初は、大多数の人間には、�dデモと思われていた学説が、 のちのち、定説となったものが「実に多い」からだ。 有名なところでは、地*球*説にしてしかり、地動説にしてしかり、大陸移動説に してしかり。 ド・プロイの電子波説にしても、提唱された当初は、物理学者一般には「物笑いの種」だったし、 また、アインシュタインの特殊相対性理論の場合も、最初は、トップクラス物理学者の中の また、ごく一部の人に認められただけだったという歴史的真実を直視すべきだろう。 ここで、ネット数学四天王と呼ばれている面々について考えてみると、 先ず、愚将：松芯痰(＝松本真吾＠鉄道総研)については、見るべき理論は無い （旧説を墨守しているに過ぎないｗｗｗ）ので、論外として、 イマイ爺(www.suzu.or.jp/pub/imai/)の場合は、一応、独自の"理論"は立てているが、　 何んせ、「程度が低くて」問題にならない。 むしろ、それを読んだ中・高生に"害"を及ぼす怖れの ほうが大きいと思われる。 一方、ヤマジン(山口人生)の例の"証明"のほうは、�dデモのままで終わると見て間違いないだろう。 注目すべきは、エムシラ(つーか、ＥＵＲＭＳの)理論だろう。 www.age.ne.jp/x/eurms/Ronri_Kaikaku.html www.age.ne.jp/x/eurms/ 四色定理の証明や不可完全性定理についての論考さえも隅っこ扱いされているような、壮大な理論で、 ちょっと判断に迷うが、ひょっとすれば ひょっとするという気持ちを抱かせる《何か》」がある。 University of Cambridgeで講演したよう（www.age.ne.jp/x/eurms/Monogatari.html）だけど、 聴衆を席巻してしまった可能性、無きにしもあらずだろう。 今後、何年後以降からは、世界の論理学の教科書はすべてＥＵＲＭＳの理論に準拠したものになる*かも*知れない。 649 名前：１３２人目の素数さん [2011/06/03(金) 07:43:31.95 ] また本人降臨かよ 650 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 10:54:49.84 ] >>646,648 ゴミはゴミ箱へ 651 名前：１３２人目の素数さん [2011/06/03(金) 11:30:17.24 ] 業務連絡、業務連絡！！！！ このスレは、エムシラとその共鳴者どもに 乗っ取られますた！　(＾＾；) 652 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 11:32:06.81 ] どうも、「M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。 例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(¬Ｑ⊃¬Ｐ) で表わされるもののこと と考えられていたのだっただが、これは、どうやら、誤りだったようだ。そして M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［¬Ｑ(ｘ)⇒/x/¬Ｐ(ｘ)］ こそが、対偶律を正しく捉えてたものと考えられる。 M_SHIRAISHI氏（たち？）の主張する「論理革命」は、おそらく、世界を席巻 することとなろう。 653 名前：１３２人目の素数さん [2011/06/03(金) 11:39:25.22 ] 官軍と賊軍との戦いが、今また始まるか（ｗ 愚将；松芯痰の出番は、無いと思われ。 654 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 11:44:14.24 ] >>651 早々と白旗を上げた香具師が居るようだ。ｗｗｗｗ 655 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 12:04:44.20 ] 御大(M_SHIRAISHI氏)つーか ＥＵＲＭＳの人たちもいろいろと、つーか 「もの凄い苦労（多分）」したろうなぁ〜。御大の ペ―ジ をよく詠んでみると、 こんな記述がある↓ >「あっちが立てば、こっちが立たず・・・」、「こっちが立てばあっちが立たず」 これって「矛盾だらけ」ってことだよなぁ〜。そりゃ苦労するわ。 それに何よりも、Fregean 理論（＝要するに今の論理学の「標準理論」ｗ）での 「もしも・・・ならば・・・」の解釈は、驚いたことに、 古代ギリシャにまでさかのぼる問題だったらしい。　それをものの見事に 解いてしまっている。　凄いぞ！　マジで！！！） それに比べて、松芯痰（＝松本真吾＠鉄道総合研究所）はどうだぁ？ そりゃ、某私立（私立と言ってもいろいろあるから、まぁ、一応ｗ 超一流の 私立の）修士課程を出てる。 でも、その程度 ---- 言ったら語弊があるかも知らんが(ｗ ---- のことで、 論理学をかじったつーか、教科書に書いてあるんだから、それが正しんだって 頭から信じ込んじゃって、今の理論には矛盾があるってことすら 気がつかなかった。 それでいて fj.sci,math に なんだぁ、「ＥＵＲＭＳのページがここにあります。 ここを読んだら３日（一週間？）笑えます」とかなんとかの趣旨の記事 投稿したんだよな〜。 そりゃ怒るは、いかに温厚な人でも。 656 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 12:09:24.46 ] このスレッドは終了いたすますた。　軽薄。　マツシン 　　　　　　　　／:::::::::::::::::::::＼ 　　　　　　　／::::::::::::::::::::::::::::::::＼ 　　　　　　　|:::::::::::|＿|＿|＿|＿|＿| 　　　　　　　|＿|＿ノ∪　＼,, ,,／ ヽ 　　　　　　　|::（ 6　　ー─◎─◎　） 　　 　 　　　|ﾉ　　（∵∴∪（ o o）∴） 　　　　　　|　　　<　　∵　　 ３　∵> 　　　　　／＼　└　　　　＿＿_　ノ 　　　　　　 .＼＼U　 　＿＿＿ノ＼ 　　　　　　　　 ＼＼＿○○＿）　　ヽ 657 名前：１３２人目の素数さん [2011/06/03(金) 12:13:16.29 ] 　　　 (~) .　 γ´⌒｀ヽ .　　{i:i:i:i:i:i:i:i:} 　 （　｀・ω・´） ｶｷｶｷ 　　ﾉ つ:::：:φ))＿＿＿＿ ￣￣＼　　　 　　　 ＼ 　　　　　　　　　　(~) 　　　　　　　　γ´⌒｀ヽ 　　　　＿＿＿{i:i:i:i:i:i:i:i:} 　　　 （　　(⌒（ ´･ω･｀）＼ 　　　　＼　ヽﾉ（,,⊃⌒O〜　ヽ 　　 　 　 ＼ ／／*;;;::*:::*::::*⌒) 　　　　　　　(　(*:::;;:*::;;::*.::::*::::（ 　　　 　 　 　 ＼＼:;;;*::::*:::*::::*:::＼ 　　　　　　　　 　＼`〜ー---─〜' ） 　　　　　　　　　　　￣￣￣￣￣￣　 658 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 12:18:25.75 ] 失礼します。 日程　　５月１８日〜４週間 　　　　　　　　午前中・・・グループレッスン 　　　　　　　　午後・・・・・１時間個人レッスン 成田空港から大韓航空機で　　　　　　　　　　　　　　　　　　　　　　　　　　　 ホームステイ（食事つき） 総費用・・・約５０万円 他に適当なコースがあれば，又紹介するということですが， とりあえずこれでＯＫしようと思います。 松本真吾は、その存在がマンガ的だ。 659 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 12:21:15.62 ] はい 660 名前：１３２人目の素数さん [2011/06/03(金) 12:29:44.68 ] ＞誰かエムシラの論理改革をコテンパンにしてくれ コテンパンにしようとして、本人がコテンパンにされてしまった （京大などの助手・助教授クラスを含む！）のが実情なんだよなぁ〜。 # コテンパンにされてしまったヤシのうちで、もっとも悲惨な例が スンゴ（＝松本真吾）。 エムシラ本人はケンブリッジ大学での講演を公言してしてるんだから、 　コテンパンにされるのを願うとしたら、頼みはケンブリッジの教授連だろ。 　日本には御大に太刀打ちできる者いないと思われ　(＾＾；) 661 名前： ◆wsw/phmDOE mailto:sage [2011/06/03(金) 12:34:18.99 ] てす 662 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 13:04:42.56 ] 荒らすためににまた古いネタひっぱりだしてきてご苦労なこった 663 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 13:28:43.32 ] 狂人に「お前は狂ってる」と言ったところで無駄。 それを認められないところが狂人の狂人たる所以。 狂人は論理的に無敵なのだ。 664 名前：M_SHIRAISHI mailto:eurms@hb.tp1.jp [2011/06/03(金) 17:35:30.37 ] ゲーデルの、いわゆる、「不完全性定理」は見直されなければならぬ。 www.age.ne.jp/x/eurms/GDL.html#00 665 名前：M_SHIRAISHI mailto:eurms@hb.tp1.jp [2011/06/03(金) 17:47:44.02 ] 論理学と同様、２０世紀の確率論の標準理論（＝コルモゴロフ理論）も 変革される運命にある。 www.age.ne.jp/x/eurms/Kaku-Mokuji.html 666 名前：１３２人目の素数さん mailto:sage [2011/06/03(金) 18:19:20.69 ] >>662 >>663 こいつらは、松芯痰（こと、松本真吾＠鉄道総合研究所）並みの「マヌケな“賊軍”」ｗｗｗｗ 667 名前：１３２人目の素数さん [2011/06/04(土) 02:49:25.18 ] んじゃここは隔離スレにでもしてロジックの本スレは別に作ろうか。彼一人でずっとここに書いてりゃ満足するだろ。 668 名前：１３２人目の素数さん mailto:sage [2011/06/04(土) 10:14:41.35 ] 御大は目下「赤碕精神病院」に入院中とか・・・・。 #それが本当だとすると、既に《隔離中》なのだが。。。 669 名前：１３２人目の素数さん [2011/06/04(土) 10:27:35.49 ] 胎児よ 胎児よ なぜ踊る 母親の心がわかって おそろしいのか 670 名前：１３２人目の素数さん [2011/06/04(土) 12:05:22.26 ] >>665 目から鱗！　 671 名前：１３２人目の素数さん [2011/06/04(土) 14:44:00.40 ] (･∀･) ﾆﾔﾆﾔ 672 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 06:11:56.11 ] >>668 精神病院に入院中の身でインターネットできるの？？？？ 673 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 06:12:19.66 ] >>668 精神病院に入院中の身でインターネットできるの？？？？ 674 名前：１３２人目の素数さん [2011/06/05(日) 09:57:57.44 ] >>687 ＞んじゃここは隔離スレにでもしてロジックの本スレは別に作ろうか。彼一人でずっとここに書いてりゃ満足するだろ。 そう言やぁ、昔、「南北朝時代」やってたなぁ〜ｗｗｗｗ 南朝スレ＝愚将：松芯痰ひきいる「賊軍」。 北朝スレー御大ひきいる「官軍」 # 因みに、前回は「官軍」の圧勝に終わった。　(＾o＾) 675 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 10:03:01.43 ] エムシラ＝ネットのオモチャ 676 名前：１３２人目の素数さん [2011/06/05(日) 11:46:10.91 ] (･∀･) ﾆﾔﾆﾔ 677 名前：１３２人目の素数さん [2011/06/05(日) 17:51:14.99 ] 松芯痰 むかしゃ（昔は）ネットの 鼻つまみ 今じゃネットの笑いもの 　　　　　　 　　　　　　　　啄木　圖 678 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 18:15:33.77 ] 某スレより引用＆編集。 m(_ _)m ＞具体的に、どの主張でもって　M_SHIRAISHI 氏が *大、dai, dai, DAI 先生* であると確信されるに到ったのですか？ 松本真吾氏と M_SHIRAISHI氏との論戦は、意外にも！、 M_SHIRAISHI氏の連戦連勝であったことです。　 罵倒が多く混っており、それは戴けないと思ったけれども、「それ」を差し引いて読んでみると、 M_SHIRAISHI氏の論旨は極めて明解／明晰であり、松本真吾氏は*完敗*に終わった。 679 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 18:55:07.22 ] どちらもキチガイなので勝った負けたは論評に値せんよ 680 名前：１３２人目の素数さん [2011/06/05(日) 18:56:14.10 ] それらを包括する概念がメドベージェフ還元。 681 名前：１３２人目の素数さん mailto:sage [2011/06/05(日) 23:03:13.21 ] 官軍は必ず勝つ。　 丸（○）書いて、しめ（〆）書いて、屁こいて、マンコ舐めて、糞して、寝るスッ！ 682 名前：猫 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 00:44:01.96 ] >理由があるかどうかはともかく、痴漢で懲戒免職後に受け入れてくれる大学などないだろう。 >未練があろうが、日本の大学への復活は無理。 >最近の研究業績はいまいちなので、海外の大学で給料をもらうのも無理。 猫 683 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 00:45:48.46 ] あんでぃ 684 名前：１３２人目の素数さん [2011/06/06(月) 02:16:53.05 ] 本スレマダー？ 685 名前：猫は根気 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 02:49:17.12 ] >>683 今後もそういう風に精進して下さいませ。 猫 686 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 06:41:01.57 ] >>685 バカですみません あんでぃ 687 名前：猫と貉 ◆MuKUnGPXAY mailto:age [2011/06/06(月) 08:35:51.83 ] >>686 『あんでぃ』へ、 貴方は馬鹿ではアリマセン。ですが貴方の計画は私が阻止スルという考 え方を私はしています。但しもし貴方の考えを私が正確に理解していれ ばですけど。 猫 688 名前：あんでぃ ◆AdkZFxa49I [2011/06/06(月) 10:46:44.22 ] >>687 私に計画はアリマセン 私の計画をどのように貴方ハ捉えていますでしょうカ？ バカですみません あんでぃ 689 名前：１３２人目の素数さん mailto:sage [2011/06/07(火) 09:47:55.46 ] >> ﾜﾗﾀ｡ ﾁｮｳ､｣ﾈｼﾞﾚｿ｡ 690 名前：１３２人目の素数さん mailto:sage [2011/06/08(水) 14:32:08.51 ] 無計画という計画が存在するか？ 無関係という関係が存在するか？ 691 名前：１３２人目の素数さん [2011/06/09(木) 22:24:03.46 ] 大学の数学の講義で，命題p→qを証明する際に 教授がq'→p'として対偶が元の命題と同値であることを 用いて証明する方法を背理法と述べていましたが 誤りですよね？ 講義後に背理法を用いて証明した内容を質問しに言ったら背理法は「q'→p'として〜」と言われて話が通じませんでした。 692 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:31:04.48 ] 対偶法ですね 693 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:54:00.85 ] 背理法の一種に対偶法があると理解するのが一般的だな。 694 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 22:57:13.64 ] 異端の中では一般的なんだろう 695 名前：266 mailto:sage [2011/06/09(木) 23:03:23.15 ] 矛盾からは何でも証明できるような体系であれば（大抵は） >>693の逆も言える つまり、背理法も対偶法も見た目が違うだけで同じこと 696 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:05:03.13 ] 失敬 名前欄の266は忘れてくれ 697 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:06:07.29 ] 釣り師の存在を把握した 698 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:17:58.84 ] 数理論理学の教科書によく書かれている、解釈、構造、モデルとか、いわゆる意味論について について聞きたいんだが、 この解釈とか構造とか呼ばれるのもって結局何なの？ 対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？ でもそうすると、実数濃度の対象領域は定義できないし、どうするの？ あと、教科書とかに解釈の例として、「peano算術公理の解釈として自然数をとる」 として、各記号を通常の自然数論と同じように解釈する、 とか平気で書いてあるけど、じゃあその「自然数」ってなんなのかという話になる。 こんな書き方が許されるなら、ZFCの解釈として、「集合を取り、各記号を通常の集合論と同じにする」といえば、 もうこれはFZCの解釈なの？ あと、解釈（構造）の定義に平気で「集合」とか、「写像」とか 集合論に属する言葉を使ってるがこれは集合論が信頼できるという前提に立っているのか？ 699 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:25:06.61 ] メタレベルで名前付けただけのところに、勝手に意味論がどうたら言い出して自ら煙に巻かれてるだけのように見える 700 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:36:06.22 ] qを仮定して矛盾するからq'というのを背理法というのは問題があるけど、 この場合はq'を仮定して矛盾するからqという議論だから 実質的には同じことをやっている。 あまり問題無いと思うけど。 701 名前：１３２人目の素数さん mailto:sage [2011/06/09(木) 23:39:13.42 ] ＞対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？ そんなこと無いけど。 「意味論」と「メタレベルの議論」の違いは、 集合論の独立性証明とかを一度勉強しないとなかなか違いは理解しにくいと思う。 数学やらずに哲学的な話ばかりしてても仕方ないし。 702 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 00:23:05.73 ] >698みたいな疑問は、チューリングマシンを勉強するのが一番の近道だと思うけど、どうかね？ 703 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:19:39.65 ] ＞＞対象領域の集合とか、関数記号の解釈とかはやはり、帰納的に構成されるものでなければならないのか？ ＞そんなこと無いけど。 じゃあ対象領域とか関数記号の解釈はどういった方法で決定（定義）するの？ そもそもこの解釈の存在で恒心、充足可能とか定義することにどれだけの意味があるんだ？ そのような用語を導入すると、何かいいことでもあるの？ どうせ、すべての解釈で命題が真になるかどうかなんて議論できないわけだし。 純粋形式的に推論規則で何かの論理式が導出できるか、できないかで論じればいいんじゃないの？ 704 名前：703 mailto:sage [2011/06/10(金) 01:31:26.30 ] ためしに、「解釈」（構造）の例を挙げてみてほしい。 有限の場合は理解できるけど、無限の対象領域を持つ「解釈」とはどういう様相をしているのか。 本とかでは有限でない場合は「対象領域として自然数全体をとり、関数記号の解釈を通常の意味での加算＋*とする」 などと書かれているが、「解釈」っていうのはこんな曖昧で直感的なものでいいのか？ 形式的体系って人間の直感や経験を排斥して完全に記号的に決められた範囲で、 理論を運用するためのものなのに、 それの議論の中で「解釈」のような直感的、曖昧な概念を使わなければならないとしたら、 形式的体系を作る意味ないじゃん。 705 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:32:40.87 ] 意味論って単にブール値函数を割り当てる程度のことのはずだけど、 この哲学厨っぽいひとが逝ってる意味論ってそれとはぜんぜん違うんだよね？ 706 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 01:35:17.32 ] 恒真てのは、（許された操作を通して）記号列として等価だから その記号列にどうブール値を割り当てても問題ないってことでしょ？ 707 名前：703 mailto:sage [2011/06/10(金) 02:01:39.58 ] >>705 まさに、 ＞ブール値函数を割り当てる程度のこと という意味の意味論ですが。 対象領域が有限のときはいいとしても、 対象領域が無限のときにどうするんだ？という疑問だが。 ためしに、デデキント実数論の解釈を与えてみてほしい。 708 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 08:10:25.00 ] タルスキーの意味論は、別に 「人間の直感や経験を排斥して完全に記号的に決められた範囲で、 理論を運用するためのもの」じゃないので。 形式主義とか直観主義とかの系列にモデル論を無理に加えようとするからおかしくなるだけ。 709 名前：703 mailto:sage [2011/06/10(金) 18:20:41.40 ] >>708 じゃあ意味論って何の意味があるの？あと、結局実数論の解釈（構造）はどうなるんだよ。 Dedekind実数論を以下の公理で定義するとき、その解釈をひとつ例示してみてほしい。 Pを任意の述語として E1. ∀x(x=x) E2. ∀x∀y(x=y∧P(x)⇒P(y)) F1. ∀x∀y∀z((x+y)+z=x+(y+z)) F2. ∀x∀y(x+y=y+x) F3. ∀x(x+0=x) F4. ∀x(x+(-x)=0) F5. ∀x∀y∀z((x*y)*z=x*(y*z)) F6. ∀x∀y(x*y=y*x) F6. ∀x(x*1=x) F7. ∀x(¬x=0⇒x*x^(-1)=1) F8. ∀x∀y∀z(x*(y+z)=x*y+x*z) O2. ∀x∀y(x≦y∧y≦x⇒x=y) O3. ∀x∀y∀z(x≦y∧y≦z⇒x≦z) O4. ∀x∀y(x≦y∨y≦x) OF1. ∀x∀y∀z(x≦y⇒x+z≦y+z) OF2. ∀x∀y∀z(x≦y∧0≦z⇒xz≦yz) C1. ∀x∀y(P(x)∧¬P(y)⇒x≦y) 　　　 ⇒∃z∀x∀y(P(x)∧¬P(y)⇒(x≦z≦y)) っていわれたときにぃ、じゃぁ対象領域が規定できないじゃない！ってたしか気づくと思うんですけどもぉ、 710 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 18:29:08.44 ] 実数は高階になるだけ。 充足可能性に付いて抽象的な理解を深めるには、 エルブラン基底などはいかが? Samuel Buss, On Herbrand's Theorem citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.5.1636 711 名前：703 mailto:sage [2011/06/10(金) 18:37:20.41 ] なんで結局解釈（構造）の具体例を挙げられないの？ このことからして、モデルとか解釈とか、 それを元に定義された恒真とか充足可能とかいう概念が怪しいものだと言えるのではないか 712 名前：あんでぃは弱虫 ◆AdkZFxa49I [2011/06/10(金) 18:48:07.38 ] >>709 顔文字にしか見えン。 あんでぃ 713 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:21:41.23 ] 実数体Rを取れば当然モデルになってるでしょ。 自明過ぎてこれが嫌ならR^NをN上の超フィルタUで割ればそれもモデルになる。 意味論というのは、いわゆる有限の立場とか云われるような奴とは違う。 あくまで無限群論とか函数解析だとかと全く同様にZFCを前提にしたその上の理論で、 >>709の公理系は完全だろうかとか、濃度κのモデルは同型を除いて どのくらいあるだろうかとか、例えばそういうことを研究する分野。 集合論は使っちゃいけないんだと>>703が勝手に思い込んでるのがまずいだけ。 714 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:30:28.54 ] 黎明期の記号論理学にはフレーゲ→ラッセル→ヒルベルトの公理論と ブール→パース→シュレーダー→タルスキーの意味論という二つの相異なる源流があって それぞれ目指すものが違うのにそれを混同するからおかしなことになる。 ゲーデルと20世紀の論理学2　完全性定理とモデル理論の第三部とか 講談社学術文庫の論理分析哲学とか読むと多少は分かるようになるかもしれない。 715 名前：１３２人目の素数さん [2011/06/10(金) 22:34:17.92 ] 論理体系と代数モデルって本読んだ人います？ この本読んで数学・論理学センスを上げたいんですが。 716 名前：１３２人目の素数さん mailto:sage [2011/06/10(金) 22:47:03.85 ] >>713 自分は>>703氏とは違うけどよーわかってない人間ですが、 >意味論というのは、・・・ZFCを前提にしたその上の理論で、 やっぱそうなんですか。 完全性定理とかも明らかにZFCを前提にしてるようだし、そのあたりがずっとひっかかって たんだけど、「ZFCを前提にしたその上の理論だ」とあからさまに言ってもらって やっと少しわかるって感じです。 一応確認させてください。 > 実数体Rを取れば当然モデルになってるでしょ。 というのは、 ・ZFCのモデルMが存在するという前提をおく ・MをいじってM'という構造を作れば実数論の公理系のモデルになることがわかる ・M'をRとよぶ ということですか？ 717 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/10(金) 23:09:40.49 ] 完全性定理はじめ、モデル理論の定理は全部通常の数学を前提にしてるよ。 さらに言えば、完全性定理は証明には選択公理が必要。 デデキントの実数論に相当する論理式が 実数体Rという議論領域での解釈で恒真になるからRをモデルと呼ぶだけだよ。 718 名前：716 mailto:sage [2011/06/11(土) 00:19:15.45 ] >>717どうも。 上2行了解します。 下2行についての実数体Rという議論領域が存在するか否かとかは そもそも問題にしないというか、理論からモノが生まれるわけじゃなく その逆だってことですよね。 ただ、完全性定理の証明についてはそういう納得の仕方ができない。 719 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 01:40:33.84 ] >>718 述語論理の完全性定理なら選択公理より少し弱いもので足りる。 選択公理のようなものが必要なことは、 LKの証明図を逆にたどる方法での証明を考えてみよう。 木の存在を要求してるだろう。 720 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 06:15:56.76 ] >>718 論理学で完全性定理を証明するのは、 解析学でコーシーの定理を証明するのと同じことだよ。 位相空間を定義するのと同じように、 言語Lや論理式を定義して、議論領域Mを定義して、 それらの間の関係や性質を調べてるだけだよ。 721 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 07:29:41.81 ] いままで猶予しておりましたが、奴のあまりのしつこさと、被害の大きさから、 見逃すわけにはいかず、不本意でですが、このようなお知らせを投稿させていただきます。 ここに現れるM.SHIRAISHIという異常者に一年以上にわたり虐待を受けております。 この男、私の居住する地域住民に対して、ひどい侮辱と罵倒を一年以上にわたり繰り返し、 ひどい名誉毀損行為を行い、我々の利益や健全な生活を妨害しております。 それによって今もひどく迷惑しています。 この男の投稿記録です。 groups.google.com/groups?hl=ja&lr=&ie=UTF-8&q=author:eurms%40apionet.or.jp+ この男について何か知っておられることがありましたら、お知らせください。 お願いします。 また他にもこの男に被害を受けられた方がいたら、ご連絡ください。 www.age.ne.jp/x/eurms/KakuRitsu-0.html 722 名前：716 mailto:sage [2011/06/11(土) 07:47:16.38 ] >>719 > LKの証明図を逆にたどる方法での証明を考えてみよう。 ん・・・わからんですｗ 「式Aがvalid → Aの証明が存在する」を示すことについて言ってるんですよね？ validであることから証明図へのとっかかりが何なのかわからんです。 >>720 > 解析学でコーシーの定理を証明するのと同じことだよ。 一瞬戸惑ったｗ たとえ話、ですよね？ 723 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 08:16:13.89 ] >>722 > >>719 > > LKの証明図を逆にたどる方法での証明を考えてみよう。 > ん・・・わからんですｗ > 「式Aがvalid → Aの証明が存在する」を示すことについて言ってるんですよね？ > validであることから証明図へのとっかかりが何なのかわからんです。 完全性定理の証明に選択公理かそれに近い言明が必要な理由を説明してるんだと思う。 （シュッテ流の証明といわれるもの。） > > >>720 > > 解析学でコーシーの定理を証明するのと同じことだよ。 > 一瞬戸惑ったｗ > たとえ話、ですよね？ そうです。 どちらも習慣による数学に基いてるということ。 ZFC、NGB、ニュー・ファンデーション、トポス...何によって 形式化されるかは不明だし、知る必要もないです。 ただし、議論領域がどういった数学に基いているのかとは別の話です。 724 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 10:41:51.18 ] 直感主義述語論理の強完全性定理の証明にはACA0があればおｋ つまりRCA0 + arithmetical comprehension axiom 725 名前：あんでぃは存在 ◆AdkZFxa49I [2011/06/11(土) 10:42:47.73 ] 難しい話しですね。 あんでぃ 726 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 10:43:46.62 ] 古典論理だとWKL0だから、RCA0 + weak K nig's lemma 727 名前：703 mailto:sage [2011/06/11(土) 12:51:09.69 ] なんだ、モデルとかは、ZFCの上での議論だったのか。それなら納得出来る。 しかし、だとすると、FZC自身の解釈、やモデルといったものは どうやって議論するんだ？他の公理系を使ってそのなかでモデルを作るとかしか思い浮かばないけど、 それだと相対的な議論しかできないような。 728 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 14:42:39.48 ] >>704 >形式的体系って人間の直感や経験を排斥して完全に記号的に決められた範囲で、 >理論を運用するためのものなのに 当初はそう思われて作られていったけれど、現実は違うんだろ。 思うに今はそもそも論を見直す段階だというか、見直しもかけずに 運用してきたことに何の疑念も覚えなかった状況をなんとかしないといけない。 729 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/11(土) 15:03:20.35 ] ある言語の理論とそのモデルとの間の 数学的な操作は通常の数学を前提としている。 しかし、通常の数学である ZFCという論理式の集合のモデルを探す場合、 ZFC上で議論することは不完全性定理によってできない。 普通ZFCとそのモデルを議論する場所はZFCよりも大きい。 例えば推移的クラスというのはクラスを扱える BGという集合論上で行われている。 730 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/11(土) 15:16:12.41 ] 例えば推移的クラスというのは ↓ 例えばZFCのモデルとなる推移的クラスというのは 731 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 17:21:57.98 ] >>664 ＞ゲーデルの、いわゆる、「不完全性定理」は見直されなければならぬ。 「ゲーデルの定理−利用と誤用の不完全ガイド−」でも読んで寝ろ。 732 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 17:56:05.10 ] >>452 ＞和書しか読竹内の本がありがたく感じる。 ＞もちろん良い本だけど。 ｶﾜｲｿ（ﾅﾐﾀﾞ 733 名前：703 mailto:sage [2011/06/11(土) 20:01:46.50 ] 誤爆かいな？ 734 名前：１３２人目の素数さん mailto:sage [2011/06/11(土) 20:35:01.15 ] ZFC自身のモデルとかも普通はZFCで議論すると思うけど。 というか現代の集合論はまさにそれをやっている。 BGとZFCは無矛盾等価なので ZFCに無いモデルがBGに存在するというようなことは無い。 もちろんZFC自身がモデルをもつことはZFCでは示せないし、 また記号∈は∈でそのまま解釈したいと言った特殊な事情があるので 実際にはZFCの任意有限部分を一つ取ってそのモデルを取ったりする。 735 名前：716 mailto:sage [2011/06/12(日) 01:56:47.78 ] 完全性定理に選択公理が必要なことについては、 必要であることそれ自体は理解できるが、かえってそれゆえに結果に対する疑念に とらわれてしまっていました。 つまり、本当に証明が存在するんだろうか、って。 この疑問自体に問題があったのかも、と今になって思い始めてますがうまく表現できません。 736 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 02:34:03.50 ] 選択公理は必要ない。もっと弱いものでいい。 737 名前：716 mailto:sage [2011/06/12(日) 06:23:59.28 ] んじゃ、 ×完全性定理に選択公理が必要なことについては、 〇完全性定理に選択公理（の弱いやつ）が必要なことについては、 738 名前：716 mailto:sage [2011/06/12(日) 09:41:25.67 ] 具体物についての「確定しているはずでは？」という考えかも。 Q平行線の存在は証明できるか？ Aできない。平行線公理は独立。 Qでも実際にどうなってるかは確定してるはずでは？ Aそれは物理学の領域。数学的には複数の選択があり得る。 Qアキレスが亀に追いついた時点でランプは点いてるの？消えてるの？ Aどっちとも言えないよ。 Qでも確定してるはずでは？ A追いつくまでの点滅過程をいくら定義しても追いついた時点の状態を規定したことにはならないよ。 ↑ここまではわかってるつもりなんだけど、 Q公理を追加していった極大点としてのcomplete theoryなんて存在するの？ A選択公理の弱い奴を必要とするけど、あるよ。 Q「証明」がwell definedな概念なら、証明可能か否かは確定してるはずでは？ A・・・ ↑最後の答えとして何が適切なのか、自分でもどんな答えを望んでいるんだかわからなくなってきた。 739 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 10:32:43.81 ] >>738 >Q公理を追加していった極大点としてのcomplete theoryなんて存在するの？ >A選択公理の弱い奴を必要とするけど、あるよ。 >Q「証明」がwell definedな概念なら、証明可能か否かは確定してるはずでは？ >A・・・ そもそも、何が「追加すべき公理」か、確定できない。 740 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 10:43:29.03 ] >>738 「･･･は確定しているはずでは？」 全般に対する返答は以下の通り 「なぜそう思ったんですか？」 741 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:11:03.47 ] 完全性定理を理解してないからでしょう。 742 名前：716 mailto:sage [2011/06/12(日) 11:13:54.23 ] >>740 > 「なぜそう思ったんですか？」 に対する返答があいまいな状態なのですよ。 何かの錯覚にとらわれているんだろうと自分でも気づき始める。 →その正体がわからない→こういう場所で質問をしてみる→わかったり、わからなかったり >>738に書いたことはかなり未整理でした。 >>739 > そもそも、何が「追加すべき公理」か、確定できない。 ちょっと戸惑ったけど、complete theoryを作る過程での公理の追加について言ってるんですよね？ してみると、「証明」というものが「well definedで確定しているはず」かどうかは問題点じゃなくて、 理論（公理系）というものが何なのか「立場によって違う」のか・・ 何が「追加すべき公理」か確定できないけどcomplete theoryというものは存在するよ。 だからそのcanaonical modelを考えればいいんだよ。 Qそんなもの存在しないって立場は？ A 設問をこう変えればいいのか・・・ 743 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:34:54.97 ] とりあえず逆数学の勉強してみれば? www.amazon.co.jp/dp/4879999709 証明論も数学の一つに過ぎないってよくわかると思う。 追加追加って言うけど、元の公理系に対して、 追加した公理も、それがないと証明できない定理も同値だから。 どっちを追加してもいい。 744 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 11:45:16.56 ] >>737 > 〇完全性定理に選択公理（の弱いやつ）が必要なことについては、 違う。選択公理とは全く違う弱い公理しか必要ない。上に書いてあるだろう。 745 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 13:38:32.60 ] 選択公理って、任意の全射 f: X --> S に対して、s: S --> X で fs が恒等射となるものがあるってことですよね？ 746 名前：716 mailto:sage [2011/06/12(日) 14:31:57.00 ] >>744 > 違う。選択公理とは全く違う弱い公理しか必要ない。上に書いてあるだろう。 上に書いてあることをさらってみると・・・ >>133 > 「数学のロジックと集合論」によると完全性定理は選択公理よりもちょっと弱いらしいよ >>717 > さらに言えば、完全性定理は証明には選択公理が必要。 >>719 > 述語論理の完全性定理なら選択公理より少し弱いもので足りる。 >>723 > 完全性定理の証明に選択公理かそれに近い言明が必要な理由を説明してるんだと思う。 >>736 > 選択公理は必要ない。もっと弱いものでいい。 選択公理（の弱いやつ）、じゃニュアンス遠いんですかね。 747 名前：１３２人目の素数さん [2011/06/12(日) 15:06:32.25 ] 弱ケーニッヒじゃなかったかな。なら選択公理の弱いやつとか言いたくないだろうな。 748 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 16:27:01.40 ] 普通の公理系は整列されているから、完全性定理の証明に選択公理はいらない。 749 名前：716 mailto:sage [2011/06/12(日) 19:02:53.66 ] >>747 情報どうも。 "弱Konig"でぐぐってみたところ京大のサイトでヒットしましたが、内容はちょっとすぐにはわかりませんね。 >>748 もうちょっと詳しくお願いできないでしょうか。 750 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:12:24.28 ] まーた出てきたか「考えない人」 751 名前：716 mailto:sage [2011/06/12(日) 20:21:25.22 ] >>750 それって前スレかどこかで活躍してたコテでしょ？それとは違いますよ。 同様にうざいよ、というんでしたらごめんなさい。 と思ったらこのスレでも>>599にいたか。 752 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:29:48.85 ] >>746 完全性定理を 古典述語論理の論理記号から代数（ブール代数になる）作って、 意味づけする方針で証明すれば、 「ブール代数がある適当な集合代数で表現できる。」ことが必要だと わかる、これがACから証明できWKLと同じだということで納得できませんか。 肝心なのをひろい忘れてるじゃないか。 >>724 >直感主義述語論理の強完全性定理の証明にはACA0があればおｋ >>726 >古典論理だとWKL0だから、RCA0 + weak K nig's lemma 753 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 20:33:01.12 ] あれウムラオトって表記できなかったっけ？ 754 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:02:44.34 ] König 755 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:10:49.16 ] kingかと思った そういやkingってどこ行ったんだ？ 756 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/12(日) 21:31:30.64 ] >>749 弱ケーニッヒは 「無限の高さを持つ木の枝分かれが有限個なら、 枝の少なくとも1本は無限の高さをもつ」 というイメージ。 757 名前：716 mailto:sage [2011/06/12(日) 21:32:59.94 ] >>752 > 納得できませんか。 いろいろ質問したあげく申し訳ないのですが、これらの説明をちゃんと理解して 納得するだけの基盤がまだ自分に整ってないと判断しました。 なので納得できるorできない、とか回答できません。 WKLも理解してないんですが、ACと同様に超越的な主張なんですよね？ 「ある理論において妥当な式はその理論で証明が存在する」という具体的な主張を 証明するために、どうしても超越的な手段を必要とする、これはなぜだ？ という疑問に対する手っ取り早い回答が得たかったんですが、まだ勉強が足りなかったようです。 758 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 21:45:09.63 ] >>756をそれほど超越的に感じるのか? >>756 イメージというか定義そのものだな。 759 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 22:18:12.51 ] >>757 とりあえず逆数学勉強することを勧めるよ。 あんたの好きそうな話題を専門的に研究する分野。 760 名前：716 mailto:sage [2011/06/12(日) 22:26:53.14 ] >>758 ああ、>>756を読む前に書き込んでました。 ACと同じ程度には超越的に感じますけどね。 WKLもACも、それを否定するor使わない、という立場が成り立つと思うんですが。 仮定：　無限の高さを持つ木の枝分かれが有限個 結論：　枝の少なくとも1本は無限の高さをもつ イメージですが、これは「普通の仮定に対する強い結論」 仮定：　ある理論のすべてのモデルに対して式Aが妥当 結論：　その理論で式Aの証明が存在する こっちは、「強い仮定に対する強い結論」というイメージ。 後者を得るために前者が必須になる？ >>759 >>743で紹介されてたやつですか。とりあえず丸善で斜め読みしてみます。安いしｗ 761 名前：１３２人目の素数さん mailto:sage [2011/06/12(日) 23:34:04.59 ] >>760 『逆数学と2階算術』安いのはいいけど、 薄くて、高度なことを説明してるので基礎知識がないと読みにくいよ。 数理論理学（数学基礎論）の基礎知識として 新井 敏康『数学基礎論』を買っておく、読み通おせとは言わないから。 齋藤 正彦 『数学の基礎―集合・数・位相』で初歩的なことを確認。 完全性定理なら林 晋「数理論理学』もおすすめ。 762 名前：超越論的数学天使 ◆xKQl9rTMwao4 mailto:sage [2011/06/13(月) 00:26:49.61 ] >>760 「高さが無限で枝分かれが有限個の木は、 その枝の少なくとも1本の高さが無限」（WKL） ↓ 「枝分かれが無限個の木は、 その高さが有限またはその枝の少なくとも1本の高さが無限」 ↓ 「枝の長さがすべて有限の木は、枝分かれが有限個」 これが、 LKの証明図を下から辿る時に必要になるが 完全性定理の肝と言うわけではない。 763 名前：１３２人目の素数さん [2011/06/13(月) 05:48:12.46 ] どうでもいいが ケーニッヒ≠弱ケーニッヒ 764 名前：超越論的数学天使 ◆xKQl9rTMwao4 [2011/06/13(月) 07:00:58.82 ] 1回の枝分かれで、 2個にしか分かれないのがWKL いくつにでも枝分かれできるのがKL。 KL→WKL。 3つ以上の論理式から1つの論理式を得るような 推論規則はないためWKLで十分。 765 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 11:20:14.65 ] >>764 > 2個 < 有限個 766 名前：716 mailto:sage [2011/06/13(月) 20:43:13.01 ] きょう丸善に『逆数学と2階算術』探しに逝ったけど「絶版在庫切れ」だと。 内容確認できないけどアマゾンで注文しました。 まあ1470円だからいいか。 767 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 20:45:21.34 ] sinθって書いて下さい 768 名前：１３２人目の素数さん mailto:sage [2011/06/13(月) 21:50:20.44 ] >>760 RCA0で完全性定理が成り立つドメインがあると思えば追求してみればいい。 769 名前：703 mailto:sage [2011/06/13(月) 22:08:58.52 ] モデルの話でZFCを前提にしていいのはわかったけど、 じゃあ「任意の解釈で」みたいな言及はどう扱うの？ ZFCにクラスを「ねじ込んだ」体系ではクラスに関して∀量化子とかは使えないわけだが、 「任意の解釈で論理値trueをもつ」とかいうのはどうやって証明するの？ はじめからクラスと集合の概念があるあの体系（名前は忘れたが）を使うしかないんじゃないか？ 770 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 00:01:21.01 ] ZFCのCを無条件に前提にする必要はない。 771 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 00:49:21.76 ] ZFの話に便乗して質問です。 ZFから無限公理を外した公理系って、何か特別な名前がついていたりしますでしょうか？ 無限公理の否定を持つ有限集合ではなくて、単に無限公理が存在しないようなものです。 772 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:15:28.50 ] 名前付いてないと思いますが、 Nの存在は仮定しても無限公理がないと証明できない定理があるのは知られています。 つまり研究対象になってます。 773 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:33:10.08 ] >>769 セマンティクスを全部放棄してシンタックスのみで議論すればよい 774 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 01:56:01.23 ] >772 サンクスです。 無限を嫌う人が多いので無限公理を外した公理系も整備されているかと思ったのですが、 そうではないようですね。 775 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 07:00:58.96 ] 普通モデルとか解釈とかは集合であるようなものをとる。 集合としてのモデルが存在することと無矛盾性が同値だというのが完全性定理なので。 クラスに対する操作は若干制限されているから集合と同様に扱う事は出来ない。 776 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 07:04:34.40 ] >>773 セマンティクスを全部放棄したら、文字列だけになるから、意味がなくなり 何をやっているかわからなくなる。 777 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 09:37:04.89 ] >>774 整備？ 研究されてます。 778 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 13:12:27.11 ] >>776 シンタックスだけで解決できるなら、どんなセマンティクス持ってきても 当然（シンタックスのレベルで）解決されるということで、任意の解釈云々は そもそもそういう話だ、と言ってる。 779 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 20:40:49.33 ] >>778 よく考えればわかることだが、シンタックスはそれを信じる人の間 で成り立つことである。一方、セマンティクスは一人の人間が信じる ことで成り立つことが基本だ。シンタックスにしがみつき一人でも そのシンタックスを固守する人は存在する。数学のできない人間に 多い。 780 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 20:53:50.41 ] ZF-無限公理とPAは互いに相手を解釈できるので 同じ強さだと思って良い Kunenに書いてあるし直観的にも結構明らか 781 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 21:06:38.78 ] >>779 ぜんぜん面白くないぞ。 782 名前：１３２人目の素数さん mailto:sage [2011/06/14(火) 22:05:45.93 ] >780 そういわれれば確かにそんな感じもするね。 全順序と半順序の違いくらい？ 783 名前：１３２人目の素数さん [2011/06/15(水) 06:41:11.51 ] どうも、「M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。 例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(¬Ｑ⊃¬Ｐ) で表わされるもののこと と考えられていたのだっただが、これは、どうやら、誤りだったようだ。そして M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［¬Ｑ(ｘ)⇒/x/¬Ｐ(ｘ)］ こそが、対偶律を正しく捉えてたものと考えられる。 M_SHIRAISHI氏（たち？）の主張する「論理革命」は、おそらく、世界を席巻 することとなろう。 784 名前：１３２人目の素数さん mailto:age [2011/06/15(水) 06:44:06.05 ] www.age.ne.jp/x/eurms/Ronri_Kaikaku.html 785 名前：１３２人目の素数さん [2011/06/15(水) 08:54:40.35 ] (･∀･) ﾆﾔﾆﾔ 786 名前：１３２人目の素数さん mailto:sage [2011/06/15(水) 08:56:09.79 ] キチガイはいつも正しく、それ故大勝利をおさめる 787 名前：１３２人目の素数さん mailto:sage [2011/06/15(水) 09:42:24.67 ] 正しさを自ら定義し、それを用いて自らの正しさを証明する。 ゆえに、常に正しい。 788 名前：官軍（一兵卒(^o^)） mailto:age [2011/06/15(水) 11:29:41.40 ] 今度こそはと 想ってみても 無駄飯よ すんごクン 爆笑 789 名前：１３２人目の素数さん mailto:sage [2011/06/15(水) 12:45:44.05 ] エムシラのなりすましご苦労様です 790 名前：１３２人目の素数さん [2011/06/15(水) 13:22:26.72 ] このネタもう飽きた 791 名前：官軍（一兵卒(^o^)） mailto:age [2011/06/15(水) 14:43:54.02 ] 次の命題を「証明」せよ：− 官軍は、常に、勝つ 792 名前：１３２人目の素数さん [2011/06/15(水) 17:42:46.87 ] ﾂﾏﾝﾈ 793 名前：１３２人目の素数さん mailto:sage [2011/06/15(水) 20:10:06.43 ] 「赤リンゴは、常に、赤い」 の証明と同レベル 794 名前：１３２人目の素数さん mailto:sage [2011/06/15(水) 20:16:41.19 ] x^2=y^2=z^2=(x+y+z)^n-n(x+y+z) nを求めよ 795 名前：１３２人目の素数さん mailto:sage [2011/06/16(木) 01:53:02.89 ] マンコ舐めさせろ 796 名前：１３２人目の素数さん mailto:sage [2011/06/16(木) 06:18:45.02 ] ↑おいクソガキ 797 名前：１３２人目の素数さん mailto:sage [2011/06/16(木) 21:54:48.22 ] xyz+xy'z'+x'y'z+x'yz' これを論理回路で表すときなるべく論理素子の数を少なくしたいんですが これ以上簡略化されますかね 798 名前：１３２人目の素数さん mailto:sage [2011/06/17(金) 02:00:26.65 ] このスレッドは終了いたすますた。　軽薄。　マツシン 　　　　　　　　／:::::::::::::::::::::＼ 　　　　　　　／::::::::::::::::::::::::::::::::＼ 　　　　　　　|:::::::::::|＿|＿|＿|＿|＿| 　　　　　　　|＿|＿ノ∪　＼,, ,,／ ヽ 　　　　　　　|::（ 6　　ー─◎─◎　） 　　 　 　　　|ﾉ　　（∵∴∪（ o o）∴） 　　　　　　|　　　<　　∵　　 ３　∵> 　　　　　／＼　└　　　　＿＿_　ノ 　　　　　　 .＼＼U　 　＿＿＿ノ＼ 　　　　　　　　 ＼＼＿○○＿）　　ヽ 799 名前：官軍（一兵卒(＾o＾)） mailto:age [2011/06/17(金) 14:48:04.17 ] 　　　　　　　　＿＿＿＿＿ 　　　　　　　　 ／　　　　　　　＼ 　　　　　　　／　　　　　　　　　　＼ 　　　　　　　|　　　　　∪　／,, ,,＼ ヽ 　　　　　　　|　（ 6　　ー─◎─◎　）　　　　白豚って、エムスラじゃなくて、確(た〜す)か、ワスのことですたよ、ネッ！ 　　 　 　　　|　　　（∵∴∪（ o o）∴）　　　因幡に行って、雌豚おっかけ、精神病院(せいすんびょういん)に収容されますた。 　　　　　　 |　　　<　　∵　　 ３　∵>　 　 　 （＾＾;）　意味わからんッス ---- ワス（涙 　　　　　／＼　└　　　　＿＿_　ノ 　　　　　 　　　　　　 .＼＼U　 　＿＿＿ノ＼ 　　　　　追伸：正装すてなくて、ゴメンさい。 何せ、どこに脱いでおいたのか、わからん様に　 　　　　　　　　 ＼＼＿ ＿）　 ヽ 　　　　　　　なっつまったもんで（＾＾；） 敬白　マツシン(鉄道総研)　亡霊 800 名前：１３２人目の素数さん mailto:sage [2011/06/17(金) 14:51:25.45 ] >>799 ﾜﾛﾀ 801 名前：仙石６１ mailto:にせものことわり [2011/06/17(金) 17:01:50.91 ] >>797 AND OR の2段なら（古典的教科書的？）　これ以上はムリかな しかし最近はFGPAはメモリとおなじだから　気にせずコンテンツを書き込めばいい。 速度？　最近はあまりかわらんよ 実装技術もかんれんするからね 802 名前：べ [2011/06/17(金) 17:17:34.44 ] >>801 荒らすな 803 名前：１３２人目の素数さん mailto:sage [2011/06/17(金) 18:56:49.06 ] 合言葉は、フレ−イ、フレ−イ、NIPPON ! フレイ、フレイ、NIPPON ! フレイ、フレイ、NIPPON ! ・・・・∞ｗ！！！！ 俺、行きたかったんや、義勇兵(Volunteer)として。 すかす(Shikashi)、行けん。　広島からは、遠い！！！！ だもんで、義援金を送った。　小額(\4,000)や。。。。情けない（涙 でもな、日本国民*全員*が　\4,000　送ってみろ。 概算で、約４千億や！！！！ 804 名前：１３２人目の素数さん [2011/06/17(金) 20:12:33.50 ] >>780>>782 メドヴェージェフ次数を考えれば、 ZF-InfとPAは同型であることが証明されている。 また自然数NとPAとロビンソンのQなども同型なのである！ 805 名前：１３２人目の素数さん mailto:にせものことわり [2011/06/17(金) 21:36:32.56 ] >>802 べ　は理解できないんだ 806 名前：１３２人目の素数さん [2011/06/17(金) 21:43:19.83 ] >>805 もしかして60歳からの数学スレの仙石６０さん？ コンピューターの開発やっていらしたんですっけ？ いつの間にか仙石61になっていますね... 807 名前：１３２人目の素数さん mailto:ｊｋ [2011/06/17(金) 22:00:31.39 ] ↑こうゆうこと書き込む奴って、いつも何考えてんだろう 808 名前：あんでぃは単細胞 ◆AdkZFxa49I [2011/06/17(金) 22:12:49.49 ] さっぱり笑。 あんでぃ 809 名前：806 [2011/06/17(金) 22:47:35.38 ] >>807 自分の頭から光が広がり世界を包む、しばしば考えます。 >>808 だろうな。 810 名前：べ [2011/06/18(土) 03:24:28.45 ] 仙石61さんへ 謝罪と賠償を求めます 811 名前：１３２人目の素数さん mailto:sage [2011/06/18(土) 06:51:29.53 ] 合言葉は、フレ−イ、フレ−イ、NIPPON ! フレイ、フレイ、NIPPON ! フレイ、フレイ、NIPPON ! ・・・・∞ｗ！！！！ 俺、行きたかったんや、義勇兵(Volunteer)として。 すかす(Shikashi)、行けん。　広島からは、遠い！！！！ だもんで、義援金を送った。　小額(\4,000)や。。。。情けない（涙 でもな、日本国民*全員*が　\4,000　送ってみろ。 概算で、約４千億や！！！！ 812 名前：Volunteer mailto:sage [2011/06/18(土) 06:57:01.18 ] 31 ：１３２人目の素数さん：2010/11/13(土) 14:38:01 こんちには みさなん おんげき ですか？　わしたは げんき です。 この ぶんょしう は ＵＫ の ケブンッリジ だがいく の けゅきんう の けっか にんんげ は もじ を にしんき する とき その さしいょ と さいご の もさじえ あいてっれば じばんゅん は めくちちゃゃ でも ちんゃと よめる という けゅきんう に もづいとて わざと もじの じんばゅん を いかれえて あまりす。 どでうす？　ちんゃと よゃちめう でしょ？ ちんゃと よためら はのんう よしろく Daitai Yomeru GA, はのんう よしろく no はのんう ga Wakaran !!!! 813 名前：官軍（一兵卒(＾o＾)） mailto:sage [2011/06/18(土) 07:17:02.09 ] >>812 ：Volunteer：2011/06/18(土)18_vi_2011 06:57:01.18; JMT >>31 ：１３２人目の素数さん：(土)13_xi_2010 14:38:01; JMT ＞ こんちには みさなん おんげき ですか？　 Welcome to YOU ! and Nice to hear YOU. Wareware-wa mi-te no tohri, Genki-desu Yo! TOH-HOKU no Pacific Ocean no HouMen wa TAIHEN da kedo ne.....。(namida わしたは げんき です。 Very very very Very Nice. この ぶんょしう は ＵＫ の ケブンッリジ だがいく の けゅきんう の けっか にんんげ は もじ を にしんき する とき その さしいょ と さいご の もさじえ あいてっれば じばんゅん は めくちちゃゃ でも ちんゃと よめる という けゅきんう に もづいとて わざと もじの じんばゅん を いかれえて あまりす。 じんばゅん ----> 順番 どでうす？　ちんゃと よゃちめう でしょ？ ちんゃと よためら はのんう よしろく Daitai Yomeru GA, はのんう よしろく no はのんう ga Wakaran !!!! 814 名前：あんでぃは単細胞 ◆AdkZFxa49I [2011/06/18(土) 11:44:51.70 ] 難しいですネ。 あんでぃ 815 名前：１３２人目の素数さん mailto:age [2011/06/18(土) 12:16:10.05 ] www.age.ne.jp/x/eurms/Ronri_Kaikaku.html www.age.ne.jp/x/eurms/Kaku-Mokuji.html 816 名前：１３２人目の素数さん [2011/06/18(土) 12:31:49.82 ] どうも、「M_SHIRAISHI氏(つーか、ＥＵＲＭＳ)の理論」のほうが正しいようだな。 例えば、対偶律は、従来は、 (Ｐ⊃Ｑ)⊃(¬Ｑ⊃¬Ｐ) で表わされるもののこと と考えられていたのだっただが、これは、どうやら、誤りだったようだ。そして M_SHIRAISHI氏の言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)］⇒/p,q/［¬Ｑ(ｘ)⇒/x/¬Ｐ(ｘ)］ こそが、対偶律を正しく捉えてたものと考えられる。 M_SHIRAISHI氏（たち？）の主張する「論理革命」は、おそらく、世界を席巻 することとなろう。 817 名前：１３２人目の素数さん mailto:sage [2011/06/18(土) 12:37:31.55 ] Ｐ：［ライオンは哺乳動物である］，Ｑ：［ライオンもクジラも共に哺乳動物である］ と おいてみると：− ［ＰはＱを内含する］： ［ライオンは哺乳動物である は ライオンもクジラも 共に哺乳動物であるを内含する］ ------ 明らかに、これは偽です。 ［Ｐでないか又はＱである］： ［ライオンは哺乳動物でないか 又は ライオンもクジラも 共に哺乳動物である］ ------- こちらは真です。 一方は偽であり、他方は真であるような二つの命題 が 同義であるはずはありません。 818 名前：１３２人目の素数さん mailto:sage [2011/06/18(土) 12:40:49.12 ] 一方でA⇒A∧Bという形の命題が恒真でないことをもって「偽」とし、 他方でA⇒A∧Bがあるvaluation（現実ではたまたまそういう値）ではtrueとなることをもって「真」 として対比することに何の意味があるのか まさか、形式的な論理だけで生物学の問題が解決すると思っているわけでもあるまい 819 名前：１３２人目の素数さん [2011/06/18(土) 12:49:14.28 ] (･∀･) ﾆﾔﾆﾔ 820 名前：べ [2011/06/18(土) 20:30:02.39 ] 仙石６１へ あなたのカキコを読んで私は怒りました したがって謝罪と賠償を求めます 821 名前：１３２人目の素数さん [2011/06/18(土) 20:35:45.38 ] 私にも謝罪と賠償を求めます 822 名前：不正義屑猫 ◆MuKUnGPXAY mailto:age [2011/06/18(土) 23:25:25.62 ] >>820 貴殿の頭の悪さと無能さに立腹致しました。従って賠償だけを求めます ので５０００００００００００００００ユーロをご準備戴きます。尚、 貴殿の知性の低さを鑑みて謝罪は求めません。どうせ不可能でしょうし。 猫 823 名前：あんでぃは屑 ◆AdkZFxa49I [2011/06/18(土) 23:27:00.29 ] あんでぃ 824 名前：べ [2011/06/19(日) 00:47:26.69 ] >>822 あなたのカキコを読んでさらなる激怒を得ました したがってあなたに賠償責任が生じます 賠償責任を果たされますよう、どうぞよろしくお願い致します 825 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 00:54:04.54 ] >>824 オウ、やっと釣れたがな。そやしオマエがワシを訴えろや。ワシがオマエ を法廷で八つ裂きにしたるがな。 猫 826 名前：あんでぃは屑 ◆AdkZFxa49I [2011/06/19(日) 01:01:49.27 ] すごい。 あんでぃ 827 名前：べ [2011/06/19(日) 01:02:11.80 ] >>825 あなたがそのようなレスをするのは想定内でしたね なので私はあなたを『釣った』ことになりますね まああなたの狼狽具合をじっくり監視させてもらいますよ どうぞ楽しませてくださいな 828 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 01:06:24.86 ] >>827 では『徹底抗戦という方法』で狼狽して差し上げるので、どうぞ楽しんで 下さいまし。 猫 829 名前：べ [2011/06/19(日) 01:07:25.96 ] >>828 ではあなたに聖戦（ジハード）を宣告することになります 大変お気の毒ですけどもね… 830 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 01:10:18.80 ] >>829 全然気の毒ではアリマセンから、どうぞ宣言して下さい。当然の事として 私も全力で逆襲を行いますので。そやしナンボでも攻撃しなはれや。 アンタの攻撃を待ってるさかいナ。 猫 831 名前：べ [2011/06/19(日) 01:15:06.33 ] To 『仙石６１』 ★ALERT★ WE NEVER FORGIVE YOU. ★ALERT★ 832 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 01:22:55.62 ] >>831 早うワシを攻撃せえや。ワシがオマエをズタボロにしたるさかいナ。 猫 833 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 01:57:29.47 ] >>831 コラ、何してんねん！　ワシが傷め付けたるさかい、出て来いや。 猫 834 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 02:11:17.52 ] >>831 今夜は放置したるさかい、朝までにタップリと馬鹿無能を晒しとけや。 ワシが精読して分析し、思いっきり撲滅したるがな。頭使えよナ。 猫 835 名前：べ [2011/06/19(日) 04:33:22.82 ] 仙石６１へ 覚悟を決めてください。 836 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:35:20.69 ] >>835 ワシはずっと馬鹿を観察してるのや。オマエの馬鹿晒しはソレだけかいな？ 猫 837 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:36:32.23 ] 徹底的に追い詰めたるさかいナ。 ケッケッケ猫 838 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:37:48.16 ] コラ、どうせ見てるんやろ。サッサと反応シロや。 猫 839 名前：１３２人目の素数さん [2011/06/19(日) 04:38:43.89 ] >>べ アンタのその屑頭をフルに活用した所であんでぃすら潰せんよｗ 840 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:43:49.04 ] >>839 いやいや、おだてて馬鹿を躍らせたら、どうせ失敗をスルので、ソコを 思いっきり叩けば宜しい。そやし皆で『「べ」の高い知性』を讃えまし ょうや。ほして調子に乗って大失敗した所でトドメを刺すのが一番有効 な処分の仕方ですワ。 猫 841 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:46:42.94 ] べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜 馬鹿馬鹿ばっばぁ〜　べべべべっべっべー　馬鹿馬鹿ばっばぁ〜　べべべべっべっべー 猫 842 名前：１３２人目の素数さん [2011/06/19(日) 04:50:10.75 ] 猫さん、下級生物である『べ』の死に場所にはこのスレは立派過ぎます。 もっと、お似合いのクソスレがあるでしょう。 843 名前：猫は不真面目 ◆MuKUnGPXAY mailto:age [2011/06/19(日) 04:53:42.79 ] >>842 いや、くたばりさえすれば、私はその場所は問いません。大切な事は完全 に息の根を止めて再起不能にスル事だけですから。 猫

---

---

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

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