数学基礎論・数理論理学　その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が導出の記号化

そして終わったｗ

>>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かどうかなんて、代数演算しなくても
ベン図を脳内にイメージすれば、直ぐ、霊感で解るのに

藁藁

トウシロウの知ったかイキリ

もし素因数分解とその解の検算が、「どちらにも指数時間かかる」のならそれはEXPTIMEで、
「どちらも多項式時間でできる」のならPに属する。そうでないからNPだってAIが言ってる

【悲報】数学板の住人x+1を変数だと思ってた

さらにx+1が変数であることも証明できたもよう

692 １３２人目の素数さん 2024/03/12(火) 18:14:42.16 ID:pMrLmsKB
＞＞691
そんなことは聞いてない
∀x∈ℕ.x<x+1
と
∀x∈ℕ.∃(x+1).x<x+1
の違いを聞いている
おまえは∃の後ろに変数以外を書くなと言ったが、x+1は変数ではないと？じゃ何？

693 １３２人目の素数さん sage 2024/03/12(火) 19:37:50.92 ID:upjnOnB4
＞＞692
∃の後ろに変数じゃないものを書いてるのは君だろ、∃(x+1)ってなんだよ
ふざけて書いてるだろ

721 １３２人目の素数さん 2024/03/13(水) 00:58:49.14 ID:5iS9phMp
ちなみに
https://web.sfc.keio.ac.jp/~hagino/logic16/07.pdf
のP4には

• 「もの」の集まり
　• 整数
　• 人間
• 「もの」の集まりを動く変数
　• 対象変数（object variable）
　• 𝑥, 𝑦, 𝑧, . . .

と書かれてる

xが「もの」の集まりである自然数を動く変数であるなら
xの後者であるx+1もやはり自然数を動くので変数の定義を満たす

頑なに変数でないと言い張る人もいるようだけどどうやら独善持論のようですね

723 １３２人目の素数さん 2024/03/13(水) 01:21:16.03 ID:5iS9phMp
ものの集まりとはつまり集合のことだし
ものの集まりを動く変数とはつまり集合の不定元のことだね

∀x∈N.(xは不定) ⇒ x+1∈N ∧ (x+1は不定)
であるから変数の定義に従い
xはNを動く変数 ⇒ x+1はNを動く変数
が成立

y＝x のグラフを左に1移動させる　⇒
y＝x-1 ｂﾌグラフをゲッャg❢
モチロン、前者も後者も、
dy/dx＝1 ですし、
yはxが変化すれば、
yはxが変化するので
yは前者も後者も変数なので
xも、x−1も、モチロン、変数なのぢゃ

というか、y＝0x は変化しない変数ぢゃなモピロン
然るに、何やかんやで、
定数∋変数　∨　変数∋定数　であると言えよう🧖

(実)変数を含む公式に、定数(それがたとえ虚数でも)を代入しても
成立はするらしいよ。何と虚数でもね

で、その逆、定数に変数は代入した数式はダメぽぃです。
と色々、思索するに、多分絶対に

変数∋定数　であり、
定数∋変数　はありえません。絶対多分。
地球人の数学の定義は知らんけど
変数∋定数　でキマリーーーー

虚数の情緒について語るオジサン

>>127　よ。早朝から、何を戯けた言霊を言ってるのぢゃ

>　マイナスはダメ∵�@がそもそも変な宇宙言語だ
いやねーーー

∀x∈ℕ　には暗に、いや明らかに
x>0 という意味を含んでますよ。
ていうか、x≧0 という意味かもだ。
ま、インド人によりゼロが発明されて
もはや、ゼロは自然数なのぢゃから🧖
てか、∞は誰が発明したんだろう。
というか、ゼロとか∞は存在しませーーーーん

エスプレッソ1杯は30ミリリットル⇒
そのカフェイン量は50ミリグラム

という命題らしき文がネット上に存在する
でこの命題は、一瞬で偽∵デタラメ　だ
∵質量保存則に反する
∴エスプレッソ1杯は30ミリリットル　は
　偽り　∵背理法

なんて、オレッて論理的なんだろう。
モピカし、オレッて超天才だ。💃
でも、ネット上は5ch以外は∀正しいハズ

いや！！　次の瞬間気づいた
自分は、
エスプレッソ1杯は30ミリリットル　を
エスプレッソ1杯は30ミリグラム　と読み違えたのだった。

以上　失礼しましたぁ　(⁠^⁠_⁠^⁠メ⁠)

超準解析って役に立つの？

構成可能宇宙LがZFCのモデルになるとWikipediaに書かれているけど
モデルって集合じゃなくてクラスでもいいの？大丈夫？

頭大丈夫？

ZFC+宇宙の公理(？)という理論の中でのモデルということだろう

https://ja.wikipedia.org/wiki/%E6%A7%8B%E6%88%90%E5%8F%AF%E8%83%BD%E9%9B%86%E5%90%88

基本的に英語版はチェックしておくべき
https://en.wikipedia.org/wiki/Constructible_universe
Constructible universe

クラスで付番されたクラスの”組”とか考えてもいいの？

>>136
>クラスで付番されたクラスの”組”とか考えてもいいの？

良いと思うが
素人なので、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) におけるクラスの扱いをコピーしておきますね

(参考)
https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A9%E3%83%B3%E3%83%BB%E3%83%8E%E3%82%A4%E3%83%9E%E3%83%B3%EF%BC%9D%E3%83%99%E3%83%AB%E3%83%8A%E3%82%A4%E3%82%B9%EF%BC%9D%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大である公理的集合論である。NBGでは、量化子の範囲を集合に限定した論理式によって定義される集合の集まりとして、クラスの概念を導入する。NBGは、すべての集合というクラスやすべての順序数というクラスといった、集合よりも大きいクラスを定義できる。モース＝ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。

NBGのキーとなる定理はクラスの存在定理である。クラスの存在定理は、量化子の範囲を集合に限定した論理式それぞれに対して、論理式を満たす集合からなるクラスの存在を述べる。クラスは、クラスの論理式を一つずつ構築することで構成される。すべての集合論的な論理式は2種類の原子論理式（所属関係と等式）と有限個の論理記号から構築されるため、論理式を満足するクラスを構築するには有限個の公理があればよい。NBGが有限公理化できるのは、こうした理由による。クラスは他の概念の構築にも用いられ、集合論的パラドックスへの対処や、ZFCの選択公理より強い大域選択公理（英語版）の説明に用いられる。

ジョン・フォン・ノイマンは1925年に集合論にクラスを導入した。彼の理論の原始概念（英語版）は関数と引数であった。これらの概念を用いて、フォン・ノイマンはクラスと集合を定義した。[1] パウル・ベルナイスはクラスと集合を原始概念とすることで、フォン・ノイマンの理論を再定式化した。[2] クルト・ゲーデルは、選択公理の相対的無矛盾性の証明と一般連続体仮説を用いてベルナイスの理論を単純化した。[3]

集合論におけるクラス
クラスの使用例

NBG, ZFC, MK
NBG は論理的に ZFC と等価ではない。なぜなら、NBG の言葉は表現的であるからである。NBG ではクラスに関して表現できる一方、ZFC ではできない。しかし集合に関しては、 NBG も ZFC で同じ内容の表現を含意する。したがって、NBG は ZFC の保存拡大である。 NBG は ZFC が含意しない定理を含意するが、 NBG は保存拡大であるため、これらの定理は真のクラスに関するものでなければならない。例えば、大域選択公理は 真のクラス V は整列可能であり、どの真のクラスも V と一対一対応することを含意するが、これは NBG の定理である。[注釈 27]

保存拡大の帰結の一つは、 ZFC と NBG が無矛盾性同値であることである。 この証明には爆発原理（矛盾からは、何でも証明可能である）を用いる。

https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory
Von Neumann–Bernays–Gödel set theory

＞良いと思うが
ド素人、考え無しに良いと●●発言

>>138
あんたは数学科で落ちコボレさんか？

>クラスで付番されたクラスの”組”とか考えてもいいの？

１）>>137の通りだが、補足しておくと、なんでクラスを制限するのか？
２）それは、下記ラッセルのパラドックスの関連していて、「全ての集合の集まり」はクラスであって
　無制限にクラスを集合とすると、パラドックスになる
３）ZFCは、クラスを認めないので、パラドックスは回避できる
４）フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG)では、クラスは制御されて矛盾が出ないようになっている（だから、クラスの付番はあり）
５）じゃあ、NBGの方が良いんじゃね？ と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい（渕野先生とか）
６）なお、圏論が流行りで、基礎論以外の人は クラスは使いたいみたいだよ

