背理法は不要なのか

背理法被害者の会

https://abel.a.la9.jp/sub11.html

U.N.オーエンは彼女なのか

そう、これは昔に議論があったのか気になっていた。
この板の住人が好きそうな話題ではないか。

ハイリハイリフレハイリホー

片桐はいり

江田勝哉が全部答えてるじゃん

そして江田勝哉もまた変な人ということで

>>4
数理論理学的に意味のない主張

私自身も、他人に強要はしないまでも、（狭義の）背理法が必要ない証明では、否定を仮定して矛盾を導く形式の証明を（見かけ上）避けていた時期があるが、証明支援系の関係で数理論理を勉強して、全く無意味なことだと分かった

「Pと¬Qを仮定して矛盾が言えたら、P⇒Qが言える」を避けて、
「¬Q⇒¬Pが言えたら、P⇒Qが言える」に統一したところで、
どちらも排中律または二重否定除去を使っているので、全く無意味。

どちらの論法が教育的に分かりやすいとかも無い。
どちらが分かりやすいかは示す命題による。

はい、終了！

√2の無理数性は、有理数であると仮定したら矛盾が導かれることを示すことでしか証明できないの？

(1) 命題Pの否定¬Pに、「(P→⊥)├¬P」以外の導入規則がある
(2) 実数xが無理数であることに、「ある述語Pに対する¬P(x)」以外の特徴づけがある

のどちらかが言えればいい

>>13
(2)は、¬P(x)以外の特徴づけがあって、それを満たすことを、xを有理数だと仮定して矛盾を導く以外の方法で証明できる

では

√2が無理数であることは背理法使わずにどう証明するの？

連分数展開が循環することによる証明を
ラグランジュが考案した

なるほど

√2 - 1 = 1/(1 + √2)から

√2 = [1; 2, 2, ...]

なので、無理数

無限連分数が無理数であることの証明には背理法 (否定導入?) 使うんじゃないの？

有理数・無理数の定義を、連分数が有限かどうかに変えればいい

実数が有限連分数と無限連分数で尽くされることの証明は？

正の実数の連分数展開の
簡単明瞭な手続きから
存在と一意性は明らかだが
連分数展開が有限で終わるか無限に続くかの
いずれかであることの証明を
したいとは思わない

「有理数の連分数展開は有限」の証明にも
背理法が必要だと強弁することは可能かもしれない

有理数の連分数展開が有限なのはユークリッドの互除法なので自然数の整列性 or 数学的帰納法だけから言えるはず

実数は連分数展開を持って一意（最後に余分な+1を加えない限り）
有限連分数展開を持つ実数を有理数、そうでない実数を無理数と定義
x^2 - 2 = 0, x > 0の解は無限連分数展開を持つ

「無限連分数展開を持つ実数は有限連分数展開を持たない」を示すのに否定導入使うからこれも駄目

無限連分数展開を持つ実数を無理数、そうでない実数を有理数と定義すればいいのでは

実数が構成できてる時点で有理数は定義されとるやろ

関係ない話かもしれないけど、無限降下法の証明も怪しいやつがいっぱいあるからなぁ（汗）

>>12
有理数で無い実数が無理数の定義だから
無理数であることの証明は
有理数で無いことの証明
有理数で無いことの証明は
畢竟
有理数であるとすると矛盾することをいう他ナイだろう

背理法って
畢竟
排中律でしょ
だから
直観主義で証明できればいいかも
直観主義だと
√２が無理数でないとは言えない
までは言えるはず

>>28
だから例を出せって
例も無しに批判だけしてどうする

>有理数で無い実数が無理数の定義
ならば

>無理数であることの証明は
>有理数で無いことの証明
無理数であることの証明は
実数であり且つ有理数でないことの証明
じゃね？

無理数の定義が「実数xは有理数」の否定であって、命題Pの否定¬Pの導入は「Pを仮定したら矛盾が導びかれること」なのだから、この前提のもと、無理数であることを示す方法は「有理数であることを仮定して矛盾を導く」以外には無い。

