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