https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%83%E3%82%BB%E3%83%AB%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9
ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。バートランド・ラッセルからゴットロープ・フレーゲへの1902年6月16日付けの書簡においてフレーゲの『算術の基本法則』における矛盾を指摘する記述に現れ、1903年出版のフレーゲの『算術の基本法則』第II巻の後書きに収録された[2]。なお、ラッセルに先立ってツェルメロも同じパラドックスを発見しており、ヒルベルトやフッサールなどゲッティンゲン大学の同僚に伝えた記録が残っている
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった
概要
「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる
そうすると、「任意の集合 X」に関しては、「 Xは Rに含まれる」←→「 Xは Xに含まれない」という定式が成り立つ
そして特に X= Rとすれば、「 Rは Rに含まれる」←→「 Rは Rに含まれない」となり、パラドックスが明示される
矛盾の解消
1.公理的集合論による解消

https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9_(%E9%9B%86%E5%90%88%E8%AB%96)
クラス (集合論)
集合論及びその応用としての数学におけるクラスまたは類（class）は、集合(または、しばしば別の数学的対象)の集まりで、それに属する全ての元が共通にもつ性質によって紛れなく定義されるものである。「クラス」の正確な定義は、議論の基礎となる文脈に依存する。例えば、ツェルメロ＝フレンケル集合論 (ZF) ではクラスは厳密には存在しないが、他の集合論（たとえば、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG)）では、「クラス」の概念は公理化されている

（どのような定式化を選んだとしても）「全ての集合の集まり」はクラスである。（ZF では厳密な言い方ではないが）このクラスだが集合でないようなものは真のクラス と呼ばれ、集合となるようなクラス（つまり集合）は小さいクラス とも呼ばれる。例えば、全ての順序数からなるクラスや全ての集合からなるクラスは、多くの形式体系において真のクラスである

追加引用しておきます
「圏 (数学)」をかじらないと、集合とクラスの関係は分かりにくいでしょうね
（圏 (数学)が、集合の範囲におさまらない（すなわちクラスを扱う）とき、大きい (large) と言う。類＝クラス）

https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9_(%E9%9B%86%E5%90%88%E8%AB%96)
クラス (集合論)

例
与えられた型の代数的対象全ての集まりは、たいてい真のクラスをなす。例えば、全ての群からなるクラス、全てのベクトル空間からなるクラス、など。圏論では、対象の集まりが真クラスをなすもの（または射の集まりが真クラスをなすもの）を大きい圏という。

超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。

集合論では、集合の集まりの多くは真クラスになってしまう。例えば、全ての集合からなるクラス、全ての順序数からなるクラス、全ての基数からなるクラスなど。

クラスが真クラスであることを証明する方法に、全ての順序数によるクラスとの間に全単射を与えるというものがある。この方法は、例えば自由完備束が存在しないことの証明などに使われる。

https://ja.wikipedia.org/wiki/%E5%9C%8F_(%E6%95%B0%E5%AD%A6)
圏 (数学)

圏の大きさ
圏 C が小さい (small) とは、対象の類 ob(C) および射の類 hom(C) がともに集合となる（つまり真の類でない）ときに言い、さもなくば大きい (large) と言う。射の類が集合とならずとも、任意の二対象 a, b ∈ ob(C) をとるごとに、射の類 hom(a, b) が集合となるならば（hom(a, b) を射集合、ホム集合などと呼び）、その圏は局所的に小さい (locally small) と言う[3]。集合の圏など数学における重要な圏の多くは、小さくないとしても、少なくとも局所的に小さい。
文献によっては、局所的に小さい圏のみを扱い、それを単に圏と呼ぶ場合もある[4][5]。

>>139 補足
>５）じゃあ、NBGの方が良いんじゃね？ と思うだろうが、基礎論屋さんはZFCの方がシンプルで良いと思うらしい（渕野先生とか）

下記を貼っておきますね
・強制法があって、ZFCと相性がいいみたい（渕野先生は、別のところでも書いていた気がする）
・“コーエンの強制法”は、連続体仮説問題に対して、ZFC上で展開されたし

https://fuchino.ddo.jp/misc/cohenx.pdf
“コーエンの強制法” と強制法1)2)渕野昌
12.November 2016 (04:31 JST) 版
1) このテキストは，『数理科学』2014年10月号に掲載予定の同名の記事の拡張版です．ページ数の制限のために記事から削除せざるを得なかった細部や，そこには含めないことにしたリマークのいくつかを加えてあります．

P13
5 連続体問題
コーエンの結果から連続体仮説は集合論の公理系から独立であることが分ったわけだが，このことは，現在の集合論の公理系がまだ拡張を必要としていることを示している，と解釈することもできる．
こう解釈する立場からは，そもそも集合論の正しい拡張が何かが議論できるのか，が問題となってくるが，巨大基数の理論と強制法の理論は，集合論の公理系の拡張の可能性をさぐるための思考実験の手法と見ることもでき，世紀末以降に得られつつある集合論でのそのような思考実験の厖大な成果は，そのような議論の可能性を強く示唆しているし，ウディンらによる研究は，そのような研究の成果による連続体問題の真の解決が手のとどくところにまで近づいていることを予感させるものですらある．

>>140
>超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。
ちょっとそれ違わない？
Knuthの「超現実数」という童話だと
「切断」を基本的なジェネレータにして空集合から作り出していく過程が描かれてるよな
0=<|>
-1=<|0>
1=<0|>
たしかこんなだっけうらおぼえだけど
だから個々の元が体じゃないでしょ
全体として体の小売を満たすクラス

>>142
>>超現実数 (en:Surreal number) 全体は、体の公理を満たす対象による真クラスである。
>ちょっとそれ違わない？
>Knuthの「超現実数」という童話だと

詳しくないので、超現実数 (en:Surreal number)のリンクから、受け売りを貼っておきます
Knuthの話も、概念史として出てきます

https://ja.wikipedia.org/wiki/%E8%B6%85%E7%8F%BE%E5%AE%9F%E6%95%B0
超現実数
超現実数（ちょうげんじつすう、英: surreal number）の体系は、全順序付けられた真のクラスとして実数のみならず（任意の正実数よりも絶対値が大きい）無限大および（任意の正実数よりも絶対値が小さい）無限小まで含む。超現実数の体系は、四則演算（加減乗除）など実数が持つ多くの性質を共有しており、順序体を成す[注釈 1] 超現実数をフォンノイマン–ベルナイス–ゲーデル集合論 (NBG) において定式化するならば、超現実数体は（有理数体、実数体、有理函数体、レヴィ゠チヴィタ体、準超実数体、超実数体などを含む）すべての順序体をその部分体として実現できるという意味で普遍的な順序体となる[1]。超現実数は、すべての超限順序数も（その算術まで込めて）含む。あるいはまた、（NBGの中で構成した）超実体の極大クラスが超現実体の極大クラスに同型であることが示せる（大域選択公理（英語版）を持たない理論では必ずしもそうならないし、またそのような理論において超現実数体が普遍順序体になるとも限らないことに注意する）。

概念史
それとは別の定義および構成法が、ジョン・ホートン・コンウェイにより、囲碁の寄せについての研究から導かれている[2]。コンウェイの構成法は1974年にドナルド・クヌースの著書 Surreal Numbers: How Two Ex-Students Turned on to Pure Mathematics and Found Total Happiness[注釈 2] に取り入れられた。対話形式で書かれたこの本においてクヌースは、コンウェイが単に「数」と呼んでいたものに「超現実数」という新たな名を付けた。のちにコンウェイもクヌースのこの造語を受け入れ、1976年には超現実数を用いてゲームを解析する On Numbers and Games（英語版） を著した[3]。

超実数との関係
Philip Ehrlich (2012) はコンウェイの極大超現実数体とNBGにおける極大超実体との間に同型を構成した。

https://en.wikipedia.org/wiki/Surreal_number
Surreal number
History of the concept
Research on the Go endgame by John Horton Conway led to the original definition and construction of the surreal numbers.[2] Conway's construction was introduced in Donald Knuth's 1974 book Surreal Numbers: How Two Ex-Students Turned On to Pure Mathematics and Found Total Happiness. In his book, which takes the form of a dialogue,
Knuth coined the term surreal numbers for what Conway had called simply numbers.[3]
Conway later adopted Knuth's term, and used surreals for analyzing games in his 1976 book On Numbers and Games.

基礎論屋さんは長文がお好き

誤　基礎論屋
正　ド素人

ド素人は、クラスとかいう言葉は知ってるが
クラスの要素が集合に限られることは知らず
クラスのクラスとか言い出す
定義を確認しないから初歩で間違う

正　ド素人： これは正しい

クラスのクラスとか言い出す：言ってない。妄想ですよ。お薬増やしておきますね。私は、自分ではほとんど語りません。ほとんどが、URLと引用です。なので間違いがあれば、それは引用先が間違っているときだね ；ｐ）

”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ
妄想がひどくなっていますね。お薬増やしておきますね。

素人ほど蘊蓄が好き