整数nは奇数、整数nは偶数のように、命題の否定が具体的に記述できるものなら、矛盾を示す以外でも証明できる

>無理数であることを示す方法は「有理数であることを仮定して矛盾を導く」
は不十分。実際、その方法で√(-1)が無理数であることが導けてしまう。

実数でね

実数の連続の公理より sup{r∈R|r>0∧r^2≦2}:=x は実数。
x≠√2 と仮定すると定義から矛盾が導かれるから x=√2。

ラグランジュの証明に一応の「なるほど」が
言えないやつとは友達付き合いがしにくい

>>33
>命題Pの否定¬Pの導入は「Pを仮定したら矛盾が導びかれること」
そうか
(P→人)→¬P
は排中律関係ないただの否定の導入だから
「有理数と仮定して矛盾を導く」
を背理法だとするのは誤りか
たんに
無理数の定義通りに示しただけと
定義通り示すことが
「有理数と仮定して矛盾を導く」
ということなのだから
これを背理法と呼ぶのであれば
無理数であることの証明に背理法は避けられないことに
（でも背理法と呼ぶことの方があやまりと思うが）

>>41
>”aa と 2bb の素因数の個数は偶数と奇数”が、天下りすぎ
任意の平方数の素因数は偶数個、よって2bbの素因数は奇数個
天下り過ぎ？　は？

そろそろ七夕

>>41 追加
実は、背理法被害者の会の話は、10年以上前に別スレで取り上げたことがある
下記は、プロ数学者の批判なので 参考になるだろう
渕野昌先生のコメントもあったのだが、検索ヒットしないので省く

(参考)
https://researchmap.jp/eda202110
江田 勝哉
基本情報
所属早稲田大学 理工学術院 基幹理工学部 名誉教授
学位
理学博士(筑波大学)

https://io.kuis.kyoto-u.ac.jp/mailman3/hyperkitty/list/[email protected]/message/QEVDOXW2PFXIMG7FCTMTKYYQALRRRLQY/attachment/4/temp.pdf
(2015 年に書いたもの）
数学基礎論の関連した、おかしな数学の先生たち
江田勝哉

脱背理法の本が出版されてしまった。今までにも、数学の先生の書
いた、数理論理学、集合論関係の本でおかしなものはある。この内容
よりも、ずっと凄まじいものもあるので、それらのおかしさを紹介し
ながら、数学基礎論(数理論理学、集合論) の専門外の人が、誤解しや
すいところを説明しようと思う。
P6
3. 背理法
関脇は初めに書いた本で「数理論理の手法- 証明の発見と背理法の
除去」安部直人中西泰雄共著で2015 年出版である。実は、この本は
読んでいない。ただ2013年2月の東京理科大の数学入試問題で、「この
問題の解答に背理法を用いてはならない」という但し書きのついた問
題が出題されたとき、安部直人先生にホームページに書かれている脱
背理法について、何をもって背理法といっているのか質問した。もち
ろん、これで話がつくはずもなく、また、丁度、ユタに3ヶ月いってい
るときであったので東京理科大のある先生と文科省にこの問題が不適
切であることを知らせた。そのため、私との間のやりとりで私の著書
に関してアマゾンに書いてあることが変であることも指摘した。そこ
で安部先生は当然、敢然と反論した、理解していないのだから仕方が
ないし、10 年以上、脱背理法にしがみついているのだから、変を認め
たら、死んでしまうかもしれない。そのようなわけで、ホームページ
の記述、アマゾンカスタマーレビューから変なことはよくわかってい
るので、本とは別に、この主張がいかに変かを書いてみる。横綱、大関
に比べると、数学的な主張としてインパクトのある点がない。その点
は三役に達していない、しかしこの教育効果という点では、横綱、大
関は引退しているのに比べ、現役でありかつ、共著者は引退に程遠い
事情から、三役入りした。

>>42
たぶん素因数分解の一意性を証明する際に
至る所で背理法使ってるはず

>>42
(引用開始)
>”aa と 2bb の素因数の個数は偶数と奇数”が、天下りすぎ
任意の平方数の素因数は偶数個、よって2bbの素因数は奇数個
天下り過ぎ？　は？
(引用終り)

背理法の
√2＝a/b
2＝aa/bb
矛盾
√2≠a/b
QED

この証明を知った後
式をこねくって
天下りに”aa≠2bb”として
”aa と 2bb の素因数の個数は偶数と奇数”だと

コロンブスのタマゴで
コロンブスのやり方（背理法）を知って
それを 少しだけ味付けと目先を変えただけに思えるってこと

>>45
>”aa と 2bb の素因数の個数は偶数と奇数”
の証明に素因数分解の一意性は不要だけど

>>45
>たぶん素因数分解の一意性を証明する際に
>至る所で背理法使ってるはず

なるほど・・・
そうかも・・・（＾＾

道具に背理法が潜んでいる罠

>>46
なるほど
君が「天下り」の意味を知らないだけでしたか

>>47
>>”aa と 2bb の素因数の個数は偶数と奇数”
>の証明に素因数分解の一意性は不要だけど

素因数分解の一意性の一つの系だということでは？
そして、そもそも 大学入試でも別解がしばしばあるように
いろんな 証明があっていいと思う

天下りに エレガントな式変形(実は知られた高等テクニックの一つ)を使うと 綺麗に解ける
昔の東大入試に多かった気がする
真正面から 力技で計算をすると 途中で式が発散して計算が大変になるとか
大学への数学の解答をみて、感心してました

背理法を目の敵にする意味わからん
証明テクニックの一つとして 自分の数学道具箱に入れて
何が悪い？ 意味わからん

>>47
素因数分解の一意性だよ？
aaと2bbの素因数が偶数個と奇数個を言うには
素因数分解に一意性が必要だし
もっと具体的に言えば
素因数分解の一意性が言えてなければ
aが偶数個の素因数分解ができてかつ奇数個の素因数分解ができるかも知れない

>>51
>>>”aa と 2bb の素因数の個数は偶数と奇数”
>>の証明に素因数分解の一意性は不要だけど
>素因数分解の一意性の一つの系だということでは？
だから違うって言ってるんだけど

>>52
>aが偶数個の素因数分解ができてかつ奇数個の素因数分解ができるかも知れない
だとしてもaaの素因数は偶数個だけど？

任意の自然数nに対して2nは偶数
たったそれだけ　中学数学

>>46 補足
背理法
√2＝a/b
2＝aa/bb
矛盾
2≠aa/bb
2bb≠aa

左右入れ替えると
aa≠2bb
”aa と 2bb の素因数の個数は偶数と奇数”だと？
これが 被害者の会の主張だと？

背理法証明を知ってるくせに
知らないふりで 言われても・・（＾＾

>>54
はぁ

aaの素因数の個数が偶数ってのが
素因数分解の一意性をフルに使った結果だっての

>>51
>天下りに エレガントな式変形(実は知られた高等テクニックの一つ)を使うと 綺麗に解ける
>昔の東大入試に多かった気がする
天下りの使い方間違ってる。

>背理法を目の敵にする意味わからん
>証明テクニックの一つとして 自分の数学道具箱に入れて
>何が悪い？ 意味わからん
古典論理なら何も
そうでないならそうでない
問題意識がズレてるよ君

>>56
>背理法
>√2＝a/b
>2＝aa/bb
>矛盾
この証明は否定の導入であって背理法と呼ぶべきではないと思うな

>>56
>”aa と 2bb の素因数の個数は偶数と奇数”だと？
うん
任意の自然数nに対して2nは偶数、2n+1は奇数。君知らないの？　中学中退？

素因数分解の一意性が言えてないとねぇ

「背理法不要論」を言う人は
(P→人)→¬P
も否定するんだろうから
直観主義論理よりもキツイ主張だね

オイラーやラグランジュが
背理法不要論者だったとは思えない

>>59
>>天下りに エレガントな式変形(実は知られた高等テクニックの一つ)を使うと 綺麗に解ける
>>昔の東大入試に多かった気がする
>天下りの使い方間違ってる。

じゃ
天下り
　↓
神がかり

とでもすればいい
ポアンカレが 馬車に乗ろうとしたとき フックス関数のアイデアが降ってきたという
ある日本の数学者が 閉店前の喫茶店でコーヒーを飲んでいると ある数式が振ってきた

aa≠2bbは、背理法証明の √2＝a/b から自然に出てくるよ （>>56）
が、背理法証明の √2＝a/bを知らない人が それをどうやって思いつく？
そこをすっ飛ばして、3行証明が 背理法証明より短いし 背理法よりえらいと言われてもね

>>65 タイポ訂正

ある日本の数学者が 閉店前の喫茶店でコーヒーを飲んでいると ある数式が振ってきた
　↓
ある日本の数学者が 閉店前の喫茶店でコーヒーを飲んでいると ある数式が降ってきた

余談
　>>41より
背理法の証明の中では、
結果的に正しくない仮定から論理的に正しくない矛盾を導くわけですから、
途中に更に多くの誤った主張が並びます。
”「私自身が、背理法のおかげで頭が腐った被害者であると実感しています。十数年前から現在もリハビリ中です。」(背理法被害者の会)”
(引用終り)

この論でいえば
夏目漱石 我が輩は猫である を読むと
読んだ人は、猫はみな人と同じように考えると思う？
そんなバカな
みんな、小説の中だけのことと分る
同じように、背理法の証明の中における 矛盾を導く過程の命題が 背理法の外で成り立つと？

少し 小説とかマンガ読んで頭を柔らかくしよう！
その方が、数学にも役立つぜ
そもそも、理科大以外の数学書に 結構背理法使っているテキストあるよ
どうするんの？ ”背理法のおかげで頭が腐った被害者”？ そんな人いないと思うよ
みんな 小説とかマンガ読んで頭を柔らかくしていますから

>>41
べつに論破する必要はない

>>10に書いてあるとおり、見かけ上「仮定する～仮定に反する□」という記述を避けたところで、

・論理学的には何の意味もない
・教育的にも分かりやすくなるわけではない

分からなさに対する耐性をつけることは
調和の精神に反することではないだろう

>>61
aがn個の素数の積で表せたとして
aaが2n個以外の素数の積で表せないことは
素因数分解の一意性を使わないと示せないよ

わ、わかんないっピ…。

証明の途中で間違った式が出てくることが問題というなら、たとえば、

∀x∈ℤ(xは4の倍数⇒xは2の倍数)

の証明も、x = 1, 2, 3などの場合も証明しているわけなので、問題ということになる。

学生の頃はネタにしてたけど……改めて見ると頭イカれてるな
そもそも数学者として業績あんの？？？HPに論文リストすらないし

>>68
ID:gbVnYdQv は、御大か
巡回ご苦労様です

>>67
中高一貫生も来るから ハッキリと書いておく
＜間接証明論：対偶法と背理法＞
１）対偶：命題 p→qに対して 対偶 ¬q→¬p(下記 進研ゼミ)は、同値（古典論理）
　（進研ゼミ ベン図見てね）
　但し、証明の容易さは 対偶の方が容易な場合がある
　例えば 3乗の因数分解 a3+b3+c3–3abc=(a+b+c)(a2+b2+c2–ab–bc–ca)（下記理系ラボ）
　この式の証明は、右辺→左辺が圧倒的に易しい(逆はテクニック要)
　pとq同値命題でも、p→qとq→pの証明容易さに差がある。対偶でも同じ
２）背理法：P かつ ¬Q を仮定して矛盾（空集合）を導く方法
　下記 chiebukuro.yahoo ベストアンサー qxx********さんの図
　P ⋀ ¬Q → Φ（空集合）です
　ここで、対偶との比較で、使える条件が 対偶の¬QとPと二つの組み合わせが使える利点がある
　そして、上記と同様 元のP→Qよりも 対偶¬Q→¬Pよりも 証明容易の場合がある
３）纏めると、命題P→Qの証明のとき、間接証明として 対偶法と 背理法とがあって
　それぞれ利害得失がある。命題P→Qが簡単証明できるときは、間接証明を考える必要がない

纏めると、命題P→Qが難しいと思ったときは、上記二つの間接証明を考えてみるべし
数学常用手筋です（＾＾

(参考)
https://kou.benesse.co.jp/nigate/math/a14m0120.html
進研ゼミ高校講座 > Ｑ&Ａトップ > 数学のＱ&Ａ一覧 > 【数と式】逆・裏・対偶の関係
・対偶の真偽が一致することは，ベン図で理解することもできます。
https://res.cloudinary.com/bend/f_auto,q_auto/shikakutimes/s3/bend-image/1152_0_contraposition-207x300.png
（上側のベン図は，P ならば Q およびその対偶が真である状況。下側のベン図はいずれも偽である状況を表しています。）

https://manabitimes.jp/math/1152
高校数学の美しい物語
対偶を用いた証明のいろいろな具体例 2021/03/06

https://rikeilabo.com/cubic-expansion-and-factorization
数学�U 3乗の因数分解（展開）公式 理系ラボ
教科書では公式として扱われていませんが、次の式も大学入試では頻出なので、覚えておきましょう。
a3+b3+c3–3abc(a+b+c)(a2+b2+c2–ab–bc–ca)

https://manabitimes.jp/math/1141
高校数学の美しい物語
背理法の意味といろいろな例 2021/12/15
対偶による証明と背理法
対偶法（対偶を用いた証明）と背理法による証明は混同されることがありますが，別物です。
ある命題 P→Q を示すときに，
背理法：P かつ ¬Q を仮定して矛盾を導く方法
対偶による証明：¬Q を仮定して ¬P を導く方法
です。しっかりと区別しましょう

つづく

つづき

https://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1399736633
chiebukuro.yahoo
ove********さん 2013/1/4
なぜp⇒qという命題の背理法では結論を否定して矛盾を見つけるんですか？

ベストアンサー
qxx********さん2013/1/5
証明方法の原理はベン図で考えると分かりやすいです。
p⇒qというのは、ベン図で言うなら、Pという集合の中に属しているなら、Qという集合の中に必ず属しているということと同義です。(図1)

背理法で行う「 p かつ (qでない) 」ことを仮定して、否定するというのはベン図で言うとどういうことか？
「 p かつ (qでない) 」は図2の斜線部分に相当します。
本当は図1のようにPは全てＱのなかにすっぽり入っていて欲しいのです。
ここで、ＰのくせにＱからはみ出している奴ら「 p かつ (qでない) 」を仮定してこいつらについて考えます。
そこで矛盾を導き出すことで、こんなはみ出し者どもは居ない、ということを証明し、PはすべてＱの中にすっぽりと入っていること、すなわちp⇒qを証明するのです。
これが背理法ですね
(引用終り)
以上

糞論はきちがいが寄り付きやすい

>>74
全然違う

>>73 補足

中高一貫生も来るから ハッキリと書いておくが

＜古典論理 vs 直観主義＞
１）特に断らない限り、普通は数学は 古典論理ベースと思っていい
　（ヒルベルトの形式主義が生き残った）
２）では、直観主義が完全に否定されたかというと 特殊分野では 生き残っている
　一つは、ラムダ計算 カリー＝ハワード対応 コンピュータプログラミング（除くAI）の世界
　（コンピュータプログラミングは、プログラム構成してなんぼの世界で、構成主義）
　一つは、量子論理の世界（流行りの量子コンピュータもこれ）
　つまり、普通のコンピュータプログラミングは 0か1のブール論理なのだが
　量子論理は 0か1に限られない（下記 en.wikipedia Boolean_algebra辺り からご自分で調べてください）

https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9_(%E6%95%B0%E5%AD%A6%E3%81%AE%E5%93%B2%E5%AD%A6)
直観主義（英: Intuitionism）とは、数学の基礎を数学者の直観におく立場のことを指す。
来歴と評価
これに類する主張は、カントールの集合論に対抗する形でクロネッカーやポアンカレによってもなされていたが、最も明確に表明したのはオランダの位相幾何学者ブラウワーである。ブラウワーの立場に対してポアンカレらの立場は前直観主義と言われることがある。ブラウワーは、数学的概念とは数学者の精神の産物であり、その存在はその構成によって示されるべきだという立場から、無限集合において背理法によって非存在の矛盾から存在を示す証明を認めなかった。それゆえ、無限集合において「排中律」、すなわちある命題は真であるか偽であるかのどちらかであるという推論法則を捨てるべきだと主張し、ヒルベルトとの間に有名な論争を引き起こした。 ヒルベルトの形式主義は、直接的にはブラウワーからの批判的主張に対し排中律を守り、数学の無矛盾性を示すためのものと考えることができる[1]。

ブラウワーの主張は感覚的で分かりにくかったが、その後ハイティング等によって整備され、結果的には古典論理から排中律を除いた形で形式化されたものが今日、直観主義論理として受け入れられている。 現代では直観主義論理は、数学の証明は全て構成的に為されなければならないという主張（数学的構成主義）と関連が深いと考えられている。

https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9%E8%AB%96%E7%90%86
直観主義論理
ラムダ計算
カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。[6]

https://en.wikipedia.org/wiki/Boolean_algebra
Boolean algebra

>>73 タイポ訂正

a3+b3+c3–3abc(a+b+c)(a2+b2+c2–ab–bc–ca)
　↓
a3+b3+c3–3abc＝(a+b+c)(a2+b2+c2–ab–bc–ca)

（補足）
右辺を展開して、左辺を得るのは簡単
左辺を因数分解して 右辺を導くのは いろいろテクニックが必要

ω

>>74
>p⇒qというのは、ベン図で言うなら、Pという集合の中に属しているなら、Qという集合の中に必ず属しているということと同義です。(図1)
背理法以前にp⇒qの真理値表から分かってないんじゃ？

ベン図は一般的な部分集合が4つある場合、真円で書くことが不可能な場合があるらしい。楕円では可能みたい。

問題に出来るかもね。
真円で書けない部分集合の例を挙げよとか。

対偶の話でベン図を持ち出す奴は十中八九何も理解できてない

>>74 補足
(引用開始)
証明方法の原理はベン図で考えると分かりやすいです。
p⇒qというのは、ベン図で言うなら、Pという集合の中に属しているなら、Qという集合の中に必ず属しているということと同義です。(図1)
背理法で行う「 p かつ (qでない) 」ことを仮定して、否定するというのはベン図で言うとどういうことか？
「 p かつ (qでない) 」は図2の斜線部分に相当します。
本当は図1のようにPは全てＱのなかにすっぽり入っていて欲しいのです。
ここで、ＰのくせにＱからはみ出している奴ら「 p かつ (qでない) 」を仮定してこいつらについて考えます。
そこで矛盾を導き出すことで、こんなはみ出し者どもは居ない、ということを証明し、PはすべてＱの中にすっぽりと入っていること、すなわちp⇒qを証明するのです。
これが背理法ですね
(引用終り)

あれあれ？
下記の高校数学の美しい物語
の対偶法説明のベン図も全く同じですぜ だんな

　>>73 より
https://manabitimes.jp/math/1152
高校数学の美しい物語
対偶を用いた証明のいろいろな具体例 2021/03/06

対偶の真偽は一致する
対偶の真偽が一致することは，ベン図で理解することもできます。
https://res.cloudinary.com/bend/f_auto,q_auto/shikakutimes/s3/bend-image/1152_0_contraposition-207x300.png
「P ならば Q」が真
  ⟺P が Q に含まれている
  ⟺Q の外側が P の外側に含まれている
  ⟺ 「Q でないならば P でない」が真

・上側のベン図は，P ならば Q およびその対偶が真である状況。
　下側のベン図はいずれも偽である状況を表しています。

>>84 補足

それで、ここで展開した論は
背理法は有用論であり
現代数学の主流の古典論理においては、
数学証明の一つの有力手法だよと

つまり、1)直説法、2)対偶法(間接法part1)、3)背理法(間接法part2)
この3つの証明手法を自由自在に 数学手筋として 使いこなす
それは数学ディープラーニングだよ
ある程度場数を踏めば、上記1〜3)のどれが良さそうか
判断がつく場合が増えるものだ

