[表示 : 全て 最新50 1-99 101- 201- 301- 401- 501- 601- 701- 2chのread.cgiへ]
Update time : 12/17 02:14 / Filesize : 227 KB / Number-of Response : 713
[このスレッドの書き込みを削除する]
[+板 最近立ったスレ&熱いスレ一覧 : +板 最近立ったスレ/記者別一覧] [類似スレッド一覧]


↑キャッシュ検索、類似スレ動作を修正しました、ご迷惑をお掛けしました

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



1 名前:132人目の素数さん [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/


663 名前:132人目の素数さん mailto:sage [2011/12/09(金) 22:30:39.29 ]
いやいや哲学方面も厳密な議論してるよ。
Strong Lier Paradoxってのが、
カントールの定理やTuringマシンの停止問題と同型。
圏論の図式レベルまで単純化すると第一不完全性定理も同型。

664 名前:132人目の素数さん [2011/12/09(金) 23:41:57.72 ]
おまいら頭悪いなw
kamome.2ch.net/test/read.cgi/psycho/1284396792/364-370

665 名前:132人目の素数さん [2011/12/10(土) 02:54:55.58 ]
いまだに第二不完全性定理の証明に必要な導出性条件の証明ができない。
ここの住人はどうやって理解したんだろうか。


666 名前:132人目の素数さん 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 名前:132人目の素数さん [2011/12/10(土) 10:46:36.38 ]
>>667
>不自然な点とは第2不完全性定理なんですが、
ここのパラグラフまだよくわからないのですが,なんとなくおもしろそうですね.
まとまったら解説をよろしく.
以下は私の中での不明点.もちろんコメントいただく必要はありません.
>理論が、自らのモデルについては言及できない
直感的には,これは理論の宿命ではないのだろうか?
>その条件がモデルを持つことであるために、自己言及できていないのでは?
これを文字通りに解釈すると「その理論が無矛盾であるために自己言及できて
いない」という意味になるが,それはナンセンスではないか
だが,こう考えることがそもそも「単一の世界」に捉われているということなのか?

669 名前:132人目の素数さん [2011/12/10(土) 10:50:28.68 ]
世界とかエージェントとかは様相論理の話だと思われる

670 名前:132人目の素数さん [2011/12/10(土) 12:14:47.43 ]
>>669
それはそうなのだが

671 名前:スレタイスレ446 [2011/12/10(土) 17:08:19.79 ]
>>667
訂正:
タルスキの定理は正確には、
すべての論理式φで、N|=φ←→R(【φ】)となる述語Rが存在しない。ですね。
>>668
基本的には理論自体のモデルと、その理論から証明される言明中の支持するモデルが同一かどうか考えていますね。
あくまで哲学的な意味でですが。



672 名前:132人目の素数さん [2011/12/10(土) 18:43:34.43 ]
>>671
ここでいう「モデル」って、たとえば完全性(無矛盾<->モデルの存在)
などの文脈で使われる「モデル」と思っていいのですよね?(それとも別の意味?)

673 名前:スレタイスレ446 mailto:sage [2011/12/10(土) 23:33:12.77 ]
そのモデルです。

674 名前:132人目の素数さん mailto:sage [2011/12/11(日) 23:29:22.34 ]
ツォルンの補題を用いて
「Aが無矛盾→Aはモデルを持つ」の証明を教えてください
お願いします

675 名前:132人目の素数さん mailto:sage [2011/12/11(日) 23:36:12.67 ]
教科書嫁

676 名前:132人目の素数さん mailto:sage [2011/12/11(日) 23:40:42.60 ]
教科書ないんです
調べてやれって言われました・・・

677 名前:132人目の素数さん mailto:sage [2011/12/11(日) 23:46:50.90 ]
図書館池

678 名前:132人目の素数さん [2011/12/11(日) 23:50:48.14 ]
フランセーンが「PAの超準モデルの存在は不完全性とまったく無関係」と
書いているのだが、これはちょっと言い過ぎでないかい?

679 名前:132人目の素数さん [2011/12/12(月) 04:18:24.46 ]
「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可
能である」
これはjに関する数学的帰納法で証明できる。

とあるのですが、どうしてjだけでよくて、iやkについては考慮しないで良いのでしょうか?
1変数の述語に関しての数学的帰納法はよく分かるのですが、複数変数の述語に関しての
数学的帰納法がよく分かりません。

初歩的な質問ですみません。

680 名前:132人目の素数さん mailto:sage [2011/12/12(月) 04:53:38.89 ]
>>679
jについて、任意の自然数iに対して或る自然数kが存在してi+j=k
を仮定し、自然数iを任意に固定して1を右から足すだけ。
あとはiを動かして終わり。


681 名前:132人目の素数さん [2011/12/12(月) 06:03:53.48 ]
jに関する数学的帰納法で証明できるというだけで、iやkを考慮しなくていいなんて書いてないだろ?
やりたければiやkに関する帰納法でも出来るんじゃない?どういう公理を採用しているのか知らないけど。



682 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/12/12(月) 06:42:49.32 ]
間違ってる