まあ、素人どうしで蘊蓄を語り合うの図かな　；ｐ）
もっとも いまどき、数学者で基礎論プロを名乗る人もすくないかも

>>150
149について
１は大学１年の線形代数　知らないヤツは理系失格
２、３は高校の数学　知らないヤツは大学の理系学部受からない

結論　ID:i+t5VZGk　は高卒か文系

>>149
>たまに自信満々で語ることが、ことごとく間違ってる

ふふふ
”クラスのクラス”で、このスレの全文検索をしたが、おサルさんの上記カキコ以外ヒットせずですよ>>147
妄想がひどくなっていますね。

幻聴幻視のぶざまを晒したあとでは、それ説得力ゼロだね　；ｐ）

>最近は怖がって高校数学レベルでも真偽について発言せず

それは、私の主義ですよ
数学の研究者でもない自分が、何かを語ったら、それはつねに誰かの受け売りで
だったら、自分で筆を起こすより、URLとそこからのコピーが正確だろうということです

>>152
>それ説得力ゼロだね
出来る高校生や大学１年生なら149は分かるけどね

>それは、私の主義ですよ
>数学の研究者でもない自分が、何かを語ったら、
>それはつねに誰かの受け売りで
>だったら、自分で筆を起こすより、
>URLとそこからのコピーが正確だろう
>ということです

そもそもコピーが見当違いなので
受け売りもやめて何も語らないのが
数学ド素人の君に最も相応しい「主義」

無知無能の自己顕示は、・・・自虐

ガロア理論だろ、wikiのコピペでスレを埋める

>>154
でも、円の17等分方程式の解き方も知らない、という・・・

未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろｗ

それくらいは誰でも読めばすぐわかるのでは？

>>153
ID:TKfxObiVさんか、面白いね 君は

・2ch時代から、チラシの裏、便所落書きと言われ、いま5chだが本質は変わっていない
・有象無象、玉石混交が、5chだ
・5chの相手に「正しいことを書いてくれ」と要求することが、大前提を外していると知れ！ ってことですよ

無知無能の自己顕示は、あ な た です！
それとも、自分が数学のプロだとでも？ 数学DR持ちかい？ アカデミック ポストは？

>>158
ハエがブンブン五月蠅いですな
令和の今も昭和の感覚で書かれましてもね

老害ですよね

>>156
>未だに箱入り無数目の問題で自称基礎論婆と罵倒合戦してるんだろｗ

これは、弥勒菩薩さまかな
箱入り無数目スレではお世話になりました

弥勒菩薩さまには
箱入り無数目のバックナンバー数学セミナーを購入いただき
記事のPDFをアップしていただきました
また、コルモゴロフの01法則のご指導も頂きました

このスレで、金魚フンとしてくっついてきた自称基礎論婆と
罵倒合戦を再開すると
皆様のご迷惑でしょう
弥勒菩薩さまの救いの手に乗って、退散いたします
では

>>160　匿名板で人物特定したがるおかしなヤツ

ある無矛盾な公理系τの任意のモデルに対してある論理式φが常に真となるならば、τからφがLKにおいて証明可能となることを示せ、という問題がわかりません

練習問題にしてはハードすぎないか？
無矛盾がなんでついてるのかよくわからんが

>>162
久しぶりに見た

>>162
https://www.st.nanzan-u.ac.jp/info/gr-thesis/2017/sasakik-ss/pdf/14ss095.pdf

>>165
サンクス

>>105
へ
プロレスは、正義のヒーローは一度ピンチになって
逆転勝利する
いま、モッチーはその過程にあるよ

ごばくスマン

ピンチだとは全然思っていないようだ

論理学のおすすめの本を教えてください

>>170
何が知りたいかによりますが
初心者には、タブロー法が書かれてる本がいいと思いますね
タブロー法が理解できれば、述語論理の完全性定理も
理解できるんじゃないでしょうか？

ちなみにゲーデルの不完全性定理は
狭義の論理学ではなく自然数論の定理です

タブロー法は、例えば線形代数でいえば消去法みたいなもんです

マイナーなタブローはどうかなあ
自然演繹が初心者には分かりやすいし
メジャーなシーケント計算を最初から学ぶのもよかろうし

>>173
シーケント計算でも、証明が存在する場合に
それを見つける「手続き」を示すなら結構ですよ

ただその目的にはタブローのほうがわかりやすいかと
別にカット除去とかしたいわけではないので
シーケント計算に固執しても仕方ない

メジャーとかマイナーとかは無意味かと
無意味なことにこだわっても賢くなれない

タブローの方法とは、真理の木あるいは意味論的タブローまたは分析タブローと呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続きの一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。

106位

４５

82位

>>175
そんな文章いくら読んでもタブロー法理解できんし
タブロー法について書かれた本を読めば方法わかるから
わけもわからず自然演繹がーシーケント計算がーとかいってんのは
３つともわからんド素人の戯言かと

素人が論理って便利と感じるのは、
この論理式がトートロジーかどうか判別できる
というところだろう

上記の問題に対して、タブロー法は「半分」回答を与える
つまり、トートロジーの場合には、その否定命題から矛盾を導くことで、答えを教えてくれる
ただし、そうでない場合、手続きが終了しない場合があるので、そうでないとわからないこともある

「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。

>>179
なにアホ言ってんの
一番分かりやすいのは自然演繹
メジャーなのはシーケント計算
タブローはマイナーってだけ

>>182
君が不勉強だからタブロー知らないだけ
勉強すればタブローなんて簡単だと分かる
つまらないことに固執するのは○違いの症状

>>183
は
だからマイナーだって言ってるだけだわw

別に簡単じゃないと言っていないんだが
自然演繹が一番分かりやすいね

最近は「ニッチ」がよく使われるそうだ

>>180
>「やらない理由はない」と言って不必要な仕事を指示された時に論理的に反論したいのですが知識がなく、できません。
>「やる理由がある」こととは違うと思うんです。先輩、教えて下さい。

ふつう定石は、Yes But法だな
１）仰る通り「やらない理由はない」ようですが・・と始める
２）しかし、今やるべき仕事が沢山あります
３）やるべき仕事に優先順位を付ける必要があります
４）いま、期日が迫っている仕事を A,Bと二つ抱えています。これを優先いたしたいと思います
と答える
これが、断る前提のロジックだが

そして、A,Bの二つの仕事を終える前に、言われた「やらない理由はない」の仕事について自分がやるべきかどうかを考えるのです
その後「A,Bの仕事が終わったので、その仕事をやらせて頂きます」と申し出るのが、一案だな
（もういい、別の人に頼んだ！と言われることも多いだろう）

会社の仕事では、自分には不必要に見える仕事でも、会社全体では意味があることも多い
そもそも、最初に仕事を振られたとき、”断るのが良いか受けるのが良いか”は、よく考えることだね
出来る人は「社長やって」と振られるのです！（下記）

(参考)
https://www.e-sales.jp/word/yesbut.html#:~:text=Yes%20But%E8%A9%B1%E6%B3%95%E3%81%A8%E3%81%AF%E3%83%BB%E6%84%8F%E5%91%B3,%E3%81%A8%E4%BD%95%E3%81%8C%E9%81%95%E3%81%86%E3%81%AE%EF%BC%9F
eセールスマネージャーRemix Cloud

Yes But話法とは・意味
応酬話法と呼ばれる話法の中の1つ。
相手の意見・主張に対し、いきなり否定・反論するのでなく、一旦納得・賛成・共感してから自身の考えを述べることによって、相手の心の障壁を取り除き、こちらの提案を受け入れやすくする話法。
お客様「A社の商品と何が違うの？あまり変わらない気がするけど・・・？」
営業「そうですね。見た目はあまり変わらないかもしれません。ですが弊社の製品は・・・」
お客様「そう。でも高いよね。。」
営業「他社と比べると確かに割高です。ただ弊社には他社にはない・・・があって、」
・・・・
あまりやりすぎるのも逆効果！？

https://www.nippon.com/ja/japan-topics/g02261/
トヨタ社長交代の舞台裏と狙い、佐藤恒治新社長の横顔とは
2023.03.15 山本 シンヤ nippon.com
章男氏から佐藤氏への社長の打診は、2022年12月にタイで開催された耐久レースの現場で行われた。
「レース中に呼ばれたので行くと、『ちょっとお願い聞いてくれない？ 社長やってくれない？』と言われました。最初は冗談だと思ったので、どうリアクションしていいのか分かりませんでした（苦笑）」（佐藤氏）
「私なりの内示の仕方があると思いました。佐藤とは社長室で話をするより、一緒にクルマに乗ることや現場で話をすることが多かった。だから、改めてどこかに呼んで話をするより、その延長線上でお願いした方がいいと思いました」（章男氏）

>>184
自分が知らない＝マイナー　
というのは自己本位な素人の戯言

恥ずかしいだけだから言わないほうがいいね
嘲笑されたくないでしょ？

