数学基礎論・数理論理学　その10

1 名前：１３２人目の素数さん [2011/10/29(土) 22:42:36.86 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その9 kamome.2ch.net/test/read.cgi/math/1317639944/ 473 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:26:00.68 ] 第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、 その場合は証明の定義を変更する必要があると 474 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:27:11.10 ] >>473 ミスしました。 第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、 その場合は証明の定義を変更する必要があるとwikipediaにはあります。 しかしそれでは定理の一般化とは言えないのではないでしょうか？ 475 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:35:59.28 ] wikipediaじゃ数学の勉強にはならん。 証明読め。 476 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:38:22.54 ] >>475 新井敏康の本では証明の定義を変えているという訳ではないようです。 wikipediaの記述が間違いなのでしょうか？ 477 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:50:53.34 ] なぜわざわざω無矛盾にしたのだろうかという考察が岩波文庫の不完全性定理本にある。 478 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:26:01.91 ] >>474 証明の定義というより可証性述語の定義。 今新井の本をちらっと見たけど 第一不完全性定理の証明の前に 算術化を行ってProv(a,b)を定義していて、 第一不完全性定理でロッサー述語を一気に導入して証明してた。 ロッサー述語は定理の条件のω無矛盾が無矛盾に広げられる。 ゲーデルも論文出したときは無矛盾にしたかったらしいよ。 479 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:30:45.57 ] >>478 ということは、純粋な一般化ということでいいのでしょうか？ 証明の中でPrの定義を変更していますが、証明する事柄にPrは現れないので。 480 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:13:54.22 ] ゲーデルとロッサーの原論文を読めばすぐに済むことをわざわざ質問する意図がわからない。 481 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:15:53.77 ] ゆとり世代なめるなよ 482 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:37:03.43 ] >>479 純粋な一般化とは何だろうか？ 483 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:41:54.66 ] >>482 「ω無矛盾な公理系には証明も反証も不可能な論理式が存在する」という定理を 「無矛盾な公理系には証明も反証も不可能な論理式が存在する」という形に一般化されますが、 この時の「証明」の定義は前者と後者で別物なのでしょうか？ 新井敏康「数学基礎論」を読む限りでは両者における「証明」の定義は同じ物のようですが、 484 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:43:16.48 ] というかそういう疑問を抱く時点で両者の証明を理解してない。 485 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:51:41.38 ] 対角線論法と不完全性定理は何と何が対応しているんだ？ 486 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:56:15.96 ] ゲーデルの完全性定理、不完全性定理の証明は面倒ではあるけど難解ではないからちゃんと読めよ。 それが解れば周辺論文もそんなに難しくないことがわかる。 広中やワイルズやペレルマンの論文よりずっと読みやすいぞ、内容も平易だし。 487 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:57:58.47 ] >>485 証明を読めば解る 488 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:06:24.94 ] >>483 同じ。 >>485 対角定理で証明も反証もできない論理式をつくる。 489 名前：483 mailto:sage [2011/11/24(木) 22:08:54.76 ] >>488 ありがとうございます! 490 名前：483 mailto:sage [2011/11/24(木) 22:18:31.37 ] 何度も申し訳ありません。 もうひとつわからない部分があります。 新井敏康「数学基礎論」においてderivability conditionsのうちの (D2)Pr(【A→B】)∧Pr(【A】)→Pr(【B】) を証明してありますがよく分かりません。 考えている公理系をPAというものとして、PAの標準モデルが存在することを用いて 原始再帰的関数の問題に帰着させて証明するのではいけないのでしょうか？ 491 名前：483 mailto:sage [2011/11/24(木) 22:25:25.50 ] >>490 (D2)PA|-Pr(【A→B】)∧Pr(【A】)→Pr(【B】)です。すみませんでした。 492 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:31:42.84 ] ここまでくると何で理解できないのかが理解できない 教科書を燃やして数学を勉強するのを諦めた方がいい 493 名前：１３２人目の素数さん [2011/11/24(木) 22:41:44.91 ] >>490 よく言っていることが理解できないけど それで証明できるなら別に良いと思う。 494 名前：１３２人目の素数さん [2011/11/24(木) 22:44:30.60 ] >>486 比べるんじゃない。 価値が全然違う。 495 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:44:33.77 ] 内容をキチンと吟味せず結果だけ質問しても何にもならないよ。 496 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:45:45.54 ] >>494 価値なんぞ較べてないだろ 難易度が違うと言っている。 497 名前：１３２人目の素数さん [2011/11/24(木) 22:49:20.70 ] そんなかじゃペレルマンのが圧倒的に難解だろうな 498 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:00:28.77 ] 予備知識のあるなしによるが内容の前提が一般数学の知識内におさまらない分 ペレルマンのが一番難解かもね。 それに較べたら予備知識ほぼゼロでも理解できるんだからゲーデルの論文なんて 有り難すぎて涙が出るくらいだ。 499 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:19:46.19 ] ゲーデルの論文ひいては数理論理学は数学ではない（から素人でも理解しやすい）、という可能性は？ 500 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:24:52.14 ] 理解しやすくはない、ゲーデルは証明は厳密詳細にやってるから、全て理解するのは面倒くさい。 でもあれが数学の証明でないなら、俺は数学の証明を読んだことがないな。 あれくらい諄い数学の証明はそうそうないぞ。 501 名前：猫にコネは不必要 ◆MuKUnGPXAY mailto:age [2011/11/25(金) 00:20:49.81 ] 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。 猫 502 名前：１３２人目の素数さん [2011/11/25(金) 00:22:29.22 ] 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。 芳雄 503 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 07:12:33.12 ] >>474 wikipediaにちゃんと 「命題の証明より小さな、否定命題の証明が存在しないという性質を追加」 って書いてあるじゃん。これが(ロッサーの方法の)全てだよ。 ところで、「矛盾の証明が存在しない」はPAで証明できないが 「すべての矛盾の証明について、 　これより小さな矛盾の否定の証明が存在する」 はPAで証明できる。もし「矛盾の証明が存在しない」ならば確かに 「すべての矛盾の証明について、 　これより小さな矛盾の否定の証明が存在する」 が、逆は真ではない。したがって、このことは、第二不完全性定理に 何ら疑念を生じさせるものではない。 504 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:37:39.57 ] >>500 それは君の数学の経験が浅いだけ。 505 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:43:33.93 ] >>499 そうだね。 高校数学すらほとんど使っていない。 帰納法くらいか。 数学というよりパズル。 506 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 09:21:51.82 ] >>503 しかし僕の持っている本では証明の定義は変えてありません。 あくまで定理を示す中で証明可能性述語を変形したものを 用いるのみで、定理のステートメントにおける「証明」の定義は ゲーデルのものとロッサーのもので 変わっていません。 507 名前：１３２人目の素数さん [2011/11/25(金) 10:02:59.16 ] >>506 その「持ってる本」を明示しなよ。伏せる必要ないだろ？ 508 名前：483 mailto:sage [2011/11/25(金) 11:00:01.17 ] >>507 新井敏康「数学基礎論」です。 509 名前：１３２人目の素数さん [2011/11/25(金) 22:01:31.69 ] >>465 それは通常ｎ番目の自然数と解釈されるような 推移的集合しか記述しない。 510 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 22:15:17.39 ] \ 511 名前：１３２人目の素数さん [2011/11/25(金) 22:51:17.77 ] >>506 定理で示される証明と 可証性述語が表現する証明はちげーよ 512 名前：483 mailto:sage [2011/11/26(土) 00:51:08.93 ] >>511 それでは>>483において両者の「証明」の定義は同じということで良いのですか？ 513 名前：１３２人目の素数さん [2011/11/26(土) 01:04:28.23 ] たりめー 可証性述語はその証明も反証もできない論理式探すためのどーぐ 何を意味してるかなんてかんけーねー 514 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 02:50:11.55 ] >>504 車種・車メーカー板に居る人？ 515 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 16:29:29.28 ] >>506 ＞あくまで定理を示す中で証明可能性述語を変形したものを用いる 「その変形を、新しい証明の定義とする」と読めない奴は池沼。 516 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 18:33:06.39 ] ゲーデルの第二不完全性定理の証明は、何をもって、証明されているか ということが問題なのだ。いかなる本にも、証明は書いてないのだ。 このような、方法で、証明ができるということが書いてあるのだ。 この違いは専門家とよく話さないとわからないもので、このような ところで説明されてわかることではない。 517 名前：１３２人目の素数さん [2011/11/26(土) 20:07:34.59 ] ゲーデルの第二不完全性定理の証明ごときで 専門家と話す事なんかない。 数学としてはエレメンタリーな組み合わせ論の証明にすぎない 518 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:09:09.83 ] 哲学や論理学としてみたら一流の結果かもしれないが、 数学としてみたら二流以下の結果 519 名前：１３２人目の素数さん [2011/11/26(土) 20:21:06.16 ] 平方剰余の相互法則のような、いつまでも高いレベルでの一般化があるようなよい定理だと思うが。 520 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:51:50.70 ] 平方剰余の相互法則の一般化の様に豊かな応用が無い。 521 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:55:04.45 ] 平方剰余の相互法則は、フェルマー予想界隈の 研究からの要請があって、一般化されてきたのであって、 単にいじくりまわしていたわけじゃ無い。 522 名前：１３２人目の素数さん [2011/11/26(土) 21:04:32.09 ] >>515 証明の定義自体は何もかわってないはず。 523 名前：１３２人目の素数さん [2011/11/26(土) 21:07:30.84 ] >>516 一応新井の本には証明が全部入ってる。 ただし冪関数ありのPAだけど。 524 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 21:39:39.54 ] >>523 ３章を読み終わっているなら聞きたいんだが、 P101の補題3.3.2は証明になっていないと思うんだが、どう？ 525 名前：１３２人目の素数さん [2011/11/26(土) 21:54:48.30 ] >>521 それは出鱈目が過ぎる 526 名前：１３２人目の素数さん [2011/11/26(土) 22:01:08.85 ] >>521 どう？ 527 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 22:02:04.34 ] 訂正 >>525 どう出鱈目？ 528 名前：１３２人目の素数さん [2011/11/26(土) 22:54:15.96 ] >>527 フェルマー予想界隈の「要請」から一般化されたとか歴史的におかしいだろ。 529 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:14:52.57 ] 第二不完全性定理をどこまで弱い算術で 証明できるかという方面の研究はあるよ まあ割と些事だけどね でも518はどうせP=?NP問題とかも 数学としてはエレメンタリーな二流の問題とか言って 切って捨てるんだろうな 530 名前：１３２人目の素数さん [2011/11/26(土) 23:25:41.21 ] >>524 確かに何をやっているのか理解できない。 「でよい。　　■」って何だよｗ 531 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:37:03.89 ] >>528 平方剰余の相互法則の重要な応用として、 全ての整数が四つの平方数の和で表されるという定理がある。 この種の問題(フェルマー予想はp乗数の和の問題)を初めとして 重要な応用を目指して一般化されてきた。 無目的に一般化してきたわけでは無い。 532 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:39:27.44 ] >>529 前半。些事、そうですね。 後半。それは解けてみてからでなくては わからないけれど、今までの状況からすると その可能性はかなり高いですね。 533 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 00:02:56.01 ] >>530 やっぱりそうだよね。 どうも破綻していると思えてならない 534 名前：１３２人目の素数さん [2011/11/27(日) 00:42:06.34 ] >>531 ルジャンドルによる四平方定理の証明は1770年。 平方剰余の相互法則を証明したガウスが生まれる前のこと。 535 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:18:37.60 ] >>534 それって証明に不備があったやつでしょ？ 19世紀にディリクレが埋めたけど。 536 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:21:34.41 ] とにかく平方剰余の相互法則の応用でそのルジャンドルの定理も 証明出来るし、相互法則の一般化でより深い整数論の定理がいろいろ証明できるのよ。 537 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:44:25.69 ] もひとつ補足しておくと、 平方剰余の相互法則は、何も無いところから いきなりガウスが見つけたものじゃなくて、 ルジャンドルの平方和の研究の中に その芽があるんです。相互法則のステートメントで 使うカッコをルジャンドル記号と言うでしょ。 538 名前：１３２人目の素数さん [2011/11/27(日) 04:00:55.62 ] >>537 相互法則を発見したのはオイラーじゃなかったっけ？ 539 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 05:41:22.25 ] >>523 普通の数学の定理と異なっている内容であることに気がついていない 証拠なのだ。 第一不完全性定理とは、全く性質が異なっていることに気がつくべき なのだが、普通気がつかない。 540 名前：１３２人目の素数さん [2011/11/27(日) 06:17:01.75 ] >>539=>>516かい？ 思わせぶりなことを書いても、2chじゃただのハッタリとしか思われないよ 541 名前：１３２人目の素数さん [2011/11/27(日) 07:18:09.67 ] suimasenga 圏論と論理学の関係について教えてください 清水によれば圏は普遍論理だそうですが 542 名前：１３２人目の素数さん [2011/11/27(日) 08:31:32.56 ] >>540 ぶっちゃけ、第一より第二が大事！と発狂する奴は 「無矛盾厨」なる人格障害の可能性が大。 >>529の研究の中には、以前、紹介があった自己検証体系も 含まれると思われるが、あれはあれでちょと面白い。 どうでもいいが平方剰余の相互法則のような エレメンタリーな「算数」をありがたがる 小学生は無限を扱うこのスレッドには 立ち入らないでいただきたい。 543 名前：１３２人目の素数さん [2011/11/27(日) 08:37:22.48 ] 論理推論を算術計算でシミュレートする、というアイデアを 数学として認めたくない人はいる。大抵は爺ィだが。 544 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 09:59:03.95 ] >>540 483 にこんなところで訊くなといっているだけ。 545 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 12:40:59.08 ] >>542 平方剰余の相互法則はエレメンタリーな ままでは終わらない、とても深い理論。 代数屋はもちろん、幾何でも解析でも こんなことは常識なのに、基礎論屋とはやっぱり 感覚が違うなと感じる。 常識をわきまえたうえであえて傍流に入ると言うなら まだわかるが、常識を最初から認識してない。 数学で無い別の価値観をもった非数学分野だと いうなら、それでいいんだけど。 546 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 14:03:31.53 ] >>545 自演乙 547 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 15:37:47.45 ] >>545 平方剰余の相互法則は、幾何や解析どころか 代数でも自分の研究とは無関係と思う人は数多い。 これこそ常識であって、545の考えは他の数学者には 通用しない「俺様常識」に過ぎない。 548 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:26:01.98 ] >>547 そんな事はない。 そんな事言ってるのは、せいぜい、数学の流れを見る余裕も無く、 学位や就職の為だけの論文作成作業におわれている 底辺院生か底辺ポスドクぐらいだろ。 549 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:32:04.61 ] >>547 たぶんあなたの言っている数学者は、 かなり広義の意味であって、志の低い人たち。 歴史に名を残す様な数学者は一人もはいっていないと思う。 550 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:33:17.10 ] コイツどんだけ数論を過大評価してるんだｗｗｗ 551 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:39:40.24 ] っていうか、まともな数学者の多くは、 代数とか幾何とか解析とか数論とか、分けてなんかいないよ。 何でも使うから。 552 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:51:54.56 ] んだ。必要ならメタ数学の定理も使う。 553 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 17:04:33.97 ] >>552 少しね。でも、基礎論のアイデアを 使うだけで、基礎論の研究は使わ無い。 というか、基礎論の重要な成果のほとんどは もともと普通の数学者が作った。彼らを後世が どう呼ぶかは後世の人が決めたのであって、 やってる数学者本人は、自分の専門分野なんて 気にしてない。 基礎論からキャリアをはじめて基礎論屋を 名乗っている人のやってる研究はみんな役に立たない。 (一部の役に立てようとして研究しているものは除いて) 554 名前：１３２人目の素数さん [2011/11/27(日) 18:55:45.54 ] 今のロジックの主流はモノイダル論理ですね。 これは∧と∨を同一視したものです。 またリテラルはAと¬Aを同一視します。 これは圏論との関連もあって非常に重要な位置を 数学基礎論において担っていますね。 数論はモノイダル論理で書き換えることができます。 例の平方剰余の相互法則もモノイダル論理の一推論規則にすぎないです。 555 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 19:51:33.51 ] >>554 何の狙いがあって、そんな事をやっているのですか？ 556 名前：１３２人目の素数さん [2011/11/27(日) 19:58:40.23 ] 「すぎない」を使う奴の文章は信用しないことにしている 557 名前：１３２人目の素数さん [2011/11/27(日) 20:23:24.33 ] >>555 まずモノダイル論理はすべての計算モデルで解釈可能です。 次に非常にシンプルでコンパクト閉圏と対応しており、 数学全体の記述をすることも可能です。 おそらくモノダイル論理が導入されたのは ジラールによる線形論理の研究がはじめてでしょうが、 今では言語哲学、分析哲学、計算機科学、公理的集合論といった あらゆる世界で運用されるようになっています。 クミルの竪琴とよばれる推論規則などは 修正クリプキ構造T1-Stepを張ったデントライトの海で 展開される特殊なモノダイル論理で、ジュークの宇宙を再現することができますね。 特にフィッシャーのSSS_ΩやF0-代数との関連で注目されています。 558 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:18:49.35 ] ＞基礎論の重要な成果のほとんどはもともと普通の数学者が作った。 まず、基礎論の重要かつ基本的な成果はゲーデルによって挙げられた。 述語論理の完全性定理、自然数論の不完全性定理、選択公理の相対無矛盾性etc． 「普通の数学者」が基礎論以外の数学でも成果を挙げている、という意味なら ゲーデルが基礎論以外の数学で挙げた重要な成果を一つでいいから教えてほしい。 559 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:20:42.82 ] >>558 ゲーデル解 560 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:22:52.18 ] >>559 残念ながら、その成果は、ゲーデルが論理学においてあげた 華々しい成果に比べると大したことがない。 561 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:26:19.72 ] ゲーデルはロジシャン中のロジシャンだろ 数学者ではない、と思う 562 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:05:06.09 ] ゲーデルは相対性理論もやった 563 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:06:38.16 ] >>557 ですから、そうする事によって、何を目指しているのですか？ 564 名前：１３２人目の素数さん [2011/11/27(日) 22:16:57.58 ] >>563 理論物理や数論幾何で頻出するユニポテント群の 構造解析にマスセル-ドーソンの創造なんていう 解釈可能世界を導入する際にユニ楽園という 議論領域の全体を動くような広義圏論のステンレステンソル代数の 一つのアイディアとなるってことですね。 パースのアイディアは存在の海なんて煩雑なものだから。 565 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:22:34.16 ] 無茶苦茶やなぁ 566 名前：１３２人目の素数さん [2011/11/27(日) 22:24:23.93 ] それからブラウンが提唱した形式の法則なんかはCalculusに基く ブール代数の構成を可能にした「区別」という、 マトゥラーナ＝ヴァレラ図式による拡大可能な システムの自己観察機能による再循環になってる。 例えば「横断」による算法、これは自己同型写像による対象aの分布関数 R：Spec(�農N0)；B(a,ε)→Vll(-<>r) を意味するもので、primary algebra の公理からアイオーンの時間の固体化、 即ちリンデンバウム補数の位相が閉であること(ArrX/R)、 また複素散乱ウカシェベッチ型ベクトルの縮減対応から得られる 「埋め込み」が線型写像であること⇔Θ：ξ(Asc(3))ΛΓ(A_0)→Γ(A_0)の作用が存在する。 直線的被覆が「シミュラークルの質料」というXの規定なんかが有名。 567 名前：１３２人目の素数さん [2011/11/27(日) 22:28:12.64 ] さらにはヒルデガルド対応ってのがる。 一般Tate仮説の∃¬%がKe(C*)の底鎖列として定義される場合に、 任意カントール空間の実効的閉集合世界のMedvedev次数構造が immunityは以下の可換図式と同値。 s → bl → bel → I 　　　　　↓　↓ 　　　　　b → tl → w つまりVintage代数がストーン双対ってこと。 あとは、identification in the limit をベール空間の集合へ一般化した 学習還元可能性。学習は以下のようなもの。 心象自制有界学習(P ≦bl Q)： (∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P & #fn :(g n) , (g n + 1)g < c]: 誤謬有界学習(P ≦bel Q)： (∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P & #f(g n) : n 2 !g < c]: 剰余類学習(P ≦tl Q)： (∃ψ,;;;;,ψ_k )(∀g∈ Q)(∃m ≦ k) limnψm(gn)(g) ∈ P: あるいは、ジュリア閉集合が、 (∀m) P ∧ Im ≠�唐ﾆなるような 有理区間の計算可能な枚挙fImg が存在しないとき。 568 名前：１３２人目の素数さん [2011/11/27(日) 22:29:33.79 ] さらに、中間休止RC0が論理のイマージュとなった「差異」、 セリーの合弁写像Fmin：など、アームストロングの公理系による裏付け、 ドゥルーズのindetermineとideeの分裂など・・・。 最近では以下のようなボニファスの記述(無限還元公理)がある。 Tc1：aを中心とした推論可能域をｒをa；ｒと記述する Tc2：消滅を∃¬%とする Tc3：∃¬%のヒルデガルド対応は∃%である Tc4：∃%の次は0；ｒとする Tc5：0；ｒ→1；ｒの対応でModanponetが一階無効 569 名前：１３２人目の素数さん [2011/11/27(日) 22:30:40.26 ] ちなみにセリーの合弁写像の根拠を与える。 ギヨーム理論が数詞と内部空間をゼロ複数、S単数などの空間的配置で 形態論に内在する意味の精神過程を捉えるエルチュードだとは自明。 P; Q 2 ω＾ω だから、P がQ にculervent還元(P s Q) とは、 ある双対アルゴリズム が存在して，任意のg 2 Q に対して (g) 2 P となるときを指すから、T の定理とL反駁の 分離関数全体の集合Sep(T) はr.e.separating class と呼ばれる特殊な実効埋蔵閉集合になる。 つまり完備側芽のTerr分解X_0[−，]：が以下のように変形される。 Ps j= (8x; y)(9z)(x < y ! x < z < y). (9e0; : : : ; ek )(8g 2 Q)(9m k) em(g) 2 P これがセリーの合弁写像と同型である。 570 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:38:25.64 ] つまらない 571 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:43:35.02 ] 知の欺瞞、ﾁｮｰひもカルト、圏論カルト 572 名前：１３２人目の素数さん [2011/11/27(日) 22:49:54.30 ] 具体的な内容についていけない場合は カルトと批判すればOKとｗ 573 名前：１３２人目の素数さん [2011/11/27(日) 23:21:58.96 ] >>566-569 止めろ。アホ！ 574 名前：１３２人目の素数さん [2011/11/28(月) 00:05:28.92 ] >>572 ｗをつければ高みに立てると思っているのだろうか 575 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 02:29:48.13 ] >554 ついていけなくて悪いが……モノダイル論理ってもしかして双対を扱えるの？ もしそうならちょっと興味があるなぁ。 576 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 03:20:01.88 ] >>575 知の欺瞞 577 名前：１３２人目の素数さん [2011/11/28(月) 10:26:41.08 ] >>566-569 もっと書け！ 578 名前：１３２人目の素数さん [2011/11/28(月) 10:37:03.52 ] 情報板ではダメそうなのでここにきました．教えて下さい． プログラムの表示意味論って何のためにあるのですか？ 分かり切ったことをあらためて書き下しているようで狙いがわかりません． おまけに継続やエラーや入出力などつまらない所（論理の範囲外である 所）で当然のようにツギハギを重ねているようにみえます． そのツギハギが表示的意味論の生き甲斐なのでしょうか？ 579 名前：１３２人目の素数さん [2011/11/28(月) 18:16:29.65 ] 質問です。 不完全性定理を証明するために、形式的体系を算術化しますよね。 その算術化の方法について、どうしてβ関数によるものを考えるのでしょうか。 田中「数学基礎論講義」には 「形式的算術では指数関数が最初から与えられているわけではないので、それとは異なるコード化技法が必要になる」pp.57 とあります。 しかし形式的体系（たとえばPA）に指数関数記号がなくても、 原始再帰関数（つまり指数関数）は表現可能なのだから、実質的には指数関数記号があると考えてもよい気がするのですが。 どうなのでしょうか。 580 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:46:48.46 ] 掛け算がないだけで第一不完全性定理も成立しませんので。 581 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:50:25.58 ] その表現可能性を示すためにβ関数を使うんじゃなかったっけ？ 582 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:58:31.98 ] 東大のゲーデルと20世紀のやつの三巻にそのあたり詳しく書いてある 583 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 19:06:59.11 ] あれは駄本個人的に 584 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 20:34:05.86 ] 理由書かないと駄レス 585 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 21:13:44.36 ] あれは良本個人的に 586 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 22:34:14.39 ] >>578 妙に的確で変な質問だな。自分からは言いたくないもんだから誰かに言わせたいみたいな。 理由自分でちゃんとわかってるだろ。 587 名前：スレタイスレ446 [2011/11/28(月) 23:54:27.03 ] >>578 表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。 大雑把に言って、 表示的意味論≡数学的意味、 操作的意味論≡抽象機械、 公理的意味論≡論理学的意味。 プログラミングの文脈で述べられるが、 見方によっては数学のモデル理論なんかも表示的意味の領域理論の一種と呼べる。 公理的意味論は普通の数理論理学だけあって 決定不能な命題が他の意味論より発生しやすい。 たとえば並列性の概念をもった理論などは、 数理論理学では一般に記述不能。 これは並列性特有の非束縛決定不能性(Unbounded nondeterminism)命題などが原因。 例えばデッドロックみたいなイメージ。 ただし時相論理なんかで計算状況の断片だけ切り取ったりするくらいは可能。 その一方でKowalskiが計算可能性よりも推論規則の方が 多くの命題を生成可能であると証明しているから、 単純に包含関係があるわけでもない。 以前向うのスレで紹介したゲーム論的意味論で不完全性定理が成り立たない自然数論の構成も、 単純な表示的意味論による解釈を2つのプレイヤーの戦略に置き換えると、 並行的な現象であるクラスの決定不能性が破れてしまうという原理によるものだろう。 ちなみにエラー補足や継続などもプログラム言語の内部。 >>579 コードとデコードの保証。算術化って素数の冪乗でもできるけど、 PAに指数関数なかったら例えば論理式なんかがゲーデル数化できない。 >>582 田中の本をまとめたのがその本だよ。 588 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 00:04:16.60 ] >>579 追記：詳しくはその本の9章参照。 589 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 01:30:11.43 ] >>578は何を読んで次の様に感じたのだろうか？ > おまけに継続やエラーや入出力などつまらない所（論理の範囲外である > 所）で当然のようにツギハギを重ねているようにみえます． 表示的意味論でもcontinuation semanticsのスタイルで最初から記述すればツギハギにはならない。 ただ初学者向けにdirect semanticsのスタイルで定式化してからエラーや入出力を扱うとなるとcontinuationスタイルに変える必要がそこで生ずるので 知らない人にはツギハギみたいに見えるかも。 因みにcpoやそれに関する再帰方程式に関する領域論は別にして、トイ言語でないプログラミング言語に対する表示的意味論については 日本語ではロクな教科書はないので、英語の教科書で勉強するしかない。日本語の教科書によっては「表示的意味定義とはインタプリタを書く事である」 なんて大きな勘違いをしているとしか思えないのが岩波の某有名教科書シリーズにあったりするからね。 >>587 > >>578 > 表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。 > 大雑把に言って、 > 表示的意味論≡数学的意味、 > 操作的意味論≡抽象機械、 > 公理的意味論≡論理学的意味。 公理的意味論は、論理的意味というよりも証明の為の形式的体系で、それに対する解釈を与え、公理的意味論の健全性の基準を与えるのが 表示的意味論と考えれば良い。公理的意味論を与えただけでは矛盾していたりする可能性があるが、同一のプログラミング言語に 表示的意味論も与えて、その表示的意味という解釈に対して公理的意味論の体系が健全である事を示せば、公理的意味論で与えた 証明体系を安心して使用できる事になる。 これが>>578が質問していた表示的意味論を与える意義は何か？という問いへの答え。 590 名前：１３２人目の素数さん [2011/11/29(火) 01:34:42.22 ] >>588 その本のpp80の注意.には PAにはすべての原始再帰関数に対する関数記号とそれらに関する公理が入っていると考えてもよい とあるので、原始再帰関数である指数関数の記号と公理もPAには入ってると考えてもよいのですよね？ となると、β関数の意義って何なのかがよく分からなくなるのですが、いかがでしょうか。 591 名前：１３２人目の素数さん [2011/11/29(火) 02:46:09.24 ] representable functor 592 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 07:12:51.67 ] こんなところで訊くなといっているのだが、わからないやつだね。 原始帰納関数が何故、表現可能となるか、とくに帰納法のところを どう書くか考えないで、結果が成り立つことばかりいっているから わからないのだ。 593 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 07:45:34.33 ] >>575 コンパクト論理のことだろう。 >>589 それが正しい回答だろう。 >>590 スコーレム関数として考えると、 理論から関数記号をとっても、 その関数に関係する論理式をユニークにとって保存拡大できるので、 はじめから原始再帰的関数をすべて入れてても結果は同じ。 しかし今回は指数関数が入っていないとして話を始めるので β関数を導入しますよ、ということ。 594 名前：１３２人目の素数さん [2011/11/29(火) 18:25:42.28 ] >>592 周りに聞ける人がいないもので。 今質問しているのは、形式的体系の算術化に関することなので、表現定理云々はあまり関係ないように思うのですが。 >>593 コメントありがとうございます。少し考えをまとめます。 第二不完全性定理を証明する際にPAの証明をPA内部で証明しますよね。 そのとき、形式的体系を指数関数を使ってコーディングするかβ関数を使ってするかで、その方法は異なってきますよね 指数関数によるコーンディングを選んだ場合、PAの証明をPA内部で証明するにはPAに予め 指数関数記号とその公理が予め含まれていないといけないように思われます。 これに対して、β関数によるコーディングを選んだ場合なら、予め指数関数記号とその公理がPAに含まれていなくても、 PAの証明をPA内部で証明することができます。これがβ関数を導入する意義であります。 しかし、>>590,593にあるように実質的にはPAには指数関数記号とその公理が備わっていると考えてもよいので、 実は指数関数でコーディングをしても、PAの証明をPA内部で証明するには何ら不都合はない。　　　　　　　□ 以上の考え方でおかしいところはあるでしょうか？ よろしくお願いします。 595 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 19:08:35.84 ] いや指数関数が入ってない場合は β関数はもっと前に第一不完全性定理を証明するときに 既に導入されるでしょ 596 名前：スレタイスレ446 [2011/11/29(火) 20:50:01.89 ] >>594 そんな感じですね。 カントール対関数でユニークにエンコード、 β関数でユニークにデコード、 両方とも可証性述語の定義に必要。 指数関数というか原始再帰的関数とそれに関する公理を すべてぶっこんだPAの保存拡大はPRAとかよく言われます。 余談：ところで不完全性定理はT|-/-Con(T)でしたが、 Π1^0文に関してはWKL0|-φ⇒PRA|-φとなり、 ヒルベルト・プログラムの断片的実現と呼ばれます。 ですからケーニッヒ補題が超越的とかいう書き込みが上の方にありますが、 ケーニッヒ補題を使った文は有限の立場の文に置き換えれますね。 597 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 20:54:48.16 ] 全くわからないやつだね。 有限列をどうやって表すかってことなんだよ。これができなければ、 なにも表現できないんだよ！ 598 名前：１３２人目の素数さん [2011/11/29(火) 22:07:07.10 ] >>595 β関数を導入しなくても、第一不完全性定理は、 PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できると思うのですが。 >>596 よかった、>>594の考え方であってたのですね。安心しました。 PRAなるものがあるのですね、知りませんでした。勉強になります。余談に関しては知識が追い付かずよく理解できませんが、 いずれ分かるようになれたら良いと思います。 >>597 私の読解力がないせいだとは思うのですが、言っていることがよくわかりません。 「有限列をどうやって表すか」というのは形式的体系を自然数に エンコードする方法のことですよね？いろいろ種類はあると思いますが、 私は素数のべき乗によるものと対関数によるものぐらいしか思いつきません。 599 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:19:13.98 ] 要するに、論理式で書くというkとがわかっていないんだね。 600 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:27:47.20 ] >>596 PRAはPAの保守拡大どころか、それより弱い体系なんだけど…… ＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる 要は E(x,y,n) : y = x^n とか P(x,y) : 「y は x の証明である」とかを 加法と乗法だけを用いた論理式で表現しないといけないわけだけど、 どうやって実行するつもりなんですか？ 601 名前：スレタイスレ446 mailto:sage [2011/11/30(水) 07:48:04.07 ] >>600 ＞PRAはPAの保守拡大どころか、それより弱い体系なんだけど…… 確かにそうでしたね・・・。 量化付きの文の帰納法が制限されていたのを忘れていました。 だから有限の立場というんだった。 602 名前：１３２人目の素数さん [2011/11/30(水) 09:33:43.93 ] >>600 表現定理により、原始再帰的関数および原始再帰的述語はPAにおいて数値別に表現できますよね。 となれば、たとえば8=2^3はPAにおいて、PA|-8=2・2・2・1　と表現できるのではないのでしょうか。 ・・・と思いましたが、なんか怪しいですね。 表現定理は一応一通り自分で証明したつもりだったんですが、改めて各文献に目を通したらきちんと理解してなかったみたいです。 とくに今になって>>592さんの言う原始帰納法の箇所が実はめちゃくちゃ大事だったことに気が付きました。 今日もう一度しっかり勉強してから、質問させていただきます。 ありがとうございました。 603 名前：１３２人目の素数さん [2011/11/30(水) 09:44:15.71 ] 追記： ＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる この発言に関して、完全に私が誤ってました。 604 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 10:10:00.35 ] cs2011_terui.pdfがピンポイントかも。 605 名前：１３２人目の素数さん [2011/11/30(水) 11:36:54.26 ] >>586 >>587 >>589 ありがとうございます．参考になりました． でもやはり表示的意味論の爽快感がどこにあるか不明です． （健全性の根拠というのも内向きの意義のようですし） λ計算の意味論は自明なほどに簡潔です． プログラミング言語と表示的意味論とは本来似合わないのでは？ 表示的，操作的，公理的の３分類もいまいちですね． 意味論といえば表示的に決まっているでしょう？ 公理的意味論はむしろ証明論ですね． 606 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 20:26:05.47 ] >>605 横からスマン、 個人的な意見だけれど、表示されるものがなんなのか明確なコンセンサスが あるわけじゃないからいろんな理論が出てくるんだろうと思っている。 表示されたものがなんであるかによってその３分類が出てくると考えると そこそこしっくりくる。 607 名前：589 mailto:sage [2011/12/01(木) 02:32:26.27 ] >>605 > でもやはり表示的意味論の爽快感がどこにあるか不明です． > （健全性の根拠というのも内向きの意義のようですし） しかし、プログラミング言語に対して定義したホーア論理の体系に対して健全性が保証されていなければ、そのホーア論理の体系で検証しても 全くの徒労となる可能性があるのだから、公理的意味論に対して健全性を示す事は最低限必要不可欠な事ですよ。 > λ計算の意味論は自明なほどに簡潔です． それはλ計算はプログラミング言語として見れば極めて単純なトイ言語だからに過ぎない。 それと、意味定義に用いるメタ言語がλ記法という、対象言語のλ計算とそっくりのを用いるから更に簡潔に見えるだけ。 > プログラミング言語と表示的意味論とは本来似合わないのでは？ プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。 プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。 それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、 表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。 プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。 > 表示的，操作的，公理的の３分類もいまいちですね． > 意味論といえば表示的に決まっているでしょう？ それは数理論理学屋の立場からすればその通りだが、プログラミング言語に対する形式的意味論の研究は、 数理論理学屋がプログラミング言語の研究に流れ込んで来るようになる前の1960年代後半〜1970年代初頭に既に始まっているから、 コンピュータ・サイエンスの歴史からすれば、君のその主張は全く正しくない。 自然言語の意味論にしても、数理論理学の立場からは「意味論」という名前が相応しくないと感じる様々な意味論がある様にね。 > 公理的意味論はむしろ証明論ですね． これも数理論理学の立場からすればその通りだし、589に書いた通り個人的には同じ意見だが、 587の人が書いている通り、プログラムの論理的な側面を「知る」為の「意味論」というのがコンピュータサイエンスの立場。 608 名前：１３２人目の素数さん [2011/12/01(木) 05:54:50.23 ] >プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。 了解です． >プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。 了解です． >それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、 >表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。 それが表示的意味論の具体的なメリットの一つですね． >プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。 そういう意味では，今のプログラミング言語は改める必要があることが既に示唆されているということでしょうか？ 609 名前：１３２人目の素数さん mailto:sage [2011/12/01(木) 08:38:45.01 ] >>605 >λ計算の意味論は自明なほどに簡潔です． 操作的意味論のこと？ λ計算だって表示的意味論、 というかスコット理論がが理論的根拠だよ？ 610 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:27:19.05 ] D無限大モデルが自明とは恐れ入るな。 611 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:28:56.89 ] 天才現る 612 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:40:45.48 ] >>393とか、ちょっとでも理解できていたら、 表示的意味論が無意味とかλ計算の意味論が自明なんて思わないだろう。 613 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 22:25:41.47 ] 写像を学んでて思ったただの感想なんだけど、一般項とか自然数てなんだろうな。数列が 2,4,6,8,10,,n,,と並んでる場合一般項は2＋2(n-1)だ。 しかしこの並びを集合と考えると、この集合はmap(N,N)に含まれる 写像の一つに過ぎない。つまり｛f(1)=2、f(2)=4、、ｎ、、｝という写像。 そう思うとmap(Ｍ、Ｎ）の一般項てなんだろう。んで別に一般項て わけじゃないけど、全単射というのがある。 そうすると自然数というかa<b<c...というように規則を持つ無際限な並びと いうのは、map(Ｍ、Ｎ）に含まれる写像のうちで、ＭからＮへの全単射を持つ 写像という様に考えたほうがいいのかもしれないと思った。まああくまで集合 ありきの考え方であって、自然数は集合から定義されるものではないのかもしれ ないけど。 614 名前：613 mailto:sage [2011/12/02(金) 22:26:55.37 ] 間違えた。｛f(1)=2、f(2)=4、、ｎ、、｝の｛は（だわ。 615 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 01:19:17.26 ] 間違えてるのは書き込むスレッド 616 名前：１３２人目の素数さん [2011/12/03(土) 01:26:34.73 ] 知的財産・受験生ブロガーの一覧 士業名鑑 www.samrai-index.com/04benrishi/benrishi_blogJ.htm 弁理士試験ストリート benrishi-street.com/ 617 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 02:06:54.44 ] >613 余代数ネタ？ ペアノの公理からして後続関数による定義だしな。 618 名前：613 mailto:sage [2011/12/05(月) 13:14:10.95 ] >>617 すまん勉強不足なもんで言ってる事がわからん、、 集合論を学んでると数に対する自明な感覚が失われてきて、もっと上手く定義 しなおせられれば気持ち良いんだが、わからないとものすご気持ち悪いまま終 わると言う感じ。が続く 順序数、とか、同型でない、とかなあ。 自然数は全然自然な無限でもなんでもないという事はよくわかったし、そういう横並びにかつ規則を 持って並んでる無限だけが無限じゃない、という事もわかった。でもそれは濃度と、写像（全単射）の 概念があれば十分なんじゃなかろうか。順序型ωと濃度アレフ０って区別のアプローチが違うだけで どっちかがあればどっちかが要らないような気がする。 619 名前：１３２人目の素数さん [2011/12/05(月) 14:46:58.37 ] >>617 0と後者関数から自然数全体を生成するのは 自由代数の最も基本的な例だから 余代数ではなくて代数。 余代数ならばωから下ってくる形の定義法になる筈。 620 名前：613 mailto:sage [2011/12/05(月) 16:41:32.92 ] ちょっと理解に苦しむまま集合への３０講を読んだ。６１３から感想を 乗せてしまって申し訳ないんですが、最後に１つ質問。 選択公理によって議論が巻き起こったと言う話があるようですが、そもそも 対角線論法は選択公理なしで行えますか？大まかな最低限の段階として １自然数の集合が持つ元から、実数の集合が持つ元をただ一つ指定する。 ２自然数の集合が持つ全ての元から、実数の集合の元をただ一つ指定する。 ３自然数の集合が持つ全ての元から指定された実数の集合の元が、実数の集合 の元全てであるとすると、実数の集合が元として持たない実数が存在する事になり、 矛盾が生ずる。 ４自然数の集合が持つ全ての元の個数（濃度）と、実数の集合が持つ全ての元の 個数（濃度）は異なる。 １の「実数の集合が持つ元をただ一つ指定する」、は選択公理なしで行えますか？ また １の「自然数の集合が持つ元から」、という部分は、つまり自然数の集合が持つ ただ一つの元からという事でしょうか（もし自然数の二つの元から指定していたら、 そのうちの一つによって実数の集合が持たない実数も指定できてしまうから）。 この場合、これは選択公理なしで行えますか？ 621 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 18:30:24.42 ] 自然数と実数に1対1対応できないと言う証明、 >>620 証明を見直してもらうといいが、 選択公理なしに具体的な関数がつくれればいいわけ。 自然数の対角線論法なら選択関数はいらない。 ついでに、 集合とそのべき集合の濃度がちがうことは選択公理なしに証明できる。 （カントールベルンシュタインの定理） 基数にしてもきちんと公理的集合論の教科書のほうがやさしく書いてあるのに。 622 名前：613 mailto:sage [2011/12/05(月) 18:53:32.78 ] >>621 回答ありがとうございます。 ＞具体的な関数がつくれればいい ふむ、、自然数と実数なら単純にf(x)=xと考えられるからと言う事でしょうか？ あんまり多分野の数学を知らないので　（a,b)　←関数によってこの形に（一意に） 出来ない集合同士というのがいまいちピンと来ないのですが、集合にも色々あるん ですね。 ＞きちんと公理的集合論の教科書 教科書選びは難しいですね。。 623 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 19:04:59.68 ] >>620 613もそうなんだけど、ちょっと何言ってるか分かんない あと「集合への30講」はちょっと古い本で、 集合論の入門書として必ずしもいい本ではないので注意した方が良い。 というかそれ以前に数学の文章のまともな書き方を勉強した方が良い。 624 名前：１３２人目の素数さん [2011/12/05(月) 23:23:39.39 ] たびたび質問してすみません。 Boolosの『THE LOGIC OF PROVABILITY』をお持ちの方に質問です。 pp.37のFinSeqという論理式の定義 : ヨa<s ヨb<s ヨk<s (s = pair(pair(a,b),k)) ∧ ∀c<s ∀d<s (pair(c,d)<pair(a,b)→ヨi<k β(c,d,i)≠β(a,b,i)) において、∧以降の定義の意味がよくわかりません。 場合によっては、(pair(c,d)<pair(a,b) かつ ¬ヨi<k β(c,d,i)≠β(a,b,i)) もありうるため、このような定義をしているのでしょうか？ よろしくお願いいたします。 625 名前：１３２人目の素数さん [2011/12/05(月) 23:59:57.03 ] >>624 しょうもないツッコミを入れるが、お前p.とpp.の使い分けの意味わかってないだろ 626 名前：１３２人目の素数さん [2011/12/06(火) 00:09:09.82 ] >>625 わかってません・・・ ちょっとかっこつけて書きたかったんです。 627 名前：１３２人目の素数さん [2011/12/06(火) 00:17:05.39 ] ページをまたがるときは、pp. なんですね。 628 名前：１３２人目の素数さん [2011/12/06(火) 00:24:54.73 ] https://svn.kwarc.info/repos/kwarc/doc/macros/fromCTAN/cv/currvita/currvita.sty 629 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:04:28.35 ] 〜広めてください。 ▼スイス政府 国民保護庁　著「民間防衛」(civil defense) 武力を使わずに他国を侵略する段階を説明しています。 マスコミは乗っ取りがほぼ完了しており機能していません。。クチコミでも身近な人に広めましょう。 日本は今、侵略されつつあります。平和ボケから目覚め、行動を起こしましょう！ 現在第五段階です。 ＴＰＰ ・ 日中韓ＦＴＡ ・ 人権擁護法 ・ 外国人参政権　などが実現してしまえば最終段階が始ってしまいます。 猶予がありません。声を挙げて下さい！ 第一段階「 工作員を送り込み、政府上層部の掌握と洗脳 」 第二段階「 宣伝。メディアの掌握。大衆の扇動。無意識の誘導 」 第三段階「 教育の掌握。国家意識の破壊 」 第四段階「 抵抗意識の破壊。平和や人類愛をプロパガンダとして利用 」 第五段階「 教育やメディアを利用して、自分で考える力を奪う 」 最終段階「 国民が無抵抗で腑抜けになった時、大量移住で侵略完了 」 630 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:11:52.60 ] ↑ 他はともかく、ＴＰＰが何でそこに入っているの？ｗ オマエも何らかの利害関係者じゃん 631 名前：１３２人目の素数さん [2011/12/06(火) 23:30:58.11 ] >>602 ゲーデル数のデコード関数定義にどうしても冪関数が必要になります。 >>605 コーディング上の爽快感と意味論は無関係だと思いますよ。 表示的意味論はドメインに重視した考えですし、 意味関数でユニークに決定するという安定さがあります。 しかしλ計算ならまだそれでいいとしても、 π計算やλμ計算だとか高階χ計算みたいな 逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 一方公理的意味論(ホア論理)はプログラムで検証する意図があったみたいですが...。 >>624 例えば有限列ってのがアルファベットの A,B,C,...Zだとして、(A,0)の対をBなどと考えてみる。 Z＝(((...(A,0)...),21),22)　のように22ステップでZに到達するイメージ。 ここで(a,b)がZより小さい、例えば((...(A,0)...),21)なんかだとすると、 (c,d)がそれより小さい、例えば((...(A,0)...),20)だとする。 このとき、β(x,y,i)でxとyで決まる列のiステップ目のアルファベットがユニークにでる。 β((...(A,0)...),21,0)＝A β((...(A,0)...),20,0)＝A のように、A,B,C,...とやっていける。しかし途中で、 β((...(A,0)...),21,21)＝Y β((...(A,0)...),20,21)＝？ のように存在しないステップが出現するはずですよね...。 632 名前：スレタイスレ446 mailto:sage [2011/12/06(火) 23:33:57.85 ] >>631 補足：ちなみに(A,0)はpair(A,0)の略記なだけなので。 そして実際はβ関数で出てくるのはゲーデル数です。 633 名前：１３２人目の素数さん [2011/12/07(水) 10:27:38.77 ] >>631 >コーディング上の爽快感と意味論は無関係だと思いますよ。 あそこの「爽快感」とは，表示的意味論によってどのような「目からウロコ 感」があるかというような意味でした． >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 その方がやりやすいだけ（あるいは単なる退却）なのではないですか？ むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います． なお「操作的」や「公理的」に「意味論」は似合わないです． （最後の３行は分かりにくいでしょうか？） 634 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 12:19:12.81 ] 操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。 ヒルベルトが幾何学の無矛盾性を算術の無矛盾性に還元したのと同じ手法。 だからモデル理論的手法を使うことが出来る。 こういうものに意味がないと思う人は数学は向いてない。 直感でしか理解したくないのなら数学は必要ない。 635 名前：１３２人目の素数さん [2011/12/07(水) 13:10:46.45 ] >>634 >操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。 機械が出てくる時点で数学（ヒルベルトの手法）からは遠い。 >だからモデル理論的手法を使うことが出来る。 だからって？操作的意味論はそういうものだから、ってこと？ >こういうものに意味がないと思う人は数学は向いてない。 こういうものって？けっこう特定したうえでその意味が不明と言って いるのだが。それに今は「数学」はどうでもよいし。 636 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:31:00.45 ] 抽象機械のことでしょ。 状態遷移マシンとかラムダ式とか。 637 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:37:24.44 ] >>631 ベキ関数無しのコーディングは可能だそうだ 代わりにBussの#関数を使う（Edward Nelsonの本で知った） 638 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 15:24:11.98 ] 元の質問者の読んでる新井さんの本も使ってないんじゃない？ 639 名前：１３２人目の素数さん [2011/12/07(水) 17:57:45.02 ] >>636 ラムダ式まで抽象機械とは言わんだろ 640 名前：１３２人目の素数さん [2011/12/07(水) 19:35:21.68 ] >>637 > Edward Nelsonの本で知った 彼の何というタイトルの本ですか？ Edward Nelsonの本で数理論理学関連と言えばPredicative Arithmeticぐらいしか思い付かないのですが（不勉強なもので、それも読んでいません）。 641 名前：スレタイスレ446 [2011/12/07(水) 21:06:19.80 ] >>633 > >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。 > その方がやりやすいだけ（あるいは単なる退却）なのではないですか？ やりやすいということですね。 >>587のUnbounded nondeterminism に関連して、 表示的意味論は並列性などの解釈とするのが困難だという趣旨の定理もあります。 とはいえ、表示的が不可能なわけでないので退却というほどでも。 > むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います． これは詳しくききたいですね。 > なお「操作的」や「公理的」に「意味論」は似合わないです． これはどういったことなのか分かりませんでした。 >>634 モデル論的手法が何かはわかりませんが、 シェラとかのモデル理論が使えるのは表示的意味論の方だと思いますが。 数学は形式的には時間の流れがまったく考慮されない逐次的処理という特徴があって、 計算機とは時間の流れが議論に混入するという理解が一般的だと思っていましたが。 >>635 機械で計算するかは余り関係ないと思いますけどね。 ま、チャーチの提唱次第ですかね。 >>637 全く知りませんでした、書名が知りたいですね。 >>638 exp関数なんかの定義に使われていると思います、計算理論入門の章ですね。 642 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:07:02.49 ] BussのBounded Arithmeticにも. x#y = 2^(|x|・|y|) 643 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:09:01.79 ] ちなみに竹内さんの日本語の書籍にも出てきたはず。 644 名前：スレタイスレ446 [2011/12/07(水) 21:48:57.88 ] 限定算術周辺は盲点だった。 しかし定義上冪と似たような性質が用いられている気もするけど。 実際エンコード方法はいくつもあるんだろうな...。 645 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 22:52:37.72 ] 最低x^log(y)くらいの演算がないとgodel numberingがうまくいかない。 冪相当のものがないとまずいのは40年くらい前から分かってきていた。 Bounded Arith.の人たちはこんな事ばっかり考えてるから。 646 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 05:22:04.87 ] スマッシュ関数の定義可能性を保証する公理は \Omega_1 と呼ばれるが、 I\Delta_0 + \Omega_1 は Robinson's Q で解釈可能（Hajek-Pudlak などを参照）。 つまりこの解釈を通せば、ゲーデル数化は Robinson's Q においても可能、ということ。 647 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 14:12:12.58 ] もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら それでも不完全性定理は証明されるの？ これ、どなたか教えてください。お願いします。もしスレ違いならすいません（´；ω；`) 648 名前：１３２人目の素数さん [2011/12/08(木) 14:50:29.19 ] >>647 おもしろそうな質問だが，これだけでは意味不明と思う． 形式的に答えるなら，少なくとも，不完全性定理の証明には，そういうパラド クスの存在はまったく前提とされていない，ということになるからね． 他の人のコメントも見てみて． 649 名前：647 mailto:sage [2011/12/08(木) 15:06:27.52 ] ありがとうございます。。 ＞もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら やっぱり、ここの部分がしっかり定義されていないというコトですか？ ちょっと調べてきます。。 650 名前：スレタイスレ446 [2011/12/08(木) 20:58:21.54 ] >>646 その考えでいくと他にもいろいろな関数ができそうですね...。 >>647 自己言及のパラドクスは不完全性定理の証明でよく見られますね。 自己言及のパラドクスは定義されているわけでなく、 それに類似した現象を指示する慣用句です。 第1不完全性定理は自己言及パラドクスのようなものとは無縁にも証明可能です。 実は最近、マルチエージェントについて考えていた際に、 不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると 不自然なことに気が付きました...これは哲学的な問題ですが。 651 名前：１３２人目の素数さん [2011/12/08(木) 21:48:07.98 ] >>650 >不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると不自然 これもうすこし聞かせてほしいな。もし可能なら 652 名前：１３２人目の素数さん [2011/12/08(木) 23:06:21.79 ] >>647 648、650が言うのでよいと思うが、647が言いたかったのが 「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である； 後者は前者を厳密に形式化したものに相当する」ということであれば （とてもそうは読めないが）、それはその通りだと思う。 フランセーンがどう言うか知らんが。 653 名前：１３２人目の素数さん [2011/12/08(木) 23:11:41.26 ] クレタ人のパラドックスもベリーのパラドックスも死刑囚のパラドックスも不完全性定理の証明に使えるなら、禿頭のパラドックスも使えないかな。 654 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:21:11.51 ] 確かに嘘つきパラドクスと不完全性定理は確かに似ているけど、 通俗的解説書しか読んだことない人にとっては 類似点よりも相違点を理解する方がずっと大切だと思ってください。 嘘つきパラドクスも不完全性も同じなんだ！ とアナロジーで物事を語る入門者の大半はとんでもないことを言ってます。 655 名前：１３２人目の素数さん [2011/12/08(木) 23:22:46.69 ] >>653 くどいのだが、そうしたなんとかパラドックスが「不完全性定理の証明 に使われている」ということはないよね。 656 名前：647 mailto:sage [2011/12/08(木) 23:23:07.06 ] 答えて下さった方々、ありがとうございます。。 >>652 ＞「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である； ＞後者は前者を厳密に形式化したものに相当する」ということであれば ようするに聞きたかったのは、このとうりです。 もし哲学の現場で「嘘つきのパラドクス」がパラドクスでも何でもない、勘違いだったとなれば、 不完全性定理は、それでも証明されるのか、という事です。 僕も>>650さんの哲学的な問題…という所、聞いてみたいです。。 657 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:30:13.21 ] まあdiagramはほとんど同じ形だけどな。 658 名前：１３２人目の素数さん [2011/12/09(金) 01:01:21.60 ] >>655 フナクイムシがシールド工法の開発に果たした役割くらいはあると思う 659 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 06:37:08.51 ] >>650 例えばタワー関数は出てこない。 I\Delta_0 にタワー関数の定義可能性を加えた体系では Robinson's Q の無矛盾性が証明できてしまうので、 不完全性定理により、その体系を Q で解釈することは出来ない。 冪も出てこないということは Hajek-Pudlak に書いてある。 この方法ではスマッシュ関数の入れ子くらいが限界。 それでもゲーデル数化に充分ってところが味噌。 660 名前：１３２人目の素数さん [2011/12/09(金) 09:18:27.66 ] >>656 不完全性定理は、そんな勘違いがあろうがなかろうが、成立します。 それから、そのような考察をするなら、「パラドックス」という言葉 を極力形式的に定義しておくべきと思います（既知の定義もありますし）。 661 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:37.02 ] ゲーデルが論文で挙げてるのはどっちかというと 嘘つきパラドックスじゃなくてリシャールのパラドックスじゃなかったっけ。 嘘つきパラドックスと不完全性定理にはいくつか大きな違いがあって、 まず前者では命題の真偽そのものについて述べているのに対し、 後者は命題の証明可能性についての話です。 前者を形式化したタルスキーの定理では、 「そのような述語は存在できない」という結論になるのに対し、 後者ではそのような命題があっても矛盾せず、それは証明できない命題となります。 但し存在しても矛盾しないというだけで、実際に 証明可能性述語が存在するかどうかは別問題なので、 不完全性定理を勉強するときはかなり手間をかけて 実際にそのような述語を作ることになります。 662 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:58.22 ] 次に嘘つきパラドックスは直接に自分自身の真偽について言及していますが、 不完全性定理で出てくる文章は、直接的には 自然数を足したり掛けたりしたら等しくなるというような命題です。 それが結果的に自分自身が証明できないということと同値になります。 最後に、哲学で出て来るこの種のパラドックスでは 「この文は」というような意味のはっきりしない指示語などが使われているので、 数学者に言わせれば、 日常言語のような曖昧な言葉を使うのが悪いんだよ、ということになります。 不完全性定理では上で見たように自然数の足し算掛け算について 述べているだけの命題なのでそういうことはありません。 663 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:30:39.29 ] いやいや哲学方面も厳密な議論してるよ。 Strong Lier Paradoxってのが、 カントールの定理やTuringマシンの停止問題と同型。 圏論の図式レベルまで単純化すると第一不完全性定理も同型。 664 名前：１３２人目の素数さん [2011/12/09(金) 23:41:57.72 ] おまいら頭悪いなｗ kamome.2ch.net/test/read.cgi/psycho/1284396792/364-370 665 名前：１３２人目の素数さん [2011/12/10(土) 02:54:55.58 ] いまだに第二不完全性定理の証明に必要な導出性条件の証明ができない。 ここの住人はどうやって理解したんだろうか。 666 名前：１３２人目の素数さん mailto:sage [2011/12/10(土) 08:44:44.06 ] 論文読め 667 名前：スレタイスレ446 [2011/12/10(土) 09:38:44.80 ] >>651>>656 不自然な点とは第2不完全性定理なんですが、 大雑把にいえば、モデルを持つ理論が、自らのモデルについては言及できないという言明について、 その条件がモデルを持つことであるために、自己言及できていないのでは？という趣旨です。 当初は単一の世界での不完全性定理を考えていて気が付かないかったのですが、 複数の世界でエージェントの信念や知識を考慮すると不自然なんです。 自己言及のパラドクス的なモノをまだ知らない状況、というものが考えられるなど...。 この考えはまだまとまっていませんが。 >>659 どうも、無料なうえに良書ですね。 >>661 それらをまとめると、タルスキの定理は、 すべての論理式φで、N|=φ←→R(【φ】)なので、 ⇔すべての論理式φで、PA∪{φ←→R(【φ】)}|-φ←→R(【φ】) だからゲーデル文ψでPA∪{ψ←→R(【ψ】)}|-ψ←→¬R(【ψ】)となり、 真偽判定は第1不完全性定理の証明判定の別モードと解釈もできますよね。 つまりそれぞれ自己言及パラドクス（ゲーデル文）が源泉。 ま、実は第1は自己言及も可証性述語も一切必要なしに証明できるんですが。 >>663 同型とは何でしょうか。 668 名前：１３２人目の素数さん [2011/12/10(土) 10:46:36.38 ] >>667 >不自然な点とは第2不完全性定理なんですが、 ここのパラグラフまだよくわからないのですが，なんとなくおもしろそうですね． まとまったら解説をよろしく． 以下は私の中での不明点．もちろんコメントいただく必要はありません． >理論が、自らのモデルについては言及できない 直感的には，これは理論の宿命ではないのだろうか？ >その条件がモデルを持つことであるために、自己言及できていないのでは？ これを文字通りに解釈すると｢その理論が無矛盾であるために自己言及できて いない｣という意味になるが，それはナンセンスではないか だが，こう考えることがそもそも「単一の世界」に捉われているということなのか？ 669 名前：１３２人目の素数さん [2011/12/10(土) 10:50:28.68 ] 世界とかエージェントとかは様相論理の話だと思われる 670 名前：１３２人目の素数さん [2011/12/10(土) 12:14:47.43 ] >>669 それはそうなのだが 671 名前：スレタイスレ446 [2011/12/10(土) 17:08:19.79 ] >>667 訂正： タルスキの定理は正確には、 すべての論理式φで、N|=φ←→R(【φ】)となる述語Rが存在しない。ですね。 >>668 基本的には理論自体のモデルと、その理論から証明される言明中の支持するモデルが同一かどうか考えていますね。 あくまで哲学的な意味でですが。 672 名前：１３２人目の素数さん [2011/12/10(土) 18:43:34.43 ] >>671 ここでいう「モデル」って、たとえば完全性（無矛盾<->モデルの存在） などの文脈で使われる「モデル」と思っていいのですよね？（それとも別の意味？） 673 名前：スレタイスレ446 mailto:sage [2011/12/10(土) 23:33:12.77 ] そのモデルです。 674 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:29:22.34 ] ツォルンの補題を用いて 「Aが無矛盾→Aはモデルを持つ」の証明を教えてください お願いします 675 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:36:12.67 ] 教科書嫁 676 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:40:42.60 ] 教科書ないんです 調べてやれって言われました・・・ 677 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:46:50.90 ] 図書館池 678 名前：１３２人目の素数さん [2011/12/11(日) 23:50:48.14 ] フランセーンが「ＰＡの超準モデルの存在は不完全性とまったく無関係」と 書いているのだが、これはちょっと言い過ぎでないかい？ 679 名前：１３２人目の素数さん [2011/12/12(月) 04:18:24.46 ] 「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可 能である」 これはjに関する数学的帰納法で証明できる。 とあるのですが、どうしてjだけでよくて、iやkについては考慮しないで良いのでしょうか？ 1変数の述語に関しての数学的帰納法はよく分かるのですが、複数変数の述語に関しての 数学的帰納法がよく分かりません。 初歩的な質問ですみません。 680 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 04:53:38.89 ] >>679 jについて、任意の自然数iに対して或る自然数kが存在してi+j=k を仮定し、自然数iを任意に固定して1を右から足すだけ。 あとはiを動かして終わり。 681 名前：１３２人目の素数さん [2011/12/12(月) 06:03:53.48 ] jに関する数学的帰納法で証明できるというだけで、iやkを考慮しなくていいなんて書いてないだろ？ やりたければiやkに関する帰納法でも出来るんじゃない？どういう公理を採用しているのか知らないけど。 682 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:40:24.97 ] >>681 任意の自然数i、jについて、i、jを固定したならペアノの公理からi+j=kも自然数であることが示せるから、jやkは考えなくてよい訳で 「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可能である」 の「任意の自然数 i,j について、i+j=k」は「任意の自然数 i,j に対してある自然数が存在してi+j=k」と解釈した訳だが。 >>679の文についてこの解釈が間違っているのか？ 683 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:42:49.32 ] 間違ってる 684 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:53:51.33 ] >>683 >>679の文章をどう解釈すればよかったのか分からない。 685 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:00:32.23 ] 「任意の自然数 i,j,k について、i+j=k のとき、PAで ”i+j=k” が証明可能である」の間違いだろ。 もしくは「任意の自然数 i,j について、自然数 k が存在して、PAで ”i+j=k” が証明可能である」でも同じことだが。 i,j に対して i+j=k となる k が存在することは小学生でも知っている自明な話。 686 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:49:04.82 ] >>685 i+j=kを満たす任意の自然数i、jについて、PAで ”i+j=k” が証明可能である を示すのか。 ペアノの公理を公理として認める限り、これはトートロジーだろう。 687 名前：１３２人目の素数さん [2011/12/12(月) 10:45:55.80 ] 「任意の自然数 ,j について、1+j=k のとき、PAで ”1+j=k” が証明可 能である」 「任意の自然数 ,j について、2+j=k のとき、PAで ”2+j=k” が証明可 能である」 「任意の自然数 j について、3+j=k のとき、PAで ”3+j=k” が証明可 能である」 … この無限個の命題を数学的帰納法で証明できる、ということでしょ 688 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 11:16:16.25 ] i+0=kに帰結させて、次はi=kであることを示す。 これには数学的帰納法は必要ない。ただし、 S(i')=S(k')と帰納的に0=0に帰結させる。 jを選ぶかどうかは証明したい人の勝手。 689 名前：検便のナウシカ ◆UVkh7uHFoI [2011/12/12(月) 19:21:09.48 ] てｓｔ 690 名前：スレタイスレ446 [2011/12/13(火) 00:37:14.98 ] >>674 それは完全性定理。 ツォルン使うところだけ言うと、 無矛盾な文の集合の族に、包含関係で順序を入れる。 任意に整列した部分集合をとれば有界になってるから、 この族は極大元をもつ。 こいつにAと共に無矛盾性を保つ文がすべて入ってるから、 こいつの解釈を定義すると...。 >>678 どういった文脈でしょうか...。 >>679 仮定の方のi+j=kは、経験的な意味での足し算。 ＞PAで ”i+j=k” が証明可能である こっちはS(S(...S(0)...))のような形をしているが、 i,j,kは数項と呼ばれるメタ変数による略記だと思う。 普通はiかjの片方を任意固定して帰納法を使う。 片方固定しているから、もう片方の選び方で ユニークにkが決まるということがi+j=k という仮定から出る。 この帰納法が第二不完全性定理がPA以上であることとつながる。 691 名前：624 [2011/12/13(火) 02:26:39.96 ] >>631 レス遅くなりましたが、解説ありがとうございます。おかげで疑問点は解消できました。 もう1つ質問させて下さい。（何度もすみません） このスレでも何度か書いていますが、私はどうしてもLoebの可導性条件、特に D3　PA|- Pr([A])→Pr([Pr([A])]) の証明が理解できません。 以下、私がどこまで理解しているかを簡単に書きます。 D3を証明するためには、任意のΣ1文Fに対して、 PA|- F→Pr([F]) が証明できればよく、そのためにはFの構成に関する帰納法で証明すればよいわけですよね。 つまり、以下の１から４の順番で証明すればよいと。 １、F ⇔ x=y, 0=x, Sx=y, x+y=z, x・y=z　のとき、PA|- F→Pr([F]) ２、F ⇔ G∧Hのとき、PA|- F→Pr([F]) ３、F ⇔ ∃xG(x)のとき、PA|- F→Pr([F]) ４、F ⇔ ∀x<y G(x)のとき、PA|- F→Pr([F]) 以上の１以降が理解できなく困っています。たとえば、 PA|- x+y=z→Pr([x+y→z]) はどのようにして証明すればよいのでしょうか。 文献[1]には、これの証明が載っているのですが私にはよく理解できませんでした。 使用している文献は [1]　Boolos「THE LOGIC OF PROVABILITY」 [2]　田中他「数学基礎論講義」 の2冊です。 長くなりましたが、どうぞよろしくお願いします。 692 名前：624 [2011/12/13(火) 02:31:02.51 ] 追記 文献[2]には、D3の証明は膨大な量になるので、これを書き下すのは実際にはかなり困難な作業とあります。 一方、文献[1]には（多少の省略はあるものの）D3の証明を最後まで書いているように思われます。 やはり私がしっかり読めていないだけで、文献[1]も大幅に証明を省略しているのでしょうか？ 693 名前：624 [2011/12/13(火) 02:34:07.71 ] >>691の PA|- x+y=z→Pr([x+y→z]) は PA|- x+y=z→Pr([x+y=z]) の間違いです。失礼しました。 694 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 03:14:10.12 ] >>690 ＞この帰納法が第二不完全性定理がPA以上であることとつながる。 少し前で、第二不完全性定理はPAより遥かに弱い体系でも成り立つ、って話が出ているのにもかかわらずこの発言ｗ 695 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:15:56.94 ] >>691 当り前だが、２は帰納法の条件が抜けている。693 では x+y=z から y=0 の場合、z=x そうでない場合 x+(y-1) = z-1 が導かれる といったことに気づくことが必要。 696 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:21:31.04 ] >>646 で述べられているやり方により、 冪もスマッシュ関数もないロビンソンのQでも第二不完全性定理は成り立つ。 しかし積は必要で、積もないプレスバーガー算術では第二不完全性定理が成り立たないのは有名な話。 697 名前：スレタイスレ446 [2011/12/13(火) 08:13:28.50 ] >>694>>696 例の文脈で言ってたのはゲーデル数化ですよね。 ところでQでは零元との加算の交換法則さえ成り立たないですよね。 PAよりもQの方がはるかに証明可能な論理式が少ないと予想できます。 ところで第一の証明の際に結構数学的帰納法を多用しますよね？ その証明を形式化した第二の可証性述語を証明するのに、 帰納法の公理が一切不要であるということは証明されているのでしょうか？ プレスバーガーにも帰納法は入ってますし。 それとも別の方法があるということでしょうか？ 698 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 17:01:02.16 ] >>697 帰納法もゲーデル数化も扱いは同じだよ。 Qは直接は帰納法を持っていないけど、>>646でいうように 「解釈された帰納法」は持っているので、それで充分。 699 名前：１３２人目の素数さん [2011/12/14(水) 00:18:55.11 ] >>647>>650>>651>>656>>667 不完全性定理と自己言及のパラドクスはかなり異なる。 まず第一不完全性定理の証明にゲーデル文などは必須ではないことに注意。 1階述語論理の充足不能判定性問題の決定不可能性が容易に証明可能だが、 このときロビンソン算術の不完全性は、 後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。 3つを∧でつなげて存在例化したのをAとする。 するとAの任意モデルは標準モデルと同型になる。 さらに文φをある一項述語に相対化してすべての関数述語定数を存在例化したものをφ*とすると、 φ*は一項述語をドメインとするモデルであるかに依存して真偽が決定する。 このテクニックで任意のφについて、 φが決定不能⇔”Aが真ならばφ*が真である”ことが決定不能。 として第一不完全性定理が成り立つ。 また第二不完全性定理については、自らの無矛盾性証明ができないだが、 T|-⊥→φなので、T|-Pr(⊥)→Pr(φ)とT|-/-¬Pr(⊥)からT|-/-¬Pr(φ)がでて、 そもそも任意の論理式が証明できないことが証明できない、 第二不完全性定理はこれの系と言える。 さらにこれらが解を持たないある種の不定方程式と同値であることと、 ほとんどの次数と変数の不定方程式が決定不能なことを考えると、 真でありながら証明可能な論理式は、ほんのわずかしかない。 700 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:05:35.73 ] >後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。 >3つを∧でつなげて存在例化したのをAとする。 >するとAの任意モデルは標準モデルと同型になる。 ほほぅ、それは世紀の大発見ですな。 701 名前：１３２人目の素数さん [2011/12/14(水) 04:33:52.08 ] 集合論は完成された学問ですか？ まだ進化し続けているのでしょうか？ 日本人で集合論を専門にしている方はいますか？ 702 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:57:56.30 ] Mitchellのアーベル圏充満埋め込み定理の読みやすい証明の有る本教えれ。 703 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 05:26:12.73 ] >>701 一般人が「集合論」という名称から想像する学問内容と、 研究現場で「集合論」と呼ばれる研究内容は必ずしも一致しないことも多い。 どのような研究内容を想像しているのか？ 704 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 06:44:06.79 ] スレタイスレ446君は偉そうなこと言う割に、不完全性定理っていう基本的な事実については余りに無知なんだね。 不完全性定理の為の条件である「ある程度の算術を含み、かくかくしかじかの性質を満たす公理系」の内、 「かくかくしかじか」の部分は得意気に解説しているブログはよく目にするが、 最初の「ある程度の算術を含み」がどういうことなのか理解が浅い連中が多い。 PAほど強い必要は全然ないし、それよりも「含む」という部分が曲者。 狭い意味で考えてしまうと、ZFC 集合論と算術は言語が違うのだから算術を含んでいないことになってしまい、 ZFC 集合論には不完全性定理が適用できないことになってしまう。 705 名前：１３２人目の素数さん [2011/12/14(水) 08:06:23.57 ] >>700 前者の存在性に関する公理から任意の論理式φについて、 φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x) の形の文が出現、これを2階述語論理で量化した ∀φ(φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x)) と「後続者関数の単射性」と「0の非後続者性」は範疇的で 何れもω_0のドメインを持つ。このことから、 ”1階の文φ”が決定不能⇔”2階の文Aが真ならばφ*が真である”が決定不能。 706 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 12:41:59.00 ] >>705 2階述語論理で量化...? 707 名前：スレタイスレ446 [2011/12/14(水) 18:53:08.34 ] >>704 >>690でPA以上といったことについてならば、 私は>>679のレスポンスを見て、第一不完全性定理の証明を形式化して 第二不完全性定理を証明しようとしていると予想したんですね。 だから第一の条件がQになるのに対し第二がPAになっている理由を述べたわけです。 PAよりも単純な体系でも証明できるのでしょうが、 例の限定算術についてはほとんど知らないので、 数学的帰納法位は必要なんじゃないだろうか、と考えた末のレスポンスが>>697なわけです。 708 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 20:23:27.08 ] ただ、普通の数学者にとってみれば、 Peano算術をどれだけ弱く出来るかとかそういうことは 専門家のみが興味を持つどうでもいいことなので、 だからこそ指数関数を最初から加えて証明を簡略化したりする 709 名前：１３２人目の素数さん [2011/12/14(水) 20:52:04.65 ] さらに言えば、 再帰的クラスの決定問題については、 去年、Rendellによって構築されたライフゲームの万能チューリング機械により、 ttp://uncomp.uwe.ac.uk/CAAA2011/Program_files/764-772.pdf すべてエデンの園に帰着できることが証明されているので、 ttp://arxiv.org/PS_cache/arxiv/pdf/0709/0709.4280v1.pdf これからは不完全性定理含め、Σ_1・Π_1階層の決定問題はすべて セルオートマトン上で実行されながら研究が進む流れとなるだろう。 710 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 21:48:34.40 ] >>706 正確にはあらゆる論理式に対して 述語定数を定義してから、その述語を量化する。 711 名前：１３２人目の素数さん [2011/12/16(金) 07:26:41.52 ] >>702 Peter Freyd 著 abelian categories 712 名前：１３２人目の素数さん [2011/12/17(土) 01:52:21.32 ] 記号論理学ってここに入りますか？

---

---

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

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