>>81
下らなさすぎ…・

Vennさんに言ってるんだよね、それは？
貴方よりはしょうもなくない人だと思うよw

>>86

>>84
>あれあれ？
>下記の高校数学の美しい物語
>の対偶法説明のベン図も全く同じですぜ だんな
説明のベン図とか言ってる時点でど素人
任意の含意とその対偶の同値性を証明できなければ大学1年で落第

下らないのなら、なんで描けないのか説明してくれw

楕円なら書けるようになる理由もねw

>高校数学の美しい物語
とか持ち出すど素人っ思考が大学受験で止まってんのかな？

トリビアルだから下らないという意味なのか。

2000年に入ってから「回転対称なベン図が描けることと、集合の個数が素数であることが同値である」ことが分かったらしい。

背理　背理振れ　背理法
大きくなれよ

>>94
>回転対称なベン図が描ける
の定義を

>>77 補足
>　一つは、ラムダ計算 カリー＝ハワード対応 コンピュータプログラミング（除くAI）の世界

下記「デカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる」

https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C
カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワード（英語版）により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈）（英語版））と関係している。[要出典]

カリー＝ハワード＝ランベック対応
ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。ここではオブジェクトは型あるいは命題に、モルフィズムは項あるいは証明に解釈される。この対応は等号レベルに於いて働き、カリー＝ハワード対応にあるような構文的・構造的同等性を表現しない：すなわち、デカルト閉圏のモルフィズムの構造と、対応する判定のヒルベルト流あるいは自然演繹の証明の構造と比較することはできない。もちろん構文的に対応するような証明体系を構成することはできる。この区別を明確にするために、デカルト閉圏の構文的な構造を次のように言い換える。すなわちデカルト閉圏を型付きの等式理論として形式化する。

