- 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/
- 46 名前：12 mailto:sage [2011/10/30(日) 15:14:47.94 ]
- >>42
ではｆの定義が、再帰の定義に沿っているかどうか
確認していただけますか？
>>43
＞・意味をなさない記号列はゲーデル数化していないから
間違ってますね。
- 47 名前：１３２人目の素数さん [2011/10/30(日) 15:15:59.23 ]
- >>41
それらの体系には無限個の公理が存在しますがどうやって整列させますか？
- 48 名前：43 [2011/10/30(日) 15:19:47.81 ]
- そうですね。
再帰的定義で項が閉じてるから
項じゃないものは当然入ってきませんね
- 49 名前：12 mailto:sage [2011/10/30(日) 15:21:32.34 ]
- >>41
＞形式化を考えないなら、
41＝35＝8 でしょうか？
>>8のいわれる「形式化」は「公理の明示」の意味ですね。
もちろん、いかなる公理に基づいているかは明示する必要があります。
（もっとも、これを「形式化」という人はあなただけですが）
>>18のいわれる証明は知らないので、なんともいえません。
- 50 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:28:42.80 ]
- >>47
>>44
よく知られていることは、初めに与えられた 述語、関数記号が整列されて
いる場合、論理式は有限列であるから、長さ n に関する帰納法で、おのおの
の n についての整列を定義することができ、これらの和が、論理式全体の整列
を与える。
- 51 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:31:16.68 ]
- >>49
当り前だが、8 は別人だよ。それより 50 をよく勉強しなさい。
- 52 名前：12 mailto:sage [2011/10/30(日) 15:40:07.63 ]
- >>50
＞初めに与えられた 述語、関数記号が整列されている場合、
で、PAやZFCでは、述語、関数記号が整列されていることは
「よく知られている」のですか？
よく御存知とはおもいますが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
- 53 名前：12 mailto:sage [2011/10/30(日) 15:42:06.10 ]
- >>51
＞当り前だが、8 は別人だよ。
書いている当人にとっては当り前でしょうが
それ以外の人にとってはそうではないんですよ。
このことが、アスペルガー症候群の人には
理解しがたいといわれていますが。
- 54 名前：12 mailto:sage [2011/10/30(日) 15:45:32.98 ]
- >>51
＞50 をよく勉強しなさい。
>>50の前提条件である
「初めに与えられた 述語、関数記号が整列されている場合」
にはその通りでしょう。重要なのは上記の前提条件は
PAやZFCにおいて成立するのか？という点です。
>>52にも書きましたが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
- 55 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:55:24.82 ]
- ZFC には定数記号はない。ε と = (述語記号か論理記号かは流儀による）
以外は変数記号と論理記号だけ。
PA の定数記号は 0 だけ。PA の関数記号は S だけ。
当たり前というのは、50 のようにすっきり書ける人と 8 のようにごてごて
書いている人の違いはわかるだろうという意味だが、52 のようなことを書いて
いる人にはわからないかもしれないね。
- 56 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 16:03:46.11 ]
- 54 のようなことを書いてあるので、変数記号についても書いておこう。
変数記号は、自然数によって番号付けられているから、整列されている。
もう少しついでに書いておこう。ゲーデル数を対応させて、有限列を自然数
に対応させることがわかれば、すべての文字列に自然数が対応し、これは単射
だから整列されていることは明らか。50に書いてあるのは、可算でなくても
整列されていればよいということ。
- 57 名前：12 [2011/10/30(日) 16:33:12.46 ]
- >>55
なるほど。定数記号に関しては明らかでした。
ところで>>8も引用は長いですが、
文章は三行なので「ごてごて」とは思えません。
したがってやはり自明とはいえません。
- 58 名前：12 [2011/10/30(日) 16:46:44.25 ]
- >>55-56
とはいえ、モデルの各元に対して、元々の理論の中に存在しない
定数記号を付加することが可能であるので、その場合、モデルの
濃度によっては、整列するために選択公理が必要でしょう。
- 59 名前：12 [2011/10/30(日) 16:54:58.46 ]
- >>58
＞ゲーデル数を対応させて、有限列を自然数に対応させることがわかれば、
＞すべての文字列に自然数が対応し、これは単射だから整列されていることは
＞明らか。
＞50に書いてあるのは、可算でなくても整列されていればよいということ。
自然数だから整列可能、といいたいようですが、それは自明ですか？
一階述語論理上で公理化された自然数論のモデルは範疇的ではありません。
当然、非標準的なモデルもありますよ。
- 60 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 17:02:39.81 ]
- >>58 >>59
いい加減にしたらよい。44のようなことを書いたことが恥ずかしい
と思ったらどうかね。
自然数論のモデルというのなら、もちろん、整列できないモデルさえ
つくれる。しかし、今、完全性定理を証明しようとしているので、
そんなものが問題にならないのは明らかだ。要するに偉そうに、答え
たり、しているが、ちっともわかっていなかったということだ。
恥ずかしいと思うことを、初めにしたらよい。
- 61 名前：１３２人目の素数さん [2011/10/30(日) 17:11:13.56 ]
- >>60
＞44のようなことを書いたことが恥ずかしいと思ったらどうかね。
あなたが41で「可算（濃度）モデルにおける完全性定理」
と書いていれば、そういうこともいえたであろうが・・・
＞自然数論のモデルというのなら、もちろん、
＞整列できないモデルさえ つくれる。
＞しかし、今、完全性定理を証明しようとしているので、
＞そんなものが問題にならないのは明らかだ。
完全性定理には、モデルの濃度の制限はない。
＞要するに偉そうに、答えたり、しているが、
＞ちっともわかっていなかったということだ。
「偉そうに」と思ったのは貴方の勝手。
あなたもモデルの濃度を全く考慮していなかった。
つまりわかっていなかった。
あなたは、わからないことは恥と思うのであれば
まず自分自身を恥じたらよい。
もっとも、そういう考え方は狂っている、と私は思うが。
- 62 名前：１３２人目の素数さん [2011/10/30(日) 17:15:13.99 ]
- ところで、私には、41が完全性定理の前提から
選択公理を除こうとする理由が理解できない。
- 63 名前：１３２人目の素数さん [2011/10/30(日) 17:30:18.48 ]
- ところで全くの脱線だが
>>60
＞いい加減にしたらよい。
＞恥ずかしいと思うことを、初めにしたらよい。
こんなおかしな喋り方をする
アニメのキャラクターでも
いるのかね？
- 64 名前：42 mailto:sage [2011/10/30(日) 17:48:15.19 ]
- >>46
>ではｆの定義が、再帰の定義に沿っているかどうか
>確認していただけますか？
IsTermの特性関数が再帰的関数になるか考えてましたが、やっぱりまだ分かりません。(直感では、IsTermが再帰的であること、計算可能であることは分かります。)
IsTerm(x)の定義の中に、m<xなるmに対して再びIsTerm(m)が出てきてるので、特性関数は原始帰納法によって一部定義されであろうことまでは分かるのですが、、、。
もしかして、IsTermの特性関数は累積帰納法で表しますか？
- 65 名前：8 [2011/10/30(日) 18:07:39.86 ]
- しばらく見ない間に議論が起きましたが
足りない部分について補足しますね＾＾；
>>29
ゲーデル数は全順序になるので、
整列可能定理が不要になるのです。
>>39>>49
私は形式化という言葉をかなり広い意味で使っています。
確かに誤解が多い書き方だったと思いますね。
>>64
再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。
定義からやり直すと煩雑すぎます。
- 66 名前：15 mailto:sage [2011/10/30(日) 18:22:01.69 ]
- >>41
論理式が整列されてるってことでなぜ救えるのかわかりませんね。
>>50
> これらの和が、論理式全体の整列を与える。
証明というものを具体的な対象物として見る場合、これはちょっと受け入れられない論法ですね。
>>60
> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
これは了解
>>61
> 完全性定理には、モデルの濃度の制限はない。
これは誤解していると思う。
- 67 名前：8 [2011/10/30(日) 18:49:24.69 ]
- >>66
だよな、そもそも1階論理の完全性の話してんのにな。
それにはじめてに論理式に識別番号つけて整列させてんなら
言語定義すんのに整列可能定理が必要ｗ
しわを伸ばしてみたら、しわの位置が変わっただけｗ
- 68 名前：42 mailto:sage [2011/10/30(日) 19:41:37.61 ]
- >>65
>再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。
定義しようとしている述語が、別の述語を使って定義されていれよいのですか、今考えているIsTerm は定義中に再びIsTermが現れているのが問題なのです。もっといえば、そうである以上原始帰納法を使って定義できるはずなのですが、それがなかなか分からないのです。
ちなみに今、考えているのは論理式ではなく形式化されていない算術の述語なのですが。
- 69 名前：15 mailto:sage [2011/10/30(日) 20:15:11.07 ]
- 別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
「超越的な方法を認めなくても結果的に有効」であって欲しいのです。
- 70 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:20:18.99 ]
- ところで42は
Proof(x,y):=yはゲーデル数xの論理式の証明である
が再帰的述語であることは理解していますか？
- 71 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:21:54.46 ]
- 訂正：証明である→証明のゲーデル数である
- 72 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:37:40.00 ]
- >>69
よく分かりませんが、あなたのその願いがいつか叶うことを祈っておきます
- 73 名前：42 mailto:sage [2011/10/30(日) 20:43:22.86 ]
- >>70
再帰的になるということは、各文献で目にしていますが、確認はしていません。
なので、現在はproof(x,y)が本当に再帰的な述語であるかどうかを確認するため、これを構成する際に必要な諸々の述語を再帰的かどうか確認しています。
とまぁ、この過程で今「ゲーデル数xはPAの項である。」でどんづまっています。
- 74 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:43:44.52 ]
- 「超越的な方法」というのがWKLのことなら、
WKL が PRA 上の保存拡大だから「結果的に有効」なんじゃない？
- 75 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:53:29.84 ]
- >>72
>>74
「超越的な方法」とはPRAそのものだろ。
- 76 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:59:37.82 ]
- >>67 >>69
チミたちには難しすぎるようだが、選択公理が必要なのは、一般的な
設定の場合で、具体的なもの、例えば、PA, ZFC では論理式は、自然な
方法で整列できるのだよ。
- 77 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 21:03:46.06 ]
- >>73
論理式Aが証明可能であるということの定義は
Aに至る論理式の有限列が存在して、その列の各項が公理か、以前の論理式から導かれること
というのは理解していますか？
もし、理解していればそれと同じような感じで
有限記号列Tが項である⇔
Tに至る有限記号列の有限列が存在して、……
と表せるのは理解できますか？
- 78 名前：69 mailto:sage [2011/10/30(日) 21:06:17.15 ]
- >>76
オレは別に「整列」とは言ってないが、お前ほんとに具体的なものについて語ってるか？
項、式、証明ってほんとに具体的なものなんだぞ？
- 79 名前：１３２人目の素数さん [2011/10/30(日) 21:20:37.41 ]
- そもそも1階述語論理が
もろに対数学用述語論理だかんね
命題論理の完全性定理だけ考えりゃええんやないの？
それに論理体系を集合論で記述せにゃあかんこともないやろ
そもそも初期の頃は高階述語論理がスタンダードやて
その後に1階論理にしぼらな決定可能な完全性こしらえた証明体系つくれへんし
LS定理やらも意味もたへんさかい現状の1階論理さ注目されたんど
わいはエルブラン領域でスコーレム＝エルブランの完全性定理使っちくりゃ
-----エルブランは有限主義で選択公理嫌いでさかい信頼できんど------
ヘンキンさにペコペコ頭下げといて極大集合こしらえる必要もあらへんやろ
まぁ論理プログラミングさまさまやないけ
- 80 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 21:31:31.69 ]
- まあもうちょっと真面目に書いていただければ助かるのですが・・・
- 81 名前：１３２人目の素数さん [2011/10/30(日) 23:16:26.46 ]
- 電線やハブや変圧器が電気メーカーにより製造される。
各家庭には様々な種類の電化製品が設置されている。
そしていくつかの発電施設が存在している。
例えば、あなたは今部屋の電灯を点けたとする。
このとき発電施設からいくつかの電線やハブや変圧器を
辿って行けばあなたの電灯に到達することは確実だ。
電灯が点けば真、発電施設が公理、ハブや変圧器が推論規則、
発電施設から電灯までの電線が証明だ。
電灯が点くなら、発電施設から電灯まで辿る電線がある。
これが完全性定理の内実である。
- 82 名前：42 mailto:sage [2011/10/30(日) 23:25:54.39 ]
- >>77
もととなるものと、それをもとにして生成する規則の二つがあればよいということでしょうか？
形式的体系でいえば、もととなるのは公理で、生成規則は推論規則になります。
項でいえば、0と変数がもとなるもので、Sと+と・が生成規則になると。
- 83 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 23:36:10.57 ]
- >>82
はい、そういうことです
今、ビデオ見てるんで一旦落ちます
- 84 名前：42 mailto:sage [2011/10/30(日) 23:44:06.37 ]
- 見当違いのことを言ってたら訂正をお願いします。
私が理解できないのは、
1. 形式的体系PAの各記号を自然数に一対一対応させる。
2. PAの記号からなる有限列(項や論理式)を、ある自然数に一対一対応させる。(エンコードの方法は、素因数分解を利用した関数とする。)
3. PAの記号からなる有限列(項や論理式)の有限列(証明のこと)を、上と同じ方法で自然数に一対一に対応させる。
4. 以上の考えをベースにして、形式的体系に関する概念を、算術上の述語として表現する。
5. 述語 IsTerm (x)「xは形式的体系PAの項である。」
⇔ x=/0/
または ヨn<x (IsTerm(n)かつx=/S/*par(n))
または ヨm<x ヨn<x ［IsTerm(m)かつIsTerm(n)かつ(x=par(m)*/+/*par(n)または x=par(m)*/・/*par(n) )］
このように考えた上で、私がわからないのは、
・5の定義は正しいのか
・正しいとしたら、5におけるIsTerm の特性関数はどのようになものになるのか
の二点です。
どうか教えてください。
- 85 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 00:46:40.15 ]
- >>84
今戻りました
項Tに対して、Tに至るまでの記号列の列T1,T2,...,Tn=Tを考える
これを項Tを生成する列と呼ぶことにして、この列にゲーデル数を対応させる
yはゲーデル数xの項を生成する列のゲーデル数であることを表す述語をMakeTerm(x,y)とでもしておく
項の生成の仕方より列に現れるT1,T2,...,Tnのゲーデル数はTのゲーデル数以下なので
xに対してyはある関数g(x)で上から抑えられるはず
そのときIsTerm(x) :=∃y<g(x) (MakeTerm(x,y)) と表される
これでわかりますか？
- 86 名前：42 mailto:sage [2011/10/31(月) 01:03:17.00 ]
- >>85
レスありがとうございます。
仰ってることは(たぶん)分かっております。
私が知りたいのは、ではそれを具体的にどうやって再帰的関数(および述語)の形で表すのか、ということです。85さんの説明でいえば、MakeTermは、ではどうやって定義されるのでしょうか。おそらくMakeTerm の特性関数は原始帰納法の形、つまり
f(0)=g(x)
f(x+1)=h(x,f(x))
という形になると思うのですが、その具体的構成方法を知りたいのです。
これを定義するには、準備としていくつかの関数と述語を定義しないとだめだということは分かってますが。。。
- 87 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:22:01.06 ]
- >>86
特性関数考えるより具体的にMakeTermがどう表現されるか考えた方が早いですよ
T1,T2,...,Tn=TがTを生成する列である⇔∀p=1,2,...,n [Tp=0∨∃q<p {Tp=S(Tq)} ∨∃r<p ∃s<p {Tp=(Tr)+(Ts) ∨ Tp=(Tr)*(Ts)}]
あとはこれをゲーデル数に書き換えればOK
- 88 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:26:58.78 ]
- >>87
すまん最後に ∧ Tn=T が抜けてた
- 89 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:32:21.66 ]
- あと気になったが変数記号は定義に無かったか？
- 90 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:52:22.65 ]
- あした早いんでもう寝ますzzzzz
- 91 名前：42 mailto:sage [2011/10/31(月) 02:08:52.15 ]
- それだと、Prove(x) (⇔ヨyproof(x,y) )が再帰的でないのと同様に、IsTerm (x)も再帰的でなくなってしまうような気がするのですが。
理解力がなく申し訳ないです。
身近に教えてくれる人がいればいいのですが、なにぶん独学なもので。。。
また明日しっかり考えてみようと思います。今日はご丁寧にありがとうございました。
- 92 名前：42 mailto:sage [2011/10/31(月) 03:50:15.46 ]
- 結局まだうだうだ考えてたのですが、
累積帰納法で得られた関数は、再帰的関数である。
ということを証明できれば、私の疑問点は解決できることがわかりました。
- 93 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 04:52:16.35 ]
- Foundations of Mathematics への入会ってどうすればいいのか誰かご存知ですか？
- 94 名前：12 mailto:sage [2011/10/31(月) 07:02:50.15 ]
- >>69
>別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
>完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
「普遍的に成り立つ」という言葉で、
どういうことを期待しているのか不明。
>「超越的な方法を認めなくても結果的に有効」であって欲しいのです。
モデル理論は超越的であると私は思いますが、
あなたは、なぜ、違うと思うのでしょうか？
- 95 名前：12 mailto:sage [2011/10/31(月) 07:05:41.79 ]
- >>76
>>58 の
＞モデルの各元に対して、元々の理論の中に存在しない定数記号を
＞付加することが可能であるので、その場合、モデルの濃度によっては、
＞整列するために選択公理が必要でしょう。
を理解できなかったようですが、付加はできないと思ってますか？
そう思う理由はなんですか？付加できるとは聞いていないからですか？
- 96 名前：12 mailto:sage [2011/10/31(月) 07:09:34.70 ]
- >>67
＞そもそも1階論理の完全性の話してんのにな。
だから「対象の個数は可算個でいい」と？なぜ？
- 97 名前：8 [2011/10/31(月) 08:12:47.78 ]
- >>96
＞> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
＞これは了解
いえここへのレスです。
- 98 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 08:33:10.20 ]
- >>91
g(x)が再帰的関数、P(x,y)が再帰的述語のとき、∃y<g(x) P(x,y) も再帰的述語になるということはご存知ですか？
Prove(x) (⇔ヨyproof(x,y) ) の場合、yを上から抑えるg(x)が存在しません
例えば、論理式Aを証明する過程でむちゃくちゃ長い論理式を経由しなければならない場合もあるかもしれないのです
一方、項の定義では、生成規則は必ず生成前のより生成後の方が記号列の長さが大きくなるように作られています
したがって、項Tを生成する列T1,T2,...,Tnで n≦(Tの長さ)、かつ∀p=1,2,...,n Tp≦Tとなるようなものを具体的に作ることが可能です
よって、yを上から抑えるg(x)が存在することになり、結果IsTerm(x)も再帰的になるのです
- 99 名前：42 mailto:sage [2011/10/31(月) 22:06:24.97 ]
- >>98
よくわかりました！！
今日一日中考えてやっと理解できました。
ありがとうございます。
- 100 名前：１３２人目の素数さん [2011/10/31(月) 22:49:21.54 ]
- g(x),f(x,y),f(x,g(x)),P(x,y)∊PR
∃y<g(x) P(x,y)
⇔ Π_[y<g(x)] f(x,y)＝0
≡ f(x,g(x))・Π_[y<g(x)-1] f(x,y)＝0
≡ f(x,g(x))・f(x,g(x)-1)・Π_[y<g(x)-2] f(x,y)＝0
：
：
≡ f(x,g(x))・f(x,g(x)-1)・...・f(x,g(x)-g(x))＝0
∃y<g(x) P(x,y)∊PR □
- 101 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 00:04:23.72 ]
- >>94-96
どうもまわりくどい書き方だな。
モデル理論は超越的だとオレも思うし、違うなんて言ってないよ。
「普遍的に成り立つ」という言葉は普通の意味にとってくれ。
完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
AがTで妥当であり、T[￢A]もT[A]も矛盾していない、
実例を作れたらな。
- 102 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 01:46:19.25 ]
- 論理学の根本的な部分について質問させてください。
論理学では論理を形式化して考察していきますが、
メタな論理としてどこまでのレベルのものを許すのかということは考慮されるんでしょうか？
たとえば述語論理の体系では集合の概念を用いて理論が展開されますが、
より初等的な概念で展開することは可能でしょうか？
- 103 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 03:21:57.74 ]
- >>102
考慮するときもある。
が、しかし、入門的な教科書ではそれは一旦脇に置いておく書き方をするのが普通。
もっと高度なことをやるときには考慮しないといけなくなるけれど、
そういうことをやる為にはまず脇に置いた議論をきちんと理解していることが前提となる。
- 104 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 06:12:25.61 ]
- 12,8 あるいは 15 という方たちは、ある程度の知識はお持ちのようだが、どう
もよくわかっていないようなので書いておこう。
述語論理の完全性という場合、述語論理をどう述べるかということがある。
述語記号、関数記号、定数記号が自然数で番号が付けられているかどうか？
あるいは順序数で番号付けられているかどうか？
次に完全性定理をどのように述べているかを調べる。例えば、無矛盾な公理
系に対してと書いてあるような場合、一般には、述語論理は、この公理系の
言語を含むものに拡大されていることになる。
これらのことが、完全性定理が選択公理と関係するかどうかの鍵である。
最初に書いた自然数で番号付けられた言語からはみ出なければ、選択公理
は不要なのだ。
- 105 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 06:37:38.03 ]
- >>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。
それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？
- 106 名前：12 mailto:sage [2011/11/01(火) 07:19:22.56 ]
- >>69 >完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
>>94 >「普遍的に成り立つ」という言葉で、どういうことを期待しているのか不明。
>>101 >「普遍的に成り立つ」という言葉は普通の意味にとってくれ。
「普遍的に成り立つ」という言い方は普通しませんので
”普通の意味”というのは意味不明です。
- 107 名前：12 mailto:sage [2011/11/01(火) 07:21:40.31 ]
- >>101
＞完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
＞AがTで妥当であり、T[￢A]もT[A]も矛盾していない、実例を作れたらな。
「妥当」という言葉の定義は御存知ですか？
AがTで妥当であって、￢AもTで妥当である、という場合も存在しますよ。
- 108 名前：12 mailto:sage [2011/11/01(火) 07:27:06.40 ]
- >>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。
>>105
>それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
>その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？
104は、論理式の整列と選択公理の関係しか見ていないようだが、
別の点にも注目する必要がある。
モデルを構築する際に、無矛盾性（妥当性、充足可能性を
チェックしているが、述語論理の決定不能性定理からいえば、
無矛盾（妥当、充足可能）か否かを判定できるアルゴリズム
は存在しない。
- 109 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 08:01:07.64 ]
- >>107
101ではないが、
T|=A⇔Tの任意のモデルにおいて、Aは真 ということだよな？
もし、T|=�魵だとしたら、Tの任意のモデルで�魵も真ということ。
ということは、Tの任意のモデルで、Aも�魵も真。こんなのってないよ、ありえないよ。
- 110 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 13:00:33.75 ]
- >>98
定義の仕方、およびそれが再帰的になっていることはしっかり確認できました。ありがとうございます。
上から抑えるためのg(x)って具体的にはどんなものになりますか？
参考書には、g (x)=(p_len(x)＾2)＾x・len (x)＾2
とありましたが、どうしてこれが抑えるために十分なのかがわかりません。
- 111 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 14:10:23.41 ]
- >>110
それはゲーデル数の定義によるから何ともいえんよ……
- 112 名前：１３２人目の素数さん [2011/11/01(火) 21:39:34.80 ]
- 普通の1階論理なら完全性は成り立つよ。
普遍的にね。
- 113 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 22:09:33.16 ]
- >>110から多分推測するに
Tをゲーデル数xの項として、Tを生成する列をT1,T2,...,Tnとする。Tの長さはlen(x)で表される
例えばT=(S1)+(S2)の形であれば、Tを生成する列の中にS1とS2があるはず。そうすると列の長さnは2^len(x)以下である
（>>98で n≦(Tの長さ)と書いたが間違いでした。すみません）また、T1,T2,...,Tnのゲーデル数はx以下である
よって列のゲーデル数は(p_1)^x・(p_2)^x…(p_len(x)^2)^x≦(p_len(x)^2)^x・len (x)＾2で抑えられる
- 114 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 22:16:15.70 ]
- >>113
ミス
×そうすると列の長さnは2^len(x)以下である
○そうすると列の長さnはlen(x)^2以下である
- 115 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 23:20:51.62 ]
- >>112
普通の1階論理ってなに？
関数や述語などが有限個であれば普通？
普遍的に成り立つって、追加の前提や仮定がまるっきり無用なの？
- 116 名前：１３２人目の素数さん [2011/11/01(火) 23:42:31.83 ]
- >>69
普遍的において何を仮定しているのか不明ですけど、
そもそも述語論理での完全性定理は、
「ほとんどの証明体系で成り立たない」です。
例えば普通の真偽値では |＝￢A→(A→B) です。
証明体系を以下で定義します。
公理型 A→A
推論規則 MP
このとき |＝￢A→(A→B) ⇒ |-/-￢A→(A→B) です、何もできません。
つまり述語論理の中で完全な証明体系を探しているのであって、
述語論理は完全じゃないです。
本によってはLKの完全性定理とかNJの完全性とかちゃんと書いています。
- 117 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 23:52:04.97 ]
- そういう話じゃないみたい
- 118 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 00:01:10.42 ]
- HJは真偽値が3つないと完全にならなかったな。
- 119 名前：12 mailto:sage [2011/11/02(水) 07:08:29.92 ]
- >>109
>T|=A⇔Tの任意のモデルにおいて、Aは真 ということだよな？
ああ、妥当を充足可能と同義だと思っていたが、誤解だった。
その場合
「AがTで無矛盾」というのは
「AがTで充足可能」という意味で、
「AがTで妥当」とは違う。
- 120 名前：12 mailto:sage [2011/11/02(水) 07:12:22.84 ]
- >>112
>普通の1階論理なら完全性は成り立つよ。
>普遍的にね。
その場合の完全性は
「1階論理のどのモデルでも真な命題
（つまり1階論理で妥当な命題)なら
1階論理で証明可能」
という意味。
- 121 名前：12 mailto:sage [2011/11/02(水) 07:17:43.40 ]
- よく述語論理の完全性定理を
「述語論理の命題Pは、かならず
P自身かその否定￢Pのいずれか
が証明可能」
と思っている人がいるが誤り。
論理の完全性は、理論の完全性とは意味が異なる。
ところで
「無矛盾で完全な理論T、つまり、理論Tが、
命題Pかその否定￢Pのいずれかを必ず証明出来る
場合には、モデルが存在する」、
という命題はWKL0ではなくRCA0で証明可能。
- 122 名前：８ [2011/11/02(水) 08:13:31.03 ]
- >>117
>>69が訊きたいのはかなり原理的なレベルの話だと思うのです。
完全性定理は「数学に使える位まともな論理」だけで成り立つということです。
例の述語論理の決定不能定理も、Qが展開できる程度の証明体系に限定されますから。
ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
>>69が問題にしているのは可算な述語論理の言語の完全性定理の
RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。
- 123 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 09:34:34.03 ]
- やはり逆数学という、基本的に後ろ向きの数学の一派の話なわけだ。
原理的というには、話をせまくしすぎている。
- 124 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 09:38:20.21 ]
- >>123 ですね。
こういうものは、基本的に
公理の数をいくら減らせるか、という話なので、
大きな目標なり企みなりがあってこそのもので、
そうでなければ、スケールの小さなテーマに終わってしまう。
- 125 名前：１３２人目の素数さん [2011/11/02(水) 13:20:55.22 ]
- 比較的新刊のフランセーン『ゲーデルの定理』を中身見ないで注文しようかどうしようか
迷っているんだが、もう読んだ人どうよ？
- 126 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 13:30:58.77 ]
- 逆噴射数学
- 127 名前：１３２人目の素数さん [2011/11/02(水) 19:16:02.80 ]
- >>125
基本的に読み物ね。
具体的な数学的内容は全くないです。
不完全性定理の社会的視点ですね。
新書のゲーデルの哲学とかのもう少し詳細なものですかね。
- 128 名前：１３２人目の素数さん [2011/11/02(水) 19:22:46.29 ]
- >> 127
ありがとう。数学的内容がないということなのでやめときます。
（さっき訳者あとがきPDFを見たらそうでもないように見えたが）
- 129 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine [2011/11/02(水) 19:29:37.64 ]
- ＞＞１２８
お前、早く、社会人にならないと、取り返しがつかないことになるぞ！
- 130 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 19:55:42.02 ]
- 彼女にフェラチオさせてから寝るか・・
- 131 名前：１３２人目の素数さん [2011/11/02(水) 20:03:02.10 ]
- >>128
数学的内容というのは語弊があった。
定義・定理・証明みたいな流れがないってこと。
不完全性定理の解説については岩波文庫の例の本の解説と同じレベル。
- 132 名前：１３２人目の素数さん [2011/11/02(水) 20:51:55.88 ]
- >> 131
了解。ありがとう。
- 133 名前：8 [2011/11/02(水) 22:34:43.03 ]
- >>123
1派ではない、Simpsonの本しか読んだことない。
>>132
ただしゲーデルの定理とかいう本はまともな本。
「どんな体系で不完全が成り立つんだろ」
「決定不能とかって不完全性とどう関係してるんだろ」
「自己言及ってどんな種類があるんだろ」
みたいな疑問があったら読んでみるといいのでは？
既に不完全性定理を知っている人は
立ち読みか図書館で興味あるとこに目を通すだけで充分。
- 134 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 00:25:00.08 ]
- 逆数学が仮に分類だから狭いとしても、代数多様体の分類とおなじく、
分類を証明する手段が数学をゆたかにするっていうこともあるよね。
- 135 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 01:52:39.31 ]
- 逆数学が狭いといわれるのは、分類だからではなく、研究対象が二次的
であることにある。
- 136 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 04:24:21.82 ]
- 研究対象が二次的だと何故狭くなる？その二つがどう結びつくのか皆目見当が付かない。
- 137 名前：8 [2011/11/03(木) 06:36:37.24 ]
- 逆数学は数学を計算クラスの視点から階層化している気がする。
例の2階算術の部分体系も様々なチューリングマシンで置き換えられるし。
純粋に好奇心をそそられる研究だと思うけど。
- 138 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 08:44:09.19 ]
- >>137 重箱の隅とも言う。
- 139 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 08:51:45.25 ]
- 二次的であれば重要度が減る。
三次、４次、とつづく研究をするか？
ある定理を証明するのに、ある公理系が必要十分であることを証明できたら、
次に、そのメタ証明を証明するのに、必要十分な公理系を証明する、
そのメタメタ証明を、、、
あ、私は135とは別人ね
- 140 名前：１３２人目の素数さん [2011/11/03(木) 08:52:33.58 ]
- >>122
>完全性定理は
>「数学に使える位まともな論理」
>だけで成り立つということです。
ん？集合論は数学には使えないトンデモ論理だといいたがってる？
もしかして8は有限主義者？クロネッカーの生まれ変わり？
- 141 名前：１３２人目の素数さん [2011/11/03(木) 08:57:37.20 ]
- >>122
> ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
> >>69が問題にしているのは可算な述語論理の言語の完全性定理の
> RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。
言語を可算に制限しても、理論が完全でない場合、
RCA0ではダメだよ。
- 142 名前：１３２人目の素数さん [2011/11/03(木) 09:08:24.32 ]
- >>135
>逆数学が狭いといわれるのは、
>･･･研究対象が二次的であることにある。
そもそも「二次的」という言葉を
どういう意味で用いているのか不明。
数学の成果を「一次的」として、
その数学の前提をどれほど弱められるかが
「二次的」だということか？
もしそうなら、別に狭いともつまらんとも思わんが。
- 143 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 09:52:04.05 ]
- （フランセーン『ゲーデルの定理』は）
>定義・定理・証明みたいな流れがない
それ、「流れ」じゃなく「スタイル」だろ。
フランセーンの本は数学書ではないよ。
読者層は数学科の学生ではなく数学に興味をもつ一般人だから。
とはいえ、いい加減なものかといえば全然違うけどね。
むしろ、数学科を出た人間も目からウロコが落ちる話が沢山書いてある。
岩波文庫「不完全性定理」とはまた違った意味で読み応えがある。
- 144 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 11:20:08.84 ]
- 重箱の隅をつつくようなマイナーな研究は、私費でやるべき
- 145 名前：8 [2011/11/03(木) 12:41:34.25 ]
- >>140
いいたがっていない。
集合論がどういった証明体系の述語論理の上にあるのか
普通は明示されないが、おそらく完全な述語論理の上で
つくられているので問題なし。
>>141
理論の完全の所を詳しくお願いします。
- 146 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 13:17:56.41 ]
- >>145
>>141は完全の意を取り違えてるだけだから質問しても無駄だろう
|
 |
