トップページ⇒math
563コメント211KB

ゲーデル不完全性定理

■ このスレッドは過去ログ倉庫に格納されています
0001132人目の素数さん05/02/28 11:27:12
勉強中なのですが、難しいです。専門のかたいたらお願いします
0153132人目の素数さん2005/05/30(月) 12:15:54
>>152
意義がよくわかりませんが。「⊥の証明が存在する」という公理があればあたり前でなんでその結論になるのか。

そもそものω無矛盾な体系のモデルはどんなものという質問とは関係ないんですね。
0154132人目の素数さん2005/05/30(月) 12:23:27
ω無矛盾な→ω矛盾な
0155132人目の素数さん2005/05/30(月) 12:28:29
でもそのT'はまさにω矛盾か、、

任意のpは⊥の証明にならないことが示せるのに∃p(pは⊥の証明)も示せる。

でどんなモデルを持つの?
0156132人目の素数さん2005/05/30(月) 16:24:00
>「⊥の証明が存在する」という公理があればあたり前で

確かに上の公理があれば
「どんな命題の証明も存在する」というのは
当たり前。

問題は、実際にそれが構築できるかといわれるとできないってこと。
0157132人目の素数さん2005/05/30(月) 16:28:47
>任意のpは⊥の証明にならないことが示せるのに

でも∀p¬(pは⊥の証明)は示せない。
上の「任意のp」は、あくまで自然数であることが証明できる
標準的な元pの全体しか考えてない。
しかし、自然数のモデルには、そのような元しか含まれないわけではない。
非標準的な元を含むのであれば、いくらでもおかしなことはおきる。
0158132人目の素数さん2005/05/31(火) 00:05:24
なるほど。では標準モデルはある意味で最小のモデルということだろうか。

ゲーデルの話はモデルの最小性を一階の言語の公理で言い表すことができないという話ととれるの?
0159132人目の素数さん2005/05/31(火) 00:12:46
>>158
それだけならば、レーヴェンハイム-スコーレムの定理で十分。
0160132人目の素数さん2005/05/31(火) 03:48:06
ただ不完全性定理はパラドクシカルに言われるけれど。

モデルが(真偽について同型のものをのぞいて)一意に決められないなら同じ問題に複数の答えがあって当たり前だよね。

標準モデルで考えるのに慣れてるからおかしな答えだと思うだけで。
0161132人目の素数さん2005/05/31(火) 04:05:20
哲学マニアは数学板によりつくなよ。
0162132人目の素数さん2005/05/31(火) 10:22:11
別に複数の答えがあるわけじゃない
教科書でも読み直せハゲ
0163132人目の素数さん2005/05/31(火) 11:04:02
>>161 >>162
バカは黙ってろ。
0164132人目の素数さん2005/06/01(水) 10:35:52
>標準モデルはある意味で最小のモデルということだろうか。

証明できる元以外存在しないという意味では最小。

>ゲーデルの話は
>「モデルの最小性を一階の言語の公理で言い表すことができない」
>という話ととれるの?

そう。
0165132人目の素数さん2005/06/01(水) 23:34:42
>>164
証明できる元の詳細求む。
次の2階の∀を使った帰納法の公理

