数学基礎論・数理論理学　その13

1 名前：１３２人目の素数さん mailto:sage [2012/06/24(日) 01:38:43.25 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学　その12 http://uni.2ch.net/test/read.cgi/math/1332549969/ 583 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 04:52:33.01 ] 例えば超準解析で実数体 R と任意の実関数 f たちを付け加えた構造を考えて その上の論理式考えたりするけど、 あんな感じで考えると普通に数学の問題を考えているときの量化の仕方と 形式的な論理式としての量化の複雑さがほぼ一緒になると思うけど。 （あくまで"便宜的に"与えた一例）。 理論が公理化可能じゃないとか素直じゃないとか言われても知ったことじゃない。 言語とか論理式ってのはロジックを一般の数学に応用するときに 便宜的に定義するものであって、応用される側から見たら そんなに本質的なものじゃないと思うんだけどね。 一般的な代数学や解析学では量化の複雑さを制限したりもしないし、 それ以前に言語を敢えて固定してその範囲で議論したりもしないように思う。 しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 定式化がやりにくいのはロジックの表現力がダメだからで、代数学や解析学の責任じゃない。 584 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 06:37:40.34 ] >理論が公理化可能じゃないとか素直じゃないとか言われても知ったことじゃない。 論理式で書けない概念についてΣ2だのΣ5だのって意味をなさないってこと分かってる？ 意味をなさない問題を議論していることになって「知ったことじゃない」じゃ済まないんだが。 （脇道に逸れるが、理論とか公理化可能など全く関係ない。 こいつが理論と言語、公理化可能と言語での表現可能を混同していることが分かる。） >言語とか論理式ってのはロジックを一般の数学に応用するときに >便宜的に定義するものであって、応用される側から見たら >そんなに本質的なものじゃないと思うんだけどね。 本質的でないのはその通りかもしれないが、 それならΣ2かどうかΣ5かどうかの議論はもっと本質的ではないことになる。 議論には乗ってきながら自分が不利になるとその議論の土台を壊すことを人は負惜しみと呼ぶ。 >しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 >定式化がやりにくいのはロジックの表現力がダメだからで、代数学や解析学の責任じゃない。 定式化しづらい性質を考えることについて誰も誰の責任も追及していない。 責任を追及しているのは、しづらい定式化をしないまま （定式化を前提とした概念である）Σ5などの複雑な論理式が出てくると主張したこと。 Δ0で済むと主張する側は、集合論という定式化を与えてそう主張している。 定式化しづらいのであれば、尚の事、具体的な定式化を明示してからΣ2だのΣ5を云々すべき。 585 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 06:51:34.85 ] >>562 その上でもう一度聞きたい。 どのような定式化の下で、コンパクト性や環の局所性がΣ5以上になるのか？ 定式化しづらい概念だからこそ、定式化を暗黙の了解に出来ない。 それ説明しなければ、Σ2だのΣ5だの言っても聞き手にはさっぱり分からない。 586 名前：STS446 [2012/09/01(土) 08:18:18.89 ] >>583 ＞あんな感じで考えると普通に数学の問題を考えているときの量化の仕方と ＞形式的な論理式としての量化の複雑さがほぼ一緒になると思うけど。 私の経験では普通の数学の問題に出現する量化は すべて∊で制限されたΔ^0_1文のみですね。 そうすると形式的な論理式もΔ^0_1になるので、 あなたのΣ2だのΣ5が出てくると言う主張と矛盾します。 ＞しかも一階論理で必要十分な定式化をしづらいような性質・対象も平気で考える。 実際一階論理の枠組みを超えた命題はあります。 それは大抵「部分集合の全体が〜〜の性質を満たす場合・・・」、 だとか2階の数学的帰納法の不足から生じます。 しかしもしも一階のZFCから展開できないのならば、 その数学的命題は素朴集合論にも基づかないことになりますね。 つまり同時に数学は集合論から展開されないということも意味します。 とはいえ2階のZFCというのもあり、モデルもありますよ。 587 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 08:59:21.46 ] あくまでTh(N)が再帰的に公理化可能でない、という意味での 公理化不可能性について言っているんであって すぐ上に素直なやり方じゃないというレスがあったこともあって 公理化できないことは或る意味で超越的であるということだから その点自然じゃないから不満だというレスが想定されるので書いただけ。 論理式で書けないことと公理化可能なことが同じだと誰が言った？ あのさあ、574≠580だし、俺は「Σ5などの複雑な論理式が出てくる」 とは言ってないんだが…… ちょっと上の方でもそうだったんだが 勝手に別人のレスと俺のレスをくっ付けて 588 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 11:00:54.99 ] 見分ける方法無いだろ。コテハン付けろや。 589 名前：１３２人目の素数さん [2012/09/01(土) 11:55:32.59 ] >>588 めちゃくちゃすぎる 590 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 13:07:07.45 ] >あくまでTh(N)が再帰的に公理化可能でない、という意味での >公理化不可能性について言っているんであって >すぐ上に素直なやり方じゃないというレスがあったこともあって >公理化できないことは或る意味で超越的であるということだから >その点自然じゃないから不満だというレスが想定されるので そんな想定している時点で、何が問題になっているのかまるっきり分かっていないことがバレバレ。 591 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 13:46:07.69 ] >>587 言い負かされそうになると別人ってことにするのは２ちゃんでは常套手段だよね コテハンつけとかなきゃそう言い張っても誰も嘘は見抜けんから 592 名前：１３２人目の素数さん [2012/09/01(土) 14:57:11.97 ] >>591 私は574だから君がめちゃくちゃを言ってることがわかる。 593 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 15:00:59.27 ] とうとうこのスレにもゆとりモンスターが現れたか 594 名前：594 mailto:sage [2012/09/01(土) 16:09:04.19 ] 5=9-4 595 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 17:28:11.86 ] 俺も同一人物説に賛成したいところ。 587は「574≠580」と主張しているってことはどちらか一方は自分だと言ってる。 >>580だとすると「Σ5などの複雑な論理式が出てくる」とは言ってなくても Σ2に言及しているのだから言い訳にならない。 >>574だとすると>>580に向けられた>>581に対して >>583でそんなムキになって反論するのか分からない。 まあもっとも>>590でも指摘されているように おばかなゆとりモンスター君の考えることはこちらの想像の斜め上なので こんな推測は無意味なのかもしれないが。 596 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 17:37:57.25 ] >>595 誰も何も言っていないのにいきなり「〜〜の責任じゃない」とか言い出す香具師の思考回路に関して なんで「そんなムキになって反論するのか分からない」とか幾ら検討を重ねても無意味では？ 597 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 18:29:38.42 ] >>579 CZF+V=L が 構成的＋　可述的＋　構成可能＋ に該当するんじゃない？ CZFでゲーデルのLは定義できないんだっけ？ 598 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 19:50:49.81 ] たとえば微分積分の授業で 各点連続は∀∃∀の形の多重量化を用いて定義するのに対して 一様連続は〜〜と教師が言っていたとして、 　「ちょっと待って下さい、今の場合、どういう言語を想定しているんですか？ 　集合論の言語を想定しているなら今挙げたような複雑な量化は出て来ない事は明らかだ。 　この質問にもし答えられないとしたらナンセンスなことしか言っていないことになる！」 とか言い出したら、もう基礎論キチガイと思われても仕方ないレベルだと思うんだが…… もちろん、明確に特定の言語を想定して居なくても、先生のremarkには十分意味はあるわけで。 599 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 20:22:13.52 ] 結論を出すための努力を放棄している例を出されてもなぁ…… 相手を罵倒するのが目的だろ、これ。 もっとマトモな例は無いの？ 600 名前：STS446 [2012/09/01(土) 20:26:02.76 ] >>598 すいませんが 貴方が例示した各点連続も一様連続も 公理的集合論ではΔ^0_1論理式だということは分かりますか？ そのうえで、それらがΣ2だのΣ5になるだのと主張されているので、 それなら一体どんな体系（言語）において各点連続や一様連続がΣ2だのΣ5論理式になるというのか尋ねているんだと思いますよ。 601 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:08:25.67 ] ＞もう基礎論キチガイと思われても仕方ないレベル わざわざ基礎論スレに出てきて突っ込まれたら逆ギレしてこれかよｗ なんというゆとりモンスターっぷり 「保健所に訴えてやる！」って話も今なら信じられる 602 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:14:28.91 ] 超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん きちんと論理式として表現できてるでしょ それをマトモに感じるかどうかは知らんけど ZFC上Δ0やΔ1であっても、それより弱い理論での量化の階層を考えることには （ロジックとしては）意味があると思うけど。 （尤も普通の数学では事実としてそんなこと一切気にしていない、という流れではあるが。） 一番簡単な例で言うとPeano算術の部分理論のreflectionを考えたりするときに 各階層ごとの真理述語とかを定義したりするでしょ。 ZFCの言明としてはΔ0なんだからそれらの言明も本当はΔ0なんだ、というのは違うと思う。 あと多重量化（つまりΣ2ないしΠ2より複雑な式）は普通の数学に表れるとは言ったが Σ5論理式が現れるなんて言ってないし、そういう例を頑張って探してくるつもりもないからね。 だいたい元から労力がやたら掛かるから言明ごとにこれはΣいくつ、これはΠいくつ、 と分類したりしない、と言う話なんだから。 603 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:23:26.83 ] 560 ：１３２人目の素数さん：2012/08/31(金) 17:34:25.01 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないってことでおk？ 　　基礎論でもΠ5やらΣ4に属する＊具体的な＊論理式は出てこないってことでおk？ 562 ：１３２人目の素数さん：2012/08/31(金) 19:17:40.84 　　>>560 　　コンパクトとか局所環とかの定義をベタに書けばそれくらい複雑になるでしょ このやり取りでは>>562はコンパクト性や局所性は「Π5やらΣ4やら」になると主張していると読み取れるが、 >>602は>>562とは別人だと言いたい？ 604 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:30:55.67 ] ＞超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん ＞あと多重量化（つまりΣ2ないしΠ2より複雑な式）は普通の数学に表れるとは言ったが どう突っ込んで良いのか分からんが、超準解析でやるような言語の設定だと （上付添字なしの）Σ2とかΠ2とかって普通は定義しないんだが。 少なくとも標準的な定義はないのだからΣ2やΠ2の定義を与えるべき。 こういう多種の言語の場合、どの種の量化かが問題になるので Σ^m_nみたいにどの種の量化を数えるのかを上付添字で明示するの普通。 >>580は別人なのか本人なのか知らないけど、それを見ていると そういうこと全く分かっていないで書いてるな、ということがよく分かる。 605 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 21:53:06.62 ] 570 ：１３２人目の素数さん：2012/08/31(金) 22:01:48.57 　　>>567 　　文句は「普通の数学」と言った人に言ってくれ 571 ：１３２人目の素数さん：2012/08/31(金) 22:13:21.80 　　>>570 　　「普通の数学」と言った香具師に責任はない。Δ0でないと主張したわけじゃない。 　　責任があるのは「普通の数学」に出てくる論理式が、Σ5とか複雑になると主張した君だ！ 574 ：１３２人目の素数さん：2012/08/31(金) 22:16:46.00 　　>>571 　　「普通の数学」と言う言葉が厳密ではないから、そんなにきちんとしたことは言わなくても良いでしょ？ このやりとりでは>>574と>>570は同一人物を推測できるが >>570は最初に「普通の数学」という言葉を出した>>532ではない顔をしている。 そしてゆとりモンスター君は>>574か>>580のいずれかだと>>587で主張しており >>580の方だとすると言い訳にならないので>>574なのだろう。 ところがゆとりモンスターは>>602で 「だいたい元から労力がやたら掛かるから言明ごとにこれはΣいくつ、これはΠいくつ、 と分類したりしない、と言う話なんだから。」と自らを>>532だと認めている。 何が言いたいかというと、都合が悪くなると別人の振りしている疑いが濃厚だということ。 606 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:03:29.65 ] >>602 Σ2とかΠ2とかは、sort(種)が一つの言語に対して定義するもの だから many-sort(多種)の言語では例にならないんだよ いや>>604と同じことなんだが 607 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:20:57.73 ] 俺様定義でしかないのに標準的な定義だと勘違いして 断りもなく俺様定義で話を続けるってのは素人と駆け出しにはよくあること。 608 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 22:41:25.97 ] 超準解析って型理論とかmany-sortedな言語による定式化しかないんだっけ？ 609 名前：STS446 [2012/09/01(土) 22:50:46.21 ] many-sortedや二階算術やNFやZFC^2ならΣ^1_nとかΠ^1_nになるだけ。 610 名前：１３２人目の素数さん mailto:sage [2012/09/01(土) 23:09:20.71 ] >>608 そりゃone-sortedに直したければできるだろう。 問題は、「超準解析で表れるような」と言っただけで 特に断りもなくone-sortedの言語を考えられるかということだろ。 こういうのはone-sortへの直し方次第でかなり変わってくるんだし。 611 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 00:17:41.65 ] 実数とか実数上の関数とかその関数とかをone-sortで表現する方法って集合論以外に有名なものある？ 通常のmany-sortをone-sortに書き換えたら、もう殆ど集合論と同じ代物だよね。 超準解析でもIST(internal set theory)とかあるけど、完全に集合論だし。 いずれにせよ標準的でないないし有名でない定式化を使うのなら説明が必要。 その説明をしようともしないで俺様用語法で教皇突破しようとするからゆとりモンスターと呼ばれるんだ。 612 名前：喜田だ mailto:sage [2012/09/02(日) 00:35:40.79 ] フーリエ積分作用素について語ろうよ 613 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 01:55:35.51 ] 基礎論スレでフーリエ積分作用素の何を語るっていうんだい？ 614 名前：１３２人目の素数さん [2012/09/02(日) 02:24:31.96 ] 実部・虚部ともに有理数の複素数と自然数は1対1に対応する。 その対応をFとしてF(n)がジュリア集合に入っているようなn全体の集合の算術的階層はどこだろう。 Fはそんなに複雑でなければ本質的な問題にはならないよね。 615 名前：STS446 [2012/09/02(日) 06:09:01.49 ] >>614 Δ^0_1 desuyo 616 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 07:36:23.36 ] たとえばユークリッド平面幾何でいうなら 〜〜は直線である、〜〜は点である、というような述語を用意して 対象領域は一つにしてしまうone-sortedな方法と、 それぞれの対象領域を別に用意するmany-sortedなやり方がある。 こういうのを「集合論と同じ代物」とは言わないんじゃないの？ 外延性公理やら分出公理やら選択公理やら冪集合の公理やらがあるわけじゃないんだし この例じゃなくてもmany-sortedとone-sortedの相互変換は同様に出来る 617 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 08:20:54.38 ] ついでにはっきり言っとくと普通の数学だと Σ_4^ZFとかΠ_5^ZFとかそういう性質は 滅多に出て来ないだろうね。たぶん。 618 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 14:15:16.50 ] >>616 だから公理とか公理化とか関係ないって言ってるのに あふぉだなー 619 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 16:31:33.89 ] >>616 実数、実数値関数、実数値関数の関数などのsortを持つ言語にそのやり方を適用しちゃうと 「関数である」とか複雑であるべき式が原始論理式になってしまうよ？ しかも高階の量化（関数量化）も低階の量化（実数量化）も区別せずに数えてΣnを定義するわけ？ もちろんそう定義するのは自由だけど、断りなしに「Σ2」とか言われて想像できるような 標準的な言語でないことは確かだよね。 それともまた別人だと主張するのかな？ 620 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 16:57:09.12 ] なんで「関数である」が複雑である「べき」なのか理解できない 621 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 17:22:44.65 ] どうして 「問題は、「超準解析で表れるような」と言っただけで 特に断りもなくone-sortedの言語を考えられるかということだろ。 こういうのはone-sortへの直し方次第でかなり変わってくるんだし」(>>610) とか 「いずれにせよ標準的でないないし有名でない定式化を使うのなら説明が必要。 その説明をしようともしないで俺様用語法で教皇突破しようとするからゆとりモンスターと呼ばれるんだ」(>>611) とか 「もちろんそう定義するのは自由だけど、断りなしに「Σ2」とか言われて想像できるような 標準的な言語でないことは確かだよね」(>>619) とかに反論しないの？無理やり作った例を幾らあげても意味ないよ。 622 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 19:06:48.95 ] 普通に数学（たとえば実解析やらRiemann幾何やら）をするときに 量化の複雑さによって性質を区別したりしない、という発端から来てる話で、 たとえば各点連続は実数値のみに関する∀∃∀の形の量化だとか そういうことを言っているのに、なんでZFCとか二階算術とかの体系の話にしようとするのさ ロジックだとよくそういう体系で論理式の複雑さを制限して議論するのは知ってるよ。 でも今はそういう話はしていないし、 個人的には普通の数学者は実解析をやるときに量化の複雑さは気にしないというときに どの形式体系についての量化の複雑さを考えないのか、という疑問の持ち方がおかしいと思う 623 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 19:55:51.50 ] >>622 >たとえば各点連続は実数値のみに関する∀∃∀の形の量化だとか >そういうことを言っているのに これは実数論の言語を使ってもΠ3だ。 （集合論以外の）標準的な言語ではΣ2ともΠ2ともいえないような例を >>562や>>580で挙げたからこんな問題になっているんだろ？ どさくさにまぎれて例をすりかえるなよ。 624 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:23:43.01 ] 532 ：１３２人目の素数さん：2012/08/28(火) 16:24:52.63 　　普通の数学では選択公理を使うか使わないか、 　　背理法を使うか使わないかなどは興味の対象になるけど 　　使う論理式がΠ2、Σ2以上の量化を使うかどうか、 　　というのは大抵気にしないし、気にしてられないな 　　それに背理法と言われているのは良く見ると否定導入であることが多い 533 ：１３２人目の素数さん：2012/08/28(火) 18:12:15.28 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないのでは？ 　　基礎論でだって出てくることはないと思う 　　一般のnに対してΠnとかΣnとか言うことはあっても 560 ：１３２人目の素数さん：2012/08/31(金) 17:34:25.01 　　普通の数学でΠ5やらΣ4やら複雑な論理式出てこないってことでおk？ 　　基礎論でもΠ5やらΣ4に属する＊具体的な＊論理式は出てこないってことでおk？ 562 ：１３２人目の素数さん：2012/08/31(金) 19:17:40.84 　　>>560 　　コンパクトとか局所環とかの定義をベタに書けばそれくらい複雑になるでしょ 580 ：１３２人目の素数さん：2012/09/01(土) 00:09:20.71 　　たとえば有界な関数が〜〜と言っただけで、 　　（実数論として）Σ2の式が出て来るんだから 　　Σ3くらいの量化は普通に考えることになる 　　実数と自然数の部分集合を同一視する場合はさらに複雑になる 625 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:24:34.38 ] 最初の>>532だけの段階では>>622の言うとおり 「普通の数学者は実解析をやるときに量化の複雑さは気にしないというとき」 といえるかもしれない。 しかしそれに対するレスやそのまたレスを踏まえるとそうではない。 これらレスと超訳すると以下のような感じ。 >>532「普通の数学では複雑さは気にしないし気にしていられない」 >>533>>560 「細かく見てみたらΠ5やらΣ4に行くものはないんじゃない？」 >>562 「いやコンパクト性や局所性はそれくらいになる」 >>580 「ほら実数論ではこんな単純なものでもΣ2になる」 言語もはっきりさせずに「Π5やらΣ4に行くかいかないか」 「単純なものでもΣ2になるかならないか」を議論すべきだというのか？ 626 名前：１３２人目の素数さん [2012/09/02(日) 20:29:49.34 ] >>623 完備距離空間なら、Xがコンパクトとは、任意のε＞0に対してXの有限集合{x_1,…,x_n}があって任意のx∈Xに対して1≦k≦nが存在してxとx_kの距離がε未満、ということだから∀∃∀∃だね。 627 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:44:05.30 ] 実数論の言語では「有限集合{x_1,…,x_n}があって」は表現できないと思うんだ 628 名前：１３２人目の素数さん [2012/09/02(日) 20:46:26.98 ] >>627 実数論に限定する理由は？ 629 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 20:51:44.67 ] 実数論でなくてもいいけど言語を決めないで∀∃∀∃と言っても意味ないでしょ。 ある言語では∀∃のものがある言語では原子論理式になったりするんだから。 まず議論の前提をはっきりしようや。 630 名前：629 mailto:sage [2012/09/02(日) 20:52:37.36 ] 6=2*√9 631 名前：632 mailto:sage [2012/09/02(日) 20:53:36.40 ] 6/3=2 632 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:15:09.54 ] ほんとにこいつゆとり君だなー 633 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:21:17.60 ] >>622は言語を指定するのを諦めたように見えるが 超準解析がどうのと言ってたのは撤回したんだろうか？ 634 名前：１３２人目の素数さん [2012/09/02(日) 21:57:23.91 ] >>629 じゃあ数学の教科書で∀とか∃とか書いてあるのは意味無いの？ 厳密じゃないというのならわかるけど 635 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 21:59:03.78 ] あふぉはもはやスルーしかなさそうだな 636 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:01:23.00 ] >>634 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 637 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:32:26.15 ] 局所環の例は俺が挙げた例じゃないから知らない そもそもイデアルやら位相をどうやって述語論理で扱えば良いのか知らない 少し解析になれれば「充分大きな M があって x, y < M のとき〜〜」というだけで、 理解がより困難になったりはしないが、これだってきちんと言うと 「∀N∈R. ∃M∈R. N＞M ∧ ∀x, y. x ＜M∧y＜M⇒〜〜」 なので、 すぐΠ3くらいにはなる。 有界な関数がどうのこうのと書いたときに言いたかったのはこういう感じの事で、 三重量化、四重量化はざらにあるということ自体は正しいと思っている。 関数の話になると確かにどういう量化なのかが不明瞭なのでこの例は取り下げる。 638 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 22:50:11.26 ] 「普通の数学」では一階論理で「定式化をしづらいような性質・対象も平気で考える」と言っていたのに、 今度は定式化しやすい性質・対象だけ考えることにしてその範囲の言語を持って来てΠ3だとかってか？ 随分と都合のいい話だな、おい。 639 名前：１３２人目の素数さん [2012/09/02(日) 22:59:26.27 ] >>533は普通の数学で論理式の話としてΣとかΠを出して来てるんだから、完備距離空間でのコンパクトの定義を出してきても問題ないじゃん。 「一見そう見えるけど実はそう簡単にはいかない」という話ならわかるけど。 640 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:06:22.94 ] >>637 あんたΠ3やΣ3と三重量化を混同してるんじゃないか？ Δ0には有界量化が何重にも入っているんだお 641 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:15:06.67 ] そうそう、言語がはっきりしてなければ有界量化が何なのか分からないのだから そもそもΣnの定義が定まらないよね。 642 名前：１３２人目の素数さん mailto:sage [2012/09/02(日) 23:30:59.86 ] >>639 >完備距離空間でのコンパクトの定義を出してきても問題ないじゃん。 誰かがその定義が問題だなんて言ったのか？ 言語をはっきりさせずにその定義が∀∃∀∃と言ったのが問題なんでしょ。 そんな調子なら、いい加減、俺も他の人と同じくスルーするよ。 643 名前：STS446 [2012/09/02(日) 23:37:23.00 ] 公理的集合論では>>626や>>637などの例にある数学的命題はΔ^0_1と同等になる。 算術的階層が単なる論理式中の∀と∃の交互の繰り返し回数だと誤解しているのではないだろうか。 集合論では数学的命題は∃ｘ∊ｙR(ｘ)のようになったりするが、 R(ｘ)がΔ^0_1なら、∊による有界量化したものも原始再帰的になるのである。 算術的階層がなぜ算術的とよばれるか考えてみるべきだろう。 644 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:12:23.01 ] >>640,>>641 算術や集合論では確かに bounded quantifier はΔ0に自由に表れていいわけだけど モデル論で出てくるような言語（実数閉体の理論など）で定義するときは Δ0は量化のない論理式とすることが多い。 言語がはっきりしなければどっちの流儀を採用するのが普通なのか判断できない、 ということなら全くもってその通り。 やっぱり言語を明示せずΣいくつと言うのは問題あり。 645 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:37:02.60 ] >>640 ZFCにおける論理式の階層の話は（私は）してない あなたはその話をしているのかもしれないけど 646 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 00:39:26.39 ] というか普通の数学では言語をはっきり固定して議論しない、 がFAかと イデアルの昇鎖列が有限ステップで止まるといったときに そんなことを考えるのはルール違反だという訳にもいかんし 647 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 01:59:13.76 ] >>645 それでどの言語で論理式の階層の話をしているんだい？ 「ZFCではない」以上のこと何も言ってないよね？ それじゃΣとか言っても意味をなさない >>646 んじゃ普通の数学の議論で出てくる概念をΣいくつとか言うのも無意味 がFAだろう 648 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 02:06:57.53 ] 言語を固定させないことにはΣnは意味をなさない って当然のことがなんで分からないのかが分からない 649 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 06:05:33.58 ] >>646 「超準解析で表れるような」実数、実数値関数などなどのsortを持つ言語で十分だろ？ 「普通の数学」では量化は全部タイプがついているんだから。 通常の数学はmany-sortなのに、Π3とかΣ2とかone-sortを前提にした用語を不用意に使ったのが問題なだけ。 自分の不用意発言を根拠に「普通の数学では言語をはっきり固定して議論しない」とか勝手に結論出すなよ。 650 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 08:12:18.90 ] 646はイデアルの話をしているけど 極大イデアルとかを別のsortで扱っても、かなり集合論的な議論を 援用せざるを得ないようになると思うよ 位相空間論を一階述語論理で取り扱う困難とそんなに変わらないと思う 651 名前：１３２人目の素数さん mailto:sage [2012/09/03(月) 18:07:15.68 ] イデアルの議論なんて二階の言語で十分表現できる。 （逆数学でイデアルが難なく扱えるのと同じこと。） 二階の言語は元のsortとそれら元の集合のsortを持つmany-sorted言語だから その意味では確かに「集合論的」なのかも知れないけれど、 階数によるsortの制約が全くないZFのような本格的な集合論は必要ない。 652 名前：STS446 [2012/09/03(月) 19:22:45.50 ] 2階の言語って普通は2階述語論理のことですね。 多領域論理は普通、型の概念が定義されていませんから1階論理ですね。 特に多領域論理で2階算術と呼ばれる体系は「集合論的」ではなく「解析的」とよばれますね。 2階算術の論理式は解析的階層でΠ^1_nとかΣ^1_mとなりますから。 653 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 07:05:44.67 ] もりさがっとるな 654 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 10:33:58.56 ] 　Maximal ideal あるいは Prime ideal の全体を考えれば、３階になる。主イデ アル環に制限しなければ　Zariski topology を使えないことになる。２階算術に 制限するのは無理がある。逆数学はまあそのへんでよいということなのかも 知れない。 655 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 11:11:06.57 ] すみません、また質問です >>466がこないだ理解できたのですが、 半直線と円は自然数として同一視するのですか？ 656 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 12:05:39.87 ] いくらゆとりでもいい加減スレ違いなことを悟れ 657 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 12:36:41.21 ] 独学で勝手に数学を勉強している者や、計算機工学の後で数学を やり直している者はどのスレで質問すればいいですか 658 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 13:15:11.31 ] つ　雑談スレ 659 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 13:31:37.33 ] >>658 なぜですか？ 660 名前：ＳＴＳ446 [2012/09/05(水) 16:15:37.87 ] よく再帰理論とかで高い算術的階層が出現するが、 これらを記述する言語は一体何なのかという疑問はある。 内包公理や帰納法はどうなっているのか。 そう考えると今回のような混乱は当然の思える。 おそらくは再帰的クラスや再帰的枚挙可能クラスの関係を基準として、 この関係にいくつ量化子をつけていくかと言う事だろうが、 この量化子は「ある〜」「すべての〜」といった自然言語、 つまり通常の数学で使われる議論の略記なのだろう。 この通常の数学での略記が形式的体系での記号と誤解されることで 今回のような議論が生じた。 661 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 17:23:50.04 ] >今回のような議論が生じた。 って、自分がその議論の中で完全に相手にされてなかったってことに気づけよ 662 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 17:35:32.22 ] >>654 >Maximal ideal あるいは Prime ideal の全体を考えれば、３階になる。 ３階の元一つ考えるだけなら３階量化は必要ないので２階で十分。 問題なのはMaximal ideal あるいは Prime ideal の全体の部分集合を走る量化がある場合。 そういう例としてZariski位相を挙げたんだろうけど、基本開集合が単純な形をしているので 開集合や閉集合上を走る量化も実際には２階の言語で十分表現できてしまう。 663 名前：１３２人目の素数さん mailto:sage [2012/09/05(水) 20:34:06.32 ] 代数幾何とか微分幾何とかをやる場合に二階「算術」で行うのは人工的な制限だと思う 664 名前：STS446 [2012/09/05(水) 23:38:56.56 ] 実際に二階算術じゃ扱えないコホモロジーとかもあるんよ。 Big Fiveも元々は算術的階層の強さ毎に帰納法と内包公理をQに加えていった結果生じている。 これらがたまたま集合・位相〜解析学の基本定理の強さ程度だったってわけさ。 もし1階算術サイドに話をすすめるなら内包公理は不要で、 帰納法の制限や帰納法の形態の種類によって QとPAの間に限定算術的階層と呼ばれるものが生じる。 2階算術の場合は、Qを内包公理で2領域に分離して拡張したものだな。 3階算術ならば2つ目の分離公理か3つの領域を同時に扱うような公理が必要になるな。 いずれにしろこれらは論理における高階とは違う。 領域が無数に分岐することで見かけ上どのような数学命題でも記述可能に拡張可能。 実際3階算術や高階算術なんかも研究されている。 665 名前：STS446 [2012/09/05(水) 23:56:58.89 ] >>664 とはいえ、もともと二階算術ってのは「人工的」なものなのですよね。 どれだけ算術を強めればどれだけの定理が証明可能か。 数学のある命題にはどれだけの公理の強さが必要か。 それを集合論のような複雑なものではなく、 古典数学的な簡素な公理である必要がある。 それらはダイレクトに再帰理論的な研究対象だからね。 まぁ代数幾何とか微分幾何レベルまで巨大化した世界には余り向かないね。 666 名前：STS446 [2012/09/06(木) 00:01:51.26 ] >>665 というより、そもそも数学の命題を テキスト通りそのまま論理式にするのがナンセンスなんだよね。 ダミー量化子使えば算術的階層なんて無限に引き上げられるし、 そもそも集合論的命題はほとんどが論理的に同値なΔ^0_1文が存在するしね。 667 名前：１３２人目の素数さん [2012/09/06(木) 00:25:21.71 ] >>666 自分との対話やめい 668 名前：１３２人目の素数さん [2012/09/06(木) 00:29:11.81 ] >>665の ＞それを集合論のような複雑なものではなく、 ＞古典数学的な簡素な公理である必要がある。 ＞それらはダイレクトに再帰理論的な研究対象だからね。 ここの文意が通らない。書き間違えですか？ 669 名前：STS446 [2012/09/06(木) 01:44:19.17 ] 訂正させてもらうと、 古典数学的に簡素な公理である必要があるのは、 再帰理論的な研究対象として扱えるようにするため。 例えば算術的階層に理論をはめ込むために、 帰納法をΣ_n文といった具合に制限している。 これは集合論では使えない手法 670 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 02:23:24.01 ] >>663 この話になった>>649から直前の>>662までよく読んでみな。 「二階」という言葉は出てきているが誰も「二階算術」とは言っていない。 （STSをスルーしていないのなら別だがｗ） >>651が二階の言語の例である二階算術を使う「逆数学」に言及しているが 「...のと同じこと」と距離をおいた書き方をしている。 >「超準解析で表れるような」実数、実数値関数などなどのsortを持つ言語で十分だろ？ という話から「二階」が話題になっているのだから、 「二階実数論」を想像するのなら分かるんだが、 どこから二階算術が出てきたんだ？ 二階の言語なんてどんなものにも定義出来る。 イデアルの話をしたければ通常の環の言語の２階拡大で十分。 671 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 03:03:19.58 ] Spec R（R:可換環）に位相を入れる話が それで自然にできる？ 672 名前：１３２人目の素数さん [2012/09/06(木) 04:39:40.73 ] umu 673 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 05:28:08.30 ] >>651 ｘが集合のときｘ∪{ｘ}も集合って、集合の直観に合ってる？ 「要素も集合」より要素と集合がはっきり分かれている方が「集合論」として自然でない？ 674 名前：STS446 [2012/09/06(木) 07:36:43.77 ] 二階算術は普通は2階の言語とはよばんゃろ。 2階の言語ってのは命題自体を量化可能な言語を言うんであって。 つまり命題を量化可能な2階述語論理のことやな。 二階算術は多領域論理の一種としてみられる。 高階算術で型理論が使われているが これは領域の分類のための識別子として用いられている。 675 名前：STS446 [2012/09/06(木) 08:13:42.50 ] 2階算術なんかは本来は2階の言語とかではなく Γ^1_n級とかいう。（ΓはΣやΠやΔの一般化） 3階算術ならΓ^2_n級、ｎ階算術についてΓ^(ｎ-1)_n級になる。 例えば2階算術で有名なBig Fiveは、 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_1-分離公理 ほら、かなり人工的だろ？ 公理の重複を許して同値な体系に置き換えてみるともっとよくわかる。 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理＋Σ^1_1-分離公理 ほら人工的だろ？ ちなみに Q＋Σ^0_n-帰納法 だけなら限定算術のIΣ^0_nになる。 帰納法は厳密には4種類あって、BΣ^0_nなどになったりする。 676 名前：STS446 [2012/09/06(木) 08:15:45.39 ] >>675訂正 ＞3階算術ならΓ^2_n級、ｎ階算術についてΓ^(ｎ-1)_n級になる。 　3階算術ならΓ^2_n級、ｎ階算術についてΓ^2_(ｎ-1)級になる。 677 名前：STS446 [2012/09/06(木) 08:33:44.30 ] ちなみに体系の同値性を≡であらわすと以下の等式が成り立つ。 Π^0_1-分離公理 ≡ Σ^0_1-選択公理 ≡ Σ^0_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理 Σ^0_1-分離公理 ≡ Π^0_1-選択公理 ≡ Π^0_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-分離公理 Π^2_1-分離公理 ≡ Σ^2_1-選択公理 ≡ Σ^2_1-従属選択公理 ≡ Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理 いやぁ中途半端で不思議な定理だよね。 帰納法とか内包公理とか選択公理とか従属選択公理とか分離公理なんてのはこうやって定量化するんだよね。 678 名前：STS446 [2012/09/06(木) 08:35:51.26 ] >>675訂正 ＞Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理 ＞Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^1_0-内包公理＋Π^1_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理 Q＋Σ^0_1-帰納法＋Δ^0_1-内包公理＋Σ^0_1-内包公理＋Π^1_1-内包公理 679 名前：STS446 [2012/09/06(木) 08:42:13.96 ] >>673 あんたは集合論で冪集合使わんのか？ 680 名前：１３２人目の素数さん mailto:sage [2012/09/06(木) 17:58:38.80 ] ぽっぽの意味不明なカキコミを禁止する方法はないものか 681 名前：STS446 [2012/09/07(金) 07:15:41.68 ] とはいっても算術的階層とか解析的階層とかって あんまり論理式を測る尺度として優れているとも思えんのだけれどもね。 そこから何か非自明な結果が出てきたともきかんしねん。 682 名前：STS446 [2012/09/07(金) 18:32:20.04 ] >>680 意味が分かるように日々学習を怠らないって選択肢は考え付かないかな？ まずは再帰理論もしくは計算論という名の分野の学習を薦める。 CooperのComputable Theroyって本が出てるから良かったら買うと良いよ。 日本語のPDFでも結構東北大の田中さんがいいものを書いてるから読んでみな。 最終的には相対化された算術的階層などが登場する。 言語の階層の最下部には計算量理論が存在していて チョムスキー階層や多項式時間階層や非決定性の時間空間階層がある。 上に行くと原始再帰的クラス、一般再帰的クラスがあり、 ここから算術的階層がはじまって上に行くにつれてウルフラムの階層や 限定算術的階層やらブール階層やらが登場、 やがて解析的階層に突入してそれらが様々な理論に相対化されてゆく。 そこから上はどれだけ強力な理論を使うかに依存しており、 公理的集合論だとかさまざま巨大基数の追加した体形への相対化が考えられ、 やがて最高峰に矛盾した体形への相対化が存在する。 有限モデル理論における記述計算量理論とかも覚えておくと良い。 PvsNP問題を限定算術的階層に対応させて解決しようと言う試みもある。 日々精進、自戒とアドバイスの二重の意味を込めてね。 683 名前：１３２人目の素数さん mailto:sage [2012/09/07(金) 20:21:04.83 ] いや普通の人は自分と会話したりしないから

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef