- 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/
- 722 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 00:25:30.01 ]
- 実数以外に実関数に関する量化を考えているのだから、
たとえば任意の関数 f が与えられたときに別の関数 g := F(f) が存在してA(f, g)が成り立つ、
（たとえば「任意の連続関数に対してそのフーリエ変換が存在する」とか）、
みたいなものも出て来るわけで、「どんな概念でも」というのはおかしいと思うんだけど。
それに実数値のみに関する量化を考えても、かなり強い形の
選択公理が公理として入っていないと同値にならない。
- 723 名前：１３２人目の素数さん [2012/09/11(火) 00:43:45.05 ]
- 何か年内にとんでもない事態が
発生するんじゃないか？
最近そんな夢ばかり見る。
- 724 名前：１３２人目の素数さん [2012/09/11(火) 01:20:15.93 ]
- , '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
- 725 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 02:43:00.35 ]
- >実数以外に実関数に関する量化を考えているのだから、
>たとえば任意の関数 f が与えられたときに別の関数 g := F(f) が存在してA(f, g)が成り立つ、
>（たとえば「任意の連続関数に対してそのフーリエ変換が存在する」とか）、
>みたいなものも出て来るわけで、「どんな概念でも」というのはおかしいと思うんだけど。
実数値関数は考えてもよくて実数値関数の関数は考えてはいけないの？
超準解析をやるときは普通は任意の有限階の関数考えると思うけど。
>それに実数値のみに関する量化を考えても、かなり強い形の
>選択公理が公理として入っていないと同値にならない。
あれー、これまで「普通の数学では」って言ってなかった？
「普通の数学」で選択公理は認めるんじゃないの？
教養の授業では連続と一様連続の違いをδ(ｘ,ε)とδ(ε)関数使って教えてたけどね。
都合が悪くなると基礎論の考え方持ち出すのかな？
- 726 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 04:51:19.76 ]
- 普通の数学の議論をロジックの言葉で表現してみるとって話なんだから
選択公理を認めるのは確かに当然だ罠
- 727 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 12:11:59.33 ]
- >>722はスコーレム化とか勉強しとくべきだな。
- 728 名前：TTT [2012/09/11(火) 18:30:35.34 ]
- 衝撃的な事実が判明した。
つまりメレオロジーは現代で言う記述集合論なのだ！
- 729 名前：TTT [2012/09/11(火) 18:32:37.69 ]
- 基本的にメレオロジーとかでやりたい部分ってのは
位相にうまく論理学をのせるという話しだったが、
記述集合論は集合位相から測度まですべてを統括してしまったのだ。
- 730 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 19:21:38.77 ]
- TTTって桟橋みたいでかっこ悪い
- 731 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 19:34:59.62 ]
- まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、
どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。
その時点で、既にメタ数学的な基礎論の話であって、普通の数学の話ではない。
その上で、別に選択公理を認めちゃいけない、と言っているのではなくて、
∀ｘ∃ｙが∃ｆ∀ｘに変わってしまうから問題だ、と言っても
「そういう操作を可能にする公理を採用してしまっているのなら」当然でしょ、という話で。
私は725さんと違って超準解析についてこれは普通のやり方、これは別法、
これは普通じゃないやり方だ、と言えるくらいいろいろ知っている訳じゃない。
それでも、言語を決めてそのモデルを考えることはどのformulationでもやるけど、
関数の関数の関数に対しての選択公理とかの公理を数え上げて、
一つの理論として考えるということは（個人的には）あまりやらない気がするんだけど。
超準解析では普通many-sortedな言語で任意の有限階の関数考える、というのは
あなたが勉強した本ではそうなっていました、というだけの話じゃないの？
- 732 名前：TTT [2012/09/11(火) 20:24:16.69 ]
- >>731
＞まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、
＞どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。
＞その時点で、既にメタ数学的な基礎論の話であって、普通の数学の話ではない。
本来Σ2論理式はメタ理論的な定義だよ。
ある理論Tと論理式Fを持ってきて、
FがTの定理であるかを判定することが計算可能か、再帰的加算かというメタ定理がある。
これらのメタ定理がΔ1とかΣ1とか呼ばれる。
そしてそのメタ定理そのものを判定するメタ定理をΣ2とかΣ3とかで定義するわけさ。
だから「どの理論の上でのΣ2論理式なのかが問題になる」というよりも、
ある理論が「Σ2論理式を表現できるか否か」が問題なわけです。
- 733 名前：１３２人目の素数さん mailto:sage [2012/09/11(火) 22:50:56.37 ]
- TTTって桟橋みたいでかっこ悪い
- 734 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 04:22:27.63 ]
- >>731
お前が自分の用語法をはっきり説明できればいいだけ。
お前が意味不明な用語法（実数と実数値関数がある言語でΣnとか）使ったから
みんなでなんとか補完して意味を取ろうとしてるがうまく行かないと議論している。
お前がきちんと説明できればいいだけのことだ。
- 735 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 14:05:09.92 ]
- >まず、Σ2の形の論理式と同値であることが示せる論理式を全てΣ2論理式扱いする用語法では、
>どの理論の上でのΣ2論理式なのかが問題になる。だから理論が少し違えば違う概念になる。
通常の数学で出てくる概念はどれだけ複雑になるかって話だったと思うが、
通常の数学では同値で区別しない概念を区別して論理式の選択によって複雑さが変わるのなら
Π3とか複雑になるのは簡単に書ける概念なのにわざわざ複雑になる論理式を選んだから当然という以上のものではない。
普通の数学で区別しない概念を同じ複雑さにするには、
通常の数学で認めるもの（選択公理など）が含まれる理論の上での同値を考えるのは当然だろう。
（理論を設定してその上での同値を考えるという君の好きな考え方に立てば。
数学的には同値だが、「標準的」なモデルでの同値で考えてもいいので。）
普通の数学を反映していない理論を持ち出した反論にどんな意味があるんだね？
>超準解析では普通many-sortedな言語で任意の有限階の関数考える、というのは
>あなたが勉強した本ではそうなっていました、というだけの話じゃないの？
部分集合や関数が出てくる普通の数学を表現できる言語として
「超準解析でやるような」言語を君（ら）が出してきたと記憶しているが、
それが君の言うとおり関数の関数（汎関数）も表現できないような言語だったら
そもそも「定式化をしづらいような性質・対象も平気で考える」普通の数学を
表現できないことになるんだがね。
- 736 名前：１３２人目の素数さん [2012/09/12(水) 19:13:03.88 ]
- ABC予想は証明されたのか。
京大数理研の望月新一さんの５００ページの大論文についての、
ネイチャー誌のニュース記事：
「もし正しければ、２１世紀数学の最も驚くべき成果の一つとなるであろう」
www.nature.com/news/proof-claimed-for-deep-connection-between-primes-1.11378
- 737 名前：TTT [2012/09/12(水) 19:20:08.90 ]
- 補足しとくけど、論理的同値な命題はすべて同じ算術的階層だよ。
算術的階層を定義するときに、対象の論理式の量化子の繰り返しを直接数えるのでなく、
対象の論理式と論理的同値な論理式の量化子の繰り返しを数えるとなっているから。
例えばダミー量化子付きの命題とそれを外した命題があったとき、
それらは論理的に同値だから量命題は階層を共有する。
Σ3とΠ2だったらそれぞれΣ3かつΠ2になる。
そうすると∃∀∃文がΠ2になるし∀∃文がΣ3になる。
それからチャーチの提唱で計算側に移ろう。
ある命題がチューリング機械でYesかNoで判定が可能なこと、
ある命題がチューリング機械でYesの判定だけが可能なこと、
ある命題がチューリング機械でYesかNoで判定が可能かどうかをYesかNoで判定可能なこと、...。
計算可能な集合のジャンプの階数 ＜----＞ 算術的階層
- 738 名前：TTT [2012/09/12(水) 20:27:11.50 ]
- そうだな、ΣｎとΠｎがメタ理論上の概念であることの分かりやすい例をあげよう。
存在例化限定2階述語論理では∀文が全く証明できない。
とはいえ、この場合は例えば存在例化限定2階述語論理における論理式が、
2階述語論理でΠｎとなる論理式である場合は、この∀文はΠｎとなる。
また別の例がある。
Tで∀ｘ∃ｙ（ｘ＜ｙ）が証明可能で、∃ｙ∀ｘR（ｘ、ｙ）が証明不可能としよう。
そして、Tの拡大T'で、∀ｘ∃ｙR（ｘ、ｙ）＜--＞∃ｙ∀ｘR（ｘ、ｙ）が証明可能としよう。
するとT'で∀ｘ∃ｙR（ｘ、ｙ）がΔ2になる。
これはTではΔ2ではないというか？
否、TにおいてもΔ2なのである。
- 739 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 23:21:25.39 ]
- いや、あなたが∀ｘ∃ｙで始まる論理式と∃ｆ∀ｘで始まる論理式が同値になるから
全ての論理式はΣ2になってしまう、と言ったんでしょ。
これは「Σ2の形の論理式と同値であることが示せる論理式を
全てΣ2論理式扱いする用語法」だと思う
（私にはそうとしかとれないけど、もし違うなら違うと言ってください）。
一方であくまで冠頭標準形の形だけに注目する定義の仕方もあって、
算術に関する本でもそういう定義をしていることは普通にある。
PA-Σ1論理式、Q-Σ1論理式、IΣi-Σ1論理式とか
ZF-Σ1論理式、ZFC-Σ1論理式、ZFC+「Mahlo基数の存在」-Σ1論理式とか
そういう風に似たようで少し違う概念が山のように出て来ても困る場合だって普通にあるでしょう？
私はこっちの流儀で考えている。それだけの話。
数学的な公理と、論理記号や等号に関する純粋に論理的な公理には身分の違いがある。
論理に関する公理だけを用いて冠頭標準形に直せることには意味がある。
これは私は、通常の数学がどうとかいう問題じゃなくて、普通の数学でも
数学的な公理なのか純粋に論理的な帰結なのかは一応区別すると思う。
- 740 名前：１３２人目の素数さん mailto:sage [2012/09/12(水) 23:33:42.66 ]
- Σ1⊂Σ2⊂Σ3⊂Σ4⊂…
- 741 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 03:27:34.85 ]
- >>739は>>735の後半への反論は諦めたの？前半にしか反論してないけど
- 742 名前：TTT [2012/09/13(木) 08:01:51.00 ]
- >>739
例えば理論Ｔの中に、∃ｘＲ（ｘ）があったとして、
述語Ｑで、∃ｙＲ（ｘ、ｙ）＜--＞Ｑ（ｘ）となっているとすると、
Ｔ-Σ1論理式を考えると、∃ｙＲ（ｘ、ｙ）が証明不可能なので、
Ｑ（ｘ）も証明不可能となって結局丸く収まるんですね。
ですから一つの算術的体系の中だけならば冠頭標準形の形だけに注目しても問題ないわけなんです。
しかしこの定義ではメタ理論に広げると、Σ1＜--＞Σ0となりおかしくなってくるわけですね。
こういった定義は個別の体系内での狭い議論でしか通用しないんです。
- 743 名前：TTT [2012/09/13(木) 08:17:18.19 ]
- とはいえ通常の算術階層は
述語ＲやＱがΔ1であることを仮定していますから、
「冠頭標準形の形だけに注目する定義の仕方」
がどういったものかによりますが。
もしも述語部分がΔ1ならば、同値な定義はすべて同じ階層という私の定義と同じものでしょう。
そうでないなら同一体系内でしか使えない狭い定義でしょう（そんなものは見たことありませんがね）。
- 744 名前：TTT [2012/09/13(木) 08:41:12.95 ]
- >>743
それよりも計算量クラスがもうすぐ500種類を超えそうですな。
qwiki.stanford.edu/index.php/Complexity_Zoo
これからは、Δ1より下側の時代ですよね。
算術的階層など古い古い。
- 745 名前：TTT [2012/09/13(木) 10:48:30.22 ]
- >>744
私も何回かワード使って全体像をマッピングしようと試みたんですが。
Ａ３で入りませんね、図面用の紙幅じゃないと駄目でした。
数学者どもが次数構造とか二階算術とか巨大基数のマッピングに
現をぬかしている間に計算機屋どもが物凄い勢いでマッピングを広げちゃった。
だから数学者はΔ1より下は怖くて触れない。
Δ1より上と違ってシンプルじゃないんだよ。
- 746 名前：１３２人目の素数さん [2012/09/13(木) 12:21:53.09 ]
- >>743-745
なにこれこわい
- 747 名前：TTT [2012/09/13(木) 13:25:12.16 ]
- >>745
ここにマッピングがあるね。
www.math.wisc.edu/~jmiller/Menagerie/ComplexityZoo.pdf
ＰｖｓＮＰとかの同値性が示されたら一気に階層が潰れる可能性もあるけど。
色つきなんかで見るとわかり易い
www.math.ucdavis.edu/~greg/zoology/diagram.xml
ただし再帰理論なんかもランダムネスなんかが登場してかなり大きくなってきた。
www.math.wisc.edu/~jmiller/Menagerie/bn1g.png
www.math.wisc.edu/~jmiller/Menagerie/bn1g.pdf
それに逆数学＆限定算術も結構頑張ってかなりのリスト化が完成した。
math.berkeley.edu/~damir/zoo/just_rm.pdf
図式も一つじゃおさまらないレベルに到達してるしね。
math.berkeley.edu/~damir/zoo/diag_rm.pdf
math.berkeley.edu/~damir/zoo/diag_rm_om.pdf
math.berkeley.edu/~damir/zoo/diag_rm_non.pdf
math.berkeley.edu/~damir/zoo/diag_rm_weak.pdf
math.berkeley.edu/~damir/zoo/diag_hs_2007.pdf
math.berkeley.edu/~damir/zoo/diag_dh_2009.pdf
意外と頑張ってるのが様相論理かな。
home.utah.edu/~nahaj/logic/structures/systems/
巨大基数は頑張りが足りないかな？
websupport1.citytech.cuny.edu/faculty/vgitman/images/diagram.jpg
- 748 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 14:21:11.17 ]
- >>739
>数学的な公理と、論理記号や等号に関する純粋に論理的な公理には身分の違いがある。
>論理に関する公理だけを用いて冠頭標準形に直せることには意味がある。
>これは私は、通常の数学がどうとかいう問題じゃなくて、普通の数学でも
>数学的な公理なのか純粋に論理的な帰結なのかは一応区別すると思う。
特に後半の一文は何を言いたいのか分からないのだけれども
∀∃で定義した連続性と modulus f continuity で定義した連続性が
別の概念であるという「普通の数学者」がいたら連れてきて欲しい。
彼らは論理式で表してから概念を把握するのではない。
概念が先にあってそれを基礎論屋が論理式で表示してるんであって
論理的公理だけで同値だったら同一の概念、
数学的公理が必要なら別の概念などと考えているわけじゃない。
- 749 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 18:14:08.62 ]
- つーか選択公理を論理的公理ではなく数学的公理とするのが標準的になったのは
ロジック業界でもかなり後になってからじゃないの？
ε計算とかあった（いまでも研究されてるのかもだけど）わけだし。
ロジシャンの間でも定まってなかった論理的公理と数学的公理の区別なんて
「普通の数学者」にとっては知ったことではないんじゃない？
- 750 名前：TTT [2012/09/13(木) 18:47:28.61 ]
- >>743
＞とはいえ通常の算術階層は
＞述語ＲやＱがΔ1であることを仮定していますから、
これは再帰理論での定義だねΔ1ってか計算可能関係で定義される。
構文論的に定義する場合は再帰的にＲがΣｎのとき∀ｘＲ（ｘ）がΠｎ＋1と定義する。
レヴィの階層とか言われている。
数学の命題ってのは集合論だとほとんどがΔ0とかΔ1になるね。
Δ1以下にならないと任意の推移的可算モデルで充足しないからね。
濃度とかモデルとか射影階層に言及すると一気に階層が上がるけどね。
- 751 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 18:52:45.03 ]
- 少し前に話題になってた論理主義は選択公理どころか
ヒュームの原理を使って算術を論理的公理から導くとか
果ては集合論すら論理的公理に還元できるとかいう主張
- 752 名前：TTT [2012/09/13(木) 19:26:23.18 ]
- そもそも数学と論理の公理ははじめ混同されてた。
ヒルベルトが一階論理を抽出したころには、
選択公理は整列可能定理やツォルンの補題との同値性もわかっていて
普通に数学の定理だった。
論理学の公理だと思われていた時代なんてないだろうな。
- 753 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine.co.jp [2012/09/13(木) 19:48:42.41 ]
-
お前たちは、定職に就くのが先決だろがああああああああああああああ！！！！！！！！！！！！！！！！！！！！！！！！
ニート・無職の、ゴミ・クズ・カス・無能・虫けらのクソガキどもがあああああああああああ！！！！！！！！！！！！！！！！！！！！！！！！！！！！！
- 754 名前：TTT [2012/09/13(木) 20:17:53.93 ]
- あと例の新論理主義者共が狙っていたのは
自然数の論理学的還元で
2階述語論理＋ヒュームの原理はペアノ算術より弱いからね。
- 755 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 20:58:42.54 ]
- これだけ書いても誰にも相手して貰えないってのは
逆人徳がすごすぎると思う
って言うか出だしが出落ちに近かったから今更誰にも相手にしてもらえなくても
しょうがないよな
- 756 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 21:51:05.55 ]
- 2ちゃんでコテ名乗るようなやつは、実社会で認められることが少ないやつ。さらに自演なんかする奴に至ってはほとんど病気だわな。
数学板なんかよりVIPとかの方が相手してもらえるよ。さあいったいった。
- 757 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 23:19:24.52 ]
- なんでTTTは自分と会話してるんだ
精神異常者なのか？
- 758 名前：１３２人目の素数さん mailto:sage [2012/09/13(木) 23:49:37.06 ]
- 博士の愛したなんとかと同じ病気なんじゃね？
- 759 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 00:26:55.65 ]
- そだ |------､｀⌒ｰ--､
れが |ﾊ{{ }} ）））ヽ､l l ハ
が |､{ ﾊリﾉﾉﾉﾉﾉﾉ）､ l l
い |ヽヽｰ､彡彡ﾉﾉﾉ} に
い |ヾヾヾヾヾヽ彡彡} や
!! /:.:.:.ヾヾヾヾヽ彡彡} l っ
＼＿＿／{ l ii | l|} ﾊ､ヾ} ﾐ彡ﾄ
彡ｼ ,ｪ､､､ヾ{{ヽ} l|l ｨｪ=ﾘ､シ} |l
lミ{ ﾞｲｼﾓ'ﾃ､ミヽ}ｼｨ=ﾗ'ｧ､ }ﾐ}} l
ヾﾐ ￣~'ｨ''': |ﾞ:ｰ.￣ lﾉ/l | |
ヾヾ " : : !､ ｀ lｲﾉ l| |
>lﾞ､ ｰ､,'ｿ /.|}､ l| |
:.lヽ ヽ ｰ_ ‐-‐ｧ' /::ﾉl ﾄ､
:.:.:.:＼ヽ 二" /::// /:.:.l:.:.
:.:.:.:.:.::ヽ:＼ /::://:.:,':.:..:l:.:.
;.;.;.;.;;.:.:.:.＼｀ｰ-- '" //:.:.:;l:.:.:.:l:.:
- 760 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 01:58:05.11 ]
- ε計算はいまでも研究されている：
www.sciencedirect.com/science/article/pii/S0168007212000802
ヒルベルトによって導入されたらしいな。
- 761 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 06:32:28.89 ]
- ε計算(Epsilon calculus)は確かに通常よりも強い形の選択公理を含んだ論理体系と言えるだろうね。
これに限らず証明論でよく使われるω規則を含んだω論理（WoodinのΩ論理ではなく）なんかも
このω規則は論理的公理の側面と数学的公理の側面があって両者の「身分の違い」ははっきりしない。
最近の入門書では論理的公理と数学的公理の区別が本によって食い違うことは（等号公理の扱いを除けば）ないだろうけど
そこから少し発展した内容を勉強してみるとその区別は結構曖昧なものだと気づかされると思うよ。
- 762 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 07:24:21.09 ]
- >>739が言ってるのは論理式だけを見て複雑さを定義して論理式間の同値を考慮しないって話で
>>748は「数学的な概念」（＝論理式の同値類？）に対して複雑さを定義しなければいけないって話ではないかと。
「普通の数学に表れる」と言ったときにどちらがまともかは言わずもがなだと思う。
前者の意味で複雑になってもそれは数ある論理式の表現の仕方の中でわざわざ複雑なものを選んできたからに過ぎず意味がないことになるわけで。
>>739は用語法の違いってことで逃げようとしているけど、場にそぐわない用語法持ち出しても正当化にはならないと思う。
なんか上の方のレスと同じこと言ってるけど。
- 763 名前：⊥⊥⊥ [2012/09/14(金) 11:43:58.16 ]
- >>744
ただしその中のほとんどが不当に水増しされた階層だということに注意。
例えばＥＥＥはＤＴＩＭＥ(2^2^2^o(n))といった具合に、
大抵はDTIMEやDSPACEの言い換えでしかない場合が多い。
こういった記述の仕方が素人への可読性を低下させている疑惑もある。
計算量ではそのクラスの特性に見合った名称をつける場合があるが、
これによって直感的な階層の高低の把握が邪魔されていることが多々ある。
- 764 名前：TTT [2012/09/14(金) 12:22:36.90 ]
- 基本的に決定性と非決定性（確率やランダム）なチューリング機械を
領域と時間で組合せ論的に作って分類しているだけだから。
それにオラクルを用いたものや論理体系の表現能力を組み合わせた図式だね。
確かに名称のせいで何をやっているのか分からくなってるね。
- 765 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 14:44:49.84 ]
- >>762
なるほど。つまり
「たとえば有界な関数が〜〜と言っただけで、
（実数論として）Σ2の式が出て来るんだから
Σ3くらいの量化は普通に考えることになる」
というのはΣ2の式でも表現できるのに
あえてΣ3の論理式で表現したからΣ3の量化が出てきた
と>>739は言ってるわけね。
- 766 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 16:08:04.04 ]
- おまいら執拗すぐる。739の言い分がナンセンスだってのはもう十分分ったから。
- 767 名前：１３２人目の素数さん mailto:sage [2012/09/14(金) 17:01:39.61 ]
- じゃあ普通の数学を形式化したら多重量化はほとんど出て来ないって言いたい訳ね？
- 768 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 19:18:35.22 ]
- ∃ｘ(ｘ＝ｘ)とか、等号がない場合には∃ｘ(Ａ∨¬Ａ)って論理的公理？
- 769 名前：TTT [2012/09/15(土) 20:21:26.72 ]
- Ａが述語変数なら論理公理（どういった公理の論理体系かによるけど）ですね。
述語が定数になると理論固有の公理になります。
- 770 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 20:31:57.82 ]
- たとえそれと同値な論理式が公理に入っていたとしても
その論理式自身が公理に入ってなければ公理とは言わない
- 771 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 20:37:02.31 ]
- もし∃ｘ(ｘ＝ｘ)が論理公理なら
ＺＦＣの公理に空集合公理は要らないのでは？
分出公理があれば空集合公理は導けるはず
- 772 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 21:03:19.23 ]
- >>771
どうやって導くの？
- 773 名前：１３２人目の素数さん mailto:sage [2012/09/15(土) 22:04:43.91 ]
- どうも767もスルー対象に認定されたようだなｗ
専門用語を正しく使えないゆとり君は専門板の専門スレなんか来ちゃダメ。
- 774 名前：１３２人目の素数さん [2012/09/15(土) 22:22:24.27 ]
- __ﾉ)-'´￣￣`ｰ- ､_
, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
- 775 名前：TTT [2012/09/15(土) 22:40:45.68 ]
- >>768
あなたの提示した論理式は、恐らく一階述語論理のものでしょうが、
一階述語論理の公理はいくつものタイプが考えられるんです。
基本的にそれらが証明する論理式はすべて同じなんですが、
何を公理とするかは決まっていないんです。
- 776 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 00:08:02.26 ]
- >>761
等号公理に限らず、∃ｘ(ｘ＝ｘ)みたいなのでも食い違うのでは？
論理的公理（から導れること）と数学的公理（同）の区別は今でも流儀によるでしょう。
「普通の数学でも数学的な公理なのか純粋に論理的な帰結なのかは一応区別する」なんてのは論外で。
- 777 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 10:39:46.03 ]
-
- 778 名前：１３２人目の素数さん [2012/09/16(日) 12:38:40.63 ]
- __ﾉ)-'´￣￣`ｰ- ､_
, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
- 779 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 12:49:43.76 ]
- >>772の回答は？
- 780 名前：１３２人目の素数さん [2012/09/16(日) 15:20:10.21 ]
- ∃ｘ(ｘ＝ｘ)は等号付き一階述語論理の論理的公理だけで出てくるよ。
空集合公理は内包性公理だけで出る。
内包性公理の任意論理式にｘ≠ｘを入れるだけ。
逆に等号なし一階述語論理でもZFCによって等号と同等のものが使えるようにもなる。
∀ｘ∀ｙ（∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｙ）-＞ｘ＝ｙ）
∀ｘ∀ｙ（-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｙ））
ｘ≠ｘ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ）
内包性図式により
∃ｙ∀ｘ（ｘ∊ｙ＜--＞ｘ∊ｚ∧ｘ≠ｘ）
∀ｘ（ｘ∊ｙ＜--＞ｘ∊ｚ∧ｘ≠ｘ）
よって
ｘ≠ｘ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ）
ｘ∊ｚ∧ｘ∊ｙ-＞∀ｚ（ｚ∊ｘ＜--＞ｚ∊ｘ）
- 781 名前：TTT [2012/09/16(日) 15:24:09.42 ]
- >>780
の下半分の論理式はミス
- 782 名前：TTT [2012/09/16(日) 16:15:44.19 ]
- とはいえ内包性（分出）公理は見かけ上だけなので
実際には外延性公理によるユニーク性をもって
空集合が定義されたとする見方も多い。
さらに分出公理中の集合は無限公理で得られる集合を使う必要がある。
無限公理でなくとも集合の存在を示す∃ｘ(ｘ＝ｘ)を使うことが出来る。
例えこれが論理公理でも見かけ上区別できないから問題ない。
そこから>>771の発言が来ているのだろう。
- 783 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 16:16:14.54 ]
- 他の人がちゃんとスルーできるようにコテ付けとけ
- 784 名前：１３２人目の素数さん mailto:sage [2012/09/16(日) 18:23:02.31 ]
- ZFCだったら∃ｘ(ｘ＝ｘ)が純粋な論理的帰結であろうとなかろうと
無限公理Infと分出公理から空集合の存在は示せるので空集合公理は冗長。
集合論の入門書ではZF(C)-Infなども考えるから入れているんだと思う。
それでも∃ｘ(ｘ＝ｘ)がいえれば不要な訳で
∀xA(x) -> ∃xA(x) が論理的帰結になる自然演繹やヒルベルト流体系の入門書とは
異なる立場に立っているというか、
少なくとも∃ｘ(ｘ＝ｘ)の身分に関して中立であろうとしているといえると思う。
- 785 名前：１３２人目の素数さん [2012/09/16(日) 21:53:42.62 ]
- __ﾉ)-'´￣￣`ｰ- ､_
, '´ _. -‐'''"二ニﾆ=-`ヽ、
／ ／:::::; -‐''" `ｰノ
/ ／:::::／ ＼
/ /::::::/ | | | |
| |:::::/ / | | | | | |
| |::/ / / | | || | | ,ﾊ .| ,ﾊ|
| |/ / / /| ,ﾊﾉ| /|ﾉﾚ,ﾆ|ﾙ'
| | | / / ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/ 私は只の数ヲタなんかとは付き合わないわ。
. | ＼ ∠イ ,ｲイ| ,`-' | 頭が良くて数学が出来てかっこいい人。それが必要条件よ。
| l＾,人| ` `-' ゝ | さらに Ann.of Math に論文書けば十分条件にもなるわよ。
| ` -'＼ ｰ' 人 一番嫌いなのは論文数を増やすためにくだらない論文を書いて
| /(l ＿＿／ ヽ、 良い論文の出版を遅らせるお馬鹿な人。
| （:::::`‐-､__ |::::`､ ﾋﾆﾆヽ、 あなたの論文が Ann of Math に accept される確率は?
| ／ `‐-､::::::::::`‐-､::::＼ /,ﾆﾆ､＼ それとも最近は Inv. Math. の方が上かしら？
| |::::::::::::::::::|` -､:::::::,ﾍ￣|'､ ﾋﾆ二、 ＼
. | /::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ | '､ ＼
| /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ ヽ、 |
| |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ /:＼__/‐､
| |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::| く:::::::::::::￣|
| /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
| |／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
| /:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/
- 786 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 05:38:24.54 ]
- ∀xA(x) -> ∃xA(x) が論理的帰結にならないような証明体系ってどんなのがあるの？
- 787 名前：１３２人目の素数さん [2012/09/17(月) 08:44:05.78 ]
- レベル堕ちたなこのスレ
- 788 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 14:32:19.88 ]
- >>786
∀xA(x) -> ∃xA(x) や、同じことだけど∃ｘ(ｘ＝ｘ)を妥当式にしない流儀は
空な構造も含めたいっていうモデル理論的観点からの場合が多い。
だから証明体系と言っていいのかだけど、
空構造を許す意味論での妥当式はすべて公理というようなモデル理論的に定義した体系が
「よく出てくる例」になるんじゃないかな。
- 789 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 16:06:19.02 ]
- >>72
＞形式体系ZFCを外側から見たメタレベルでは
＞１、φが証明可能である
＞２、φの否定が証明可能である
＞３、φは独立である
＞４、ZFCが矛盾している
＞のいずれかである。
４が正しいなら１も２も正しくなるがね
逆にいえば、４でない場合に限り、任意の命題φについて
１，２，３の３つの場合がありえるというわけだ。
ところで実は、４でない場合、４を示すつもりのZFCの命題が３になる。
ここでわざわざ「つもり」と書いたのは、ZFC内では、ZFCの無矛盾性を
完全に表現できないのである。つまり、ZFCが無矛盾であっても、
それを表わしたつもりの式が偽となるモデルが存在し得るわけだ。
- 790 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 16:20:49.38 ]
- 「PAはモデルをもつ。したがって、完全性定理により無矛盾である。」
これって正しいですか？
- 791 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 17:26:00.91 ]
- 話題を無理やり切り替えるために昔のネタを引っ張り出してきた？
- 792 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 18:53:44.41 ]
- >>786
きっとTTTが、君の求めるような体系について
半分正しくて半分勘違いに基づいた解説をしてくれるだろうよ。
色んな体系の解説を沢山読んではいるようだから。
読んだからって勘違いだらけなのは見ての通りだがｗｗ
- 793 名前：１３２人目の素数さん mailto:sage [2012/09/17(月) 19:11:55.00 ]
- 人を貶すしか能のない792みたいなのはどうにかならんのかなあ
786の質問のどこに792みたいに言われなきゃならない要素があるんだか
- 794 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 16:45:31.20 ]
- >>784 >>788
集合論やモデル理論の人は∀xA(x)→∃xA(x)や∃ｘ(ｘ＝ｘ)を恒真とは考えないってことですか？
- 795 名前：TTT [2012/09/18(火) 22:53:11.57 ]
- >>794
∀xA(x)→∃xA(x)は恒真になる。
∃ｘ(ｘ＝ｘ)は述語論理の式なので恒真じゃない。
- 796 名前：１３２人目の素数さん [2012/09/18(火) 23:00:50.33 ]
- 韓国を国際司法裁判所へ引きずり出す署名へご協力ください
staff.texas-daddy.com/
半角英数で本名でお願いします、漢字とかイニシャルはNGです
違うアドレスで家族の名前でもおkです ステアドでもおｋ
台湾の人も署名してくれてます
日本政府に圧力をかけましょう
- 797 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 23:29:34.53 ]
- いくら署名したって韓国政府の同意がなきゃ駄目なんじゃ
- 798 名前：１３２人目の素数さん mailto:sage [2012/09/18(火) 23:30:41.02 ]
- >述語論理の式なので恒真じゃない。
？
- 799 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 00:54:29.17 ]
- ZFCGってなに？
- 800 名前：800 mailto:sage [2012/09/19(水) 01:10:44.35 ]
- うそ 800
- 801 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 04:21:11.13 ]
- どこに書いてあったの？
たぶんその本なり論文なりに定義してあると思うよ
- 802 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 05:16:04.23 ]
- generalized Cantor hypothesis
- 803 名前：１３２人目の素数さん mailto:sage [2012/09/19(水) 06:15:57.18 ]
- >>794
集合論者はZFCの公理（上で言われているように弱めることはよくあるが）の下でしか考えない。
集合論の公理を全部取っ払うことはまずないので「数学的な公理なのか純粋に論理的な帰結なのか」なんて気にしない。
- 804 名前：TTT [2012/09/19(水) 09:31:04.95 ]
- >>798
恒真ってのは命題論理で個々の原始論理式の真偽値と無関係に式全体が真になることだから。
∃ｘ(ｘ＝ｘ)が真になるには、モデルの領域中にこの式を満たす個体がないと駄目。
|
 |
