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

数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。

前スレ
数学基礎論・数理論理学　その18
https://rio2016.5ch.net/test/read.cgi/math/1474357543/

基礎論村へようこそ

思う存分暴れてくれ

>>3
これは、もと弥勒菩薩こともと天皇陛下
某スレのスレ主です
スレ立て GJです！！

メモ
https://en.wikipedia.org/wiki/List_of_paradoxes
List of paradoxes

https://en.wikipedia.org/wiki/Foundations_of_mathematics
Foundations of mathematics

https://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E5%9F%BA%E7%A4%8E%E8%AB%96
数学基礎論（すうがくきそろん、英: foundations of mathematics[1], mathematical logic and foundations of mathematics[2]）は、現在の日本では、もっぱら数理論理学[3][4][5]（mathematical logic[3]）を指す言葉として使われる[3][4][5][注 1]。

歴史
19世紀末に、ゲオルク・カントルにより、集合が考えられた。集合にもとづいた数学の再整理は大きな成果を生み、数学において欠くべからざる道具となってきた。一方、バートランド・ラッセルは、素朴な集合の取り扱い（内包公理）により「自分自身を要素としない集合全体の”集まり”」も集合とされるが、左記の集合は、それ自身を要素としない時、その時に限り自身を要素とするという矛盾を引き起こすことをラッセルのパラドックスとして指摘した。ここに、数学の基礎付けの問題が発生した。

パラドックスをめぐる立場は、大きく論理主義、直観主義、形式主義の３つに分けられる。

日本では、数学基礎論は、歴史的経緯により、本来の数学の基礎付けの意味だけでなく、それに用いられる超数学および数理論理学の意味でも用いられる。

メモ

https://amonphys.web.エフシー2.com/amonfm.pdf
あもんノート
目次
第21章数学基礎論入門
数学基礎論は理論物理学を学ぶ上で必須というわけではないのですが、科学の言葉である数学の基礎がどのようになっているかは、多くの人が気になるところだと思われます。特に理系の人は教養としてここに記した概要だけでもきちんと知っておくべきでしょう。論理学、ZFC集合論、数や写像の定義、一般連続体仮説、不完全性定理などについて記してゆきます。
http://amonphys.web.エフシー2.com/
あもんノート
　学生の頃に学んだ理論物理学に関するまとめノートです。 基礎を網羅しながら、素粒子論、宇宙論、そして超ひも理論まで到達しています。 各章の難易度表はこちら。

メモ
https://ja.wikipedia.org/wiki/%E3%83%84%E3%82%A7%E3%83%AB%E3%83%A1%E3%83%AD%EF%BC%9D%E3%83%95%E3%83%AC%E3%83%B3%E3%82%B1%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
集合論において、ツェルメロ＝フレンケル集合論 (英: Zermelo-Fraenkel set theory) とは、ラッセルのパラドックスなどのパラドックスのない集合論を定式化するために20世紀初頭に提案された公理系である。名前は数学者のツェルメロとフレンケルにちなむ。歴史的に議論を呼んだ選択公理 (AC) を含むツェルメロ＝フレンケル集合論は公理的集合論の標準形式であり、今日では最も一般的な数学の基礎となっている。選択公理を含むツェルメロ＝フレンケル集合論はZFCと略される。Cは選択 (Choice) 公理を[1] 、 ZFは選択公理を除いたツェルメロ (Zermelo)＝フレンケル (Fraenkel) 集合論の公理を表す。

20世紀後半～21世紀を代表する論理学者って誰がいる？
情報科学者とか言語学者みたいな人ならいくらか思いつくんだけど

僕はずっと君のものだよ

表示的意味論で使う⊆みたいな角ばった近似の関係の記号ってLaTeXでどうやって出すの？

表示的意味論って何？

\sqsubseteq

>>10
\section{TeX の時間} %%% 第 XIV 節 %%%
https://rio2016.5ch.net/test/read.cgi/math/1684875684/