∀P(P(0)∧∀y(P(y)⊃P(y'))⊃P(x))

を満たすxの値のことだと思うけれど。
0166132人目の素数さん2005/06/02(木) 08:17:34
>>165
詳細なし。考えればわかる。
0167132人目の素数さん2005/06/03(金) 08:21:27
http://wiki.fdiary.net/moikomi/?%B8%F8%CD%FD%BC%E7%B5%C1
↑なんかよくある誤解の典型のようなページですが、このひと何者なんでしょう?
0168132人目の素数さん2005/06/03(金) 09:40:25
>>167
>なんかよくある誤解の典型のようなページですが
そうですね
『(1)「いかなる論理体系でも無矛盾であるとき、
 その無矛盾性をその体系の公理系だけでは証明できない」
 (第2不完全性定理)。したがって、
 (2)「いかなる論理体系において、その論理体系によって
 作られる論理式のなかには、証明する事も反証することも
 できないものが存在する。」(第1不完全性定理)』

順序が逆だな。
1)第1不完全性定理を証明してから第2不完全性定理が証明される。
2)自然数論を含まない理論ならば、完全な理論が存在する。
0169132人目の素数さん2005/06/03(金) 09:42:59
続き
『(3)この「証明する事も反証することもできないもの」を「公理」と呼ぶ。
したがって、すべての論理体系は証明不可能な公理を基礎として
組み立てられている、と言い換えることができる。
公理を基礎とする論理体系を「公理系」と呼ぶ。』

公理はそれ自体で証明とみなされる。
ゲーデルが示した証明も反証もできない命題は
もちろん自然数論の公理ではない。
0170132人目の素数さん2005/06/03(金) 09:49:06
続き
『(5)ゲーデルの第2不完全性定理は
「自分自身の無矛盾性を証明する」
という意味での自己言及である。
ゲーデルの定理は、論理学への
自己言及のパラドックスの導入である。』

自己言及は第1不完全性定理で
「この命題は証明できない」
という形で示される。
ところでゲーデルの定理は不完全性を示すものであって
パラドックスではない。
「この命題は偽である」とするとパラドックスになるが
その理由は真偽の(算術的)定義が可能としたところにある。
0171132人目の素数さん2005/06/03(金) 09:59:03
続き
『(7)自己言及のパラドックスが生じる由縁は、
 自己言及という行為自体が、コトバの世界からの
 脱出を意味しているからであろう。
 コトバの世界がそれ自体に言及するためには、
 そのコトバが置かれている世界を経由しなければ
 なし得ない行為だからだ。
 コトバの世界はモノの世界の中に浮かんでいる
 モノなのである。』

実際にはパラドックスの原因は自己言及ではなく
(再帰的)関数が、不動点をもつにもかかわらず
不動点のないような関数を考えようとすることにある。
つまりモノの世界は《思いこみ》でしかないのに、
それを前提してコトバでモノの世界を語りきろうと
するから破綻するのである。
0172132人目の素数さん2005/06/03(金) 10:13:28
ところでゲーデルの不完全性定理の何を功績とするかについて
2つの異なる立場がある。
1)対角線論法を用いた自己言及のトリックの考案
2)証明検査手順の算術言語による"プログラミング"

1)だという人は
「証明検査手順なんて地道にやれば
 プログラミングできるに決まってる」
といい
2)だという人は
「証明検査手順がプログラムとして書けるから
 自己言及のトリックが意味をもつんだぞ。
 大体対角線論法なんてカントルもラッセルも使ってる」
という。
0173132人目の素数さん2005/06/03(金) 10:16:42
当然のことながら、ゲーデルの功績が
0)数学自身の無矛盾性が証明できないことを示したこと
だという人は、ゲーデルの証明を読んだことがないか、
読んだことはあるが、何をいってるのかわからなかった
人である。
後者には同情するが、前者は単に怠惰なだけである。
0174132人目の素数さん2005/06/03(金) 13:59:36
>>173
どうもよくわからない。一階のどの公理系で真偽が決定できない一階の言葉で書かれた命題が存在する。

でも二階の証明系があれば決定できるならそれは決定できるんじゃないか?たとえばGは自然数の標準モデルを完全に言い表すことのできる系では証明される。

でもそもそも二階の証明系ってどんなもの?
01751732005/06/03(金) 14:44:41
あまり正確でなかった。

1階の広く認められている公理系である PA や ZF では真偽が決定できない1階の言葉で書かれた命題が存在する。たとえば無矛盾性やG。

だけれど実際はPA や ZFは無矛盾なこととかG の意味は真であることは当然と思われている。つまりそれはより強い(2階の?)証明系で証明されているということじゃないんだろうか?どうでしょう。

そうするとつまり。。。より強い立場で証明できれば十分なんじゃないか?公理と証明したい命題が同じ言葉で書かれている必然性があるのか?というのが疑問。
0176132人目の素数さん2005/06/03(金) 15:09:42
>>175は、173じゃなくて174だろ?

まず、二階論理の完全な証明系は存在しない。それが不完全性定理。

つぎに、二階算術では、一階算術の無矛盾性が証明できるだけで
二階算術自身の無矛盾性はやっぱり証明できない。

最後に、より強い立場を持ち出すのは、問題をより難しいものに
棚上げしているだけである。(実際に難しくなっているのか
どうかはわからないが)
0177132人目の素数さん2005/06/03(金) 15:21:09
ところで、非決定性命題が存在する条件は
「広く認められている」ことではない(笑)
01781742005/06/03(金) 15:23:46
うーん。単に素朴な疑問を言っていますが。最初に証明したい命題があってその後に公理系を考えるとしよう。

無矛盾というだけでは直感に反する公理系も入ってしまうから。もう少し別の基準で公理系をだんだん強力にしてゆく列を考える。そうやっていくといつかは証明できるというようなことはいえないんだろうか?
0179132人目の素数さん2005/06/03(金) 15:27:38
>>178
>もう少し別の基準で公理系をだんだん強力にしてゆく列を考える。

で、その「もう少し別の基準」ってズバリ何?(笑)

>そうやっていくといつかは証明できる
>というようなことはいえないんだろうか?

証明ヲタクは神経症だから、神経科にいって治してもらいな。
01801742005/06/03(金) 15:49:25
でもちょっと考えたけどいえなそう。

>証明ヲタクは神経症だから、神経科にいって治してもらいな。

