数学基礎論・数理論理学 その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/ >>18
それは19世紀的な構成主義（直観主義）じゃないかと。 勝者は数学者が普通に使ってる論理的だけどゆるくしか形式化してない数学やろ
他のシステムは全部その数学を用いて形式化するわけだし それ数理論理学のスレで言う？
話し戻すと、ヒルベルトは数学の無矛盾性を示したかったというよりは、解析学を基礎づけたかったんだね。
ざっくりと数学というから勘違いを呼び起こすことになる。「解析学」ってちゃんと言えばいい。
ブルーバックスとか岩波文庫とか一般向けだから結果的にミスリード多いとわかった。 数理論理学って数学を使って論理学を形式化するのがやっぱメインやろ ？
数学は数の概念に基づいている。では数の概念は何に基づいているかと言えば、数学に基づくというと循環論法になる。
論理に基づくとしたのが論理主義。
直観に基づくとしたのが直観主義。
だけど、自分の理解だと、現代的には論理主義を直観主義で基礎づける直観主義論理で、数じゃなくて論理演算を直観で基礎づけて
その上に数を構築してさらにその上に数学を構築するという形態をとっている、と思っている。
少なくとも論理学を数学を形式化するとかは意味わからん。どうやるんだ？ 数学使って直観主義論理を基礎づけてそれで数学を直観主義論理で基礎づけるのか。 >>20
グロタンディーク「埋葬された。呪ってやる。 >>30
直観は人間の機能だよ。心象とかのことじゃん。 公理に含まれる無定義概念をどうやって把握するかといえば直観を用いるしかない。
論理学は言語というかある種道具であって、前提として道具を使う人間がいる。
その人間にいくつか機能があってその機能の一つが直観。直観が道具の中にあるというのはおかしい。 そんな客観性のかけらもないものより数学のほうがはるかに信頼できるんだから、数学を使って論理学をやれよ 客観性のかけらもないとかいうが、では無定義概念をどう把握するんだよ。 解釈するという行為は人間の機能を使っている。数学で完結してない。
ただ、言いたいことエスパーすると、定理証明機にデータ読み込ませれば解釈が一意的に定まるはずだ、と言いたいんだろうと思う
でもたぶん、解釈があってるかどうかというところを判断するのは人間だから人間の機能使っているというところは同じ。 定理証明器なんて使うより人間が数学やったほうが効率的だし正しさにも大して貢献しないだろ
数学で記述できないんなら板違いだろ
哲学板で言葉遊びしてればいいじゃん 定理証明機って数理論理学の夢じゃないか？現代数学とか物理って規模的にもう人力でやるの無理じゃない？
別に俺もこんな話したいわけじゃないからやめるが。 計算機で可能だとわかってることを計算機でやることのどこが夢なんだよ
夢があるのは証明の自動化だけど今は人間がやったほうがはるかに速いし、速いから何かが変わるな話は今してないでしょ 止めると言いつつ書いてしまうが、なんで数理論理学やってんの？
人間の行ってしまう間違った推論を排除したいとかそういう目的あるわけじゃないの？ そもそもなんで数学を使って論理学を形式化する気がない人間がこのスレにいんの？
数理論理学ったらそれがメインコンテンツだろ
間違った推論とか興味ないがな だから我々は数学を共通言語として学問をやってるんだから、それに文句があるんなら哲学板にいけよ だから、数学で論理学やるって意味不明だといってるんだ。
数学基礎論、数学の基礎付けのために出てきた学問だぞ。数学で論理学やったら循環論法だろ。 数学基礎論が何かなんて>>1に書いてあるだろ
書いてある項目は全部数学を使って論理学を記述する話じゃねーか
それ以外のことは哲学板でやれよ トンデモ数学の話なんてどこでやっても時間の無駄だから哲学板でやれ 数学基礎論でやってる学問に哲学でやってるよその学問を勝手に合体させて循環論法になったとか騒いで何が楽しいんだか
共存できないのが分かってんなら好きな片方だけやればいいわけだし、君の方は哲学なんだから哲学板でやれよとしか言えんだろ なんで哲学屋ってなんの成果も上げてないのによその学問に喧嘩売ってくるんだろうな
その時間をもっと建設的なことに使えよ 数学を使わずに論理学やってなんか成果出してみせろよ
どうせなんにも出てこないけどな というか数理論理学が理解できないから哲学に走ったんだろ正直に言えよ
循環論法になってるとか主張するのも、理解できないものの存在を認めたくないから自分への言い訳を作ってるだけだろ 哲学は訓詁学よ
誰々が何々と言った
みたいなのの重層
もはや意味もなし 学生の時に論理学か何か教えに来てた非常勤講師嫌なやつだったな
あんま覚えてないけど 「どうのこうの」ではわからん
集合論が訓詁学、というのは
集合論が理解できん馬鹿の戯言 >>67 選択公理知らないなら知りましょう
>>69 選択公理がどうでもいいというのは嘘ですね 日本の計算機科学の弱さとITの駄目さ加減は密接な関係がある。日本は計算機寄りの数学が弱い。 尺度を変えれば世界的な研究者だって雑魚の１人、と考えて自分の研究を淡々と進めるのみ 全ての矛盾を「矛盾」として一括りにするのはどうなの？
矛盾とは「A∧￢A」の形の命題全てということにしても
これらがお互いに同等の「矛盾」（人）なるものとなるべきか？
具体的にいうと「A∧￢A→P」がどんな命題A,Pについても成立するとすべき理屈はなんだろ
矛盾律「人→P」を疑問視する人もいるようだがそもそも「矛盾」として一括りにしていいかどうかという疑問 矛盾を区別したければしてもいいよ
⊥を使わなくても論理は作れる >>81
その場合互いに同等であるとは言えないことになってその否定の
「真」も互いに同等にならないような理論になるの？
まあ矛盾の否定が真だというのも疑問視する人いると思うが 見た目の割に証明が難しいと言う意見のあるもの
連続体仮説 >>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が矛盾の一つになる
みたいなのだけでどう？ 書いてて思ったけど人使わないだけで最小論理と同じかも
人を使うのは「矛盾に属している」と自分が書いたのと
同じことを記号にしてるだけかもな
しかし最小論理で
￢(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が導出の記号化 >>88
>A∧¬AとB∧¬Bは同等でない
こういうことはあり得るのかというのは
オレも気になってた 最小論理だとA∧￢A→人は出るけど人→A∧￢Aは出ない
それは人に真理値1を割り当てる最小論理のモデルで
恒真にならないから（このモデルで￢Aの真理値は恒に1）
人→A∧￢Aには矛盾律必要だね
>>95
>書いてて思ったけど人使わないだけで最小論理と同じかも
と書いたけど
最小論理との違いは
矛盾の集合（どう定義すべきか？）の極大元としての人が
存在するか存在しないかってことかなとも思う >>103
最小論理だと人とA∧￢Aは同等でなくAとBが異なる命題変数なら
A∧￢AとB∧￢Bも同等じゃない
それは上記のモデルで両者の真理値はAとBの心理値に一致するので
それぞれ異なる真理値なら同等であり得ないから 背理法的には、A∧￢A⇒¬A だよな❓
ていうか、¬A⇔B なら、
¬B∧B⇒¬B となり、Bに¬Pを代入すると
P∧¬P ⇒ P となり、これは、背理法を否定するな🤔
変なの。背理法ってヘンです。 >>104
>矛盾の集合（どう定義すべきか？）の極大元としての人が
>存在するか存在しないかってことかなとも思う
逆に言えば
最小論理の場合「真」の集合（矛盾の否定）の極小元として￢人が存在するけど
人がないなら「真」の極小元の存在も言えないね
でも
それだと矛盾の集合をどう定義すべきか悩ましい
最初論理なら
{P|P→人}
みたいな定義ができるけど >>106
>A∧￢A⇒￢A だよな
それは成立するけど背理法はそうじゃない
(￢A→人)→A
が背理法（の一つ） A→BかつB→Aを同等というのは初めて聞いた
同値のことだろう
矛盾命題は全て同値であることを示す
その前に矛盾命題が任意の命題を証明できる(爆発律)ことを示す
P∧¬Pとすると、Qを任意の命題として、
P∧¬PからPが成り立つ
PからP∨Qが成り立つ
P∨Qと¬Pから、Qが成り立つ
よってP∧¬Pから任意の命題Qが成り立つ
A∧¬AとB∧¬B、2つの矛盾命題を考えると、爆発律より、A∧¬A→B∧¬BもA∧¬A←B∧¬Bも成り立つ
したがってA∧¬A⇔B∧¬B 矛盾を人って書くの気持ち悪いからやめてください
⊥を使ってください >>109
>P∨Qと￢Pから、Qが成り立つ
それは矛盾律ですよ
それを仮定すれば同等となるのは上>>104に書いた通りです
ですので
この違和感>>80を正当化するには最小論理あるいはそれに類する>>93のようなものが必要
そっちは矛盾とは何かの定義が思いついてないのでまだ不完全ですが
最小論理なら>>105の通り同等とはならないので
これでもいいかなと思い始めたところ >>110
\top, \botですね
むしろそっちあんまり好きじゃなくて >>109
>A→BかつB→Aを同等というのは初めて聞いた
>同値のことだろう
同値はどうしてもモデルに関連した
つまり真理値を前提とした用語のように思うので
逆に違和感があるのでね
まあこれは別にどうでもいいけれど >>111
>>P∨Qと￢Pから、Qが成り立つ
>それは矛盾律ですよ
矛盾律と同等ですよ P ⇔ √2は有理数
¬P ⇔ √2は無理数 ∵P
とおく。そして、Q ⇔ アタシは美人である とおくと
モチロン、P∨Qと￢Pから、Qが成り立つ ので、
「アタシは美人である」は当然成り立つ 💃💃💃 自己解決∵宇宙からの閃き💡 >>115 よ 1.5hの自分ぢゃな
思慮深さが欠如しておるぞ。というか、今の自分は違います。
「P∨Qと￢Pから、Qが成り立つ」 とは、
［(P⇒Q) ∧ (¬P⇒Q)］ ⇒ Q という意味ぢゃないかな
P:今直ぐ ¬P:いつでも Q:出来る とおくと、解り良い
というか、「いつか出来るから今出来る」なんてタイトルのウタに釣られてはダメ🙅 ┻ ∧ P ⇒ P なのだろう
矛盾したことを💃が喋ろが、
「P ⇔ 💃は美人である」は当然成立💃
しかし、┻ ∧ P ⇒ ┻ ∴¬P
トスルやつがいる。
「P ⇔ 💃は美人である」はモチロンなのに 117とか自分で書いたのに、今みると意味不明だな。というか
色々ネットサーフィン🏄したら
【選言三段論法】 というのがあった。当たり前の論理だが
之がダメヤツは、地球人に多いという、イメージはある
(P or Q) and not(P) がQかどうかなんて、代数演算しなくても
ベン図を脳内にイメージすれば、直ぐ、霊感で解るのに