ヒルベルトって最終的に直観主義者（有限の立場）になってたんだね。
幾何学の基礎7版の付録を改めて読み返してみたら、直観主義、構成主義的考察がいっぱいで笑った。
形式主義負けてんじゃんって（S.MacLaneの機能的形式主義というのもあるがあれは真理関係ない）。
結局、形式主義、論理主義、直観主義の3者のうち勝者は直観主義だったというのは、数理論理学では常識だったのか？
やたら直観主義論理が出てくるのが不思議だったんだが、そういう理由だったのか？

何か根本的な勘違いをされているようです

https://www.msz.co.jp/book/detail/08828/

よかったね

>>14-15
計算機科学が現実の勝者です。

>>18
それは19世紀的な構成主義（直観主義）じゃないかと。

勝者は数学者が普通に使ってる論理的だけどゆるくしか形式化してない数学やろ
他のシステムは全部その数学を用いて形式化するわけだし

それ数理論理学のスレで言う？

話し戻すと、ヒルベルトは数学の無矛盾性を示したかったというよりは、解析学を基礎づけたかったんだね。
ざっくりと数学というから勘違いを呼び起こすことになる。「解析学」ってちゃんと言えばいい。
ブルーバックスとか岩波文庫とか一般向けだから結果的にミスリード多いとわかった。

数理論理学って数学を使って論理学を形式化するのがやっぱメインやろ

？
数学は数の概念に基づいている。では数の概念は何に基づいているかと言えば、数学に基づくというと循環論法になる。
論理に基づくとしたのが論理主義。
直観に基づくとしたのが直観主義。
だけど、自分の理解だと、現代的には論理主義を直観主義で基礎づける直観主義論理で、数じゃなくて論理演算を直観で基礎づけて
その上に数を構築してさらにその上に数学を構築するという形態をとっている、と思っている。

少なくとも論理学を数学を形式化するとかは意味わからん。どうやるんだ？

数学を使って論理学を形式化する、な。

教科書読めば書いてあるだろ

数学使って直観主義論理を基礎づけてそれで数学を直観主義論理で基礎づけるのか。

数学の基礎付けなんて誰もやってないことはスレチ

>>20
グロタンディーク「埋葬された。呪ってやる。

論理学を使って数学を形骸化する

>>23
直観だって論理学奈乃だが

>>30
直観は人間の機能だよ。心象とかのことじゃん。

公理に含まれる無定義概念をどうやって把握するかといえば直観を用いるしかない。
論理学は言語というかある種道具であって、前提として道具を使う人間がいる。
その人間にいくつか機能があってその機能の一つが直観。直観が道具の中にあるというのはおかしい。

そんな客観性のかけらもないものより数学のほうがはるかに信頼できるんだから、数学を使って論理学をやれよ

客観性のかけらもないとかいうが、では無定義概念をどう把握するんだよ。

数学を使って解釈すればいいだろ何言ってんだ

解釈するという行為は人間の機能を使っている。数学で完結してない。

ただ、言いたいことエスパーすると、定理証明機にデータ読み込ませれば解釈が一意的に定まるはずだ、と言いたいんだろうと思う
でもたぶん、解釈があってるかどうかというところを判断するのは人間だから人間の機能使っているというところは同じ。

定理証明器なんて使うより人間が数学やったほうが効率的だし正しさにも大して貢献しないだろ
数学で記述できないんなら板違いだろ
哲学板で言葉遊びしてればいいじゃん

定理証明機って数理論理学の夢じゃないか？現代数学とか物理って規模的にもう人力でやるの無理じゃない？
別に俺もこんな話したいわけじゃないからやめるが。

計算機で可能だとわかってることを計算機でやることのどこが夢なんだよ
夢があるのは証明の自動化だけど今は人間がやったほうがはるかに速いし、速いから何かが変わるな話は今してないでしょ

証明の自動化なんかできんの

止めると言いつつ書いてしまうが、なんで数理論理学やってんの？
人間の行ってしまう間違った推論を排除したいとかそういう目的あるわけじゃないの？

