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