https://ja.wikibooks.org/wiki/Haskell/%E3%82%AB%E3%83%AA%E3%83%BC%3D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B
Haskell/カリー=ハワード同型
カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。

>>96
とりあえず「ベン図　～その2～」って検索して、見てくれない？
かなり壮大な話に発展しているが、それでも下らないの一言で済ませられるのか、一晩寝かせて考えてほしい。
詳しいことはお昼前に書くつもり。

>>98
>とりあえず「ベン図　〜その2〜」って検索して、見てくれない？
>かなり壮大な話に発展しているが、それでも下らないの一言で済ませられるのか、一晩寝かせて考えてほしい。
>詳しいことはお昼前に書くつもり。

あの〜（＾＾
下記のオイラー図も入れた話をおねがいします

https://ja.wikipedia.org/wiki/%E3%82%AA%E3%82%A4%E3%83%A9%E3%83%BC%E5%9B%B3
オイラー図（オイラーず、英語: Euler diagram）は、集合の相互関係を表す図。 ベン図 と類似しているが、ベン図では、存在しない集合関係を含め、異なる集合間のすべての可能な関係を示すのに対し、オイラー図では、実際に意味のある関係のみを示し、不要な領域を省略するという違いがある（下図）

https://upload.wikimedia.org/wikipedia/commons/thumb/d/d0/EulerDiagram.svg/langja-500px-EulerDiagram.svg.png
オイラー図
https://upload.wikimedia.org/wikipedia/commons/thumb/d/df/VennDiagram.svg/500px-VennDiagram.svg.png
ベン図

