数学基礎論・数理論理学のスレッド　その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/ 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 ] 日本語の本は入門書のみで十分。 後は英語の世界。

---

---

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

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