- 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/
- 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 ]
- 記号論理学ってここに入りますか？
|
 |