>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが

まず、上司が「やらない理由はない」という場合
大体は「やらない理由が思いつかない」というだけで
証明になっていません

一方、部下としては「やらない理由」を提示するのが効果的ですが
そうしなければならないというわけではありません

そこで弥縫策ですが、上司に
「やらない理由が存在すると矛盾する、と証明できますか？」
といってみる手はあります

ただ大抵の上司は激怒するでしょうね
彼らは部下に仕事させることしか頭にありませんから

ところで「不必要な仕事」であることは証明できるのでしょうか？
あなたが「必要ない」と勝手に思ってるだけなら、それも証明ではありませんね

まず、上司に対して、自分がその仕事を必要ないと考える理由を述べた後
その理由を否定するような必要性について示してほしいと　述べたらいかがでしょう

まあ、明確な理由もなく、単に面倒くさいからやりたくないということで
いわれてもサボりまくる、という手はありますけどね

実はそれでも会社が困らないならいいんじゃないですか？

>>188
あのねw
数理論理学の本でほぼほぼ言及されてるのは
自然演繹とシーケント計算
タブロー方は本当にマイナーなのよ
例えばここどう？
http://www2.yukawa.kyoto-u.ac.jp/~kanehisa.takasaki/edu/logic/
あと
>恥ずかしいだけだから言わないほうがいいね
>嘲笑されたくないでしょ？
自己紹介どうも

> ID:doVY1jXx
>>171,172
と
>>170
それと
> ID:8OeQUrrJ
>>189,190
と
>>181
か
触らんとこ

>>189-190
フォローありがとう

そもそも
>>181
>「やらない理由はない」と言って不必要な仕事を指示された時に
>論理的に反論したいのですが

これで、理屈っぽいフランス人ならどうするかを、頭に置いて考えてみました
「やらない理由はない」など、サギセールスまがいの理由をいうのは、いまどき？

昔は「君、これやってくれ」だったけどｗ　パワハラと言われるのがいや？ｗ
会社に、セールス電話で「だんな先物取引で儲かります。”やらない理由はない”です」とかあったなｗ

君がやらなくても会社は困らないは正しいと思うが
会社から見て、「君はいなくても困らないよ」と言われないようにしないとね

>>191
自分が読んだ本はメジャーで読まない本はマイナーって
どんだけ自己中心的なんですかねぇ

https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

Tableaux can be intuitively seen as sequent systems upside-down.
This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).

https://web.archive.org/web/20160305011658/http://www.cle.unicamp.br/jancl/logica/Nova%20pasta/Vol%208/vol8part1/59a76.pdf

＞会社から見て、「君はいなくても困らないよ」と言われないようにしないとね
会社からみて、必要なのは労働者　不必要なのは社長をはじめとする管理職

これ明らかね　管理職の仕事ってただのブルシット・ジョブだから

馬鹿乙

今日見つけた怪しい書き込み

>1.ラッセルのパラドックスの発見（1902年）
>1902年、哲学者のバートランド・ラッセルが論理学における矛盾を発見しました。
>このパラドックスは、通常の論理学では回避できないことが判明し、
>哲学に大きな衝撃を与えました。
>2.ラッセルによる新しい論理学の構築（1903年〜）
>1903年以降、ラッセルはパラドックスの原因が論理学の仕組みにあると見抜きました。
>自己と自己言及を明確に区別して混同しないルールを導入し、
>パラドックスが起こらない新しい論理学の仕組みを構築しました。

>4.ゲーデルの不完全性定理（1931年）
>1931年、クルト・ゲーデルもラッセルの論理学に影響を受け、
>「論理学によって仮定そのものの正しさをその仮定から証明できるか？」を考察しました。
>ゲーデルは、それが不可能であることを証明しました（ゲーデルの第一不完全性定理）。
>この定理は、当初ペアノ算術におけるω無矛盾性が証明不可能として確立されましたが、
>後にロッサーの証明ではペアノ算術における単純無矛盾性、
>シェファードソンの表現定理により任意のΣ1集合で構成される任意の論理式に対して
>無矛盾性の証明が不可能であることまで拡張されました。

続き
>ラッセルのパラドックスは、ある集合が自分自身を含むかどうかという自己言及から生じる矛盾です。
>このパラドックスが発生する論理体系では、自己言及によって簡単に矛盾を作り出すことができてしまいます。
>しかし、実際にはラッセルが開発した新しい論理学によって、このパラドックスは解決されました。
>つまり、ラッセルのパラドックスは本来矛盾ではないのです。
>問題は、ラッセルのパラドックスが矛盾を引き起こす論理体系では、
>本来矛盾ではないものを自動的に矛盾していると仮定してしまうことです。
>この「矛盾ではないもの=矛盾している」という誤った前提が常に存在していることになります。
>この誤った前提が存在すると、爆発律という原理が成立してしまいます。
>爆発律とは、矛盾から任意の結論を導き出せるという原理です。
>つまり、矛盾を前提とすれば、どんなことでも真とも偽とも証明できてしまうのです。
>そのため、ラッセルのパラドックスを引き起こす論理体系で導かれた結論は、意味がないということになります。
>矛盾を前提としているため、導かれた結論が真であるのか偽であるのか判断できないからです。
>したがって、ラッセルのパラドックスを回避する仕組みを持たない論理体系で得られた結論は、
>信頼性に欠けると言えます。
>ラッセルが開発した新しい論理学のように、
>矛盾を回避する仕組みを備えた論理体系を使用することが重要なのです。

>>197-198
>今日見つけた怪しい書き込み

ご苦労さまです

　早めの証拠保全（下記）
　https://rio2016.5ch.net/test/read.cgi/math/1676110842/219-222
『なぜ数学の非専門家は「選択公理」や「不完全性定理」が好きなのか？』より

１）”哲学者のバートランド・ラッセルが論理学における矛盾を発見”は、ヘン（正しくは素朴集合論）
２）”通常の論理学では回避できないことが判明”も、ヘン（正しくは素朴集合論）
３）”ラッセルによる新しい論理学の構築”も、ヘン（正しくは型理論による集合論）
４）”1931年、クルト・ゲーデルもラッセルの論理学に影響を受け”も、ヘン（正しくは、ヒルベルト・プログラムの研究）

ともかく、『怪しい書き込み』でした

https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%83%E3%82%BB%E3%83%AB%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9
ラッセルのパラドックスとは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった
概要
「それ自身を要素として含まない集合」を「M集合」とし、「すべてのM集合を成分とする集合R」を作ってみる。そうすると、「任意の集合X」に関しては、「XはRに含まれる」⇄「XはXに含まれない」という定式が成り立つ。
そして特にX=Rとすれば、「RはRに含まれる」⇄「RはRに含まれない」となり、パラドックスが明示される。
矛盾の解消
公理的集合論によって何をもって集合とするかについての形式的な整備が進められ、素朴（だが超越的）な
R の構成を許容しない体系が構築された。

1.公理的集合論による解消[注 1]
具体的には内包公理を次の分出公理に弱める（ツェルメロによる版）。
（なお現在のZFC集合論では、フレンケルが設定した置換公理から分出公理が導けるため、分出公理自体は公理としていない。）
2.単純型理論による解消[注 2]
略す
3.部分構造論理による解消[注 3]
略す

https://ja.wikipedia.org/wiki/%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E3%81%AE%E4%B8%8D%E5%AE%8C%E5%85%A8%E6%80%A7%E5%AE%9A%E7%90%86
ゲーデルの不完全性定理 または不完全性定理とは、数学基礎論[1]とコンピュータ科学（計算機科学）の重要な基本定理[2]。（数学基礎論は数理論理学や超数学とほぼ同義な分野で、コンピュータ科学と密接に関連している[3]。）　不完全性定理は厳密には「数学」そのものについての定理ではなく、「形式化された数学」についての定理である
クルト・ゲーデルが1931年の論文で証明した定理であり[5]、有限の立場（英語版）（形式主義）では自然数論の無矛盾性の証明が成立しないことを示す[3][5]。なお、少し拡張された有限の立場では、自然数論の無矛盾性の証明が成立する（ゲンツェンの無矛盾性証明（英語版））

ゲーデルはヒルベルトと同様の見解を持っており、彼が不完全性定理を証明して示したのは、ヒルベルトの目的（「無矛盾性証明」）を実現するためには手段（ヒルベルト・プログラム）を拡張する必要がある、ということだった

>>195
わからなくもないが
どこかかび臭い言い方

