11/10/29 22:42:36.86
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
URLﾘﾝｸ(www.math.tohoku.ac.jp)
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学 その9
ｽﾚﾘﾝｸ(math板)
2:１３２人目の素数さん
11/10/29 22:58:12.73
king.
3:１３２人目の素数さん
11/10/29 23:07:02.01
king.
4:１３２人目の素数さん
11/10/29 23:08:15.09
やっちまったな
5:１３２人目の素数さん
11/10/29 23:27:39.24
URLﾘﾝｸ(iup.2ch-library.com)
6:１３２人目の素数さん
11/10/30 03:40:17.06
このスレタイが基地外の色がなくて常識的。このままでよい。
7:１３２人目の素数さん
11/10/30 05:56:52.63
つーか、いくら議論しても反論になってない反論（しかも毎回同じ内容）ばかりで
この先いつまで議論しても噛み合うようには思えない。
このスレタイで嫌だって奴だけで別のスレッドに移行すればいいんでない？
板の分割とかもあるわけだから、スレッドを二つに分けても問題ないでしょ。
新しいスレッドは基地外だらけになりそうだがなｗ
8:１３２人目の素数さん
11/10/30 08:18:03.13
＞997 名前：１３２人目の素数さん[sage] 投稿日：2011/10/29(土) 11:23:35.35
＞完全性定理の内容って
＞「理論が無矛盾ならモデルが存在する」（ただしこのモデルは超越的方法で作られる）
＞で、これから
＞ Aがどんなモデルでも真
＞ → ￢Aを満たすモデルは存在しない ①
＞ → もし超越的な方法を許したとしても￢Aのモデルは存在しない ②
＞ → ￢Aを仮定すると理論が矛盾する //定理の対偶
＞ → Aは証明可能
＞が成り立つってことだけど、
＞超越的な方法を認めない場合でも②は有効と言えるんだろうか？
超越的だか何だかは関係ない。
極大無矛盾集合の証明で論理式を並べているので
完全性定理の証明を形式化したとき論理式に選択公理が入ってるってこと。
9:１３２人目の素数さん
11/10/30 09:46:50.40
数学基礎論、数理論理学は数学ではなく、
論理学なのだから、哲学板か、情報学板へ
言った方が良いよ。
10:１３２人目の素数さん
11/10/30 10:04:58.75
>>8
「論理式に選択公理が入ってる」って日本語がわからん。
完全性定理だけは1階述語論理一般で普遍的に成り立ってくれなければ
困るので、弱ケーニヒだかの超越的な手法を使えない。
11:１３２人目の素数さん
11/10/30 10:13:59.80
>>9
数学基礎論、数理論理学が数学か否かについては
本スレッドではなく別途、スレッドを立てて
そこで議論していただくことを強く勧める。
12:１３２人目の素数さん
11/10/30 10:19:33.13
>>10
一階述語論理の完全性定理は、一階述語論理上の定理ではなく
集合論（もしくは二階算術）の定理である。
逆数学においては弱いケーニヒの補題が成立するＷＫＬという
２階算術の体系で成立することが知られている、ということ。
とはいえ、本来はモデルを考えるのに、集合論を前提している。
13:１３２人目の素数さん
11/10/30 10:35:18.10
「任意のモデルでAが成り立つ。よってAは定理(証明が存在する)」
という証明の手法は い つ で も 使える。これが完全性定理じゃないの？
項、論理式、証明といった再帰的に定義された具体物の存在について言っているので、
「実は集合論の上の定理でした」じゃ困る。
14:１３２人目の素数さん
11/10/30 10:37:15.31
新スレがたったので、改めてこちらで質問させてもらいます。
「ゲーデル数xは、PAの項である」を再帰的に表す算術上の述語
はどのようにして定義すればよいのでしょうか。
15:１３２人目の素数さん
11/10/30 10:41:31.14
>>12
とはいえモデルってものはそのユニバースを集合としているわけで、
決して「集合論なんて知りません」というスタンスではない。
集合論という理論の中で成立している特定の定理を、どうすれば具体物に適用できるのか、
正当化できるのか、という質問です。
16:１３２人目の素数さん
11/10/30 11:01:53.49
弱ケーニッヒ補題と1階論理の完全性定理の同値性はRCA0だけで書ける。
これは見かけ上の記述がRCA0でOKということ。
実際にこれらの同値性を証明する議論に
どういう体系(最低でも公理的集合論？)が必要かは
明確に述べられないと思う。
1階論理とその完全性定理をすべて公理的集合論(例えばZFC)で書いたとき、
完全性定理を意味する長大な論理式の中に、
選択公理から推論される何らかの論理式を使わなければ、
論理式を整列することはできないことは簡単に想像できる。
ところが論理式をゲーデル数化することで、この選択公理が不要になることもわかっている。
事実不完全性定理の対角定理で選択公理が不要なのはこの議論による。
17:16
11/10/30 11:04:25.55
ちなみに>>12とは別人（一応
18:１３２人目の素数さん
11/10/30 11:32:19.55
初等ダイアグラム使えばモデルなんて必要ないよ。
PA上での完全性定理は田中さんの本で多少触れられている。
19:１３２人目の素数さん
11/10/30 12:03:48.40
>>14
例えば、
ゲーデル数xがPAの項に該当することをIsTerm(x)とすれば、
IsTerm(x)：xが0∨xが無限個の変数∨xが項を引数に持つ関数
で定義される。
20:１３２人目の素数さん
11/10/30 12:08:31.63
一般に、数学の定理は集合論の定理でも、自然数論の定理でもない。
当然、完全性定理も同じ。12 も 13 もおかしい。
完全性定理は、普通はモデルという集合概念を使って述べられている。
そのまま、PA の定理にはならない。大体、普通の完全性定理は集合論
の形式言語で書かれてさえいない。
21:１３２人目の素数さん
11/10/30 12:26:27.48
あほめ
モデルも言語も両方形式化するんだよ
22:１３２人目の素数さん
11/10/30 12:30:07.65
バカだね。
形式化というのは色々な選択しがある、そのことが不完全性定理のもと
であるのに、何のことわりもなく、そのようなことができると思って
いるのは、数理論理学をよくわかっていない証拠だ。
23:１３２人目の素数さん
11/10/30 13:32:17.92
>>15
1階論理とかってのはコンセンサスなのでは？
現時点で代替的な手段がまったくないから。
数学に必要な論理的構造は1階論理でOK、というのは前提としてよいと思う。
数学の中には1階論理で記述不可能な命題もあるけれど、
それらは同値の命題に置き換えることで記述可能になっている。
また普通数学をやるときには素朴集合論の命題をミニマムな前提としてやるから、
素朴集合論の命題がすべて正当化できる論理なら間違いないと思う。
24:12
11/10/30 13:39:01.69
>>13
＞「任意のモデルでAが成り立つ。よってAは定理(証明が存在する)」
＞という証明の手法は い つ で も 使える。
＞これが完全性定理じゃないの？
２行目がおかしい。
理論Tにおいて、Aという命題を証明するのに
「理論Tの任意のモデルでAが成り立つ」
という方法は使えない。
例えばTがPAの場合とか。
25:12
11/10/30 13:45:22.21
>>16
＞弱ケーニッヒ補題と1階論理の完全性定理の同値性はRCA0だけで書ける。
＞これは見かけ上の記述がRCA0でOKということ。
RCA0は二階算術。つまり自然数の集合について記述できる。
「弱い集合論」と思えばいい。
一階算術では、自然数については記述できるが、
その集まりについては記述できない。
＞実際にこれらの同値性を証明する議論に
＞どういう体系(最低でも公理的集合論？)が必要かは
＞明確に述べられないと思う。
集合を扱える必要はある。ZFCである必要はないが。
26:１３２人目の素数さん
11/10/30 13:48:56.22
今のところ分かっていることは、
・PAでは組合せ論の命題ではみ出るのが結構ある。
・Z2では実解析や関数解析周辺ではみ出るのが結構ある。
・ZFCではゲイル・スチュワートの定理など無限ゲーム系命題がはみ出る。
・1階述語論理では書けず、しかも同値命題が発見されていないものあり。
・シェラーはZFC＝数学説指示。
・ZFCに様々な公理を付けると2^ω＝ω2となることが多い。
27:12
11/10/30 13:50:24.04
>>20
＞一般に、数学の定理は集合論の定理でも、
＞自然数論の定理でもない。
＞当然、完全性定理も同じ。
一般の数学者が、集合論を意識しないのは随意だが
大抵のものは集合論の定理となる。
完全性定理を記述する際には集合の概念が必要。
＞完全性定理は、普通はモデルという集合概念を
＞使って述べられている。
＞そのまま、PA の定理にはならない。
その通り。>>10は、ある理論Tの完全性定理は
Tもしくはそれより弱い理論の定理だと誤解
している。
28:12
11/10/30 13:56:59.90
>>15 >>23
モデルは、一階論理上では直接扱えないが。
少なくとも、集合を扱える理論が必要。
そのような理論を、一階論理上の公理系として
実現することはできるが。
29:12
11/10/30 14:08:37.52
>>16
＞完全性定理を意味する長大な論理式の中に、
＞選択公理から推論される何らかの論理式を使わなければ、
＞論理式を整列することはできないことは簡単に想像できる。
日本語の文章になっていないと思われる。
完全性定理の証明において、論理式の整列が必要であり、
そのために、選択公理が必要という意味か？
＞ところが論理式をゲーデル数化することで、
＞この選択公理が不要になることもわかっている。
＞事実不完全性定理の対角定理で
＞選択公理が不要なのはこの議論による。
これまた意味不明。
ゲーデル数化によって選択公理なしに完全性定理が証明できる
といっているのか？それは初耳だ。あなたが証明したのなら
ぜひ論文を書いて、専門誌に発表したほうがいい。
30:12
11/10/30 14:11:40.14
>>15
＞集合論という理論の中で成立している特定の定理を、
＞どうすれば具体物に適用できるのか、正当化できるのか
もし15=13で、
「理論Tの任意のモデルでAが成り立つ」
という手法を理論Tで使うことが正当化できるのか
という意味なら、そもそもそういう目的で考えられた
ものではないというしかない。
31:12
11/10/30 14:16:41.51
>>14
>「ゲーデル数xは、PAの項である」を再帰的に表す算術上の述語
>はどのようにして定義すればよいのでしょうか。
それは、PAの項をいかなる形で数に翻訳するかによる。
もちろんやり方は一つではない。
32:12
11/10/30 14:22:50.24
>>23
>普通数学をやるときには素朴集合論の命題を
>ミニマムな前提としてやるから、素朴集合論の命題が
>すべて正当化できる論理なら間違いないと思う。
「素朴集合論」という言葉が指し示す理論が明確でない。
おそらくラッセルのパラドックスが起きるようなものではない
だろうが、その場合の公理系が明確ではない。
例えば、フレンケルの置換公理を採用せず、そのかわりに
分出公理を採用するというようなものだろうか？。
33:１３２人目の素数さん
11/10/30 14:29:17.25
>>19
レスありがとうございます。
xが項を引数に持つ関数
具体的には、どのように表すのですか？
34:１３２人目の素数さん
11/10/30 14:33:09.27
>>31
PAの各記号に一対一で自然数を対応させて、それを素数の指数に当ててやる方法で考えた場合は、どうなるんでしょうか？
35:１３２人目の素数さん
11/10/30 14:33:34.82
>>27
> 一般の数学者が、集合論を意識しないのは随意だが
> 大抵のものは集合論の定理となる。
> 完全性定理を記述する際には集合の概念が必要。
これらには、形式化とは何かということの考察が抜けている。何をどう表現
するかを考察すれば、最後の「集合の概念」というのは形式化された集合論
のことではないことに気がつくはずだ。
36:１３２人目の素数さん
11/10/30 14:42:41.82
メタ理論のこと？
それ言ったらロジックなんて何もはじまんないと思うけど。
37:12
11/10/30 14:44:11.80
>>35
＞これらには、形式化とは何かということの考察が抜けている。
ええ、形式化については言及していませんから。
（終）
38:１３２人目の素数さん
11/10/30 14:52:05.30
参考にしている本には、IsTerm(x)を以下のように定義するとありました。
:= x=/0/
または ヨn<x (IsTerm(n)かつ/S/*par(n))
または ヨm<x ヨn<x ［IsTerm(m)かつIsTerm(n)かつ(par(m)*/+/*par(n)または par(m)*/・/*par(n) )］
とありました。
ただし、/x/はxのゲーデル数、x*yはxとyを連結させたゲーデル数を、par(x)は/(/ * x * /)/とします。
これは正しい定義になってるのでしょうか？
・再帰的な定義になっている
・" )(+-0S(0) "などというPAの項にはならないテキトーな記号列のゲーデル数は、IsTermでも真にならない。
この二点がよくわかりません。
39:12
11/10/30 14:54:31.74
>>8
＞完全性定理の証明を形式化したとき
＞論理式に選択公理が入ってるってこと。
この人の「形式化」という言葉の使用法は独特ですね。
どうも、数学の命題を必要な前提条件をつけた上で
一階述語論理の論理式で書き表す行為を「形式化」
とよんでいるようです。
それはともかく、この言葉、実際は不要ですね。
なぜなら単純に
「完全性定理を証明するのに選択公理が必要」
と書けばいいだけなので。
40:12
11/10/30 14:56:33.92
>>38
まず再帰的という言葉の意味は御存知ですか？
41:１３２人目の素数さん
11/10/30 15:03:22.33
よく知られたことだが、完全性定理を証明するのに選択公理が必要なのは
公理系あるいは、論理式が整列されていない場合で、PA, ZFC など自然な公理
系に関する完全性定理には不必要だ。形式化したときという意味が不明。
>> 37
形式化を考えないなら、18 にあるような PA での完全性定理という表現は
ナンセンスになる。
42:１３２人目の素数さん
11/10/30 15:05:48.23
>>40
ある関数fが再帰的
⇔初期関数であるか、または再帰的関数から関数合成で得られた、または再帰的関数から原始帰納法でえられた、または再帰的関数から最小化でえられた関数
ある述語が再帰的
⇔特性関数が再帰的関数である。
と理解してます。
43:１３２人目の素数さん
11/10/30 15:10:32.52
>>38
・IsTermの定義にIsTermが出てくるから
・意味をなさない記号列はゲーデル数化していないから
44:12
11/10/30 15:12:48.17
>>41
＞よく知られたことだが、（中略）
＞PA, ZFC など自然な公理系に関する
＞完全性定理には（選択公理は）不必要だ。
いつ、どこでお知りになられましたか？
この件に関して「よく知っている」のは
あなた一人である可能性が高いので。
45:１３２人目の素数さん
11/10/30 15:14:06.58
>>41
上の議論の完全性って1階論理の話じゃないだろうか。
46:12
11/10/30 15:14:47.94
>>42
ではｆの定義が、再帰の定義に沿っているかどうか
確認していただけますか？
>>43
＞・意味をなさない記号列はゲーデル数化していないから
間違ってますね。
47:１３２人目の素数さん
11/10/30 15:15:59.23
>>41
それらの体系には無限個の公理が存在しますがどうやって整列させますか？
48:43
11/10/30 15:19:47.81
そうですね。
再帰的定義で項が閉じてるから
項じゃないものは当然入ってきませんね
49:12
11/10/30 15:21:32.34
>>41
＞形式化を考えないなら、
41＝35＝8 でしょうか？
>>8のいわれる「形式化」は「公理の明示」の意味ですね。
もちろん、いかなる公理に基づいているかは明示する必要があります。
（もっとも、これを「形式化」という人はあなただけですが）
>>18のいわれる証明は知らないので、なんともいえません。
50:１３２人目の素数さん
11/10/30 15:28:42.80
>>47
>>44
よく知られていることは、初めに与えられた 述語、関数記号が整列されて
いる場合、論理式は有限列であるから、長さ n に関する帰納法で、おのおの
の n についての整列を定義することができ、これらの和が、論理式全体の整列
を与える。
51:１３２人目の素数さん
11/10/30 15:31:16.68
>>49
当り前だが、8 は別人だよ。それより 50 をよく勉強しなさい。
52:12
11/10/30 15:40:07.63
>>50
＞初めに与えられた 述語、関数記号が整列されている場合、
で、PAやZFCでは、述語、関数記号が整列されていることは
「よく知られている」のですか？
よく御存知とはおもいますが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
53:12
11/10/30 15:42:06.10
>>51
＞当り前だが、8 は別人だよ。
書いている当人にとっては当り前でしょうが
それ以外の人にとってはそうではないんですよ。
このことが、アスペルガー症候群の人には
理解しがたいといわれていますが。
54:12
11/10/30 15:45:32.98
>>51
＞50 をよく勉強しなさい。
>>50の前提条件である
「初めに与えられた 述語、関数記号が整列されている場合」
にはその通りでしょう。重要なのは上記の前提条件は
PAやZFCにおいて成立するのか？という点です。
>>52にも書きましたが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
55:１３２人目の素数さん
11/10/30 15:55:24.82
ZFC には定数記号はない。ε と = (述語記号か論理記号かは流儀による）
以外は変数記号と論理記号だけ。
PA の定数記号は 0 だけ。PA の関数記号は S だけ。
当たり前というのは、50 のようにすっきり書ける人と 8 のようにごてごて
書いている人の違いはわかるだろうという意味だが、52 のようなことを書いて
いる人にはわからないかもしれないね。
56:１３２人目の素数さん
11/10/30 16:03:46.11
54 のようなことを書いてあるので、変数記号についても書いておこう。
変数記号は、自然数によって番号付けられているから、整列されている。
もう少しついでに書いておこう。ゲーデル数を対応させて、有限列を自然数
に対応させることがわかれば、すべての文字列に自然数が対応し、これは単射
だから整列されていることは明らか。50に書いてあるのは、可算でなくても
整列されていればよいということ。
57:12
11/10/30 16:33:12.46
>>55
なるほど。定数記号に関しては明らかでした。
ところで>>8も引用は長いですが、
文章は三行なので「ごてごて」とは思えません。
したがってやはり自明とはいえません。
58:12
11/10/30 16:46:44.25
>>55-56
とはいえ、モデルの各元に対して、元々の理論の中に存在しない
定数記号を付加することが可能であるので、その場合、モデルの
濃度によっては、整列するために選択公理が必要でしょう。
59:12
11/10/30 16:54:58.46
>>58
＞ゲーデル数を対応させて、有限列を自然数に対応させることがわかれば、
＞すべての文字列に自然数が対応し、これは単射だから整列されていることは
＞明らか。
＞50に書いてあるのは、可算でなくても整列されていればよいということ。
自然数だから整列可能、といいたいようですが、それは自明ですか？
一階述語論理上で公理化された自然数論のモデルは範疇的ではありません。
当然、非標準的なモデルもありますよ。
60:１３２人目の素数さん
11/10/30 17:02:39.81
>>58 >>59
いい加減にしたらよい。44のようなことを書いたことが恥ずかしい
と思ったらどうかね。
自然数論のモデルというのなら、もちろん、整列できないモデルさえ
つくれる。しかし、今、完全性定理を証明しようとしているので、
そんなものが問題にならないのは明らかだ。要するに偉そうに、答え
たり、しているが、ちっともわかっていなかったということだ。
恥ずかしいと思うことを、初めにしたらよい。
61:１３２人目の素数さん
11/10/30 17:11:13.56
>>60
＞44のようなことを書いたことが恥ずかしいと思ったらどうかね。
あなたが41で「可算（濃度）モデルにおける完全性定理」
と書いていれば、そういうこともいえたであろうが・・・
＞自然数論のモデルというのなら、もちろん、
＞整列できないモデルさえ つくれる。
＞しかし、今、完全性定理を証明しようとしているので、
＞そんなものが問題にならないのは明らかだ。
完全性定理には、モデルの濃度の制限はない。
＞要するに偉そうに、答えたり、しているが、
＞ちっともわかっていなかったということだ。
「偉そうに」と思ったのは貴方の勝手。
あなたもモデルの濃度を全く考慮していなかった。
つまりわかっていなかった。
あなたは、わからないことは恥と思うのであれば
まず自分自身を恥じたらよい。
もっとも、そういう考え方は狂っている、と私は思うが。
62:１３２人目の素数さん
11/10/30 17:15:13.99
ところで、私には、41が完全性定理の前提から
選択公理を除こうとする理由が理解できない。
63:１３２人目の素数さん
11/10/30 17:30:18.48
ところで全くの脱線だが
>>60
＞いい加減にしたらよい。
＞恥ずかしいと思うことを、初めにしたらよい。
こんなおかしな喋り方をする
アニメのキャラクターでも
いるのかね？
64:42
11/10/30 17:48:15.19
>>46
>ではｆの定義が、再帰の定義に沿っているかどうか
>確認していただけますか？
IsTermの特性関数が再帰的関数になるか考えてましたが、やっぱりまだ分かりません。(直感では、IsTermが再帰的であること、計算可能であることは分かります。)
IsTerm(x)の定義の中に、m<xなるmに対して再びIsTerm(m)が出てきてるので、特性関数は原始帰納法によって一部定義されであろうことまでは分かるのですが、、、。
もしかして、IsTermの特性関数は累積帰納法で表しますか？
65:8
11/10/30 18:07:39.86
しばらく見ない間に議論が起きましたが
足りない部分について補足しますね＾＾；
>>29
ゲーデル数は全順序になるので、
整列可能定理が不要になるのです。
>>39>>49
私は形式化という言葉をかなり広い意味で使っています。
確かに誤解が多い書き方だったと思いますね。
>>64
再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。
定義からやり直すと煩雑すぎます。
66:15
11/10/30 18:22:01.69
>>41
論理式が整列されてるってことでなぜ救えるのかわかりませんね。
>>50
> これらの和が、論理式全体の整列を与える。
証明というものを具体的な対象物として見る場合、これはちょっと受け入れられない論法ですね。
>>60
> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
これは了解
>>61
> 完全性定理には、モデルの濃度の制限はない。
これは誤解していると思う。
67:8
11/10/30 18:49:24.69
>>66
だよな、そもそも1階論理の完全性の話してんのにな。
それにはじめてに論理式に識別番号つけて整列させてんなら
言語定義すんのに整列可能定理が必要ｗ
しわを伸ばしてみたら、しわの位置が変わっただけｗ
68:42
11/10/30 19:41:37.61
>>65
>再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。
定義しようとしている述語が、別の述語を使って定義されていれよいのですか、今考えているIsTerm は定義中に再びIsTermが現れているのが問題なのです。もっといえば、そうである以上原始帰納法を使って定義できるはずなのですが、それがなかなか分からないのです。
ちなみに今、考えているのは論理式ではなく形式化されていない算術の述語なのですが。
69:15
11/10/30 20:15:11.07
別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
「超越的な方法を認めなくても結果的に有効」であって欲しいのです。
70:１３２人目の素数さん
11/10/30 20:20:18.99
ところで42は
Proof(x,y):=yはゲーデル数xの論理式の証明である
が再帰的述語であることは理解していますか？
71:１３２人目の素数さん
11/10/30 20:21:54.46
訂正：証明である→証明のゲーデル数である
72:１３２人目の素数さん
11/10/30 20:37:40.00
>>69
よく分かりませんが、あなたのその願いがいつか叶うことを祈っておきます
73:42
11/10/30 20:43:22.86
>>70
再帰的になるということは、各文献で目にしていますが、確認はしていません。
なので、現在はproof(x,y)が本当に再帰的な述語であるかどうかを確認するため、これを構成する際に必要な諸々の述語を再帰的かどうか確認しています。
とまぁ、この過程で今「ゲーデル数xはPAの項である。」でどんづまっています。
74:１３２人目の素数さん
11/10/30 20:43:44.52
「超越的な方法」というのがWKLのことなら、
WKL が PRA 上の保存拡大だから「結果的に有効」なんじゃない？
75:１３２人目の素数さん
11/10/30 20:53:29.84
>>72
>>74
「超越的な方法」とはPRAそのものだろ。
76:１３２人目の素数さん
11/10/30 20:59:37.82
>>67 >>69
チミたちには難しすぎるようだが、選択公理が必要なのは、一般的な
設定の場合で、具体的なもの、例えば、PA, ZFC では論理式は、自然な
方法で整列できるのだよ。
77:１３２人目の素数さん
11/10/30 21:03:46.06
>>73
論理式Aが証明可能であるということの定義は
Aに至る論理式の有限列が存在して、その列の各項が公理か、以前の論理式から導かれること
というのは理解していますか？
もし、理解していればそれと同じような感じで
有限記号列Tが項である⇔
Tに至る有限記号列の有限列が存在して、……
と表せるのは理解できますか？
78:69
11/10/30 21:06:17.15
>>76
オレは別に「整列」とは言ってないが、お前ほんとに具体的なものについて語ってるか？
項、式、証明ってほんとに具体的なものなんだぞ？
79:１３２人目の素数さん
11/10/30 21:20:37.41
そもそも1階述語論理が
もろに対数学用述語論理だかんね
命題論理の完全性定理だけ考えりゃええんやないの？
それに論理体系を集合論で記述せにゃあかんこともないやろ
そもそも初期の頃は高階述語論理がスタンダードやて
その後に1階論理にしぼらな決定可能な完全性こしらえた証明体系つくれへんし
LS定理やらも意味もたへんさかい現状の1階論理さ注目されたんど
わいはエルブラン領域でスコーレム＝エルブランの完全性定理使っちくりゃ
-----エルブランは有限主義で選択公理嫌いでさかい信頼できんど------
ヘンキンさにペコペコ頭下げといて極大集合こしらえる必要もあらへんやろ
まぁ論理プログラミングさまさまやないけ
80:１３２人目の素数さん
11/10/30 21:31:31.69
まあもうちょっと真面目に書いていただければ助かるのですが・・・
81:１３２人目の素数さん
11/10/30 23:16:26.46
電線やハブや変圧器が電気メーカーにより製造される。
各家庭には様々な種類の電化製品が設置されている。
そしていくつかの発電施設が存在している。
例えば、あなたは今部屋の電灯を点けたとする。
このとき発電施設からいくつかの電線やハブや変圧器を
辿って行けばあなたの電灯に到達することは確実だ。
電灯が点けば真、発電施設が公理、ハブや変圧器が推論規則、
発電施設から電灯までの電線が証明だ。
電灯が点くなら、発電施設から電灯まで辿る電線がある。
これが完全性定理の内実である。
82:42
11/10/30 23:25:54.39
>>77
もととなるものと、それをもとにして生成する規則の二つがあればよいということでしょうか？
形式的体系でいえば、もととなるのは公理で、生成規則は推論規則になります。
項でいえば、0と変数がもとなるもので、Sと+と・が生成規則になると。
83:１３２人目の素数さん
11/10/30 23:36:10.57
>>82
はい、そういうことです
今、ビデオ見てるんで一旦落ちます
84:42
11/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:１３２人目の素数さん
11/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
11/10/31 01:03:17.00
>>85
レスありがとうございます。
仰ってることは(たぶん)分かっております。
私が知りたいのは、ではそれを具体的にどうやって再帰的関数(および述語)の形で表すのか、ということです。85さんの説明でいえば、MakeTermは、ではどうやって定義されるのでしょうか。おそらくMakeTerm の特性関数は原始帰納法の形、つまり
f(0)=g(x)
f(x+1)=h(x,f(x))
という形になると思うのですが、その具体的構成方法を知りたいのです。
これを定義するには、準備としていくつかの関数と述語を定義しないとだめだということは分かってますが。。。
87:１３２人目の素数さん
11/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:１３２人目の素数さん
11/10/31 01:26:58.78
>>87
すまん最後に ∧ Tn=T が抜けてた
89:１３２人目の素数さん
11/10/31 01:32:21.66
あと気になったが変数記号は定義に無かったか？
90:１３２人目の素数さん
11/10/31 01:52:22.65
あした早いんでもう寝ますzzzzz
91:42
11/10/31 02:08:52.15
それだと、Prove(x) (⇔ヨyproof(x,y) )が再帰的でないのと同様に、IsTerm (x)も再帰的でなくなってしまうような気がするのですが。
理解力がなく申し訳ないです。
身近に教えてくれる人がいればいいのですが、なにぶん独学なもので。。。
また明日しっかり考えてみようと思います。今日はご丁寧にありがとうございました。
92:42
11/10/31 03:50:15.46
結局まだうだうだ考えてたのですが、
累積帰納法で得られた関数は、再帰的関数である。
ということを証明できれば、私の疑問点は解決できることがわかりました。
93:１３２人目の素数さん
11/10/31 04:52:16.35
Foundations of Mathematics への入会ってどうすればいいのか誰かご存知ですか？
94:12
11/10/31 07:02:50.15
>>69
>別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
>完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
「普遍的に成り立つ」という言葉で、
どういうことを期待しているのか不明。
>「超越的な方法を認めなくても結果的に有効」であって欲しいのです。
モデル理論は超越的であると私は思いますが、
あなたは、なぜ、違うと思うのでしょうか？
95:12
11/10/31 07:05:41.79
>>76
>>58 の
＞モデルの各元に対して、元々の理論の中に存在しない定数記号を
＞付加することが可能であるので、その場合、モデルの濃度によっては、
＞整列するために選択公理が必要でしょう。
を理解できなかったようですが、付加はできないと思ってますか？
そう思う理由はなんですか？付加できるとは聞いていないからですか？
96:12
11/10/31 07:09:34.70
>>67
＞そもそも1階論理の完全性の話してんのにな。
だから「対象の個数は可算個でいい」と？なぜ？
97:8
11/10/31 08:12:47.78
>>96
＞> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
＞これは了解
いえここへのレスです。
98:１３２人目の素数さん
11/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
11/10/31 22:06:24.97
>>98
よくわかりました！！
今日一日中考えてやっと理解できました。
ありがとうございます。
100:１３２人目の素数さん
11/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:１３２人目の素数さん
11/11/01 00:04:23.72
>>94-96
どうもまわりくどい書き方だな。
モデル理論は超越的だとオレも思うし、違うなんて言ってないよ。
「普遍的に成り立つ」という言葉は普通の意味にとってくれ。
完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
AがTで妥当であり、T[￢A]もT[A]も矛盾していない、
実例を作れたらな。
102:１３２人目の素数さん
11/11/01 01:46:19.25
論理学の根本的な部分について質問させてください。
論理学では論理を形式化して考察していきますが、
メタな論理としてどこまでのレベルのものを許すのかということは考慮されるんでしょうか？
たとえば述語論理の体系では集合の概念を用いて理論が展開されますが、
より初等的な概念で展開することは可能でしょうか？
103:１３２人目の素数さん
11/11/01 03:21:57.74
>>102
考慮するときもある。
が、しかし、入門的な教科書ではそれは一旦脇に置いておく書き方をするのが普通。
もっと高度なことをやるときには考慮しないといけなくなるけれど、
そういうことをやる為にはまず脇に置いた議論をきちんと理解していることが前提となる。
104:１３２人目の素数さん
11/11/01 06:12:25.61
12,8 あるいは 15 という方たちは、ある程度の知識はお持ちのようだが、どう
もよくわかっていないようなので書いておこう。
述語論理の完全性という場合、述語論理をどう述べるかということがある。
述語記号、関数記号、定数記号が自然数で番号が付けられているかどうか？
あるいは順序数で番号付けられているかどうか？
次に完全性定理をどのように述べているかを調べる。例えば、無矛盾な公理
系に対してと書いてあるような場合、一般には、述語論理は、この公理系の
言語を含むものに拡大されていることになる。
これらのことが、完全性定理が選択公理と関係するかどうかの鍵である。
最初に書いた自然数で番号付けられた言語からはみ出なければ、選択公理
は不要なのだ。
105:１３２人目の素数さん
11/11/01 06:37:38.03
>>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。
それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？
106:12
11/11/01 07:19:22.56
>>69 >完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
>>94 >「普遍的に成り立つ」という言葉で、どういうことを期待しているのか不明。
>>101 >「普遍的に成り立つ」という言葉は普通の意味にとってくれ。
「普遍的に成り立つ」という言い方は普通しませんので
”普通の意味”というのは意味不明です。
107:12
11/11/01 07:21:40.31
>>101
＞完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
＞AがTで妥当であり、T[￢A]もT[A]も矛盾していない、実例を作れたらな。
「妥当」という言葉の定義は御存知ですか？
AがTで妥当であって、￢AもTで妥当である、という場合も存在しますよ。
108:12
11/11/01 07:27:06.40
>>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。
>>105
>それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
>その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？
104は、論理式の整列と選択公理の関係しか見ていないようだが、
別の点にも注目する必要がある。
モデルを構築する際に、無矛盾性（妥当性、充足可能性を
チェックしているが、述語論理の決定不能性定理からいえば、
無矛盾（妥当、充足可能）か否かを判定できるアルゴリズム
は存在しない。
109:１３２人目の素数さん
11/11/01 08:01:07.64
>>107
101ではないが、
T|=A⇔Tの任意のモデルにおいて、Aは真 ということだよな？
もし、T|=�魵だとしたら、Tの任意のモデルで�魵も真ということ。
ということは、Tの任意のモデルで、Aも�魵も真。こんなのってないよ、ありえないよ。
110:１３２人目の素数さん
11/11/01 13:00:33.75
>>98
定義の仕方、およびそれが再帰的になっていることはしっかり確認できました。ありがとうございます。
上から抑えるためのg(x)って具体的にはどんなものになりますか？
参考書には、g (x)=(p_len(x)＾2)＾x・len (x)＾2
とありましたが、どうしてこれが抑えるために十分なのかがわかりません。
111:１３２人目の素数さん
11/11/01 14:10:23.41
>>110
それはゲーデル数の定義によるから何ともいえんよ……
112:１３２人目の素数さん
11/11/01 21:39:34.80
普通の1階論理なら完全性は成り立つよ。
普遍的にね。
113:１３２人目の素数さん
11/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:１３２人目の素数さん
11/11/01 22:16:15.70
>>113
ミス
×そうすると列の長さnは2^len(x)以下である
○そうすると列の長さnはlen(x)^2以下である
115:１３２人目の素数さん
11/11/01 23:20:51.62
>>112
普通の1階論理ってなに？
関数や述語などが有限個であれば普通？
普遍的に成り立つって、追加の前提や仮定がまるっきり無用なの？
116:１３２人目の素数さん
11/11/01 23:42:31.83
>>69
普遍的において何を仮定しているのか不明ですけど、
そもそも述語論理での完全性定理は、
「ほとんどの証明体系で成り立たない」です。
例えば普通の真偽値では |＝￢A→(A→B) です。
証明体系を以下で定義します。
公理型 A→A
推論規則 MP
このとき |＝￢A→(A→B) ⇒ |-/-￢A→(A→B) です、何もできません。
つまり述語論理の中で完全な証明体系を探しているのであって、
述語論理は完全じゃないです。
本によってはLKの完全性定理とかNJの完全性とかちゃんと書いています。
117:１３２人目の素数さん
11/11/01 23:52:04.97
そういう話じゃないみたい
118:１３２人目の素数さん
11/11/02 00:01:10.42
HJは真偽値が3つないと完全にならなかったな。
119:12
11/11/02 07:08:29.92
>>109
>T|=A⇔Tの任意のモデルにおいて、Aは真 ということだよな？
ああ、妥当を充足可能と同義だと思っていたが、誤解だった。
その場合
「AがTで無矛盾」というのは
「AがTで充足可能」という意味で、
「AがTで妥当」とは違う。
120:12
11/11/02 07:12:22.84
>>112
>普通の1階論理なら完全性は成り立つよ。
>普遍的にね。
その場合の完全性は
「1階論理のどのモデルでも真な命題
（つまり1階論理で妥当な命題)なら
1階論理で証明可能」
という意味。
121:12
11/11/02 07:17:43.40
よく述語論理の完全性定理を
「述語論理の命題Pは、かならず
P自身かその否定￢Pのいずれか
が証明可能」
と思っている人がいるが誤り。
論理の完全性は、理論の完全性とは意味が異なる。
ところで
「無矛盾で完全な理論T、つまり、理論Tが、
命題Pかその否定￢Pのいずれかを必ず証明出来る
場合には、モデルが存在する」、
という命題はWKL0ではなくRCA0で証明可能。
122:８
11/11/02 08:13:31.03
>>117
>>69が訊きたいのはかなり原理的なレベルの話だと思うのです。
完全性定理は「数学に使える位まともな論理」だけで成り立つということです。
例の述語論理の決定不能定理も、Qが展開できる程度の証明体系に限定されますから。
ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
>>69が問題にしているのは可算な述語論理の言語の完全性定理の
RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。
123:１３２人目の素数さん
11/11/02 09:34:34.03
やはり逆数学という、基本的に後ろ向きの数学の一派の話なわけだ。
原理的というには、話をせまくしすぎている。
124:１３２人目の素数さん
11/11/02 09:38:20.21
>>123 ですね。
こういうものは、基本的に
公理の数をいくら減らせるか、という話なので、
大きな目標なり企みなりがあってこそのもので、
そうでなければ、スケールの小さなテーマに終わってしまう。
125:１３２人目の素数さん
11/11/02 13:20:55.22
比較的新刊のフランセーン『ゲーデルの定理』を中身見ないで注文しようかどうしようか
迷っているんだが、もう読んだ人どうよ？
126:１３２人目の素数さん
11/11/02 13:30:58.77
逆噴射数学
127:１３２人目の素数さん
11/11/02 19:16:02.80
>>125
基本的に読み物ね。
具体的な数学的内容は全くないです。
不完全性定理の社会的視点ですね。
新書のゲーデルの哲学とかのもう少し詳細なものですかね。
128:１３２人目の素数さん
11/11/02 19:22:46.29
>> 127
ありがとう。数学的内容がないということなのでやめときます。
（さっき訳者あとがきPDFを見たらそうでもないように見えたが）
129:あのこうちやんは始皇帝だった
11/11/02 19:29:37.64
＞＞１２８
お前、早く、社会人にならないと、取り返しがつかないことになるぞ！
130:１３２人目の素数さん
11/11/02 19:55:42.02
彼女にフェラチオさせてから寝るか・・
131:１３２人目の素数さん
11/11/02 20:03:02.10
>>128
数学的内容というのは語弊があった。
定義・定理・証明みたいな流れがないってこと。
不完全性定理の解説については岩波文庫の例の本の解説と同じレベル。
132:１３２人目の素数さん
11/11/02 20:51:55.88
>> 131
了解。ありがとう。
133:8
11/11/02 22:34:43.03
>>123
1派ではない、Simpsonの本しか読んだことない。
>>132
ただしゲーデルの定理とかいう本はまともな本。
「どんな体系で不完全が成り立つんだろ」
「決定不能とかって不完全性とどう関係してるんだろ」
「自己言及ってどんな種類があるんだろ」
みたいな疑問があったら読んでみるといいのでは？
既に不完全性定理を知っている人は
立ち読みか図書館で興味あるとこに目を通すだけで充分。
134:１３２人目の素数さん
11/11/03 00:25:00.08
逆数学が仮に分類だから狭いとしても、代数多様体の分類とおなじく、
分類を証明する手段が数学をゆたかにするっていうこともあるよね。
135:１３２人目の素数さん
11/11/03 01:52:39.31
逆数学が狭いといわれるのは、分類だからではなく、研究対象が二次的
であることにある。
136:１３２人目の素数さん
11/11/03 04:24:21.82
研究対象が二次的だと何故狭くなる？その二つがどう結びつくのか皆目見当が付かない。
137:8
11/11/03 06:36:37.24
逆数学は数学を計算クラスの視点から階層化している気がする。
例の2階算術の部分体系も様々なチューリングマシンで置き換えられるし。
純粋に好奇心をそそられる研究だと思うけど。
138:１３２人目の素数さん
11/11/03 08:44:09.19
>>137 重箱の隅とも言う。
139:１３２人目の素数さん
11/11/03 08:51:45.25
二次的であれば重要度が減る。
三次、４次、とつづく研究をするか？
ある定理を証明するのに、ある公理系が必要十分であることを証明できたら、
次に、そのメタ証明を証明するのに、必要十分な公理系を証明する、
そのメタメタ証明を、、、
あ、私は135とは別人ね
140:１３２人目の素数さん
11/11/03 08:52:33.58
>>122
>完全性定理は
>「数学に使える位まともな論理」
>だけで成り立つということです。
ん？集合論は数学には使えないトンデモ論理だといいたがってる？
もしかして8は有限主義者？クロネッカーの生まれ変わり？
141:１３２人目の素数さん
11/11/03 08:57:37.20
>>122
> ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
> >>69が問題にしているのは可算な述語論理の言語の完全性定理の
> RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。
言語を可算に制限しても、理論が完全でない場合、
RCA0ではダメだよ。
142:１３２人目の素数さん
11/11/03 09:08:24.32
>>135
>逆数学が狭いといわれるのは、
>･･･研究対象が二次的であることにある。
そもそも「二次的」という言葉を
どういう意味で用いているのか不明。
数学の成果を「一次的」として、
その数学の前提をどれほど弱められるかが
「二次的」だということか？
もしそうなら、別に狭いともつまらんとも思わんが。
143:１３２人目の素数さん
11/11/03 09:52:04.05
（フランセーン『ゲーデルの定理』は）
>定義・定理・証明みたいな流れがない
それ、「流れ」じゃなく「スタイル」だろ。
フランセーンの本は数学書ではないよ。
読者層は数学科の学生ではなく数学に興味をもつ一般人だから。
とはいえ、いい加減なものかといえば全然違うけどね。
むしろ、数学科を出た人間も目からウロコが落ちる話が沢山書いてある。
岩波文庫「不完全性定理」とはまた違った意味で読み応えがある。
144:１３２人目の素数さん
11/11/03 11:20:08.84
重箱の隅をつつくようなマイナーな研究は、私費でやるべき
145:8
11/11/03 12:41:34.25
>>140
いいたがっていない。
集合論がどういった証明体系の述語論理の上にあるのか
普通は明示されないが、おそらく完全な述語論理の上で
つくられているので問題なし。
>>141
理論の完全の所を詳しくお願いします。
146:１３２人目の素数さん
11/11/03 13:17:56.41
>>145
>>141は完全の意を取り違えてるだけだから質問しても無駄だろう
147:１３２人目の素数さん
11/11/03 14:23:15.33
>>145
＞集合論がどういった証明体系の述語論理の上にあるのか
＞普通は明示されないが、おそらく完全な述語論理の上で
＞つくられているので問題なし。
8のいう「完全」の定義とは？
148:１３２人目の素数さん
11/11/03 15:27:59.99
どんな図形が描画可能か、という問題がある。
使っていいのは定規とコンパスだけか？
それとも２次曲線は描けるとするか？
使える道具はいろいろ仮定できるが、それらを組み合わせて「実際に」描画するのは
具体的で有限なプロセスでなければならぬ。
149:１３２人目の素数さん
11/11/03 16:20:22.38
>>148
なにやら唐突な書き込みだが、
過去の書き込みへの返答なのか？
150:１３２人目の素数さん
11/11/03 16:26:05.53
fdg
151:１３２人目の素数さん
11/11/03 16:27:03.44
代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。
角の三等分は存在することが分かっているのに、作図できないことを示すのも二次的だ。
つまりガロア理論の金字塔的といわれる結果は重要度が低いのね。
152:150
11/11/03 16:31:17.57
間違えて書き込んでしまった...
ところで命題論理で￢、→、∧、∨だけでは
2値論理をすべて網羅することはできないみたいですね。
＝を付け加えてようやく16パターンが完成する。
153:１３２人目の素数さん
11/11/03 16:42:28.85
>>151
PAが不完全にもかかわらず、偽命題がPAで証明可能を意味する文を
PAの中で証明しようとしている。に対してはその理屈は成り立つ。
しかし逆数学が研究しているのは計算可能性の次数や算術や再起関数の階層であって、
今証明されている数学の定理をどれだけ少ない公理で証明できるかを研究しているわけではない。
154:１３２人目の素数さん
11/11/03 16:43:36.63
>>151
＞代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
＞わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。
逆数学の話なら、「代数的な解法を持つかどうか考える」
という理解が間違ってる。
代数的な解の存在が、いかなる前提によって証明されるのか
を考えている。
155:１３２人目の素数さん
11/11/03 16:49:48.77
ああ、151は
解の存在証明が一次的
解法の存在が二次的
といいたいわけね。
そういう意味でいうと、
無矛盾性の証明不能性は一次的
命題の決定不可能性は二次的
ってことかい？
156:１３２人目の素数さん
11/11/03 16:49:51.40
>>154 で、その代数解の存在を証明するのに必要な前提が証明できたら、
その次には、その証明のためにはどんな前提が必要なのか、考えるのですね。
わかりまつ
157:１３２人目の素数さん
11/11/03 16:51:13.61
それは逆数学が二次的だから重要でないのではなくて、
逆数学が逆数学だから重要でない、と言っているに等しいが。
二次的だから重要でないのなら同じく二次的な代数的解法の不存在も重要ではないことになる。
158:１３２人目の素数さん
11/11/03 16:51:33.32
数学では無く論理学ですね。
159:１３２人目の素数さん
11/11/03 16:53:44.43
>>156
ん？「代数解の存在を証明するのに必要な前提」は証明しないよ。
ミュンヒハウゼン（あるいはアグリッパ）のトリレンマって知ってる？
全ての命題に証明を求めるなら無限背進か循環論法に陥る。
独断は排除できないよ。
160:１３２人目の素数さん
11/11/03 16:57:21.32
ガロア理論にとって、代数解の存在云々は
理論のごく一部です。数の演算に関する本質的洞察を
含み、数学全土に応用があります。
本当にガロア理論勉強した事あります？
161:１３２人目の素数さん
11/11/03 17:00:11.57
>>157
「それ」とは>>153のコメント？
「計算可能性の次数や算術や再帰関数の階層」は一つの尺度に過ぎない。
例えばRCA0とWKL0の違いは何なのか、理解しないのなら意味がない。
二次的かどうかが問題なわけではないだろう。
代数的解法の存在も、代数的解法による解の意味が重要。
162:１３２人目の素数さん
11/11/03 17:00:32.02
>>159 そういう意味じゃ無い
163:１３２人目の素数さん
11/11/03 17:04:21.38
>>160
＞数の演算に関する本質的洞察
では、ガロア理論によって明らかになった、
「数の演算の本質」とはズバリ何？
あなた本当にガロア理論理解できてます？
教科書の記述を丸ごと記憶するのは勉強と違うよ。
164:１３２人目の素数さん
11/11/03 17:05:03.23
>>162 ではどういう意味？
165:１３２人目の素数さん
11/11/03 17:07:07.82
>>163 あなたはガロア理論理解してますか？Yes or No?
166:153
11/11/03 17:14:05.37
RCA0とWKL0の違いはチューリングマシンの違いですね。
確かに次数やクラスは1つの視点ですね。
167:１３２人目の素数さん
11/11/03 17:22:16.38
>>166
具体的に説明されたい。
168:8
11/11/03 19:15:30.11
>>152
複雑だけど￢と→だけできる。
￢(A→￢B)
￢(A→B)
￢(￢A→￢B)
￢(￢A→B)
の4つで1パターンで真になる命題が網羅できるので、
これの否定で3パターン真で命題が網羅できて、
4つの内2つを組み合わせて2パターンで真になる命題を網羅する。
4つ全部を組み合わせて恒真、その否定で偽をつくる。
これで16パターンが網羅できる。
169:１３２人目の素数さん
11/11/03 19:49:36.91
>>148
証明可能性を描画可能性になぞらえているのか？
コッホ曲線をどうやって描画する？
170:１３２人目の素数さん
11/11/03 20:22:00.87
>>163 まぁ、簡単にいうと、ガロア理論の
本質とは、
ある集合の構造を調べるときに、その集合を直接調べるのではなく、
その集合からその集合への写像の族を考え、
その族の構造を調べることが有効である。
ということ。それ以降の数学のあらゆる所で出てくる重要な考え。
171:１３２人目の素数さん
11/11/03 21:16:48.67
>>170
わざわざガロア理論とか数の演算の本質とかいうから
実に高尚極まりない整数論の奥義を語るかと思えば
数学のどこでもでてくるヌルい一般論じゃんｗ
172:１３２人目の素数さん
11/11/03 21:22:30.85
>>171
>>151が、ガロア理論を誤解して過小評価していたので、
ガロア理論の本質論が出たまで。
そう、今ではいたるところに普及した
重要な考え。
173:１３２人目の素数さん
11/11/03 21:36:59.04
>>172
ガロア理論の本質でもなんでもない。
例えば、ガロア理論→幾何学、集合→空間、写像→変換と置き換え
「幾何学の本質とは
空間の構造を調べるのに、空間を直接調べるのではなく
空間から空間への変換の族を考え、
その族の構造を調べることが有効だということ」
といっても通じてしまう。
こんなヌルイ一般論を重要というのは・・・馬鹿ｗ
174:１３２人目の素数さん
11/11/03 21:37:49.72
>>168
その4つの式の最初に￢をつける意味は？
175:１３２人目の素数さん
11/11/03 21:46:35.36
>>174
￢(A→￢B)＝A&B
￢(A→B)＝A＆￢B
￢(￢A→￢B)＝￢A&B
￢(￢A→B)＝￢A&￢B
と思われ。
176:１３２人目の素数さん
11/11/03 21:50:53.37
以前ツイッターで
「複素数は本来、数じゃ無い！」
とわめいていた数学者(？)がいた。
実数ではなく複素数、というところが素人っぽくて面白い。
どうも、全順序集合でないと、本来の数ではないらしいｗ
177:１３２人目の素数さん
11/11/03 21:55:30.41
角度の値は、実数ではなく円周群の要素と考えたほうがいい。
円周群の要素を数と呼ばないのは、どう言い訳しても手抜かりである。
178:8
11/11/03 22:03:22.17
>>174ない。
179:１３２人目の素数さん
11/11/03 22:04:44.77
辞書的順序入れれば複素数も全順序になるよ
180:８
11/11/03 23:21:16.14
￢と∧∨は1つの述語にまとめられる。
A○Bを￢(A∧B)、
A◎Bを￢(A∨B)で定義すれば
どちらも2項述語1つだけで真理値表をすべて満たす。
A○Bの否定が(A○B)○(A○B)になったりする。
代数の演算を考えれば自明だが。
181:１３２人目の素数さん
11/11/03 23:21:35.62
>173
ガロア理論の重要なところの一つはその一般化できる構造なんじゃないの？
ガロア理論の説明で良く幾何学の証明不可能性の話が出てくるから
そうなんだと思ってたけど。
182:１３２人目の素数さん
11/11/04 04:35:29.49
>>160
ほんじゃガロア理論のごく一部であるところの
代数解の不存在云々（アーベルの定理？）は
二次的なので重要でないってことでおk?
つーか、ガロア理論の一部とか思ってるの？
一部ではなくて、単に金字塔的な応用例ってだけだろｗ
君こそ勉強しなおしてきたらどうだい？
183:１３２人目の素数さん
11/11/04 05:04:11.68
>>176
実数ってのがそもそも「数」ではない。実数で表されるものは「量」だ。
従って「数学」という名称は名が体を表していない。「量学」と改称すべきである。
184:１３２人目の素数さん
11/11/04 06:36:50.32
>>183
量と数と実数の関係をはっきり述べないと議論にならない
185:１３２人目の素数さん
11/11/04 07:13:03.86
>>184
こんな定義だそうだ：
ｽﾚﾘﾝｸ(math板:21番)
186:１３２人目の素数さん
11/11/04 08:02:31.27
>>185
要するに
離散量＝自然数＝真の数
連続量＝実数＝数でない
といいたいわけか。
なんか窮屈だな。
窮屈を好むのはやっぱ精神異常？
187:１３２人目の素数さん
11/11/04 08:04:26.33
なんでもかんでも数と呼んだらええんちゃうｗ
自然数も有理数も実数も複素数も四元数も数。
それどころかベクトル空間の元も数。だから関数も数。
ええい、もう、集合も数とよんだらええがなｗ
188:１３２人目の素数さん
11/11/04 08:13:49.78
人数とか個数とはいうけど、水数とは言わないだろ、水量だ。
つまり日本語の「数」は、本来連続量には使われない。
連続量である実数に「数」とつけるのはテクニカルタームでだけだ。
189:１３２人目の素数さん
11/11/04 08:14:59.70
いま思ったが、数学で扱うものはみな集合だから
数学は集合論だってことだなｗ。
ということで、数学板を集合論板に改名すべしｗ
190:１３２人目の素数さん
11/11/04 08:18:33.42
>>188
もうええよ、数学も量学もせますぎ。
今の数学は全て集合論だからｗ
♪これも集合、あれも集合
たぶん集合、きっと集合
191:１３２人目の素数さん
11/11/04 08:23:09.84
>>190
というと、圏論ヲタから
「圏の重要性を全く無視している！」
といわれそうだな。
それなら、まあ、圏論の立場も立てて
数学板を集合論・圏論板に変えるのはどうだ？ｗ
192:１３２人目の素数さん
11/11/04 09:27:38.04
>>181 ガロア理論の胆は、
集合(体)の構造を調べたい時に、
その集合上の写像の族(変換群)の
族としての構造(群構造)を調べるという所。
個々の写像が具体的にどの元をどの元に
移すかどうかは忘れて、写像の族が織り成す
性質(群としての性質)を調べるという所。
ここに既に圏論の考えがある。
193:１３２人目の素数さん
11/11/04 09:59:33.66
上がガロア理論の本質だけど、
代数方程式に絡めて、もう少し詳しく書く。
有理数係数代数方程式に代数解があるということは、
有理数体に解を付加した体が、
有理数体に1の冪根を付加した体の
部分体になっていること。(本当は嘘だが遠くない)
だから、ある体はある体を部分体をもつか？
という問題になる。
体上の(自然な)変換群を考えると、
部分体と部分変換群との間に自然な対応がつく。
(ここがガロア理論の胆。以下は代数的な話)
有理数体に冪根を添加したという特別な体に対し、その体の変換群は、冪根の性質からある制約をうける。その制約は、部分変換群へも伝播し、対応する部分体へも伝播する。
この部分体が、有理数体に代数方程式の解を添加した体なら、その制約は、
その代数方程式へも伝播する。
五次以上の代数方程式では、この制約を外れるものが出る。
こういうシナリオです。
194:１３２人目の素数さん
11/11/04 20:05:57.67
逆数学が二次的って言われるのは、
ある定理や理論にどの公理がどの程度本質的に効いてくるのか
ってことが分かるってのがメインで、基本的にはそれ自体から
数学のレベルで新しい定理が出てくるってわけじゃない
（メタレベルで数学がより分かるようになるだけ）って意味じゃねーの？
195:１３２人目の素数さん
11/11/04 21:07:21.61
でも、再帰的に逆数学の定理も素材になるじゃん。
196:１３２人目の素数さん
11/11/04 21:48:52.44
>>195
逆数学が逆数学自体を研究対象にしたところで、それが数学からみて
二次的な存在であることは変わらない（というかむしろ三次的存在になってしまう）
のではないの？
197:１３２人目の素数さん
11/11/04 21:53:55.21
>>194
そういうことを言いたいのであれば、最初からそう言えばいい。
例のアホは、そんな詳しいことは言ってない。
「逆数学は二次的だ」としか言ってない。だから
A：じゃあガロア理論も二次的だな。
B：何を言うか。お前はガロア理論を分かってない。
とかいうワケの分からない方向に進むのだ。Aが言っていることは
「お前の言う いい加減な "二次的" に従えば、ガロア理論だって
二次的になってしまうぞ。それでいいのか？」
ということである。すなわち、Aの発言の本質は
「 "二次的" とは何なのか詳しく説明しろ 」
ということであり、Aが問題にしているのは "二次的" の定義である。
従って、A自身はガロア理論のことを "二次的" だとは思ってない。
Aは、"二次的" という内容を皮肉っているだけである。
実際、>>151の書き方は明らかにこのような意図に読める。
よって、Bのような返答は見当違いであり、正しい返答の仕方は
「 いや、二次的とはこういう意味だ。ガロア理論はこの意味で二次的では無い 」
というものでなければならない。"二次的" の定義に触れない返答は意味が無く、
話がこじれるだけである。
198:１３２人目の素数さん
11/11/04 21:57:25.73
要するに>>197は話にならんレベルのアホってことか。了解した。
199:１３２人目の素数さん
11/11/04 21:59:57.78
答えられないから逃げるね
まで読んだ
200:１３２人目の素数さん
11/11/04 22:02:01.64
>>198
いくら煽っても、例のアホが何も言ってないことには変わらない。
今の段階で分かっていることは
・例のアホ本人による、「逆数学は二次的だ」の説明が未だに無い。何も言ってないのと同じ。
・別人である>>194による、「二次的だ」の見解は登場している。
ということにすぎない。
201:１３２人目の素数さん
11/11/04 22:06:55.85
まあいくら誤魔化したところで、そんなつまらないことをいつまでも愚痴愚痴ネチョネチョやってるアホが
一人居るってことはずっと変わらんということにすぎない。
202:１３２人目の素数さん
11/11/04 22:24:51.74
まあ、いくら つぶやいたところで、例のアホが何も言ってないことには変わらない。
圏論スレのころから内容が全く無い。
203:１３２人目の素数さん
11/11/04 22:29:58.48
ガロア理論に先行する圏論の萌芽はないの？
204:１３２人目の素数さん
11/11/04 22:47:08.09
>>197 他人に日常用語の定義定義とうるさくて、
当の本人は何も定義しないし、何も主張しない。
他人の話にケチつけてれば自分の立場が
崩れないと考えている。完全なアホ。
自分がアホ出ないことを主張してみな。
205:１３２人目の素数さん
11/11/04 22:52:44.88
アホ本人を納得させるつもりで書いてないから。
第三者(特に若者)がみてこっちに分がありそうだと
思ってくれればそれでじゅうぶん。
206:１３２人目の素数さん
11/11/04 23:08:22.36
>>205
君には分がないよ。
よく考えればわかるので説明はしない。
207:１３２人目の素数さん
11/11/04 23:29:45.39
あ、言っとくが、二次的という言葉で
逆数学を最初に批判したのは私じゃない。
でも充分私には言いたいことは伝わった。
私は彼に分があると思った
208:１３２人目の素数さん
11/11/05 01:19:12.75
>>194
代数的解法があるかどうかはメタレベルではなく数学の問題だと？
ある定理や理論にどの公理がどの程度本質的に効いてくるのかは二次的で
ある解を求めるのにどういう手法（代数的か超越的か）が本質的に必要かは一次的なのか？
随分と恣意的な境界線だこと。というか逆数学を二次的にするための定義だな。
「二次的とは逆数学のようであること」と言っているのと大差ない。
209:１３２人目の素数さん
11/11/05 02:09:51.06
二次的だと狭いってのも意味不明だな
210:１３２人目の素数さん
11/11/05 02:16:07.40
ﾁｮｲｽしてはいけない公理をﾁｮｲｽするから球分割の矛盾が生じるのだ
211:１３２人目の素数さん
11/11/05 03:16:55.47
ちゅうか、「方程式を代数的に解く」ってのは数学の話で、
連続体仮説を公理に入れるか入れないかはメタ数学の話で、
重力を含む超統一理論があるかどうかってのは物理学の話で、
……etc.
って中で、数学のレベルでの話以外は数学にとっては二次的三次的なもんだろ。
どんだけ頭沸いてるんだか。
212:１３２人目の素数さん
11/11/05 03:23:28.11
で、その「数学のレベル」ってのはなんなんですかね。
213:１３２人目の素数さん
11/11/05 03:35:16.66
>>211
それって「逆数学は重要でないから重要でない」とか言っているのと同じだから。
真面目に議論する気がないなら出て行ってね。
214:１３２人目の素数さん
11/11/05 03:38:54.08
>>213
逆数学は逆数学で、
逆数学からすれば数学も物理も国文学も等しく二次的三次的だ
と言っているのに、君こそまじめに話する気がはじめからないんだろ？
215:１３２人目の素数さん
11/11/05 03:41:12.51
つか、>>214は二次的＝重要でないとか、言ってるも同然なんだが、
んなわけないだろ、ドンだけ頭悪いんだこの阿呆は
216:１３２人目の素数さん
11/11/05 03:42:03.55
おっと、滑った。
つか、>>213は二次的＝重要でないとか、言ってるも同然なんだが、
んなわけないだろ、ドンだけ頭悪いんだこの阿呆は
217:１３２人目の素数さん
11/11/05 04:13:40.16
URLﾘﾝｸ(dictionary.goo.ne.jp)
にじ‐てき【二次的】
［形動］主となる物事に対して、それに付随する関係にあるさま。また、ある物事から派生したもので、それほど重要でないさま。副次的。「―な災害」「―な問題」
218:１３２人目の素数さん
11/11/05 04:18:53.04
１．主となる物事に対して、それに付随する関係にあるさま。
２．また、ある物事から派生したもので、それほど重要でないさま。
３、副次的。
ってのは意味が並立なわけだが。
219:１３２人目の素数さん
11/11/05 04:19:44.54
辞書も読めないとか、やっぱり幼稚園児並の脳みその持ち主だったｗ
220:１３２人目の素数さん
11/11/05 04:21:54.87
逆数学は二次的 と最初に言ったのは>>135
二次的＝狭い と最初に言ったのも>>135
二次的＝重要度が減る と最初に言ったのは>>139
>>135にとっては、逆数学は二次的で、狭い
>>139にとっては、逆数学は二次的で、重要度が減る
二次的だとなぜ重要度が減るのか、あるいは、
二次的だとなぜ重要でないのか、そのことに答えたレスはまだない
二次的だとなぜ狭いのか、そのことに答えたレスもまだない
とりあえず、スレを見渡す限りは、二次的だと重要でないという考え方は
マイナーのようである
221:１３２人目の素数さん
11/11/05 04:24:29.24
並列なら「二次的＝重要でない」も正しい解釈の一つ。
従ってそれを「んなわけないだろ」と言っている奴こそ辞書が読めないんだな
222:１３２人目の素数さん
11/11/05 04:26:00.30
いや、>>217で答えは出ていたか
そうか、最初から重要でない意味が含まれているのか
223:１３２人目の素数さん
11/11/05 04:27:53.94
ワロタ藁ｗ
224:１３２人目の素数さん
11/11/05 05:05:00.64
>>221
並立なんだから、他の意味で言っている場合を完全無視して
「二次的＝重要でない」と言ってると主張するのは、
幼稚園児にも笑われるレベルの阿呆だ。
225:１３２人目の素数さん
11/11/05 05:09:13.82
正しい解釈の一つである可能性を無視して
「んなわけないだろ」だろと全面否定した人間は
幼稚園児に笑われるレベルだろ
226:１３２人目の素数さん
11/11/05 05:14:54.56
並列に複数の意味がある言葉は、文脈によって最も適切な意味で解釈するべきであろう。
しかるに139が「二次的であれば重要度が減る。」と述べている。
更に逆数学批判派は同語反復的な主張が多数であった。
かような文脈において、二次的＝重要でない、という解釈は
139の発言をまさに同語反復とするものであり、
この文脈において最も適切な「二次的」の解釈であると考えられるのである。
227:１３２人目の素数さん
11/11/05 05:17:26.03
というか、俺も逆数学は数学にとって二次的だというレスをしているが、
全く逆数学批判派ではないぞ。そこまで興味を持っても居ないが。
228:１３２人目の素数さん
11/11/05 05:18:16.08
重要度が減ると重要でないをイコールで結ぶのはさすがに赤ん坊以下だよ。
229:１３２人目の素数さん
11/11/05 05:32:12.01
逆数学が副次的なものでないという主張の意味が分からん。
230:１３２人目の素数さん
11/11/05 05:47:21.72
>>228
お、辞書の読み方では勝ち目がないと悟って論点のすり替え？
しかし残念だが>>226の主張は「重要度が減る」と「重要でない」の同値は必要ない。
後者から前者への implication さえあればいい。
231:１３２人目の素数さん
11/11/05 08:01:47.04
俺は逆数学は、二次的だとは思わんな。寧ろ根本的だろう。
例えばRCA0とWKL0の違いが明らかになったのは面白い。
前者は明らかに構成的だが、後者は何らかの超越的な仮定がある。
こういうことに対して何の面白みも感じない人は
数学的感覚が鈍磨しているといっていい。
232:１３２人目の素数さん
11/11/05 09:09:38.10
>>231 それって単なる盆栽趣味。ないしはスケールが小さい。
ないしはスケールの大きな数学を知らない
233:１３２人目の素数さん
11/11/05 10:21:18.06
>>232 スケールの大きいことをやりたがる人は
数学なんかやらないｗ
微細構造を好む人がやるのが数学。
234:１３２人目の素数さん
11/11/05 10:28:58.83
計算理論の壮大さを知らんようだな。
全数学を包括しかき回すほどの規模。
21世紀の主流は計算論＋理論計算機＋集合論
235:１３２人目の素数さん
11/11/05 10:35:20.73
>>234
別に壮大だとは思わない。
そもそも壮大だからスゲーとはおもわんし。
なにかといえば大きさを求める奴は
きっと●ん●んが小さいんだろうｗ
いっとくけど、♀の＊＊＊は鈍感だから
入れたって正確な大きさなんかわかりゃ
せんってｗ
236:１３２人目の素数さん
11/11/05 12:13:54.61
逆数学が2次的ってｗ
本来逆数学のような計算論の視点が1次的で、
これまでの数学が2次的なものなのだが。
ユークリド言論が1次的で非ユークリッドが2次とか言っているようなものw
237:１３２人目の素数さん
11/11/05 12:18:44.87
>> 234
これ興味あるからもうすこし聞かせて。
オレは、本当にそうであればよいと思う者だが、今の計算論や理論計算機にそんな兆候があるか？
何あるいは何処がその兆候だと思うんだ？
238:１３２人目の素数さん
11/11/05 12:23:15.54
>232
無限と同じぐらいの深淵じゃないの？
可算数と非可算数の境界の話だよね？
239:１３２人目の素数さん
11/11/05 13:58:14.73
>>236
逆数学にとって数学が二次的な対象でしかないことは誰も否定して無いと思うが。
240:１３２人目の素数さん
11/11/05 14:49:37.41
>>239
逆数学は、直接、数学の成果を得る活動ではないが
その結果が、数学でないかといえば、そんなことはないから
結局、フツウの数学と変わるところはない。
241:１３２人目の素数さん
11/11/05 17:17:43.15
逆数学の井の中の「数学」を大海の数学と称する腹か。
自分で「フツウの数学」と区別しておいてそれは詭弁ではあるまいか。
242:１３２人目の素数さん
11/11/05 17:25:08.36
>>241
要は対象の選び方の違いにすぎない。
こんなことに難癖をつける奴は●違いだろう。
243:１３２人目の素数さん
11/11/05 19:00:04.00
>>243
述語論理ですが、
言語Lってのは
論理的述語記号∧、∨、￢、→、∀、∃
変数記号x1、x2、x3、...
関数変数記号F1、F2、F3、...
述語変数記号R1、R2、R3、...
の記号の組合せの事ですよね。
この記号の組合せの総数、つまり2^Lの中で、
変数記号、引数に項をとる関数の形をしたものが項ですよね。
項の集まりをTermとすればTerm⊆2^Lになりますよね。
引数に項をとる述語と、述語を引数にとる論理的述語が論理式ですよね。
論理式の集まりをFlmとすればFlm⊆2^L。
244:１３２人目の素数さん
11/11/05 20:50:08.36
LによってTermやFlmが規定されることから、
これらをTerm(L)やFlm(L)と書き換えよう。
M(L)という対が＜M,Pri,Fnc,m,v＞と定義される。
Mは集合。
Priは定義域がMを動く述語の集合。
Fncは定義域・値域がMを動く関数の集合。
mは定義域が定数記号ならば値域がM、
定義域が述語定数記号ならば値域がPri、
定義域が関数定数記号ならば値域がFnc、
となる全単射関数。
vはFlm(L)から{0,1}への関数。
さてここまで来れば私の主張したい内容が想像つくだろう。
つまり、「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」
245:１３２人目の素数さん
11/11/05 21:23:51.57
>>244
＞「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」
上記の文章は理解できない。
もし、
「論理記号によって書かれた述語だけを
述語として認めるのはおかしいだろう？」
といいたいのであれば、全くその通りである。
実は一階述語論理と二階述語論理の違いはそこにある。
一階述語論理では、論理式として書けるものしか拘束できない。
しかしながら、二階述語論理では、述語全体を束縛する演算子
として∀、∃を用いることができる。
246:１３２人目の素数さん
11/11/05 21:33:28.20
>>241 ははは。
基礎論って、妖怪人間ならぬ妖怪数学みたいなものか？
普通の人間や数学は、日夜、立派な人間や立派な数学になりたいと
切磋琢磨しているのに、
普通の人間か数学になりたい、それで充分だからならせてくれと。
247:１３２人目の素数さん
11/11/05 22:09:00.71
さて、途中まで書いていたのだが以下続き。
論理的述語記号は通常、
A B A∧B
------------
1 1 1
1 0 0
0 1 0
0 0 0
のような真理値が定義されているのだが、
これはいささか早計ではないだろうか。
これが前提となるのは非常に不快である。
そこで論理的述語記号を関数や述語と同様に、
論理的述語変数と論理的述語定数に分離して考えてはどうだろうか。
つまり論理的述語記号∧、∨、￢、→、∀、∃ を
論理的述語変数L1、L2、L3、...
にすげ替えてしまうのである。
同時に論理式の定義を以下のように拡張する。
・引数に項をとる述語。
・引数に引数に述語か論理的述語をとる論理的述語。
248:１３２人目の素数さん
11/11/05 22:27:27.03
>>211
同意。
逆数学や基礎論と数学は別物。
別物なんだから、価値観が違う。
基礎論にとっては、代数方程式論より逆数学のほうが重要かもしれないが、
数学にとっては、代数方程式論の方がはるかに大事。
価値観が違うんだから、はっきり分けるべき。
数学は数学。論理学は論理学。
刃物をつかっているという点では同じでも、
サムライと板前くらい違う。目的も価値観も違う。
249:１３２人目の素数さん
11/11/05 22:32:31.65
>>245
まったくそのとおりである、私はさらにその考えを推し進めようとしている。
注意すべきは論理的述語は引数に直接項をとることができない。
これは既存の1階述語論理と同様である。
（いや、∀と∃の存在保証が失われた今、1階というのは意味をなさない言い方か。）
さて、今述語論理の言語は以下の述語を持つ。
論理的述語変数 L0、L1、L2、...
論理的述語定数 -
非論理的述語変数 R1、R2、R3...
非論理的述語定数 -
ここで論理式の定義と比較したとき、ある事実に気が付くだろう。
論理式の非論理的述語は引数に項をとる。
論理式の論理的述語は引数に非論理的述語と論理的述語をとる。
つまり項で非論理的述語の真偽が決まり、非論理的述語で論理的述語の真偽が決定する。
250:１３２人目の素数さん
11/11/05 22:54:57.82
非論理的述語を1階の述語、
論理的述語を2階の述語と考えると、
当然3階4階...n階と階層化をすすめたくなる。
重要なのは、n階の述語は引数にn階以下の述語をとるということ。
そして1階だけが極小の述語となり、引数に項しかとれない。
述語はどの階層でも真偽が決定するが、項は単独では真偽決定できない。
251:１３２人目の素数さん
11/11/05 23:29:23.60
さて、構造の側はどうするかというと、
{Pri_n(L)}n∊N とでもして述語を階層ごとに分けとけばよいだけだ。
さて言語Lの論理式は今や以下の定義となる。
・項を引数に持つ1階述語。
・n階以下の述語を引数に持つn階述語。ただしn≧2。
こうすると構造の側はどのように真偽を判定するのか。
なおn階の述語すべてのアリティの個数制限をなくす。
252:１３２人目の素数さん
11/11/05 23:45:50.00
なお真偽値をいくつにしても構わないし、
どういった場合においてもここまで一般化された
言語では任意の証明体系で完全性定理が成り立つ。
というより論理記号がないため恒真が意味をなさない。
こう考えると1階述語論理とは、
述語が2階までで、
2階の述語定数記号が各アリティ2の∧、∨、￢、→、∀、∃ である。
ここで通常の1階論理と同じような真理値を2階の述語に与えれば良い。
（勿論構造の側の解釈を与える全単射の関数mもn階分に対応している。）
また、高階述語論理や様相論理も自由に展開できることを確かめたれたい。
了
253:１３２人目の素数さん
11/11/06 02:12:56.62
話をバッサリ切ってごめんけど、なんでこんなに難しい文章で説明しようとするの？
254:１３２人目の素数さん
11/11/06 02:14:56.35
バカだから
255:１３２人目の素数さん
11/11/06 02:18:17.96
ロボットに説明するわけじゃあるまいし。
何で数学の証明とか解説ってやたら難しい事書くんだろう。人間が人間に説明するんだから(ry
256:１３２人目の素数さん
11/11/06 03:51:17.42
>>255
解釈の方法を限定するためじゃね。
自然言語で意味が一意になるように書くと、更に長くなるよ。
試しに選択公理を論理式と自然言語で書いて見比べてみたら。
257:１３２人目の素数さん
11/11/06 07:15:28.38
難しいと言うか
普通の教科書の書き方をパロッてるんだろう
258:１３２人目の素数さん
11/11/06 08:11:19.75
>>248
何がいいたいのか意味不明。
そもそも代数方程式でも解の存在が大事だという人と
解の性質が大事だという人がいるだろう。
数学の中で分野わけすればいいだけのこと。
整数論至上主義者は、整数論のために
関数解析を「数学ではない」といって
切るつもりか？
259:１３２人目の素数さん
11/11/06 08:18:45.68
>>249-252
ゲーデルのLを知らんのか？
あれはまさに無限階論理といってもいいわけだが。
しかし、全ての階をいっしょくたにできるような
最上階というものは存在しない。
260:１３２人目の素数さん
11/11/06 08:53:31.44
さて、いよいよ本論に入ろう。
前回、真偽の決定可能な論理式は1階以上の述語とした。
一方でn階の述語はそれ以下の階層の述語を引数にとるとした。
ここで項も論理式に加えてしまうのが合理的だと思わないだろうか。
また2階以上の階層の真偽が同様に決定するのも不自然だ。
はじめてに論理式の定義を以下のように書き換える。
・従来の変数は0階の論理式である。
・従来の関数は1階の論理式である。
・従来の述語は2階の論理式である。
・従来の論理的述語は3階の論理式である。
さらに
・n階の論理式はそれ以下の論理式を引数に持つ。
ここで問題が発生する。f(x)∧y、a＜(b＜c) のようなものが発生する。
これは容易に解決する。
261:１３２人目の素数さん
11/11/06 09:41:26.91
>>259
ある段階で導入する可能性もある。
かつて関数vは論理式と真理値を関連付けていた。
これは解釈という考え方で一般化することが可能である。
例えば、従来のx＜y∧y＜zという論理式を考える。
x＜y∧y＜zの真理値は、x＜yとy＜zの真理値によって決定する。
ここでx＜y∧y＜zの真理値とx＜yとy＜zの真理値は実は違うものだと考える。
そして真理値というよりは、例えば集合{t0,t1}を値が動くと考える。
一方f(x)やg(y)は構造の領域Mを動いている。
3階以上の述語も同様にふるまう。
ここで各階の論理式は解釈により集合へ対応付けられる。
各階の論理式に対応する集合は、M0、M1、M2、...とでも定義しておけばよい。
例えばPAの標準モデルは、
M0＝N、M1＝N、M2＝{0,1}、M3＝{0,1}となるだろう。
ここで先ほどのf(x)∧y、a＜(b＜c)。
f(x)∧yだが、f(x)はM1、yはM0に対応付けられる。
∧は{t0,t1}に対応付けられている。
ここで∧を解釈する関数の定義域が{t0,t1}だけならば、
それ以外の不正な値を定義不能としてはじくことが出来る。
つまり、f(x)∧y、a＜(b＜c)などは決定不能になる。
もちろんM0＝M1＝M2＝...と定義することで
意図的に関数値や定義域を混同させることも可能だ。
つまり完全性定理での論理式が、決定可能な論理式に制限されるだけだ。
262:１３２人目の素数さん
11/11/06 09:55:54.14
ところで真理が真偽2択から解放された今、
モデルの定義も変えねばなるまい。
矛盾許容論理などを考えればモデルとは、
ある言語のすべての論理式を定義可能な領域を持つ構造。
これにより先ほどの完全性定理は再び従来通りの論理式に対するものとなる。
263:１３２人目の素数さん
11/11/06 10:06:41.41
>>260、261
お前アホか。全部既知のことを今頃お勉強が終わったということ。
それからn階なんて言っている時点で古過ぎ。循環だってあるんだから。
264:１３２人目の素数さん
11/11/06 10:34:01.28
>>263
ご立腹かね？ワトソンくん！
265:１３２人目の素数さん
11/11/06 16:26:20.00
流れをぶった切って。
物理なんかの測定から理論を抽出するところに逆数学的なものを感じるんだけど、
逆数学にそういった応用例とかないのかしらん？
266:１３２人目の素数さん
11/11/06 16:43:51.03
>>243-244 >>247 >>249-252 >>260-261
トンデモ？
267:１３２人目の素数さん
11/11/06 17:16:49.63
>>266
すでに知られていることを独自の発想のように書いてるスレ潰し
268:１３２人目の素数さん
11/11/06 17:19:39.30
>>267
既知？全く荒唐無稽の既知外だろｗ
269:１３２人目の素数さん
11/11/06 17:32:12.02
>>258 わかってないなぁ。
数学はひとつなの。
関数解析にとっても代数方程式は重要なの。
整数論と関数解析は分けることができないの。
向かう方向はおなじだから。
だが、逆数学はわけることができる。
価値観が違うんだから、どうどうと違う学問だと
なのって、数学の外で一国をつくればよい。
関数解析と整数論が違う学問だと思うのは、
きっと、現在の教育を途中で投げ出すと、
そういう感覚を覚えるようになってしまっているのが
原因。
270:１３２人目の素数さん
11/11/06 17:43:37.04
ロジックだって、完全性定理のレベルでさえ、
束、位相、代数が基盤だろ。
271:１３２人目の素数さん
11/11/06 17:48:05.83
>>270 いや、高校数学で充分足りる
272:１３２人目の素数さん
11/11/06 18:02:19.72
ロジックって、一体何を目的にして何に向かって
研究してるの？
273:１３２人目の素数さん
11/11/06 18:20:57.12
証明論とかって計算機畑の方が主流？
ここ最近の研究事情がどうなってるのかわからん。
274:１３２人目の素数さん
11/11/06 18:23:49.45
>>269
＞数学の外で一国をつくればよい。
ずいぶん壮大なことをのたまっているようだが、今の体制で
本当にそのようなことを実現するなら、政治的な力が必要だな。
内部から変化することはありえないから。
こんなところで愚痴ってないで、お前が先頭に立って
排斥運動の1つでもやってみたらどうだねｗ
275:１３２人目の素数さん
11/11/06 18:28:10.07
ロジックというのは、ロジックに関係しているというだけの
雑学の総称？
276:１３２人目の素数さん
11/11/06 18:48:03.53
「AはAに関係してるものの総称」
277:１３２人目の素数さん
11/11/06 19:35:09.95
>>276
アニメやゲームはそういう感じで使われているね
278:１３２人目の素数さん
11/11/06 21:24:26.00
>>271
基礎的な定理には初等的な証明、理解の仕方があるのは、
代数だって変わらんでしょ。けどそれじゃ数学的構造理解しているとは言えない。
279:１３２人目の素数さん
11/11/06 21:38:02.64
>>243-244 >>247 >>249-252 >>260-261
あなたのスタイルがちょっと古かったりおおげさだったりするのが皆の癇にさわって
いるだけかも。既知かも知れんが、学生だとすればなかなか力ある。
しつこくがんばれば将来性あるよ。めげるな。
280:１３２人目の素数さん
11/11/06 22:05:42.78
基礎論による理論の構造分析を、通常数学の学習や理論の創造に役立てたい。
オススメの基礎論学習コースある？
学習者は代数専攻の数学修士として。
281:１３２人目の素数さん
11/11/07 05:44:38.12
>>279
人を駄目にする褒め方をしてはいけない
282:１３２人目の素数さん
11/11/07 05:50:42.76
むしろボロクソにけなしまくる方が駄目にするんじゃねえの？？
283:１３２人目の素数さん
11/11/07 07:16:52.39
>>279
全然見当違い。
そもそも論理式の値が真偽値でないとする発想が既知外。
てゆーか自画自賛だろ。トンデモがよくやる手だｗ
284:１３２人目の素数さん
11/11/07 07:52:43.55
ファジー論理
285:１３２人目の素数さん
11/11/07 08:00:25.69
過去にもいたよね、方程式の解が実数でないものを認めようとしたり
小さい数から大きな数を減じてみようとしたり。
286:１３２人目の素数さん
11/11/07 10:17:53.15
>>285
それを今やって大発見だと思う人がいたら可哀相な人だよね。
287:１３２人目の素数さん
11/11/07 10:28:23.70
>>272 とか、
>>280 とか、
真面目な質問に答える能力のある人はいないの？
288:１３２人目の素数さん
11/11/07 11:13:58.64
じゃあ俺が、
といっても俺も素人なんであんまり真に受けないでね。
さしあたり完全性定理とか不完全性定理を知りたいなら、
朝倉 現代基礎数学 15 数理論理学 鹿島亮著
を読んで、証明とか説明に不足を感じたら
J.R.Shoenfied著のMathematical Logic
を読めばいいと思う。
モデル理論の代数幾何への応用とかは知らないんで。
289:１３２人目の素数さん
11/11/07 11:50:14.30
完全性定理、不完全性定理は、エンダートンで
勉強しました。その次にくるのは何がよいでしょうか？
290:１３２人目の素数さん
11/11/07 17:31:06.56
>>289
エンダートンを読了したのならば数理論理学に関して一通りの基礎は身に付いたはずなので
次は自分が特に興味のあるテーマのモノグラフやサーベイに進むのが良いでしょう。
291:１３２人目の素数さん
11/11/07 18:52:20.60
代数方面の人なら幾何的モデル理論とかが良いんじゃないかな
別にモデル論の知識は無くても読めるように書いてあるよ
基礎論全般の勉強なら新井敏康の数学基礎論が良いよ
包括的な入門書の中では一番レベルが高いんじゃないかな
292:１３２人目の素数さん
11/11/07 20:37:37.55
Endertonたけぇｗ
仕方ないからこれにしよう・・・
Lectures in Logic and Set Theory: Volume 1, Mathematical Logic (Cambridge Studies in Advanced Mathematics) [ペーパーバック]
George Tourlakis (著)
293:１３２人目の素数さん
11/11/07 20:49:01.48
>>291
へえ、モデル理論仕込まなくても読めるんですか。
アリ。
294:１３２人目の素数さん
11/11/07 21:15:27.88
モデル理論の代数幾何への応用なら
江田の数理論理学、これは絶対おススメ。
295:１３２人目の素数さん
11/11/07 22:10:14.58
証明論で良い本ある？
296:１３２人目の素数さん
11/11/07 22:48:43.42
Umm
APPLIED LOGIC SERIESとかCambridge University Pressのコンピュータサイエンスの
論理シリーズは良書が多いねぇ
297:１３２人目の素数さん
11/11/07 23:32:17.19
>>294
生協で見たことあるが、そんな特徴ある本なの？
読んでみないと分からんもんだね。
298:１３２人目の素数さん
11/11/08 17:18:48.13
ウィトゲンシュタインの論考ってどうなの？
基礎論的には。
299:１３２人目の素数さん
11/11/08 18:05:45.72
数学としての基礎論にとっては無価値だろ。
300:１３２人目の素数さん
11/11/08 18:10:42.83
数学として基礎論は無価値だろ。
301:１３２人目の素数さん
11/11/08 18:54:12.25
ウィトゲンシュタインの像とかいう概念を
直観主義で再現するみたいなパワポ見たことあるよ
302:１３２人目の素数さん
11/11/08 20:17:17.36
論理学なんかやって何の意味があるんだ？
303:１３２人目の素数さん
11/11/08 21:46:59.04
もちろん数学の基礎付けですよ！
304:１３２人目の素数さん
11/11/08 21:53:03.38
論理学は木の研究
目標は新たな計算機の創造
うひ
305:１３２人目の素数さん
11/11/08 22:39:11.92
論理学なんかで数学の基礎付けができるのか？
306:１３２人目の素数さん
11/11/08 22:49:07.15
量化の代入的解釈(substitutional quantification )って何ですか？ぐぐってもよくわからなかったのですが。。。
307:１３２人目の素数さん
11/11/08 23:36:34.25
例えば述語論理で言語の定数が0,1,2のとき、
「∀xP(x)が真」を、「P(0)が真＆P(1)が真＆P(2)が真」
と置き換えて解釈をする流儀。
モデルの側の領域と無関係と考えるような意味論。
ただ強完全性とコンパクト定理が成り立たない。
308:１３２人目の素数さん
11/11/09 00:09:01.98
>>307
なるほど。解説ありがとうございます。
>モデルの側の領域と無関係と考えるような意味論。
領域と無関係というのは、領域自体考えに入れないということですか？
たとえば、普通ならP(0)が真 iff V(0)∈V(P)と考えると思うのですが、上の意味論ではP(0)の真理値はどうやって決まるのでしょうか？
309:１３２人目の素数さん
11/11/09 08:14:34.34
例えば
P(x)のモデルMでの解釈が{2,3}で、
言語の定数記号がa,b、
そのMでの解釈がそれぞれ2と3だとする。
このとき代入したもの
P(a/x)とP(b/x)を解釈すると両方真。
つまり∀xP(x)が真。
ところがモデルMの領域全体がどうなっているかは不明！
310:１３２人目の素数さん
11/11/09 13:40:46.76
>>309
そういうことでしたか、よく分かりました。
311:１３２人目の素数さん
11/11/10 15:23:53.16
論理学なんかで数学の基礎付けができるのか？
312:１３２人目の素数さん
11/11/10 15:25:57.13
それは未来人に訊いてください
313:１３２人目の素数さん
11/11/10 16:50:53.13
ロジック抜きでどうやって数学を構築するのかと…
314:１３２人目の素数さん
11/11/10 18:28:52.13
トポスとか圏論とか
315:１３２人目の素数さん
11/11/10 18:47:35.69
>>314
そりゃ集合論抜きでロジック構築する方法だろ＾＾；
316:１３２人目の素数さん
11/11/10 19:42:13.85
数学の基礎付けがどうとかいうのは
今時（ロジックの中でも）時代遅れで、
研究者はほとんどそんなこと気にしちゃいない
317:１３２人目の素数さん
11/11/10 19:55:31.55
きさまら同じ話題を難解ループしてんだよｗ
318:１３２人目の素数さん
11/11/10 20:20:19.96
お前もいつまでこのスレ読んでるつもりだ？
319:１３２人目の素数さん
11/11/10 20:33:33.69
命ある限り読むつもりだよｗ
その5辺りから読んでるんだから
320:１３２人目の素数さん
11/11/10 20:34:33.65
その１からのログを保持してる俺はそろそろ飽きてきた
321:１３２人目の素数さん
11/11/10 20:39:10.71
なぜなにスレッドの
洗濯小売はどうなったのか？
322:１３２人目の素数さん
11/11/10 22:44:01.56
>>316 では、今のロジシャンは何をやりたいの？
323:１３２人目の素数さん
11/11/10 22:47:13.21
ただのパズラー？
324:１３２人目の素数さん
11/11/10 22:58:40.05
従来の論理学は
コンピュータサイエンスに移ったよ。
洋書のCSシリーズのが充実している。
325:１３２人目の素数さん
11/11/10 22:59:07.72
パズラーに失礼の無いように
326:１３２人目の素数さん
11/11/11 09:49:01.53
第二不完全性定理の証明がわかりません。具体的には、
PA|- Pr(【φ】)→Pr(Pr(【φ】))
をどうやって証明するのかがわかりません。
不完全性定理ってなかなか難しいですね。
327:１３２人目の素数さん
11/11/11 19:49:22.09
補題
Σ1文φについてPA|-φ→Pr(【φ】)
328:１３２人目の素数さん
11/11/11 21:57:15.05
>>327
定義に関する帰納法で証明すればいいんですかね？
φが原子論理式のとき
φが��Ψのとき
φが、、、、
んーいまいちまだ分からないんですが。
329:１３２人目の素数さん
11/11/11 22:14:05.71
たとえば
PA|- ∀x∀y(x=y→Pr(【x=y】))
はどうやって証明するんでしょうか？
330:１３２人目の素数さん
11/11/11 22:56:20.05
>>329
PAの定義や証明体系に依存する。
331:１３２人目の素数さん
11/11/12 01:49:07.93
>>330
たしかにそうですね、、、定義も書かずすみませんでした。
ところで、第二不完全性定理を証明する際に使われる導出性条件(derivability conditions)というのが３つありますよね。
D1 PA|- φ→Pr(【φ】)
D2 略
D3 PA|- Pr(【φ】)→ Pr(【 Pr(【φ】) 】)
このうちのD1とD3は何が異なるのでしょうか？ Pr(【ψ】)をD1のφとして考えれば、 D3はD1に含まれる気がするのですが。
332:１３２人目の素数さん
11/11/12 03:39:12.71
D1が間違っているように見えるが、君の参考にしている本には本当にそう書いてあるかい？
333:１３２人目の素数さん
11/11/12 06:54:09.56
>>331
D1はPA|-φならばPA|-Pr(【φ】) だと思いますよ。
334:１３２人目の素数さん
11/11/12 09:05:16.20
D1が間違っていました、失礼しました。
335:１３２人目の素数さん
11/11/12 09:38:08.20
次の論理法則を証明せよ：－
「前提が偽であることは帰結も偽であることを何ら保証するものではない。」