- 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/
- 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は完全の意を取り違えてるだけだから質問しても無駄だろう
- 147 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 14:23:15.33 ]
- >>145
＞集合論がどういった証明体系の述語論理の上にあるのか
＞普通は明示されないが、おそらく完全な述語論理の上で
＞つくられているので問題なし。
8のいう「完全」の定義とは？
- 148 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 15:27:59.99 ]
- どんな図形が描画可能か、という問題がある。
使っていいのは定規とコンパスだけか？
それとも２次曲線は描けるとするか？
使える道具はいろいろ仮定できるが、それらを組み合わせて「実際に」描画するのは
具体的で有限なプロセスでなければならぬ。
- 149 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:20:22.38 ]
- >>148
なにやら唐突な書き込みだが、
過去の書き込みへの返答なのか？
- 150 名前：１３２人目の素数さん [2011/11/03(木) 16:26:05.53 ]
- fdg
- 151 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:27:03.44 ]
- 代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。
角の三等分は存在することが分かっているのに、作図できないことを示すのも二次的だ。
つまりガロア理論の金字塔的といわれる結果は重要度が低いのね。
- 152 名前：150 [2011/11/03(木) 16:31:17.57 ]
- 間違えて書き込んでしまった...
ところで命題論理で￢、→、∧、∨だけでは
2値論理をすべて網羅することはできないみたいですね。
＝を付け加えてようやく16パターンが完成する。
- 153 名前：１３２人目の素数さん [2011/11/03(木) 16:42:28.85 ]
- >>151
PAが不完全にもかかわらず、偽命題がPAで証明可能を意味する文を
PAの中で証明しようとしている。に対してはその理屈は成り立つ。
しかし逆数学が研究しているのは計算可能性の次数や算術や再起関数の階層であって、
今証明されている数学の定理をどれだけ少ない公理で証明できるかを研究しているわけではない。
- 154 名前：１３２人目の素数さん [2011/11/03(木) 16:43:36.63 ]
- >>151
＞代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
＞わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。
逆数学の話なら、「代数的な解法を持つかどうか考える」
という理解が間違ってる。
代数的な解の存在が、いかなる前提によって証明されるのか
を考えている。
- 155 名前：１３２人目の素数さん [2011/11/03(木) 16:49:48.77 ]
- ああ、151は
解の存在証明が一次的
解法の存在が二次的
といいたいわけね。
そういう意味でいうと、
無矛盾性の証明不能性は一次的
命題の決定不可能性は二次的
ってことかい？
- 156 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:49:51.40 ]
- >>154 で、その代数解の存在を証明するのに必要な前提が証明できたら、
その次には、その証明のためにはどんな前提が必要なのか、考えるのですね。
わかりまつ
- 157 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:51:13.61 ]
- それは逆数学が二次的だから重要でないのではなくて、
逆数学が逆数学だから重要でない、と言っているに等しいが。
二次的だから重要でないのなら同じく二次的な代数的解法の不存在も重要ではないことになる。
- 158 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:51:33.32 ]
- 数学では無く論理学ですね。
- 159 名前：１３２人目の素数さん [2011/11/03(木) 16:53:44.43 ]
- >>156
ん？「代数解の存在を証明するのに必要な前提」は証明しないよ。
ミュンヒハウゼン（あるいはアグリッパ）のトリレンマって知ってる？
全ての命題に証明を求めるなら無限背進か循環論法に陥る。
独断は排除できないよ。
- 160 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:57:21.32 ]
- ガロア理論にとって、代数解の存在云々は
理論のごく一部です。数の演算に関する本質的洞察を
含み、数学全土に応用があります。
本当にガロア理論勉強した事あります？
- 161 名前：１３２人目の素数さん [2011/11/03(木) 17:00:11.57 ]
- >>157
「それ」とは>>153のコメント？
「計算可能性の次数や算術や再帰関数の階層」は一つの尺度に過ぎない。
例えばRCA0とWKL0の違いは何なのか、理解しないのなら意味がない。
二次的かどうかが問題なわけではないだろう。
代数的解法の存在も、代数的解法による解の意味が重要。
- 162 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:00:32.02 ]
- >>159 そういう意味じゃ無い
- 163 名前：１３２人目の素数さん [2011/11/03(木) 17:04:21.38 ]
- >>160
＞数の演算に関する本質的洞察
では、ガロア理論によって明らかになった、
「数の演算の本質」とはズバリ何？
あなた本当にガロア理論理解できてます？
教科書の記述を丸ごと記憶するのは勉強と違うよ。
- 164 名前：１３２人目の素数さん [2011/11/03(木) 17:05:03.23 ]
- >>162 ではどういう意味？
- 165 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:07:07.82 ]
- >>163 あなたはガロア理論理解してますか？Yes or No?
- 166 名前：153 [2011/11/03(木) 17:14:05.37 ]
- RCA0とWKL0の違いはチューリングマシンの違いですね。
確かに次数やクラスは1つの視点ですね。
- 167 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:22:16.38 ]
- >>166
具体的に説明されたい。
- 168 名前：8 [2011/11/03(木) 19:15:30.11 ]
- >>152
複雑だけど￢と→だけできる。
￢(A→￢B)
￢(A→B)
￢(￢A→￢B)
￢(￢A→B)
の4つで1パターンで真になる命題が網羅できるので、
これの否定で3パターン真で命題が網羅できて、
4つの内2つを組み合わせて2パターンで真になる命題を網羅する。
4つ全部を組み合わせて恒真、その否定で偽をつくる。
これで16パターンが網羅できる。
- 169 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 19:49:36.91 ]
- >>148
証明可能性を描画可能性になぞらえているのか？
コッホ曲線をどうやって描画する？
- 170 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 20:22:00.87 ]
- >>163 まぁ、簡単にいうと、ガロア理論の
本質とは、
ある集合の構造を調べるときに、その集合を直接調べるのではなく、
その集合からその集合への写像の族を考え、
その族の構造を調べることが有効である。
ということ。それ以降の数学のあらゆる所で出てくる重要な考え。
- 171 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:16:48.67 ]
- >>170
わざわざガロア理論とか数の演算の本質とかいうから
実に高尚極まりない整数論の奥義を語るかと思えば
数学のどこでもでてくるヌルい一般論じゃんｗ
- 172 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:22:30.85 ]
- >>171
>>151が、ガロア理論を誤解して過小評価していたので、
ガロア理論の本質論が出たまで。
そう、今ではいたるところに普及した
重要な考え。
- 173 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:36:59.04 ]
- >>172
ガロア理論の本質でもなんでもない。
例えば、ガロア理論→幾何学、集合→空間、写像→変換と置き換え
「幾何学の本質とは
空間の構造を調べるのに、空間を直接調べるのではなく
空間から空間への変換の族を考え、
その族の構造を調べることが有効だということ」
といっても通じてしまう。
こんなヌルイ一般論を重要というのは・・・馬鹿ｗ
- 174 名前：１３２人目の素数さん [2011/11/03(木) 21:37:49.72 ]
- >>168
その4つの式の最初に￢をつける意味は？
|
 |