>>199
>正しくは素朴集合論
　というか無制限の内包公理
https://ja.wikipedia.org/wiki/%E5%88%86%E5%87%BA%E5%85%AC%E7%90%86#%E7%84%A1%E5%88%B6%E9%99%90%E3%81%AE%E5%86%85%E5%8C%85%E5%85%AC%E7%90%86
>正しくは型理論による集合論
あるいは、新基礎集合論
https://en.wikipedia.org/wiki/New_Foundations
ただ、この理論では、杓子定規にいえば、自然数はそれぞれ異なる階層に属する
0={}　0階
1={{}}　1階
2={{}，{{}}}　2階
3={{}，{{}}，{{}，{{}}}　3階
…
また、公理的集合論でも同様だが、
全ての自然数の集合の存在を規定するため
人工的な公理（無限公理）を設定せざるを得なくなる

>>199
>正しくは、ヒルベルト・プログラムの研究
>有限の立場（形式主義）
ここでいう有限の立場は具体的に言えば原始帰納的算術(PRA)
https://ja.wikipedia.org/wiki/%E5%8E%9F%E5%A7%8B%E5%B8%B0%E7%B4%8D%E7%9A%84%E7%AE%97%E8%A1%93
これはペアノ算術より弱い体系である

>>202
PRAで定義される帰納的関数の全体って可算じゃない？比嘉さんになりそうな気がしないけど

>>203　？

>>204
単純な疑問
非可算か可算かわかる？

>>204　なんで非可算が突然出てくるの？

それから、可算だと何がいけないの？

>>207
だから単純な疑問だって
そうなるかなって思ったの

>>208　
ただの疑問なら、202へのアンカーは不必要かと

>そうなるかな
そう（＝可算に）なるとして、あなたならどうやってそれを示しますか？
それが数学ですよね？　数学したいなら、一度考えてみてくださいね

R=Map(N,2)だと群構造表さないよなあ
コンパクトオープンで位相定義するとまた色々できそうだけど

>>209
PRAについて知ってると思ったから
もしかしたらわかる人かなと
自分にはそうなりそうと思うだけで
可算かどうかはわかんない

>>211　
検索すれば答えは書いてありますけどね　ネットの検索方法知りませんか？

>>212
書いてある？
よければ教えて？

ゲーデルの算術化で帰納的関数全体は可算になる？
もっと具体的な証明が知りたいなあ

>>212
> ID:kr5FQ87d
PRAを紹介しただけで詳しくは知らないということ？
それが悪いと言ってるわけじゃないよ
君に聞くべきではなかったと反省すべきだったみたい

>>215
ネトネトした気持ち悪さを感じる
控え目に言って汚物

>>216
ごめんね

>>213 何を？　検索ワードを？
>>214 ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
>>215 有限の立場＝PRA、と述べただけで、PRAについて皆様に説明する義務は負っておりませんが

>>216
>>203の書き込みから、ID:1s3pLI9Iを不審者と感じました。

>>218,219
ごめんね

>>218
>ゲーデルコーディングで、でこれ以上無いほど完全に具体的かと
やっぱそれか
サンクス
さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
できそうには思うけどよくわからないなあ

>>220　何かやましいことがあったのですか？

>>222
君に聞くべきではなかったのを聞いてしまってごめんてこと

>>221
>>ゲーデルコーディング
>やっぱそれか
やっぱそれです

>さまざまな定義の帰納的関数に対してどうゲーデル数を指定するのか
文字で関数を記載することは認めますか？
文字から数へのコード化もできるのだから
文字列から数へのコード化もできますね
だったらそんなに難しいことではないですよ

>よくわからないなあ
何がわかりませんか？
わからないことがわからないですが

>>223
>君に聞くべきではなかったのを聞いてしまってごめんてこと
「聞けば即座に答えてもらえると思ったのに答えてもらえなかった」
としてもそれはあなたの罪ではないのではないですか？

おかしな人だ

もし、203に202へのアンカーがなく
「脱線ですが
　PRAで定義される帰納的関数の全体って可算じゃない？」
とだけ質問したならば、こう答えましたけど

「ええ、そうですが　それが何か？」

脱線質問なのに過去の書き込みと関連があるかのごとく書いたのが不審ということです
数学板に限ったことではないですが、不審者が多いのでね

Xで掛け算の順序について支離滅裂な主張を延々としている奴が居て笑える

>>228
https://rio2016.5ch.net/test/read.cgi/math/1690886079/

>>228
小学校の先生に言わせると
足し算も順序があるらしい

掛け算順序論（というか掛け算定義教）は
「a✕ｂはａをｂ回足すという定義　これ以外は定義ではない」
というカルト宗教だそうである

しかしながら掛け算の定義の仕方は１つではないし
算数における掛け算の定義を１つに決める必要もない

これを掛け算無定義論と呼ぶことにしようかと思う

私は全てのa,bの対してa×b=0と定義します
そうすれば計算が楽でいいですよ
おすすめです

界隈の定義がこうだから、解釈も定義に従って行わないといけないっていう感じが理解できん
定理に基づいて式を立ててもいいじゃない

独自の定義をした上で、それが標準的な定義と同じ結果を与えることを証明してから回答を書いてもいいんですよ？

掛け算の順序が問題となる小学校の算数でそこまでできる人がいるかは知りませんけど

>>234
＞独自の定義をした上で、
＞それが標準的な定義と同じ結果を与えることを
＞証明してから回答を書いてもいいんですよ？

最後の？が気持ち悪いですね

もし、文章の末尾が「よね」だったらそう感じないんですが

「よ」だったら断定なので「？」はつかない
「？」とつけたら問いかけなので末尾は「よね」でしょう

こういうチグハグな文章を２１世紀のネットではよくみますが
国語力の低下というか人類の知的退化の現れでしょうか？

さて本題

＞掛け算の順序が問題となる小学校の算数で
＞そこまでできる人がいるかは知りませんけど

いないでしょう　求められているのは証明ではなく定義の柔軟性かと

算数は数理論理学ではないので、これ以上の言及はいたしませんが
（完）

K〇〇oとかいう馬鹿が他人を見下して支離滅裂なこと書いているから痛すぎる
あいつ自分の書いていることが論理矛盾だと気付かないんだな
アメリカだと日本とは逆の順序で計算するという指摘には規則を決めて計算
するのだから別に問題ないみたいに書いているのに、日本のような順序でないと
論理的な意味がないみたいなこと書いていて自己矛盾していて正直馬鹿だと
しか思えん

KONO氏は昔から逆張り大好きな人だったなあ
要するに定義に従えってことでしょう
そもそもどう定義しても同じなら
定義の仕方にこだわっても意味ない
って発想はないみたいだけど

某スレに、「小学科校から国語のやり直し」を連呼する基礎論婆（数学落ちこぼれ）がいた

このスレに居そう

KONO酷いな
あいつ幼稚園児並みの勘違いをしているな
スカラー×ベクトルの例で非対称性を主張し続けているけれど論題はそこ
ではないだろ
スカラー×スカラーの積の可換性はネーターの定理の保存則の存在から
対称性が存在するんだから対称と捉えるのが当然だろ
（一つの籠の中のリンゴの数をa個）、（籠の数をb個）とした場合に合計
何個リンゴがあるかという問題であいつの主張は原理主義者が（一つの籠
のリンゴの数をb個）、（籠の数をa個）として計算することを許容している
即ち無理やり対称性を仮定しているとか言ってんだよな
頭がが悪すんじゃないのかなあいつ

掛け算順序に固執する人の発想が「スカラー×ベクトル」なのはなんとなく見当がつく
で、問題はそう考えなければならないか、というところで、個人的には「んなこたぁない」と思ってる

KONO氏はレスバしたがってるだけなので相手しても時間の無駄よ

>>241
そんな高度な話じゃないぞ
定義の問題

全ての🎁の中に🍎🍎🍎🍎🍎　ある。
そして🎁🎁🎁だ。🍎はいくつあるかというと
地球人は、3+3+3+3+3って計算するのかな❓
ポクは、5+5+5で計算します。ピミ達はどっちで計算するの❓

🎁🎁🎁からそれぞれ１コ🍎を取り出すなら3+3+3+3+3ですが何か？

直観主義論理で西村巌という人が重要な仕事をしているらしい
ネットで調べてみても岐阜大にいたこと以外何の情報もない

>かけ算に順序はない」の(ひとつ分)x(いくつ分)と異なる間違った定義のリスト。これで尽きてる

0)値が同じなら式も同じ(式に意味はない)
1)定義はない (半環など未定義演算
2)アレイ図を数える (直積濃度
3) (いくつ分)x (ひとつ分)の両方が成立
4) (いくつ分)x (ひとつ分)との不定状態

やっぱりこいつ真性の馬鹿なんだな

>>247　レスバしたい人を相手すると時間空費するからやめとき

論理学において、「矛盾」の扱いが雑なように感じる。
数理論理学では「矛盾」をどう扱っているのだろう。
単純に排除されるべきものとして扱われているのだろうか、
という疑問。
矛盾は数学的対象なのか？

Pと¬Pの両方が導かれることを矛盾という
矛盾からはいかなる命題も導かれることになっている
これは空集合がいかなる集合の部分集合でもあることに対応している