そもそもなんで数学を使って論理学を形式化する気がない人間がこのスレにいんの？
数理論理学ったらそれがメインコンテンツだろ
間違った推論とか興味ないがな

>>23
に戻る。同じやつだな。

だから我々は数学を共通言語として学問をやってるんだから、それに文句があるんなら哲学板にいけよ

だから、数学で論理学やるって意味不明だといってるんだ。
数学基礎論、数学の基礎付けのために出てきた学問だぞ。数学で論理学やったら循環論法だろ。

じゃあ質問スレで聞いて来いよ

数学基礎論が何かなんて>>1に書いてあるだろ
書いてある項目は全部数学を使って論理学を記述する話じゃねーか
それ以外のことは哲学板でやれよ

懇切丁寧に回答して時間の無駄だった。

トンデモ数学の話なんてどこでやっても時間の無駄だから哲学板でやれ

>>40
自動定理証明？

数学基礎論でやってる学問に哲学でやってるよその学問を勝手に合体させて循環論法になったとか騒いで何が楽しいんだか
共存できないのが分かってんなら好きな片方だけやればいいわけだし、君の方は哲学なんだから哲学板でやれよとしか言えんだろ

ぴったりのスレがあるじゃんそっちでやれよ

数学基礎論「数学を使って数学の基礎を作ります」←循環論法じゃん
https://rio2016.5ch.net/test/read.cgi/math/1681799705/

>>45
循環するに決まってるだろ

なんで哲学屋ってなんの成果も上げてないのによその学問に喧嘩売ってくるんだろうな
その時間をもっと建設的なことに使えよ

建設的なことやったら哲学じゃなくなるから

数学を使わずに論理学やってなんか成果出してみせろよ
どうせなんにも出てこないけどな

というか数理論理学が理解できないから哲学に走ったんだろ正直に言えよ
循環論法になってるとか主張するのも、理解できないものの存在を認めたくないから自分への言い訳を作ってるだけだろ

哲学は訓詁学よ
誰々が何々と言った
みたいなのの重層
もはや意味もなし

>>57
哲から数学に走るやつもおるで

学生の時に論理学か何か教えに来てた非常勤講師嫌なやつだったな
あんま覚えてないけど

基礎論やってる奴は厭な奴

基礎論の訓詁学をひけらかす奴は嫌な奴

「訓詁学」とは？具体的にｋｗｓｋ

そもそも論理学に何の訓詁もないが

ZFがどうのこうの

「どうのこうの」ではわからん
集合論が訓詁学、というのは
集合論が理解できん馬鹿の戯言

選択公理がどうのこうの

入門者が習うのが確定事項なのは当たり前

集合論のどうでも良いところをくどくどと

>>67　選択公理知らないなら知りましょう
>>69　選択公理がどうでもいいというのは嘘ですね

日本の計算機科学の弱さとITの駄目さ加減は密接な関係がある。日本は計算機寄りの数学が弱い。

選択公理婆

>>71
スレ違い

計算論は数学やで

雑魚がいくら頑張ったところで高が知れてる

尺度を変えれば世界的な研究者だって雑魚の１人、と考えて自分の研究を淡々と進めるのみ

井の中だろ

井の中のゝ

井の中で成果を出せばいいだけ

全ての矛盾を「矛盾」として一括りにするのはどうなの？
矛盾とは「A∧¬A」の形の命題全てということにしても
これらがお互いに同等の「矛盾」（人）なるものとなるべきか？
具体的にいうと「A∧¬A→P」がどんな命題A,Pについても成立するとすべき理屈はなんだろ
矛盾律「人→P」を疑問視する人もいるようだがそもそも「矛盾」として一括りにしていいかどうかという疑問

矛盾を区別したければしてもいいよ
⊥を使わなくても論理は作れる

>>81
その場合互いに同等であるとは言えないことになってその否定の
「真」も互いに同等にならないような理論になるの？
まあ矛盾の否定が真だというのも疑問視する人いると思うが

見た目の割に証明が難しいと言う意見のあるもの

