11/12/07 13:10:46.45
>>634
>操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。
機械が出てくる時点で数学（ヒルベルトの手法）からは遠い。
>だからモデル理論的手法を使うことが出来る。
だからって？操作的意味論はそういうものだから、ってこと？
>こういうものに意味がないと思う人は数学は向いてない。
こういうものって？けっこう特定したうえでその意味が不明と言って
いるのだが。それに今は「数学」はどうでもよいし。
636:１３２人目の素数さん
11/12/07 14:31:00.45
抽象機械のことでしょ。
状態遷移マシンとかラムダ式とか。
637:１３２人目の素数さん
11/12/07 14:37:24.44
>>631
ベキ関数無しのコーディングは可能だそうだ
代わりにBussの#関数を使う（Edward Nelsonの本で知った）
638:１３２人目の素数さん
11/12/07 15:24:11.98
元の質問者の読んでる新井さんの本も使ってないんじゃない？
639:１３２人目の素数さん
11/12/07 17:57:45.02
>>636
ラムダ式まで抽象機械とは言わんだろ
640:１３２人目の素数さん
11/12/07 19:35:21.68
>>637
> Edward Nelsonの本で知った
彼の何というタイトルの本ですか？
Edward Nelsonの本で数理論理学関連と言えばPredicative Arithmeticぐらいしか思い付かないのですが（不勉強なもので、それも読んでいません）。
641:スレタイスレ446
11/12/07 21:06:19.80
>>633
> >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。
> その方がやりやすいだけ（あるいは単なる退却）なのではないですか？
やりやすいということですね。
>>587のUnbounded nondeterminism に関連して、
表示的意味論は並列性などの解釈とするのが困難だという趣旨の定理もあります。
とはいえ、表示的が不可能なわけでないので退却というほどでも。
> むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います．
これは詳しくききたいですね。
> なお「操作的」や「公理的」に「意味論」は似合わないです．
これはどういったことなのか分かりませんでした。
>>634
モデル論的手法が何かはわかりませんが、
シェラとかのモデル理論が使えるのは表示的意味論の方だと思いますが。
数学は形式的には時間の流れがまったく考慮されない逐次的処理という特徴があって、
計算機とは時間の流れが議論に混入するという理解が一般的だと思っていましたが。
>>635
機械で計算するかは余り関係ないと思いますけどね。
ま、チャーチの提唱次第ですかね。
>>637
全く知りませんでした、書名が知りたいですね。
>>638
exp関数なんかの定義に使われていると思います、計算理論入門の章ですね。
642:１３２人目の素数さん
11/12/07 21:07:02.49
BussのBounded Arithmeticにも.
x#y = 2^(|x|・|y|)
643:１３２人目の素数さん
11/12/07 21:09:01.79
ちなみに竹内さんの日本語の書籍にも出てきたはず。
644:スレタイスレ446
11/12/07 21:48:57.88
限定算術周辺は盲点だった。
しかし定義上冪と似たような性質が用いられている気もするけど。
実際エンコード方法はいくつもあるんだろうな...。
645:１３２人目の素数さん
11/12/07 22:52:37.72
最低x^log(y)くらいの演算がないとgodel numberingがうまくいかない。
冪相当のものがないとまずいのは40年くらい前から分かってきていた。
Bounded Arith.の人たちはこんな事ばっかり考えてるから。
646:１３２人目の素数さん
11/12/08 05:22:04.87
スマッシュ関数の定義可能性を保証する公理は \Omega_1 と呼ばれるが、
I\Delta_0 + \Omega_1 は Robinson's Q で解釈可能（Hajek-Pudlak などを参照）。
つまりこの解釈を通せば、ゲーデル数化は Robinson's Q においても可能、ということ。
647:１３２人目の素数さん
11/12/08 14:12:12.58
もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら
それでも不完全性定理は証明されるの？
これ、どなたか教えてください。お願いします。もしスレ違いならすいません（´；ω；`)
648:１３２人目の素数さん
11/12/08 14:50:29.19
>>647
おもしろそうな質問だが，これだけでは意味不明と思う．
形式的に答えるなら，少なくとも，不完全性定理の証明には，そういうパラド
クスの存在はまったく前提とされていない，ということになるからね．
他の人のコメントも見てみて．
649:647
11/12/08 15:06:27.52
ありがとうございます。。
＞もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら
やっぱり、ここの部分がしっかり定義されていないというコトですか？
ちょっと調べてきます。。
650:スレタイスレ446
11/12/08 20:58:21.54
>>646
その考えでいくと他にもいろいろな関数ができそうですね...。
>>647
自己言及のパラドクスは不完全性定理の証明でよく見られますね。
自己言及のパラドクスは定義されているわけでなく、
それに類似した現象を指示する慣用句です。
第1不完全性定理は自己言及パラドクスのようなものとは無縁にも証明可能です。
実は最近、マルチエージェントについて考えていた際に、
不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると
不自然なことに気が付きました...これは哲学的な問題ですが。
651:１３２人目の素数さん
11/12/08 21:48:07.98
>>650
>不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると不自然
これもうすこし聞かせてほしいな。もし可能なら
652:１３２人目の素数さん
11/12/08 23:06:21.79
>>647
648、650が言うのでよいと思うが、647が言いたかったのが
「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である；
後者は前者を厳密に形式化したものに相当する」ということであれば
（とてもそうは読めないが）、それはその通りだと思う。
フランセーンがどう言うか知らんが。
653:１３２人目の素数さん
11/12/08 23:11:41.26
クレタ人のパラドックスもベリーのパラドックスも死刑囚のパラドックスも不完全性定理の証明に使えるなら、禿頭のパラドックスも使えないかな。
654:１３２人目の素数さん
11/12/08 23:21:11.51
確かに嘘つきパラドクスと不完全性定理は確かに似ているけど、
通俗的解説書しか読んだことない人にとっては
類似点よりも相違点を理解する方がずっと大切だと思ってください。
嘘つきパラドクスも不完全性も同じなんだ！
とアナロジーで物事を語る入門者の大半はとんでもないことを言ってます。
655:１３２人目の素数さん
11/12/08 23:22:46.69
>>653
くどいのだが、そうしたなんとかパラドックスが「不完全性定理の証明
に使われている」ということはないよね。
656:647
11/12/08 23:23:07.06
答えて下さった方々、ありがとうございます。。
>>652
＞「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である；
＞後者は前者を厳密に形式化したものに相当する」ということであれば
ようするに聞きたかったのは、このとうりです。
もし哲学の現場で「嘘つきのパラドクス」がパラドクスでも何でもない、勘違いだったとなれば、
不完全性定理は、それでも証明されるのか、という事です。
僕も>>650さんの哲学的な問題…という所、聞いてみたいです。。
657:１３２人目の素数さん
11/12/08 23:30:13.21
まあdiagramはほとんど同じ形だけどな。
658:１３２人目の素数さん
11/12/09 01:01:21.60
>>655
フナクイムシがシールド工法の開発に果たした役割くらいはあると思う
659:１３２人目の素数さん
11/12/09 06:37:08.51
>>650
例えばタワー関数は出てこない。
I\Delta_0 にタワー関数の定義可能性を加えた体系では
Robinson's Q の無矛盾性が証明できてしまうので、
不完全性定理により、その体系を Q で解釈することは出来ない。
冪も出てこないということは Hajek-Pudlak に書いてある。
この方法ではスマッシュ関数の入れ子くらいが限界。
それでもゲーデル数化に充分ってところが味噌。
660:１３２人目の素数さん
11/12/09 09:18:27.66
>>656
不完全性定理は、そんな勘違いがあろうがなかろうが、成立します。
それから、そのような考察をするなら、「パラドックス」という言葉
を極力形式的に定義しておくべきと思います（既知の定義もありますし）。
661:１３２人目の素数さん
11/12/09 22:11:37.02
ゲーデルが論文で挙げてるのはどっちかというと
嘘つきパラドックスじゃなくてリシャールのパラドックスじゃなかったっけ。
嘘つきパラドックスと不完全性定理にはいくつか大きな違いがあって、
まず前者では命題の真偽そのものについて述べているのに対し、
後者は命題の証明可能性についての話です。
前者を形式化したタルスキーの定理では、
「そのような述語は存在できない」という結論になるのに対し、
後者ではそのような命題があっても矛盾せず、それは証明できない命題となります。
但し存在しても矛盾しないというだけで、実際に
証明可能性述語が存在するかどうかは別問題なので、
不完全性定理を勉強するときはかなり手間をかけて
実際にそのような述語を作ることになります。
662:１３２人目の素数さん
11/12/09 22:11:58.22
次に嘘つきパラドックスは直接に自分自身の真偽について言及していますが、
不完全性定理で出てくる文章は、直接的には
自然数を足したり掛けたりしたら等しくなるというような命題です。
それが結果的に自分自身が証明できないということと同値になります。
最後に、哲学で出て来るこの種のパラドックスでは
「この文は」というような意味のはっきりしない指示語などが使われているので、
数学者に言わせれば、
日常言語のような曖昧な言葉を使うのが悪いんだよ、ということになります。
不完全性定理では上で見たように自然数の足し算掛け算について
述べているだけの命題なのでそういうことはありません。
663:１３２人目の素数さん
11/12/09 22:30:39.29
いやいや哲学方面も厳密な議論してるよ。
Strong Lier Paradoxってのが、
カントールの定理やTuringマシンの停止問題と同型。
圏論の図式レベルまで単純化すると第一不完全性定理も同型。
664:１３２人目の素数さん
11/12/09 23:41:57.72
おまいら頭悪いなｗ
ｽﾚﾘﾝｸ(psycho板:364-370番)
665:１３２人目の素数さん
11/12/10 02:54:55.58
いまだに第二不完全性定理の証明に必要な導出性条件の証明ができない。
ここの住人はどうやって理解したんだろうか。
666:１３２人目の素数さん
11/12/10 08:44:44.06
論文読め
667:スレタイスレ446
11/12/10 09:38:44.80
>>651>>656
不自然な点とは第2不完全性定理なんですが、
大雑把にいえば、モデルを持つ理論が、自らのモデルについては言及できないという言明について、
その条件がモデルを持つことであるために、自己言及できていないのでは？という趣旨です。
当初は単一の世界での不完全性定理を考えていて気が付かないかったのですが、
複数の世界でエージェントの信念や知識を考慮すると不自然なんです。
自己言及のパラドクス的なモノをまだ知らない状況、というものが考えられるなど...。
この考えはまだまとまっていませんが。
>>659
どうも、無料なうえに良書ですね。
>>661
それらをまとめると、タルスキの定理は、
すべての論理式φで、N|=φ←→R(【φ】)なので、
⇔すべての論理式φで、PA∪{φ←→R(【φ】)}|-φ←→R(【φ】)
だからゲーデル文ψでPA∪{ψ←→R(【ψ】)}|-ψ←→￢R(【ψ】)となり、
真偽判定は第1不完全性定理の証明判定の別モードと解釈もできますよね。
つまりそれぞれ自己言及パラドクス（ゲーデル文）が源泉。
ま、実は第1は自己言及も可証性述語も一切必要なしに証明できるんですが。
>>663
同型とは何でしょうか。
668:１３２人目の素数さん
11/12/10 10:46:36.38
>>667
>不自然な点とは第2不完全性定理なんですが、
ここのパラグラフまだよくわからないのですが，なんとなくおもしろそうですね．
まとまったら解説をよろしく．
以下は私の中での不明点．もちろんコメントいただく必要はありません．
>理論が、自らのモデルについては言及できない
直感的には，これは理論の宿命ではないのだろうか？
>その条件がモデルを持つことであるために、自己言及できていないのでは？
これを文字通りに解釈すると｢その理論が無矛盾であるために自己言及できて
いない｣という意味になるが，それはナンセンスではないか
だが，こう考えることがそもそも「単一の世界」に捉われているということなのか？
669:１３２人目の素数さん
11/12/10 10:50:28.68
世界とかエージェントとかは様相論理の話だと思われる
670:１３２人目の素数さん
11/12/10 12:14:47.43
>>669
それはそうなのだが
671:スレタイスレ446
11/12/10 17:08:19.79
>>667
訂正：
タルスキの定理は正確には、
すべての論理式φで、N|=φ←→R(【φ】)となる述語Rが存在しない。ですね。
>>668
基本的には理論自体のモデルと、その理論から証明される言明中の支持するモデルが同一かどうか考えていますね。
あくまで哲学的な意味でですが。
672:１３２人目の素数さん
11/12/10 18:43:34.43
>>671
ここでいう「モデル」って、たとえば完全性（無矛盾<->モデルの存在）
などの文脈で使われる「モデル」と思っていいのですよね？（それとも別の意味？）
673:スレタイスレ446
11/12/10 23:33:12.77
そのモデルです。
674:１３２人目の素数さん
11/12/11 23:29:22.34
ツォルンの補題を用いて
「Aが無矛盾→Aはモデルを持つ」の証明を教えてください
お願いします
675:１３２人目の素数さん
11/12/11 23:36:12.67
教科書嫁
676:１３２人目の素数さん
11/12/11 23:40:42.60
教科書ないんです
調べてやれって言われました・・・
677:１３２人目の素数さん
11/12/11 23:46:50.90
図書館池
678:１３２人目の素数さん
11/12/11 23:50:48.14
フランセーンが「ＰＡの超準モデルの存在は不完全性とまったく無関係」と
書いているのだが、これはちょっと言い過ぎでないかい？
679:１３２人目の素数さん
11/12/12 04:18:24.46
「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可
能である」
これはjに関する数学的帰納法で証明できる。
とあるのですが、どうしてjだけでよくて、iやkについては考慮しないで良いのでしょうか？
1変数の述語に関しての数学的帰納法はよく分かるのですが、複数変数の述語に関しての
数学的帰納法がよく分かりません。
初歩的な質問ですみません。
680:１３２人目の素数さん
11/12/12 04:53:38.89
>>679
jについて、任意の自然数iに対して或る自然数kが存在してi+j=k
を仮定し、自然数iを任意に固定して1を右から足すだけ。
あとはiを動かして終わり。
681:１３２人目の素数さん
11/12/12 06:03:53.48
jに関する数学的帰納法で証明できるというだけで、iやkを考慮しなくていいなんて書いてないだろ？
やりたければiやkに関する帰納法でも出来るんじゃない？どういう公理を採用しているのか知らないけど。
682:１３２人目の素数さん
11/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:１３２人目の素数さん
11/12/12 06:42:49.32
間違ってる
684:１３２人目の素数さん
11/12/12 06:53:51.33
>>683
>>679の文章をどう解釈すればよかったのか分からない。
685:１３２人目の素数さん
11/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:１３２人目の素数さん
11/12/12 07:49:04.82
>>685
i+j=kを満たす任意の自然数i、jについて、PAで ”i+j=k” が証明可能である
を示すのか。
ペアノの公理を公理として認める限り、これはトートロジーだろう。
687:１３２人目の素数さん
11/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:１３２人目の素数さん
11/12/12 11:16:16.25
i+0=kに帰結させて、次はi=kであることを示す。
これには数学的帰納法は必要ない。ただし、
S(i')=S(k')と帰納的に0=0に帰結させる。
jを選ぶかどうかは証明したい人の勝手。
689:検便のナウシカ ◆UVkh7uHFoI
11/12/12 19:21:09.48
てｓｔ
690:スレタイスレ446
11/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
11/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
11/12/13 02:31:02.51
追記
文献[2]には、D3の証明は膨大な量になるので、これを書き下すのは実際にはかなり困難な作業とあります。
一方、文献[1]には（多少の省略はあるものの）D3の証明を最後まで書いているように思われます。
やはり私がしっかり読めていないだけで、文献[1]も大幅に証明を省略しているのでしょうか？
693:624
11/12/13 02:34:07.71
>>691の
PA|- x+y=z→Pr([x+y→z])
は
PA|- x+y=z→Pr([x+y=z])
の間違いです。失礼しました。
694:１３２人目の素数さん
11/12/13 03:14:10.12
>>690
＞この帰納法が第二不完全性定理がPA以上であることとつながる。
少し前で、第二不完全性定理はPAより遥かに弱い体系でも成り立つ、って話が出ているのにもかかわらずこの発言ｗ
695:１３２人目の素数さん
11/12/13 06:15:56.94
>>691
当り前だが、２は帰納法の条件が抜けている。693 では x+y=z
から y=0 の場合、z=x そうでない場合 x+(y-1) = z-1 が導かれる
といったことに気づくことが必要。
696:１３２人目の素数さん
11/12/13 06:21:31.04
>>646 で述べられているやり方により、
冪もスマッシュ関数もないロビンソンのQでも第二不完全性定理は成り立つ。
しかし積は必要で、積もないプレスバーガー算術では第二不完全性定理が成り立たないのは有名な話。
697:スレタイスレ446
11/12/13 08:13:28.50
>>694>>696
例の文脈で言ってたのはゲーデル数化ですよね。
ところでQでは零元との加算の交換法則さえ成り立たないですよね。
PAよりもQの方がはるかに証明可能な論理式が少ないと予想できます。
ところで第一の証明の際に結構数学的帰納法を多用しますよね？
その証明を形式化した第二の可証性述語を証明するのに、
帰納法の公理が一切不要であるということは証明されているのでしょうか？
プレスバーガーにも帰納法は入ってますし。
それとも別の方法があるということでしょうか？
698:１３２人目の素数さん
11/12/13 17:01:02.16
>>697
帰納法もゲーデル数化も扱いは同じだよ。
Qは直接は帰納法を持っていないけど、>>646でいうように
「解釈された帰納法」は持っているので、それで充分。
699:１３２人目の素数さん
11/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:１３２人目の素数さん
11/12/14 04:05:35.73
>後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。
>3つを∧でつなげて存在例化したのをAとする。
>するとAの任意モデルは標準モデルと同型になる。
ほほぅ、それは世紀の大発見ですな。
701:１３２人目の素数さん
11/12/14 04:33:52.08
集合論は完成された学問ですか？
まだ進化し続けているのでしょうか？
日本人で集合論を専門にしている方はいますか？
702:１３２人目の素数さん
11/12/14 04:57:56.30
Mitchellのアーベル圏充満埋め込み定理の読みやすい証明の有る本教えれ。
703:１３２人目の素数さん
11/12/14 05:26:12.73
>>701
一般人が「集合論」という名称から想像する学問内容と、
研究現場で「集合論」と呼ばれる研究内容は必ずしも一致しないことも多い。
どのような研究内容を想像しているのか？
704:１３２人目の素数さん
11/12/14 06:44:06.79
スレタイスレ446君は偉そうなこと言う割に、不完全性定理っていう基本的な事実については余りに無知なんだね。
不完全性定理の為の条件である「ある程度の算術を含み、かくかくしかじかの性質を満たす公理系」の内、
「かくかくしかじか」の部分は得意気に解説しているブログはよく目にするが、
最初の「ある程度の算術を含み」がどういうことなのか理解が浅い連中が多い。
PAほど強い必要は全然ないし、それよりも「含む」という部分が曲者。
狭い意味で考えてしまうと、ZFC 集合論と算術は言語が違うのだから算術を含んでいないことになってしまい、
ZFC 集合論には不完全性定理が適用できないことになってしまう。
705:１３２人目の素数さん
11/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:１３２人目の素数さん
11/12/14 12:41:59.00
>>705
2階述語論理で量化...?
707:スレタイスレ446
11/12/14 18:53:08.34
>>704
>>690でPA以上といったことについてならば、
私は>>679のレスポンスを見て、第一不完全性定理の証明を形式化して
第二不完全性定理を証明しようとしていると予想したんですね。
だから第一の条件がQになるのに対し第二がPAになっている理由を述べたわけです。
PAよりも単純な体系でも証明できるのでしょうが、
例の限定算術についてはほとんど知らないので、
数学的帰納法位は必要なんじゃないだろうか、と考えた末のレスポンスが>>697なわけです。
708:１３２人目の素数さん
11/12/14 20:23:27.08
ただ、普通の数学者にとってみれば、
Peano算術をどれだけ弱く出来るかとかそういうことは
専門家のみが興味を持つどうでもいいことなので、
だからこそ指数関数を最初から加えて証明を簡略化したりする
709:１３２人目の素数さん
11/12/14 20:52:04.65
さらに言えば、
再帰的クラスの決定問題については、
去年、Rendellによって構築されたライフゲームの万能チューリング機械により、
URLﾘﾝｸ(uncomp.uwe.ac.uk)
すべてエデンの園に帰着できることが証明されているので、
URLﾘﾝｸ(arxiv.org)
これからは不完全性定理含め、Σ_1・Π_1階層の決定問題はすべて
セルオートマトン上で実行されながら研究が進む流れとなるだろう。
710:１３２人目の素数さん
11/12/14 21:48:34.40
>>706
正確にはあらゆる論理式に対して
述語定数を定義してから、その述語を量化する。
711:１３２人目の素数さん
11/12/16 07:26:41.52
>>702
Peter Freyd 著 abelian categories
712:１３２人目の素数さん
11/12/17 01:52:21.32
記号論理学ってここに入りますか？