684 名前:132人目の素数さん mailto:sage [2011/12/12(月) 06:53:51.33 ]
>>683
>>679の文章をどう解釈すればよかったのか分からない。

685 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/12/12(月) 07:49:04.82 ]
>>685
i+j=kを満たす任意の自然数i、jについて、PAで ”i+j=k” が証明可能である
を示すのか。
ペアノの公理を公理として認める限り、これはトートロジーだろう。

687 名前:132人目の素数さん [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 名前:132人目の素数さん 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 ]
てst

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の構成に関する帰納法で証明すればよいわけですよね。
つまり、以下の1から4の順番で証明すればよいと。

1、F ⇔ x=y, 0=x, Sx=y, x+y=z, x・y=z のとき、PA|- F→Pr([F])
2、F ⇔ G∧Hのとき、PA|- F→Pr([F])
3、F ⇔ ∃xG(x)のとき、PA|- F→Pr([F])
4、F ⇔ ∀x<y G(x)のとき、PA|- F→Pr([F])

以上の1以降が理解できなく困っています。たとえば、
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 名前:132人目の素数さん mailto:sage [2011/12/13(火) 03:14:10.12 ]
>>690
>この帰納法が第二不完全性定理がPA以上であることとつながる。
少し前で、第二不完全性定理はPAより遥かに弱い体系でも成り立つ、って話が出ているのにもかかわらずこの発言w

695 名前:132人目の素数さん mailto:sage [2011/12/13(火) 06:15:56.94 ]
>>691
当り前だが、2は帰納法の条件が抜けている。693 では x+y=z
から y=0 の場合、z=x そうでない場合 x+(y-1) = z-1 が導かれる
といったことに気づくことが必要。



696 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/12/13(火) 17:01:02.16 ]
>>697
帰納法もゲーデル数化も扱いは同じだよ。
Qは直接は帰納法を持っていないけど、>>646でいうように
「解釈された帰納法」は持っているので、それで充分。

699 名前:132人目の素数さん [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 名前:132人目の素数さん mailto:sage [2011/12/14(水) 04:05:35.73 ]
>後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。
>3つを∧でつなげて存在例化したのをAとする。
>するとAの任意モデルは標準モデルと同型になる。
ほほぅ、それは世紀の大発見ですな。

701 名前:132人目の素数さん [2011/12/14(水) 04:33:52.08 ]
集合論は完成された学問ですか?
まだ進化し続けているのでしょうか?
日本人で集合論を専門にしている方はいますか?



702 名前:132人目の素数さん mailto:sage [2011/12/14(水) 04:57:56.30 ]
Mitchellのアーベル圏充満埋め込み定理の読みやすい証明の有る本教えれ。

703 名前:132人目の素数さん mailto:sage [2011/12/14(水) 05:26:12.73 ]
>>701
一般人が「集合論」という名称から想像する学問内容と、
研究現場で「集合論」と呼ばれる研究内容は必ずしも一致しないことも多い。
どのような研究内容を想像しているのか?

704 名前:132人目の素数さん mailto:sage [2011/12/14(水) 06:44:06.79 ]
スレタイスレ446君は偉そうなこと言う割に、不完全性定理っていう基本的な事実については余りに無知なんだね。
不完全性定理の為の条件である「ある程度の算術を含み、かくかくしかじかの性質を満たす公理系」の内、
「かくかくしかじか」の部分は得意気に解説しているブログはよく目にするが、
最初の「ある程度の算術を含み」がどういうことなのか理解が浅い連中が多い。
PAほど強い必要は全然ないし、それよりも「含む」という部分が曲者。
狭い意味で考えてしまうと、ZFC 集合論と算術は言語が違うのだから算術を含んでいないことになってしまい、
ZFC 集合論には不完全性定理が適用できないことになってしまう。

705 名前:132人目の素数さん [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 名前:132人目の素数さん 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 名前:132人目の素数さん mailto:sage [2011/12/14(水) 20:23:27.08 ]
ただ、普通の数学者にとってみれば、
Peano算術をどれだけ弱く出来るかとかそういうことは
専門家のみが興味を持つどうでもいいことなので、
だからこそ指数関数を最初から加えて証明を簡略化したりする

709 名前:132人目の素数さん [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 名前:132人目の素数さん mailto:sage [2011/12/14(水) 21:48:34.40 ]
>>706
正確にはあらゆる論理式に対して
述語定数を定義してから、その述語を量化する。


711 名前:132人目の素数さん [2011/12/16(金) 07:26:41.52 ]
>>702

Peter Freyd 著 abelian categories



712 名前:132人目の素数さん [2011/12/17(土) 01:52:21.32 ]
記号論理学ってここに入りますか?






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

前100 次100 最新50 [ このスレをブックマーク! 携帯に送る ] 2chのread.cgiへ
[+板 最近立ったスレ&熱いスレ一覧 : +板 最近立ったスレ/記者別一覧]( ´∀`)<227KB

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