連続体仮説

>>83
またお前か

>>82
真が同等とかの意味がよく分からん
様相論理に「必然的に真」とかの区別ならあるが

仮に矛盾A∧¬Aの否定を排中律A∨¬Aと考えるならば
(正確には¬(A∧¬A)とA∨¬Aは違う命題だが)
直観主義論理では排中律は仮定されないけど、個別の命題がA∨¬Aを満たすことはある
その意味で矛盾の否定は同等でない

>>85
>真が同等とかの意味がよく分からん
ここで書いた同等とはP→QとQ→Pがどちらも成立すること
>>86
排中律を仮定しない直感主義論理の場合でも¬(A∧¬A)は真のはず
Aが変わっても同等なのでは？
しかしA∧¬Aが区別されお互い同等でないなら¬(A∧¬A)も同等でなくなるのかなって疑問

たとえばA,Bを別々の命題変数として
A∧¬AとB∧¬Bは同等でない矛盾とするなら
A∧¬A∧B∧¬Bがこれらより「より矛盾」てことになって
逆に
￢(A∧￢A)と￢(B∧￢B)も同等でない「真」なら
￢(A∧￢A)∨￢(B∧￢B)は「より真」てことになるのかなと
たしか¬P∨¬Q→¬(P∧Q)は排中律も矛盾律もなく証明できたから
¬(A∧¬A∧B∧¬B)は￢(A∧￢A)∨￢(B∧￢B)よりも「より真」みたいな感じで
矛盾や「真」にも優劣というか同等性の違いが出てくるのかもと思った

>>87
>P→QとQ→Pがどちらも成立すること
PとQがどちらも真ならP→QとQ→Pはどちらも成立する

>>89
それは単純すぎ
真理値でしか考えてないでしょ
真理値は副次的なものだから
矛盾を区別するてのはどうかと考えたわけ
つまり「矛盾」（人）なしの命題論理
矛盾律人→Pは当然ないだけでなく
A∧￢A→人もないし(A→人)→¬Aもない

ただし
P∧¬Pの形の命題は矛盾に「属する」もの
¬(P∧¬P)の形の命題は「真」に「属する」もの
みたいな扱いにするかなと
もちろん矛盾や真に属するものがこれだけではないだろうけど
矛盾も真も同等にしないような命題論理があり得るかなと

>>91
>矛盾も真も同等にしないような
矛盾も真もそこに属するもの同士が同等にならないような
か

>>89
￢(A∧￢A)→￢(B∧￢B)
を排中律矛盾律および人を使わず証明してくれてもいいよ
使えるのは∧∨→のEとIと
¬Iの代わりに
(A→（なんらかの矛盾）)→¬A
と
¬Eの代わりに
A∧¬Aが矛盾の一つになる
みたいなのだけでどう？

なんか始まったぞw

書いてて思ったけど人使わないだけで最小論理と同じかも
人を使うのは「矛盾に属している」と自分が書いたのと
同じことを記号にしてるだけかもな
しかし最小論理で
￢(A∧￢A)→￢(B∧￢B)
またはそもそも区別したかった矛盾の同等性
A∧￢A→B∧￢B
はどう証明できるのかな

>>94
すまんな色々思考が巡ってしまった
そもそも
>>80
>全ての矛盾を「矛盾」として一括りにするのはどうなの？
というのが疑問

>>90
「P→Qが成り立つ」ということの意味を(真理値による定義ではなく)「PからQが証明できる」こととするならば、PとQが真でもP→QとかQ→Pが成り立つとは限らない

>>97
命題論理におけるP→Qの扱いはPからQが導かれたという流れを抽象化したものだよ
→EがModus Ponensで→Iがそれ

抽象化というか
記号で表したということ

>>98
真偽というのはモデルを指定すると「このモデルではこの命題は真」と決まるものであって、論理体系の証明力が弱ければPとQが真でもPからQが証明できないことはある

シーケント計算なら→Lと→Rか
→LはMPのようなもので→Rが導出の記号化