https://en.wikipedia.org/wiki/Euler_diagram
Euler diagram
(google訳)
オイラー図（/ ˈ ɔɪ l ər /、OY -lər）は、集合とその関係を表す図式的な手段です。複雑な階層構造や重複する定義を説明するのに特に役立ちます。別の集合図法であるベン図に似ています。[ 1 ]異なる集合間のすべての可能な関係を示すベン図とは異なり、オイラー図は関連する関係のみを示します。[ 2 ]

スイスの数学者レオンハルト・オイラー（1707〜1783）はこの種の図の歴史において最も重要な著者の一人ですが、彼は名前の由来となっただけで、発明者ではありません。オイラー図は当初、論理、特に三段論法のために開発され、後に集合論に転用されました。米国では、 1960年代の新しい数学運動の一環として、ベン図とオイラー図の両方が集合論の指導の一部として取り入れられました。それ以来、読書[ 3 ]などの他のカリキュラム分野や組織、企業 でも採用されています。

ベン図は、オイラー図よりも制約の厳しい形式です。ベン図は、構成要素となる集合の包含／除外のすべての組み合わせを表すn本の曲線間の、論理的に可能なすべての重なり合う領域を含まなければなりません。集合に含まれない領域は黒色で示されます。これは、集合への所属が色だけでなく重なりによっても示されるオイラー図とは対照的です。