ありがとう

Pと¬Pの両方が導かれる場合、排中律は成り立っていない。
爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
さらに、Pが自己同一性をもっていないとすれば、命題ではない。
それなのに爆発律があるかのように扱われているのは矛盾する。
爆発律は、妥当でない推論の例なのではないか？
爆発律が存在する（形式）論理体系なんてものは存在するのだろうか、という疑問。

＞Pと¬Pの両方が導かれる場合、排中律は成り立っていない。
実際は排中律もその否定も導かれる
＞爆発律の推論は、排中律を除外して成り立っていなければ妥当とは呼べない。
排中律も導かれるという意味では成り立つ
＞Pが自己同一性をもっていないとすれば、命題ではない。
自己同一性とは？意味がわからんが
＞それなのに爆発律があるかのように扱われているのは矛盾する。
だから矛盾してるっていってるんだが　記憶能力ゼロ？
＞爆発律は、妥当でない推論の例なのではないか？
そもそも矛盾してない場合、爆発律を使うことはない
＞爆発律が存在する（形式）論理体系なんてものは存在するのだろうか
いかなる命題を前提してもトートロジーは導ける
この対偶が、矛盾からいかなる命題も結論できるという爆発律

爆発率てのは人→Pのことだけど
これをそう呼ぶのはいかがなものか
P→Qとは単にモデルによる真理値割り当てにおいて
P≦Qであるということを言っているにすぎない
つまり人の真理値がボトムだという主張が人→Pの意味であり
人がどういうものであるべきかを意味している公理と言える
矛盾を定義しているという意味から
この公理は矛盾律と呼ばれるべきかと思うけどね

うーん、理解されなかったか。
Pがなんらかのタイプの矛盾であるとき、
P ⊢ Pは妥当なのか。

>>255
自分が理解していないから問題点を明確に書けない

>>252
>爆発律は、妥当でない推論の例なのではないか？
P∧¬P→人
は¬Eという推論規則を公理化したもので
矛盾律人→Pと合わせて
P∧¬Pは人と同等であることを言っている
（ここで同等とはお互いを導き合うこと
一般には同値と呼ばれるが自分は同等と呼びたい）
矛盾律を公理としない場合でも
人がある論理体系ならP∧¬P→人は公理もしくは推論規則にするだろうから
矛盾にさまざまな階層が生まれることになる
つまり人はもはやモデルによる真理値割り当てでボトムではなく
もっと低い真理値も容認されることになる

>>255
Pが矛盾でも何でもP→Pは成立するよ

P→Pが成立しないような矛盾は数理論理学では
扱えないということなら納得します。

大概の論理で
Pを矛盾として
P→Pは成立するよ
成立しないのは
PからQが導かれてもP→Qが成立しないとするような
相当つまらない論理だけでしょ

つまらない論理ではないと考えているから質問しています。
まあ、そこだけみて閉じてしまえばつまらない論理でしょう。
数学屋ではないのでちょっとやろうとしていることが違うのであしからず。
ありがとうございました。やくにたちました。

>>261
>つまらない論理ではないと考えている
PからQが論証できてもP→Qが成立しないような論理が
どうしてつまらなくないと思えるのかしれないけど
お好きにどうぞとしか

>いかなる命題を前提してもトートロジーは導ける
>この対偶が、矛盾からいかなる命題も結論できるという爆発律

矛盾からいかなる命題も結論できる、というのを否定するなら
いかなる命題を前提してもトートロジーが導ける、も否定される

トートロジーの否定は構文上はFalseではなくね？

矛盾はFalseだが

P⋁¬PがTrueなら¬P∧PはFalseだが？

¬(P∧¬P)とFalseは構文としては違うじゃん

爆発律って
P∧¬P→Q
か
False→Q
ぐらいしか流儀はないと思うのだが、
Pがトートロジーのとき
¬P→Q
なんて流儀は無理やろ

Pがトートロジーのときは¬PからFalseが導けるからFalse→Qから¬P→Qが云える

トートロジーかどうかを推論規則の前提にするわけにはいかんじゃろ

>>226
自然数の帰納的関数であるこれってどうコーディングされるの？

a,b,cは自然数
Xは0個以上の非負整数
a#bはb個のa

