| … |
つ[wikipedia] |
| … |
つ[天書の証明] |
| … |
>ひょっとしてZFや圏論からすべての数学領域を記述した論文ってないの? 通常の公理的集合論として扱われるZFCは、 [一階の述語論理]∧["∈"と"＝"についての規則としてのZFC] として、ほぼ全数学を形式的に記述する一面を持っているというだけ。そもそもそういう目的もあったから。 圏論も同様で、集合概念が対象の所属関係と半順序に注目したアイディアなのに対して、主に基礎論としての圏論は結合則と半順序に注目して形式化するもので、クラス概念を伴う集合論とは同程度に根源的記述が可能というだけ。 どちらにしても、数学の全分野を一編の論文に記述するのは膨大な労力と紙数を必要とし、すでに記述可能であることが分かっているほとんどの数学分野をワザワザ一編の論文にまとめる人はなかなかいない。 |
| … |
さらに、例えば[一階の述語論理]∧["∈"と"＝"についての規則としてのZFC]だけの形式的表現だけでは、現在当たり前のように使われている数学上のいくつかの表現は全てが表現できるわけではない。 例えば、ZFCでは真のクラス（固有クラス）概念は明示的に表現できない。だから、一階の述語論理の言語L（これも定義が無数にある）にはじめから入れておくのが楽だ。 また、そうやって組まれたZFC言語は一階述語論理なので、”すべての部分クラスにおいて〜〜”のような記述も表現できない。 これは二階以上の述語論理で表現できる。 しかしながら、数論、代数学、解析学、幾何学、などなどと大まかな大分野で区切ってみても、それらのほとんどすべてが、[一階の述語論理]∧["∈"と"＝"についての規則としてのZFC]で事足りる。 二階の言語を必要とする数学的言明は確かに無数に存在するが（そのため数学の自然な記述では皆が二階以上の述語論理を意識せずに使っている）、自然数と実数等によって組み上げられるおよそ全数学は、それらの二階の表現を今の所は回避して記述することが可能である。（厳密にはヘンキンの結果を参照） |
| … |
書き込みをした人によって削除されました |
| … |
そもそも、こういった質問が出るということはZFCがどんなものなのか学んだことすらないからだろう。 ZFCの概要は、形式によらない、やや正確ではない説明でまとめれば、次のようになる。 1：集合の同等はその所属関係の下方対象を比較した同等性によって決まる（外延性） 2：要素を一つも持たない集合が存在する（空集合） 3：x,yが集合のとき、それらだけを要素としてもつ対集合が存在する（対集合） 4：集合族からその和集合が作られる（和集合） 5：任意の集合からその部分集合全てからなる集合が作られる（べき集合） 6：空集合から帰納的に作られるある集合の列の全ての集まりも集合である（無限公理） 7：任意のx∈uとなる集合uにおいて、論理式ψ(x)を真とする要素だけを集めた集合vが存在する（内包公理図式） 8：x,yが集合で、ψ(x,y)は右一意的な”関数クラス”であるとき、ψ(x,y)を真にするyのみを集めた集まりもまた集合である（置換公理図式） 9：集合aが空でないなら、aの要素でa自身と共通部分を持たない要素xが集合として存在する（正則性公理） 10：選択公理（略） |
| … |
これらから、集合の順序n組（2つ組みなら順序対）を構成できて、和集合、2つ以上の集合の合併や、複数の集合の共通部分が作れる。 順序組を用いて、二項関係が作れれば、そのクラスに条件を付け加えて写像も構成できる。 ここまでくれば、代数も解析も幾何学も、ほぼ全分野がこの集合論言語の範囲で表現可能だとわかる。 |
| … |
基礎論の表現言語としての圏論も同様。 関数と集合（対象）の直積が定義できるように圏論言語の公理を定めれば、以下同様。 |
| … |
ついでに、時々巷に現れるが、「基礎論による数学の基礎付け」について書かれている書物の評で、「〜〜が説明されていない」、「〜〜は説明されているのにその先のこの概念は載っていない」とか文句を言う輩が時々いる。 挙げ句に「基礎論による説明程度では〜〜などというような現代数学の高度な概念は理解できない」などと結論づけたりする。 これは全く頓珍漢。 「あらゆる日常的に見られる物質が全て原子からなる」ということを説明した書物に飛行機や自動車の作り方が載っていないといって、文句をいうやつは馬鹿だろう。飛行機について知りたければ飛行機の専門書をあたればいい。 数学では、数学のあらゆる高度な構造物が、いずれもより基本的な概念による論理的な構造によって成り立っていて、それらの基本構造もより基本的な対象と構造に組み替えていけば、概ね集合論や圏論あたりで事足りるということを説明した理論が、基礎論のある一面だ。 こういう文句を言う連中は、そもそも数学の基本が分かっていないし、上っ面の衒学的な文言に妄想を抱いて拗らせているだけ。 |
| … |
書き込みをした人によって削除されました |
| … |
>つ[天書の証明] 全ての数学領域を記述はしてないし、ZFCや圏論による基礎づけを厳密に意識しているわけではない。 |
| … |
>ほぼ全数学を形式的に記述する一面を持っているというだけ。そもそもそういう目的もあったから。 基礎論って言うからそこから全ての数学が成り立っているって言う風に理解してたけど、単に様々な数学の領域に共通な部分が基礎論、って言う風にとらえた方がいいのかな? どのみち様々な数学領域はそれぞれ独自な定義や条件を導入して特殊化してるしね でもそうなると、そういう条件がZFや圏論の公理と会わない場合はどうなるんだろう? |
| … |
書き込みをした人によって削除されました |
| … |
書き込みをした人によって削除されました |
| … |
>そういう条件がZFや圏論の公理と会わない場合はどうなるんだろう? いや、ZFCや圏論の公理と矛盾する解析や代数幾何の概念はでてこないでしょ？ 全ての数学者がZFCの公理をその概要でも書き下せるわけじゃないけど、その論理的機能は頭に入っている。だから、基礎理論に矛盾するような理論は組まない。 組んだとしたら間違ってるんだよ。人間だから間違うこともあるけどね。 さっきも言ったけど、集合（クラス）論や圏論では順序組から関係の概念を基本的構造として構成し、それらが定まれば、基本的な代数も解析も、その先の表現論だの作用素環論だの、調和解析だのミラー対称性だの何だのも全て、ZFCと述語論理上に形式展開できる。 |
| … |
>どのみち様々な数学領域はそれぞれ独自な定義や条件を導入して特殊化してるしね これだって、その局所分野の独自の定義や条件はZFCなどの基礎理論と独立して定義されているわけじゃなくて、それらの定義や条件の形式表現もZFC言語で記述される。 まぁ強いて言えばZFCは固有クラスを直接は扱えないから、それが扱える別の公理的集合論（例えばBG)や固有クラスを対象として扱うことを始めから述語論理の言語で許可しておくと便利だけどね。 例えば群という基本構造ですら、「すべての群の集まり」はZFCの集合ではなく固有クラスになってしまう。 |
| … |
>基礎論って言うからそこから全ての数学が成り立っているって言う風に理解してたけど、単に様々な数学の領域に共通な部分が基礎論、って言う風にとらえた方がいいのかな? 「基礎論とはなんぞや」をその成り立ちから説明するとなると、今まで書いたレスよりずっと長くなるから止めておく。 ざっくり言えば、数理論理学（ML)によって既存の数学の全分野を形式化する一方で意味付けするという目標があって、それを実現する方法のなかで現在でも一応有力とされている方法として、「公理的方法」が選ばれているということ。 現在の意味では数理論理学≒数学基礎論として考えても、公理的集合論はその副産物に過ぎない。 ZFCのような公理的集合論が便利なのは、ZFC自体が公理（公理図式）の集まりなので、ZFC自体をZFC言語によって解析（解釈して調べる）事ができるという点。 |
| … |
書き込みをした人によって削除されました |
| … |
書き込みをした人によって削除されました |
| … |
数学基礎論は、論理や集合、圏などのおよそ数学全般を記述可能な基本ツールを提供する一方で、それらの基本ツールそのものの構造もそれらの基本ツールをメタにつかって研究する学問と考えればいい。 そして、ZFC+クラス言語から圏論が構築できるし、逆に圏論言語からZFCのモデルも構築できる。 つまり、数学の基礎付けの方法は一通りである必要すらない。 しかし、集合論から始めた数学も、圏論言語から始めた数学もその機能はおなじになるように組まれている。 そもそも数学の定理導出に使われる述語論理が共通しているから、数理論理や基礎論以外の数学分野で現れる、より構造階層が上の高度な数学的構造物も、述語論理には矛盾してはならない。 大雑把に言えば、ZFCを基礎においているといっても、述語論理上の言語に∈と＝の規則を加えただけだから。 そして、カントールの慧眼は∈による構造の射程が、およそ数学のすべてを射程に収めるほど根源的であったというところ。（圏論も同程度かそれ以上に射程が長い） ツェルメロらはそれを公理的手法によってより洗練したということ。 |
| … |
どちらかと言うとZFや圏論がどうかと言うより、一階述語論理が数学の基本っぽいね |
| … |
>一階述語論理が数学の基本っぽいね それは当然。 でも学生にはその重要さがあんまり意識されない。 |
| … |
>つ[天書の証明] チャイティンのオメガの方が計算機科学畑の構成的な対象だからより好ましく思えるな俺は |
| … |
>>一階述語論理が数学の基本っぽいね >それは当然。 >でも学生にはその重要さがあんまり意識されない。 計算機でも解釈できるようにプログラムするの相当意識的に強要されてるじゃん社会的な要請の上でも |
| … |
意識的に強要されてるとか社会的な要請とか馬鹿が賢い振りをする時の常套句だな。 |
| … |
文系基礎論厨の方がバカが無理してる感じしかしないんだけど？ |
| … |
>文系基礎論厨の方がバカが無理してる感じしかしないんだけど？ この一行でバカなのがわかる 本人は気付いてないんだろうけどさ |
| … |
そんなに僻むなよｗ |
| … |
書き込みをした人によって削除されました |
| … |
>そんなに僻むなよｗ この一行でバカされてることに気付いたことがわかる いずれにしてもバカなんだけどさ |
| … |
× 文系基礎論厨の方がバカが無理してる感じしかしないんだけど？ △ 文系基礎論厨の方がバカが無理してる感じがするんだけど？ ○ 文系基礎論厨の方がバカが無理してる感じが多く感じられるんだけど？ |
| … |
数学基礎論はそもそも文系じゃないんだが。 |
| … |
>計算機でも解釈できるようにプログラムするの相当意識的に強要されてるじゃん社会的な要請の上でも まぁ、なんというか突っ込みどころはあるけど。 計算機でも解釈できるようなプログラム言語だって、述語論理から見れば、表現機能としてはそれをより制限した機能をもつ言語。 概ねプログラム言語の多くは一部を除いて形式言語としては文脈自由型言語となるだろう。（Bakus- Naur form:BNFは文脈自由型言語のクラスと同じになる。） そして、これらの形式言語理論だって、述語論理と集合論を前提に組まれているだろう？ |
| … |
このスレの人coqとか好きそう |
| … |
ちょっと前に自動証明に関係したスレの流れもあったね。 スレ建て自体は別のお題だったっけか？ |
| … |
coq theories はゼロから集合論や整数論を証明するから好きだ |
| … |
ゼロからって、最初からってこと？ そもそも公理は証明できないよ。 |
| … |
例えば、公理的集合論で言うところの構成的ユニバースの発想を見ればわかるように、ZFCに代表される集合論の公理系（理論）は、その公理を満たす対象たちからなるモデルの一つに”∈推移的有向グラフ”がある。有向グラフをZFCを満たすように定義すれば「ものの集まり」というイメージから離れてもZFCの公理を満たすようにできるわけ。 同じく圏だって、そのわかりやすい具体例は有向グラフであるわけで、その有向グラフを定義できるところまで基礎定義をさかのぼってみれば、基礎の構造を集合としても圏としてもどっちでもいいってこと。 |
| … |
ZFCなどに代表される数学の基礎理論の体系は、例えば集合という対象を扱うなら、その体系で扱う対象とそれらに関する演算が定義されていて、その基礎体系はそれら演算について閉じているって言うことを言っているわけ。 ZFCで言えば、各公理で存在を認める対象はすべてが「集合」であって、それぞれの公理を組み合わせて集合算を定義しても、ZFCそのものがそれらすべての演算について閉じているといっている。 自然数は、一階の述語論理に自然数の算術公理を持つ言語を入れれば定義できるけれど（例えばペアノによる方法）、それをせずにZFCの無限公理と内包公理によって自然数と同等の台集合を構成して、各種二項関係を定義することで定義したっていい。 |
| … |
そうやって、空集合から構成していった自然数NはZFCの集合であり、直積集合N×Nから適当な同値類による商集合を構成して整数の集合Zが作れる。 Zが集合なら、そのZからZ×Zを集合としてつくって、その部分集合を有理数Qと同一視できるように構成できる。 実数も関数も（それほど大きくない）空間や構造も集合として構成することができる。 これらの例は、集合によって構成する方法を取らずに、述語論理上の言語に、自然数のときと同じように、整数を対象とする言語、有理数を対象とする言語、実数を対象とする言語などなどと付け加えていく方法によって定義していくこともできるわけ。 ZFCやBGなどの公理的集合論の理論は、対象（集合やクラス）に施される演算によってその理論の対象領域が閉じていることを確認しているので、その理論によって、例えば「亜群の直積集合」などといった構造がその公理系で認められた集合演算の組み合わせで表現できるなら、それもZFC（あるいはBG）上の集合だといえるってこと。 |
| … |
発表する場を持たない者の掃き出し口になってる |
| … |
書き込みをした人によって削除されました |
| … |
述語論理でも対象領域は「ものの集まり」のようなもので、それを集合としてもいいし、集合ではないが集合のようなものとして述語論理上に定義しておいてもいい。 単純な論理では、それらの対象を表す領域と、論理上の形式を評価する領域（例えば真・偽の二値が格納された領域）があることがおそらく最低条件となるだろう。 あえて、集合を表に出さないようにする場合はそれらの領域をタイプやクラスと定義していることが多い。当然、対象領域の定義はZFCの集合のようなものである必要はないし、集合であっても問題ない。 そして、それらの異なる対象の間に定義される規則が定義されている。 この規則とは関数（写像）なので、集合論的に定義もできるし、圏論ならもっと大雑把に定義できる。 集合論的にいえば、これらは論理体系の構造と呼ばれ、圏論的には論理規則を関数としてみた場合の合成に関する圏になる。 |
| … |
あ、まだ続くのねｗ |
| … |
>どちらかと言うとZFや圏論がどうかと言うより、一階述語論理が数学の基本っぽいね ここに戻るんだけど、たしかに先に書いたように、述語論理が数学の最も基本な原理・形式といってもいいんだけど、その述語論理にも「ものの集まり」だとか「対象同士の関連」といった、「集合のようなもの」・「関係・写像のようなもの」がその構造を記述する時にでてくるわけで、述語論理を語る時にはすでになんらかの集合のようなものは定義されていることが望ましいわけ。 |
| … |
あぁそれと、気になっていたんだけど、なんでスレ主はZFCじゃなくてZFにしてるわけ？ 選択公理は確かに強すぎる仮定かもしれないけど、多少弱めるとしても、「選択公理のような仮定」がないと、いくつかの数学上の古典的な定理は捨てないといけなくなるよ。 |
| … |
それにそもそも論として、ZFCの公理だって、その言語だって一階の述語論理の形式でかかれてるだろと。 圏の公理だって、述語論理だろ？ |
| … |
固有クラスを対象として量化表現を伴う表現にすることは普通の数学の領域では必要ないから、およそすべての数学的対象とその構造は一階述語論理とZFCの範囲ですでに記述されていると言ってもいいし、圏論上でZFCのモデルを組み立てられるから、同時に圏論で表現することもすでに成されているとも言える。 |
| … |
>そうやって、空集合から構成していった自然数NはZFCの集合であり、直積集合N×Nから適当な同値類による商集合を構成して整数の集合Zが作れる。 俺グロタンディーク構成が好き |
| … |
>俺グロタンディーク構成が好き 好きというだけじゃなぁ。 それについて、同じぐらい説明してくれないか？ |
| … |
環の局所化〜＞K群〜＞導来圏 って感じ？ >グロタンディーク構成 |
| … |
じゃ、それを純粋な形式的論理の論理式だけで表そうと思う？ 当然に表現可能だけど、スレ主の質問がどれだけトンチンカンなのかわかるでしょ？ |
| … |
小学生の頃に読んだマシン語の本は最後の方に補数表現で負の値を計算機上で表現する方法が載ってた グロタンディーク構成とかなり近い |
| … |
そりゃ、無限と有限の違いはあっても機能としては同じ目的の拡大構成だからな。 |
| … |
まあぶっちゃけるとグロタンディークの構想のひとつのトポスとか有名だよね 幾何学的じゃない方の位相と集合論を圏論の言葉で書き換えた奴 俺は個人的には幾何学的な方の位相の代数的位相幾何方面なコホモロジーの方が好きだけど |