https://upload.wikimedia.org/wikipedia/commons/thumb/f/fc/Euler_diagram_of_solar_system_bodies.svg/960px-Euler_diagram_of_solar_system_bodies.svg.png
太陽系のさまざまな天体間の関係を示すオイラー図

つづく

つづき

ベン図の時代におけるオイラー図
ジョン・ヴェン（1834年〜1923年）は、オイラー図の驚くべき普及について次のように述べている。

「…この目的のために参照された、過去100年ほどの間に出版された最初の60の論理学論文のうち、最も入手しやすいものであったため、やや無作為に選ばれたもののうち、34が図表の助けを借りており、そのほとんどすべてがオイラー図法を使用していた。」[ 24 ]

ベン（1881a）の115〜116ページからの2ページを合成したもので、3つの部分からなる三段論法を彼独自の図に変換する方法の例を示しています。ベンは円を「オイラー円」と呼んでいます[ 25 ]。
しかし、彼は「このスキームは真に一般的な論理の目的には適用できない」と主張し[ 24 ]（100ページ）、そして次のように指摘した。

「それは、通常適用される共通論理の4つの命題にも適合するが、うまく適合しない。」[ 24 ]（101ページ）
ヴェンは、以下の例で示されているように、それらの使用は厳密なアルゴリズムに基づくものではなく、実践と直感に基づくものであるという観察で章を締めくくっている。

いずれにせよ、これらの観察と批判を武器に、Venn [ 24 ] (pp 100–125)は、どのようにして「…昔ながらのオイラー図」から、後にVenn図として知られるようになった図を導き出したかを示している。特にVennは、左に示す例を挙げている。

オイラー図の現代的利用
1990年代には、オイラー図が論理システムとして開発されました。[ 30 ]図の認知上の利点はすぐに明らかになりました。[ 31 ] [ 32 ]そのため、図は集合図としてだけでなく、人工知能やソフトウェア工学、情報技術、生命科学、医学、経済学、統計学など、コンピュータ科学のさまざまな方法や機能で使用されてきました。 [ 33 ]また、その哲学や歴史についても議論されています。[ 34 ] [ 35 ] 2000年には、オイラー図に関する最新の研究などを定期的に取り上げる国際会議シリーズ「The Theory and Application on Diagrams: An International Conference Series」が始まりました。

オイラー図とベン図の関係
ベン図は、オイラー図のより制約の厳しい形式です。

例：オイラー図からベン図とカルノー図へ
(引用終り)
以上

オイラー図やカルノー図は聞いたことがありませんね。
ベン図を調べ終わったら見てみますね。