数学基礎論・数理論理学　その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/ 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がピンポイントかも。

---

---

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

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