そうかも。
0181132人目の素数さん2005/06/03(金) 15:50:39
先送り.. (r
0182132人目の素数さん2005/06/03(金) 23:07:39
早送り
0183132人目の素数さん2005/06/03(金) 23:18:18
とりあえず「任意のPAの記号を使った閉じた命題PについてPか¬Pのどちらかを証明できる無矛盾な公理系が存在する」は定理だから。
0184132人目の素数さん2005/06/04(土) 10:28:05
>>183
>PAの記号を使った
ワロタ
0185132人目の素数さん2005/06/04(土) 10:34:39
多分、PAじゃなくて一階述語論理の完全性定理
のことをいいたいんだろうけど、肝心なところで
間違ってるね。

正しくは
「一階述語論理の任意の閉じた命題Pについて
 Pがどのような解釈でも真であることと
 Pが証明可能であることは同値」

ちなみに、閉論理式だからといってPか¬Pのどちらかが
必ず証明できるとはいえない。
これは、閉論理式Pで、これが真であるような解釈と
偽であるような解釈の両方が存在するようなものを
実際に構成すればよい。サルでもできる。
0186132人目の素数さん2005/06/04(土) 11:16:19
>>185
バカみたい。

「モデルを持つ公理系は無矛盾」でしょ。PAの標準モデルでPか¬Pのうち真な方を公理とした公理系はやはりモデルを持つ。だから無矛盾。

文脈読んでないみたいだけど>>178への答えのひとつです。
0187132人目の素数さん2005/06/04(土) 11:38:27
>>178
Consis を付け加えていけば、いつか complete theory に到達するというのは
S.Feferman の結果にある。ただ、ずっとつけくわえていくという場合、極限順序
数のところで何を付け加えるかは、それまで付け加えたものを、どうコード化
するかによるから一意ではない。詳しくは論文を読んでください。
0188132人目の素数さん2005/06/04(土) 11:49:47
Consisは無矛盾性の公理ですか?順序数にどう対応させるんだろう。
0189132人目の素数さん2005/06/04(土) 12:01:01
>>188
Construction は Tree の形で分岐して行う。この Tree の長さは帰納順序数で
公理は recursive code でコード化したものを使う。最後に branch をとれば
complete theory が得られるといった筋。帰納関数論の知識がないと読めない。
0190132人目の素数さん2005/06/04(土) 15:42:48
>>186
>「モデルを持つ公理系は無矛盾」でしょ。
(中略)
>PAの標準モデルでPか¬Pのうち真な方を公理とした公理系は
>やはりモデルを持つ。だから無矛盾。

で、肝心の「PAの標準モデルが存在する」はどこの定理ですか?

あなた、自分の言ってることが
「正しいから正しい!」っていう
同語反復に陥ってることに気づけませんか?
それ、病気ですよ。パラノイアっていう。
0191187-1892005/06/04(土) 15:55:27
>Consis を付け加えていけば、いつか complete theory に到達する

で、そのcomplete theoryの公理の全体を記述できますか?

適当な命題をもってきたときに、どのレベルのConsisを公理とすれば
真偽判定に十分であるか知る手続きがありますか?
0192132人目の素数さん2005/06/04(土) 18:05:54
>>190
ん?どういうレベルの話?

PAの標準モデルは領域に自然数の集合を割り当て。関数記号や等号の意味は自然数の演算をでしょう。公理がすべて妥当式になるからモデルですよ。
0193132人目の素数さん2005/06/04(土) 19:45:24
ちなみにPAというのが適切なのかは知らない。

そもそも一階の言葉では自然数のモデルをいいあらわし切れないという結果のすべての原因は帰納法の公理が本来いうべきことを言えていないこと。

これは全ての空でない「部分集合」は下限を持つという整礎の公理でなくてはならなかった。帰納法「すべての命題が、、」はこの結論にすぎない。

ペアノの本来の公理はこういう二階の言葉で書かれるんですよね?
0194132人目の素数さん2005/06/04(土) 20:25:09
>>192
>PAの標準モデルは領域に自然数の集合を割り当て。
>関数記号や等号の意味は自然数の演算をでしょう。

ん?自然数の集合ってどうやって決めるの?
この質問で間違いに気づけないなら・・・馬鹿。
0195132人目の素数さん2005/06/04(土) 20:30:44
>>193
連続自爆か。整礎の公理は無関係。
述語全体をしばる二階の限量子を持ち出せば
いいかといえばそうでもない。
二階論理自体の正当性が示せないから。
だから、問題の先送りは赤字の先送りと同じく
最後には破綻する。
0196132人目の素数さん2005/06/04(土) 21:02:15
純粋に数学の基礎だけを与えるという試みなら命題と公理と推論だけを定義すればいいけど。モデル論もいらない。

そのかわり任意の公理系の性質なんて議論できないでしょ。その範囲が自分では定められないんだから。自分で完全性定理を持ち出したのにね。
0197132人目の素数さん2005/06/04(土) 21:07:59
>>196
誰にいってるのか不明。
日本語が話せない人にロジックは無理だが・・・
0198132人目の素数さん2005/06/04(土) 21:14:47
公理系の性質をいうときにはみな標準モデルを仮定していってるでしょ。

完全性定理も不完全性定理も標準モデルの定理ですよ。
0199132人目の素数さん2005/06/04(土) 21:23:44
> 不完全性定理も標準モデルの定理ですよ。

違うよ。不完全性定理は、モデルとは無関係に述べることができる。
0200132人目の素数さん2005/06/05(日) 01:25:18
正確には

標準モデルの定理→標準モデルを同定できる証明系の定理

>>142
例えば第一不完全性の前提のω無矛盾。任意の自然数kについてP(k)ならば∃k¬P(k)は証明できない。この任意の自然数ってじゃ何?
02012002005/06/05(日) 01:32:17
アンカー間違えた

>>142→>>199
0202132人目の素数さん2005/06/05(日) 01:37:56
>>200
numeral のことでしょ。
numeral は言語レベルの概念ですが。
02032002005/06/05(日) 02:20:35
じゃその先は。

言語自体は普通は集合論で自然数と同じように定義されるけど。そこはどうにか与えるつもりだろうけど。

たとえばゲーデル数化とかどうなるの?集合論以外で定義された言語をどう解釈できるんでしょう。
0204132人目の素数さん2005/06/05(日) 02:44:54
> 言語自体は普通は集合論で自然数と同じように定義されるけど

一階の述語論理に基づく(帰納的な)理論を展開するのに、集合論は必要ないでしょ。
02052002005/06/05(日) 03:08:17
確かに命題や証明のゲーデル数化を上から与えられたものとしておけば第一不完全性の証明のようなものを形式化できる。

ていうのが第二不完全性の証明の内容だったけど。そういうことを言ってる?

でもそのときに形式化できたのは今あなたが作った公理系Tにおける証明だけだよね。任意の公理系についてはいえないよね。
0206132人目の素数さん2005/06/05(日) 03:10:45
哲学厨のなにがいやかって

「命題」=「疑問」と理解しているやつが多いこと。

高校数学シラネーのか?
02072002005/06/05(日) 03:20:31
命題は変数の集合X、述語の集合P、、が与えられたら

x∈Xは項
aが項、p∈Pならp(a)が命題
a
bが命題ならa⊃bが命題
、、

以上を満たす「最小の集合」が命題。最小の集合のところで集合論を使うと思うんだけど。。
0208132人目の素数さん2005/06/05(日) 06:32:42
自然数の例でいうと、x+y=y+x の証明には数学的帰納法が必要だけれども、
3+8=8+3 の証明には必要ない。

同じように、論理式や証明図の全体を本当の集合として扱う必要があるときは、
集合論のようなものが必要だけれど、述語論理上の理論を展開する上で必要なことは、
個々の論理式や証明図についての超数学的な取り扱いであり、本物の帰納法のような
ものはいらない。

論理式の構成に関する帰納法での証明は集合論的な本当の帰納法ではなく、個々の命題の
具体的な証明の略記として扱うことができる。もちろん、本物の帰納法ではないので
これにより証明できる超数学的命題は限られた形のものになるだろうし、「すべて」や
「存在」については通常の解釈ができないけれど、それなりに十分役に立つ。
0209132人目の素数さん2005/06/05(日) 07:36:57
>>104
最近は別の場所から飛来。VIPPERという。
0210132人目の素数さん2005/06/05(日) 12:56:09
>>208
論理式や証明図の構成に関する帰納法を用いるということは、
論理式や証明図の全体を考えることになる。

一般でないからいいというのは間違っている
0211132人目の素数さん2005/06/05(日) 13:34:46
もう少し整理した言い方をすると、(帰納的な)理論を展開するだけならば PRA で十分ということ。
PRA だけではモデルの概念を議論できないでしょ。
02122002005/06/05(日) 15:38:18
僕としては1階の言葉でいえる弱い帰納法を使うのが間違いかどうかは立場の問題だからどっちでもいい。

知りたいのはそれで不完全性定理が(集合論からいえるバージョンを弱めることなく)本当にいえるかどうか。
0213132人目の素数さん2005/06/05(日) 22:52:43
第一不完全性ならPRAで形式化できるんじゃないか
0214132人目の素数さん2005/06/06(月) 20:41:56
212\のような疑問はナンセンス。
例えば、PA で証明できないが(もちろん PA が無矛盾であることは仮定する
ということだが)、ZFC で証明できる数論的命題はある。
PA でも ZFC でも排中律は証明可能である。証明可能な命題はその体系で
同値である。これから、PA の排中律は ZFC の排中律より真に弱いという
ことになるが、そういうことを訊きたいのだろうか?
0215132人目の素数さん2005/06/08(水) 04:22:52
テキストとして比べて同じかあるいは同等か。背中律って命題の上を動く公理でしょ。言えることはかわると思う。

でも不完全性定理はひとつの命題で書けるはず。あとはどの公理を使うか。
0216ウルトラマン2005/06/08(水) 17:32:05
ゲーデルの不完全定理について。一つひとつ秩序に従って考える思考がある
これが言葉の思考つまりデジタル思考である。左脳思考である。アナログ思考
は右脳思考である。アナログ思考はゲーデル数には表せない。ゲーデル数があらわしているのはデジタル言葉の思考である。
現在はデジタル思考文明である。ゲーデルの不完全定理は現在のデジタル文明に限界があることを示している。その限界はアナログ思考で乗り越えられる
今日はコンピュータ、デジタル思考文明である。そして限界に来ている。この限界を乗り越えるためにはアナログ右脳文明に変革せねばならない。
0217132人目の素数さん2005/06/08(水) 18:10:43
ゲ
こ
は
現
今
0218132人目の素数さん2005/06/08(水) 18:22:09
>>215
214 を読めばわかるが、証明可能な命題は 1 = 1 と同値である。
だから、ZFC と 1 = 1 と PA の 1 = 1 では後者の方が真に弱い
ってことになるという解釈でよいのか? ということである。
つまり、自分の疑問が、たずねて意味のある疑問になっていない
だろうとご指摘してるわけだが、おわかりにならないようだね。
0219132人目の素数さん2005/06/09(木) 05:06:50
強いか弱いかだってシンタクスでわかるよね。たとえば含意の左の連言の節が増えてれば弱くなってる。

だいたい逆じゃないか?より強い論理=より多くの公理ではじめていえる定理はより少ない公理でいえる定理より弱い定理だと思うんだけど。
0220132人目の素数さん2005/06/09(木) 05:12:08
ACを使って言えたことがACを使わないで言えたら驚くけど。逆は驚かない。
0221132人目の素数さん2005/06/09(木) 05:24:01
まあ質問の意図はだから前提のω無矛盾とかRE公理化可能とかをより強い条件にしなくてもPRAで証明できるかってこと。
0222132人目の素数さん2005/06/09(木) 07:59:02
>>221
>PRAで証明できるか
何を?不完全性定理をかい?
>ω無矛盾とかRE公理化可能とかをより強い条件にしなくても
そもそもなぜPRAをもってきたのかい?
てゆーか、君PRAってなんだか分かってる?(笑)
0223132人目の素数さん2005/06/09(木) 11:40:19
ペアノの公理を一階にしたものじゃないの?Rは何?
0224132人目の素数さん2005/06/10(金) 09:33:22
PRAとは・・・
原始再帰的算術(Primitive Recursive Arithmetic)
02252252005/06/10(金) 18:20:54
√225 = 15
0226132人目の素数さん2005/06/26(日) 01:28:21
407
0227132人目の素数さん2005/07/31(日) 06:38:30
629
0228132人目の素数さん2005/09/14(水) 14:23:59
>>105
に便乗して質問、
組(数、数)を入力して、それが、
ロビンソン算術の公理系の、ある証明のゲーデル数とその論理式のゲーデル数の関係になっていないときに必ず0を出力するチューリング機械
というのもつくれるのでしょうか?
0229132人目の素数さん2005/09/14(水) 18:18:10
帰納的関係なんだから(ry
0230132人目の素数さん2005/09/14(水) 19:32:32
Yesということですか?
0231132人目の素数さん2005/09/14(水) 19:49:37
証明の最後の行を取り出せば、その論理式のゲーデル数が
分かるでしょ?
だからyes
なっていないときに0を出力してなっているときには1を出力する機械だって作れる
0232132人目の素数さん2005/09/19(月) 16:27:53
( ´∀`)⊃
0233132人目の素数さん2005/09/19(月) 17:07:04
チューリングはオナニーをしていて停止問題に気づいた
だけどそのままだと論文に難ありなので比ゆを用いた

ゲーデルはビニール袋を使った
0234132人目の素数さん2005/09/20(火) 13:17:57
本を読んでて、
Qにおいて、ある論理式(ゲーデル数がm)が証明可能であるとき、∃yProv(y、m)がQで証明可能、という文にぶちあたったんですが、
これは、∃yProv(y、m)という論理式が、Qの公理と推論規則(S0+S0=SS0みたいなのを証明する目的で設定しているあれ)から、導出されるということですか?
0235132人目の素数さん2005/09/20(火) 18:56:43
>(S0+S0=SS0みたいなのを証明する目的で設定しているあれ)
ってのが何のことを言ってるか分からないけど多分その理解でいいんじゃないかと

∃yProv(y,m)って言っても(S0+S0=SS0みたいなのを証明する目的で設定しているあれ)要するに
∃y∀x_1∀x_2……x_25・x_26+x_27=…みたいな(適当だけど)ただの論理式でしょ?
その論理式が証明可能、ということ
0236132人目の素数さん2005/09/20(火) 21:47:34
∃yProv(y,m)という形で導出されるみたいではないみたいですね

で、
>∃yProv(y,m)が、∃y∀x_1∀x_2……x_25・x_26+x_27=…みたいな(適当だけど)ただの論理式
というくだりがよくわからないんですが、
なにか別の論理式
>∃y∀x_1∀x_2……x_25・x_26+x_27=…みたいな(適当だけど)ただの論理式
を、∃yProv(y,m)という形で表してる、ということでしょうか?
0237132人目の素数さん2005/09/20(火) 22:21:30
論理式は、quantifierや変数記号や函数記号やらが一定の規則で
並んだものでしょ?∀x∀y x+y=y+xみたいに.
で、その中で、ある性質を持つような、自由変数を二つ持つ論理式に
Prov(x,y)と名前を付けてるだけでしょ?そういう風に書いてあるはず
0238132人目の素数さん2005/09/21(水) 00:23:06
可証述語って書いてあって、
2項関係Prov(n、m)を考えるとあったので、
Provってのを、2項述語記号と思ってたんですけど、

勘違い?

>>235
>>237
が言うところの、
Prov(x,y)のxのところにnをyのところにmを入れたやつ、という書き方のほうの、Prov(n、m)ということっすか?(なんだよこの括弧はとは、思ってたんだが・
0239132人目の素数さん2005/09/21(水) 00:31:47
まず、上の方は明らかに勘違いかと、、
自然数論なんだから述語記号は=(と場合によっては不等号<)
しか無いです

あとはSuccesser函数Sとか足し算の記号+とか
掛け算の記号とかquantifierの組み合わせとかを使って
Prov(n,m)は実際に書き下すことが出来ます

ただ実際は膨大な長さになるので手で書き下すのは一寸きついかも
0240132人目の素数さん2005/09/21(水) 00:34:17
あと自然数nと数項SSS.........0は区別して考えたほうが良いっすよ
0241132人目の素数さん2005/09/21(水) 10:35:19
>>235
>>237
>>239
>>240
ありがとうございました。
0242132人目の素数さん2005/09/22(木) 10:49:39
>>239
どういう方針で書き下すんですか?
原理的には虱潰しで見つかるにしても。
0243132人目の素数さん2005/09/23(金) 00:13:26
下のほうから
f_1(n):nで表される記号列のながさ
n*m;nで表される記号列の後ろにmで表される記号列を続けた記号列のGoedel数

P_1(n):nはある論理記号/変数記号のGoedel数である
P_2(n):nはある記号列のGoedel数である
P_3(n):nはある論理式のGoedel数である
P_4(l,n,m):nはGoedel数lの論理式とGoedel数nの論理式から推論規則1によって導かれる論理式のゲーデル数である
…
P_5(n):nはある証明(図)のGoedel数である
P_6(n,m):nはGoedel数nの論理式P、mはPの証明(図)のGoedel数である
∃m P_6(n,m):Goedel数nの論理式に対してある証明が存在する
つまりProv(n)

見たいな感じで気合で作ります
虱潰しよりはましだけど、これが面倒なことこの上ない
0244132人目の素数さん2005/09/24(土) 14:52:38
>>243
ありがとうございます。
0245132人目の素数さん2005/10/08(土) 01:26:22
ゲーデルの完全性定理の証明が載っているサイトを教えて下さい。不完全じゃなくて完全性定理です
0246132人目の素数さん2005/10/08(土) 02:09:02
ttp://www.math.tsukuba.ac.jp/~tsuboi/gra/complete.pdf
あとは適当に「完全性定理」「completeness theorem」
でぐぐって出てきたページだけど
ttp://research.nii.ac.jp/~terui/mita03b.pdf
ゲーデルの「完全性定理の証明」ってことなら
http://en.wikipedia.org/wiki/Original_proof_of_G%C3%B6del's_completeness_theorem

ってかぐぐりゃ結構出てくるよ
0247132人目の素数さん2005/10/19(水) 23:39:28
不完全性定理についての本を探しています。

定理の理解よりも、この定理にまつわる物語を知ることが主な目的なんですが、お勧めありますかね?
アマゾンだと沢山出てくるんですけど、定理の理解がメインの書籍が多くて。

数学力は、高校数学はほぼ理解できてる程度です。
0248132人目の素数さん2005/10/20(木) 07:13:19
定理にまつわる物語ってのがよくわからんが
「ゲーデルの謎を解く」(岩波科学ライブラリー)
講談社現代新書「ゲーデルの哲学」ぐらいがよろしかろう。
0249132人目の素数さん2005/10/20(木) 14:26:16
>>247
つ 高橋昌一郎
 「ゲーデルの哲学 不完全性定理と神の存在論」
 講談社現代新書

  別冊宝島EX
 「現代数学で遊ぶ本」
  → 書中 廣瀬健 監修「ゲーデルの不完全性定理」はメタメタ超難し理論か?
    の章部分を参照のこと

 後者はおそらく絶版の上入手困難だと思う

 質問はageとくのがオススメ。
 あと自分のバックグラウンドくらいは入れとこう。それによってオススメ書は全然変わってくる。

 オイラの想定は「>>247は数学専攻以外の理系の大学生(哲学や数学史にも興味あり」ってとこ
で回答
0250132人目の素数さん2005/10/20(木) 14:39:51
で>>1はどこ行ったのよ? age
0251132人目の素数さん2005/10/20(木) 17:51:18
ゲーデルは何を証明したか 数学から超数学へ
著者:E ナーゲル、J.R.ニューマン共著、林一訳 出版元:白揚社

いい本っぽい、一寸詰め込みすぎで消化不良ぎみっぽい

ゲーデルの謎を解く
著者:林晋 出版元:岩波書店

値段の割りに本の分量が少なすぎるような、、

ゲーデル未完哲学論稿
著者:ロドリゲス-コンスエグラ著、好田順治訳
出版元:青土社

訳が微妙らしい

Logical Dilemmas
著者: J.W. Dawson, Jr.
出版元:A K Peters, Wellesley, Massachusetts

ゲーデルの伝記的事項について徹底的に書いた本
0252132人目の素数さん2005/10/20(木) 17:53:38
林さんのページ
ttp://www.shayashi.jp/HistorySociology/HistoryOfFOM/Books/books.html

定理にまつわる物語、じゃゲーデルがアインシュタインに招かれてアメリカに
亡命して、入国のための試験を受けたときに、、といった伝記的事項が知りたいのか
それとも当時の思想的な潮流を知って、どうして不完全性定理が衝撃的だったのか
を知りたいのか、といった周辺事情を知りたいのか、どっちか分かりにくいんだが、、
■ このスレッドは過去ログ倉庫に格納されています