a{}0=a
a{}b=1+(a{}(b-1))
a{0}0=0
a{0}b=a{}(a{0}(b-1))
a{c}0=1
a{c}b=a{c-1}(a{c}(b-1))
g()=1{}1{}1
g(0)=g(){}1
g(a)=g(){g(a-1)}g()
G()=g(g(0){1}g())
G(0)=g(G())
G(a)=g(G(a-1))
G(0#c,0)=G(G()#c)
G(0#c,a)=G(G(0#c,a-1)#c)
G(X,b,0#c)=G(X,b-1,G()#c)
G(X,b,a)=G(X,b-1,G(X,b,a-1))
G(X,b,0#c,a)=G(X,b-1,G(X,b,0#c,a-1)#(c+1))
GG()=G(G()#G())
GG(0)=G(GG()#GG())
GG(a)=G(GG(a-1)#GG(a-1))

>>270
Pがトートロジー　⇔　¬Pから矛盾が導ける　は認めないの？　
認めないとして反例示せる？

>>270
そこまで書けるならできるじゃん　脳味噌あるだろ？

ヒント（というよりほぼ答え）
文字を数に置き換えてそこから文字列を数に置き換える方法を考える

>>274
それは単純な式なら分かるけどさ
複数の式で定義されている
しかもその複数の式に使われている
帰納的な記法が一定の範疇に収まらないのを
どうするのかなと

人間が見て帰納的だと分かる記述でも
いくらでも記法を新しく追加できるから
あるコーディング手法で定義された関数全体が加算だったとして
そこで使われる帰納的記法に収まらない記法を使って記述される帰納的関数は
そのコーディング手法では記述できないから
その帰納的関すに使われた記法も含めたさらに大きなコーディング手法を導入してコーディングするんでしょ？
でもまたその範疇に収まらないのが出てきて・・・・って終わらないんじゃないの？
可算集合の可算なcofinalな集合は可算でも
帰納的記法はいくらでもつまり非可算でもあり得るんじゃ無い？

その困難を避けるには
どんな非可算に多い帰納的記法を使って定義した帰納的関数も
ある一定の記法にしたがって定義した帰納的関数と同じ関数になることを証明できればいいんだけど
はてさてソレ可能なのかしらん
だって人間の想像力は「無限大」で>>271みたいなへんてこな記述だって思いつくわけでしょ

各個撃破で>>271は一定の記法に書き直せるかもしれないけど
それじゃ安心できないんだなあ

ゲーデル数のようなコーディング手法によってすべての帰納的関数をfnと付番できたとすると
g(n)=max_(m<n)fm(n)
と定義した関数はいずれはどのfnよりも値が大きくなるから
gが帰納的関数なら
すべての帰納的関数よりいずれは大きくなるはずなのに
g<g+1だから矛盾よね
だからgは帰納的関数じゃ無いんだけど
この定義ってホントに帰納的な記述じゃないのかな？
ゲーデル数みたいなコーディング手法って算術化つまり数式で表せるんでしょ？
ならfnみたいな付番も帰納的にできるんじゃなくて？

>>275
>帰納的な記法が一定の範疇に収まらない
そんなことある？

>>276
>いくらでも記法を新しく追加できる
>そこで使われる帰納的記法に収まらない記法を
>使って記述される帰納的関数は
>そのコーディング手法では記述できないから
>その帰納的関すに使われた記法も含めた
>さらに大きなコーディング手法を導入して
>コーディングするんでしょ？
収まらないってことある？

>>277
>どんな非可算に多い帰納的記法を使って定義した帰納的関数も
>ある一定の記法にしたがって定義した帰納的関数と
>同じ関数になることを証明できればいいんだけど
なんで帰納的記法が非可算になるの？
そんなことないけどな

>>278
>各個撃破で一定の記法に書き直せるかもしれないけど
>それじゃ安心できないんだなあ
包括的に一定の記法で書き表せるけど
安心できないのはそれが理解できてないからじゃね？

あと、いっとくけど、原始帰納的関数ね

>>279
「PRAで」って条件忘れてる？
primitive recursive arithmeticだよ

君がいう関数はもちろん作れるけど
それってprimitive recursive functionではないよ

アッカーマン関数ってあるじゃん
あれって原始帰納的関数じゃないよ

もしかして帰納的可算集合は帰納的集合かって聞いてる？
それならもちろん違うよ

Konoとかいう馬鹿を見ていて強く感じることはあいつは双対性の
概念を理解していない
それに尽きる

>>272
認めるって何？
トートロジーの否定から任意の命題が出るっての形では推論規則や公理には採用できないって話してるつもりなんだけど

>>280
>あと、いっとくけど、原始帰納的関数ね
ということは原始帰納的関数全体は定義の仕方が一定のルールに基づくものだから可算だけれど
何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？

>>281
>アッカーマン関数ってあるじゃん
>あれって原始帰納的関数じゃないよ
じゃあ>>271も原始帰納的関数ではない？

>>272
結局これなんだったん？
推論規則のどれを削るとどうなるかみたいなコンテキストだと思ってたんだけど、排中律取り除いたらその主張は成り立たないよね？トートロジーであることの定義をこねくり回したりしたら知らんけど

>>285
>何らかの意味で帰納的（人間が帰納的に考えうる）関数全体は可算ではないとか？

というより帰納的関数だけを数えその他の関数を除くような帰納的関数は存在しない
ここで「除く」というのは「帰納的でない」という返答を返すという意味
帰納的な場合だけ「帰納的だ」といえばいいのであればOK　これが帰納的可算集合

>>286
原始帰納的関数の定義を確認してごらん
その上で、その定義の方法で実現可能か確認してごらん
それが答えだよ

>>284
＞トートロジーの否定から任意の命題が出るっての形では
＞推論規則や公理には採用できないって話してるつもりなんだけど

矛盾を導くのに、全く無関係な命題が入っていてもOKなら
それが爆発律と同じことっていってるけど理解できてる？

論理に限ったことではないけど、考えないと見て感じるだけでは理解はできないよ

>>288
>帰納的な場合だけ「帰納的だ」といえばいいのであればOK
その関数は帰納的でない関数を与えた場合は終わらなくなるみたいな？
つまり関数と言っても数学的な意味（値が定まる）でなくて
プログラミングでいう関数なのね？

>>290
関数の記法は決まっている筈（つまりプログラムとして書けることが必須）
その上で、答えが返ってこない場合は終わらない、という感じ（停止判定）

＞関数と言っても数学的な意味（値が定まる）でなくてプログラミングでいう関数なのね？
プログラムで書けない関数は初めから勘定外かと
（プログラムとして書ける＝ゲーデルコード化可能）

>>291
ふむサンクス

>>289
何言ってるのか全然わからん

>>293
脳味噌ある？

>>289
なんの話をしてるのかそこからまずわからん
爆発律に関して何を話してるのかいな？

　矛盾Q∧¬Qから任意の命題Pが証明可能
⇔矛盾Q∧¬Qかつ任意の命題の否定¬Pが矛盾
⇔任意の命題の否定¬Pから排中律（矛盾の否定）¬Q∨Qが証明可能

>>296
爆発律が推論規則に入ってる場合の話をしてるの？入ってない場合の話をしてるの？
問題の建て付けのところからすでにわからんのだが

爆発律を推論規則に入れる意味ある？

>>298
古典論理なら
二重否定の除去DNEから
自然と導かれるよ
逆に言えば
それがトートロジーでないなら
二重否定の除去がいつもできると限らないことになる

>>298
自分の想定してるのは直観主義のヒルベルトスタイルに排中律をいれたりいれなかったりだから入ってる

>>300
>ヒルベルトスタイルに排中律
ヒルベルト式だと排中律は内包されてるんじゃないの？
たとえばP∨Qは¬P→QにP∧Qは¬(P→¬Q)にするんでしょ？
論理演算が→と¬しかないから
排中律ないと制限きついでしょ

>>296
> 　矛盾Q∧¬Qから任意の命題Pが証明可能
これは「任意のPとQにたいして、Q∧¬Q ⊢ P」を意図してるの？それとも「⊢Q∧¬Q ならば ⊢P」なのか？
他の行も同じで何を書いてるつもりなのかさっぱりわからんし
⊢の定義をまずしないと何を言ってるのかさっぱりなんだが…

>>301
直観主義だとwikipediaの直観主義論理の項目のヒルベルト流の計算の節の形にするんよ

なんかurl貼ろうとしたら怒られたんだが…

>>301
あと古典と違って、君の言ってる問題があるから

＞しかしながら、直観主義的な論理結合子は、古典論理におけるように、他の論理結合子を用いて定義することはできない。（そのため {→,⊥}, {∧,¬},
{∨,¬} などの論理結合子だけを用いて定式化することはできない。）直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する。

こうなってる

>>304
>直観主義命題論理では習慣的に→,∧,∨,⊥ を基本的な結合子として採用する
が普通だからヒルベルト式で直観主義論理ってどうなんだろと思った

>>305
ヒルベルトスタイルの直観主義のいいところは、→しかない型付きラムダ計算に直積型とかを追加していく手順と同じことをやったら完成するところが気持ちいいんよ

結局、トートロジーおじは何が言いたかったんやろ

自説

>>306
たとえば
P∨Qを¬P→Qとするか¬Q→Pとするか
これらが同等であるべきことから
Q=¬Pのとき
¬P→¬Pと¬¬P→Pが同等
つまりDNEがトートロジーになるので
必然的に古典論理になるでしょ

爆発律君こそ、何がしたいんだろ？

制限するって何をどう？
まあ、Weakeningを入れないとかそういうことなんだろうけど

>>309
なので、wikipediaの直観主義論理の項目のヒルベルトスタイルの節にあるような公理を使うんよ

>>311
ゲンツェンのシークエント計算ではいかんのかい？
そこの構造規則っていうのがあるだろ？
それ見直すってのはどうよ

>>312
爆発律が公理じゃないのと自分が慣れてないから、どこいじればいいのかすぐには想像つかんな

>>311
見たけどこれ
ヒルベルト式じゃ無いやん
てか
これなら普通の直観主義論理で
なんでコレをヒルベルト式て呼びたいのか
意図が知れん

>>314
そうなんかな
ヒルベルトスタイルが何かなんて人によってマチマチかもしれんけど、とりあえず自分はこの体系で爆発律をつけたり外したりしてた

>>312
ちょっと考えてみたけど
A ⊢ A
A, ¬A ⊢
A, ¬A ⊢ B
で爆発律がでるから、右側は1個以上に限るってのか、0個から1個への弱化を禁止するかが候補じゃないかなあ
LJからの類推だと前者がそれっぽい気がしない？

とここまで考えてカンニングしたら左側を1個に限定しろって書いてあったわ

横だけど、こういうとき論理の規則、p->q等、は何を前提とするの？

＞0個から1個への弱化を禁止

これが正解じゃね？

>>318
A ⊢ A
A, ￢A ⊢
A, ￢A, B ⊢
A, ￢A ⊢ ¬B
ちょっと弱い爆発律が導けちゃった

>>318
A ⊢ A
A ⊢ A, B
A, ￢A ⊢ B
わいの挙げた2つは両方ゴミだったw

>>317
形式的体系
• ヒルベルト流
• 自然演繹
• シーケント計算LK

こんな感じね、中味はしらんけど

二重否定の除去から爆発律がどうやってでるのか未だにわからんのだが
これどうやるんだ？体系になんか秘密があるのか？

40−16÷4÷2=

>>322
1）シーケント計算で最小論理はどういうもの？
2）シーケント計算でLJは後件が一つ以下となる理由は？

>>324
1しらん
2そうするとなんかうまくいったから

これ何の話なんだ？なんで急に質問が飛んできたんだ…

やっぱり二重否定除去から勝手な命題を降って越させるプランが全く想像つかん…

>>326
google(二重否定除去と矛盾の公理の関係に関する一考察)

>>327
さんくす
そっかFalse→¬Aの形は爆発律いらんのだったわ

>>325
>2そうするとなんかうまくいったから
何でうまくいくのかよくわからなくて

自然演繹ならそもそも使える道具に
排中律や二重否定の除去を入れないから
ああ直観論理だなあと思えるけれど
LJで健全性完全性を証明できても
どこに後件を1つ以下にすることが
効いてくるのか感覚がよくわからなくて

もちろん複数の後件を許せば排中律や
二重否定の除去が出てしまうから
出ないようにするには1つ以下に
しなくてはならないことはいいのだけど
証明能力がちょうど直観論理と一致する
ことと後件を1つ以下に限ることの
関連性が感覚的にわからない

>>324
>1）シーケント計算で最小論理はどういうもの？
自然演繹なら矛盾律人→Pと排中律P∨¬Pおよび
二重否定の除去¬¬P→Pを公理や推論規則から外すだけだけど
明示的に矛盾律を含めないLJから矛盾律を外すには
どうしたらいいんだろ

>>319
こちらは許容し（最小論理で証明できるから)
>>316
こちらはできないようにするために
>>318
これで上手くいくんだろうか？
A, ￢A ⊢ ￢B
もできなくなるからそもそもダメそうだし
>>316はできなくなるけれど
>A, ￢A ⊢ B
A, ￢A ⊢ Bが証明できないことが
証明できるようなA,Bの例が示せないといけないし

>>314
>見たけどこれ
>ヒルベルト式じゃ無いやん
これてクリーネの体系ていうやつの変種では？
NOT-1,2,3を除いてFALSEってのを入れてる

とりあえず、左側を1個以下にするのは
A, ￢A ⊢ ¬B
もなくなっちゃうんだよなあ
A∧￢A ⊢ ¬B
ならでるんかな
でなさそうだけども

ウィキペのシーケント計算の項目に
∧LL
○,A⊢○
○,A∧B⊢○
∧LR
○,B⊢○
○,A∧B⊢○
∧R
○⊢A,○　○⊢B,○
○⊢A∧B,○
∨L
○,A⊢○　○,B⊢○
○,A∨B⊢○
∨RL
○⊢A,○
○⊢A∨B,○
∨RR
○⊢B,○
○⊢A∨B,○
→L
○⊢A,○　○,B⊢○
○,A→B⊢○
→R
○,A⊢B,○
○⊢A→B,○
¬L
○⊢A,○
○,¬A⊢○
¬R
○,A⊢○
○⊢¬A,○
カット
○⊢A,○　○,A⊢○
○⊢○
Identity公理
A⊢A
あとはweakening cntraction permutationで
これは推論規則というよりは
論理式の列の性質というべき

結局カンニングして、¬はいれずにFalseをいれて、右側をピッタリ1個に制限すればいいということが分かった

ここでシーケント（推件）とは自然演繹における推論図の状況を表し
カットは自然演繹で2つの推論図をAで繋げること
∧Lは自然演繹の∧E
∧Rは自然演繹の∧I
∨Lは自然演繹の∨Eと∨Iの組み合わせ
∨Rは自然演繹の∨I
→Lは自然演繹の→Eとカットの組み合わせ
→Rは自然演繹の→I
¬Lは自然演繹の¬Eと後件における人の消去
¬Rは後件における人の導入と自然演繹の¬I
Identity公理は自然演繹における無駄な推論図を意味している
となると
シーケント計算における矛盾律は¬LRに内包されているんだと思うね
というのもなぜ後件で人を導入消去できるかといえば人∨A→Aがトートロジー
すなわち人→Aが成り立つことから来てるから
てことでLJから矛盾律を除外するなら
¬LRを制限するあるいは別の推論規則にする必要があるはず

やっぱ自然演繹の方がずっと自然だわ
シーケント計算は形が対称で綺麗だけど
かなり技巧的というか本質が覆われてる

>>337
>￢はいれずにFalseをいれて、
¬を入れないとは¬LRを使わないということ？
それはやりすぎだろ
>右側をピッタリ1個に制限
常に後件に論理式が1個？？
それでどうやって
A,¬A⊢¬B
導くの？

あーもしかして¬を入れないとは
演算として∧∨→だけてこと？
なんかそれもやりすぎなような気もするけど
確かに
¬Aはまず最初にA→人で置き換えればいいし
結果にA→人の部分があったらそれを¬Aにすればいいのか
（この置き換えは最小論理でも許されるはず）
その上で人⊢Aを公理にするかしないかで
LJとMLを区別すればいいのかな

>>340
¬のルールは消して、¬A := A→Falseにして
Γ ⊢ Δ
---------
Γ, False ⊢ Δ
を追加

目標は
A, A→False ⊢ B→False
なので、後ろ向きに機械的に適用できるルール使っていって逆順に証明を書くと
A, A→False,B ⊢ False →右
A, A→False ⊢ False 弱左
A ⊢ A とFalse ⊢ False →左

でできたぽい

¬LRを推論規則から削除して矛盾律人⊢Aも入れないことにして
A,A→人⊢B→人
を導けばいい
これはこんな風にできるね
A⊢A
人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人

>>341
LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず

こっちのがいいか
A⊢A　人⊢人
A,A→人⊢人
A,A→人,B⊢人
A,A→人⊢B→人
>>342
同じね

>>344
>右側が1つに制限するかか1つ以下に制限するかの違い
¬の代わりに人を導入することで
後件が空であることを明示的に
人と書いているだけじゃないかな
¬Lが無くなることで
後件が元々空でない推件からは
後件を空の推件を導けなくなってるよ

>>344
>LJとの違いは右側が1つに制限するかか1つ以下に制限するかの違いのはず
じゃあ
後件が空であってもいいことにした場合に
A,A→人⊢B
はどう導くの？

A⊢Aは公理だけど
⊢は公理じゃないから（むしろこれは真から偽が出ることを意味するからありえない推件）
¬Lを除外したことで後件が空の推件は決して現れないようになった
だから後件が空であることを許しても仕方ない
よってLJに戻すにはなんらかの公理なり推論規則を追加しないと
追加するのは矛盾律そのものである人⊢Aでいいと思うんだけどね

A⊢A　人⊢人　人⊢B
A,A→人⊢人　人⊢B
A,A→人⊢B
こんな感じ

>>347
なんかカンニングした
https://ncatlab.org/nlab/show/sequent+calculus
をだいぶ読み間違えてたわ

>>348
そう、そこ読み間違えてたっぽい

ここFランばっかだなw

>>352
Fランに詳しい人キタ

東都路地

↑これが数学板の実力です
専門板なのに異常にレベルが低い
せいぜい数学の少しできる高校生レベル

糖登呂爺

1階の述語論理で
∀xP(x)はxの全てについてのP(x)の∧で
(∀xP(x))⊢P(t)は∧Eに
P(x)⊢(∀xP(x))は∧Iに過ぎないし
∃xP(x)はxの全てについてのP(x)の∨で
P(t)⊢(∃xP(x))も∨Iに
(∃xP(x)),P(x)→Q⊢Qも∨Eに過ぎない
論理式の列を有限に限る必要はないと思う
むしろ上記のように全ての集合に対して全部とすることを許せば
1階の述語論理と変数のない命題論理（ただし命題変数は全ての集合に対するP(t)の全て）は全く同じものと分かる
なぜ
全ての集合に対しての論理式の列を許さず
∀xP(x)や∃xP(x)にするのだろう
全ての集合に対しての論理式の列を考えることで
何かパラドクスが起こるのかしらん

＞なぜ全ての集合に対しての論理式の列を許さず
＞∀xP(x)や∃xP(x)にするのだろう

論理式が有限文字数で書けないから
推論が有限回ですまないだろう
そんなものを人間は扱い得ないと思われる
パラドックスとかいう以前

いきなり全ての集合を登場させなくても
たとえば
∀x∈N∃n∈N(x<n)
=∀x∈N(x<0∨x<1∨x<2∨…)
=(0<0∨0<1∨0<2∨…)∧(1<0∨1<1∨1<2∨…)∧(2<0∨2<1∨2<2∨…)∧…
でいいのでは？
意味的には全く同じものだし
論理式の全体が定義できないかも？と思わなくもないが
多分大丈夫じゃないかな

>>358
>論理式が有限文字数で書けないから
なんだけど
想定はできるよ
書けなくてはいけないということ自体に意味があるのかな？

>>358
>そんなものを人間は扱い得ないと思われる
コンピュータには無理そうと思われるけどね

＞多分大丈夫じゃないかな
　楽天家はみなそういうが、皆死んでった・・・

無限論理というものがあるのは知ってるが
普及してないのはきっと上手くいってないからだろう

>>362,363
自然で∀も∃もいらないのに上手くいかないのってなぜかな
人間が無限を知覚するのにある一定の型にそったもの（P(x)）しか考えられないてこともないと思うんだけど不思議

ω矛盾してるようなのはどうするんやろ

>>364
>なぜかな
僕のせいじゃないよ
>不思議
だから僕のせいじゃないって

>>365
それは全部に証明がつけられてもその全部を∧したものに証明がないてことで
感覚的には当然かなと思える
てのは
証明の長さは有限じゃないといけないように思うから
無限を許すのは論理式の列だけで
証明の長さも無限を許すてのはどうかなあ
まあ絶対禁止というのでもなくてもいいかとも思うが

>>365
そうか
P(x)だけ考える場合
証明はどのxについても同じ長さだから
全部合わせても並列で同じ長さてことが効くのかも？

>>357
>なぜ
>全ての集合に対しての論理式の列を許さず

？
全ての集合を範囲とする量化はできるよ
∀S:Set. S=S

>>369
∀使わずそれを並列にするってことよ

内容は同じでしょ？許容してもいいんじゃないかな

>>368
それは長さだけじゃなくて、証明も完全に一致してるときねこれが∀I
全く同じじゃなくても再帰的な構造をもつ証明を要求するのが数学的帰納法
∧が有限個だと全く規則を要求しない
この関係を保ったまま無限に持っていくのは気持ち悪いね

>>372
全く同じ証明でなくても長さが同じなら
無限の証明を並列にまとめて一つにみなして
長さ有限の証明としていいように思うけどね

並列性を許容した上で証明の深さを有限とするなら、式の記述は無限長とするしかない
式の記述を有限長にするなら、そもそも記載できる内容が制限される