背理法は不要なのか

背理法被害者の会

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

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

>>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」が始まりました。

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

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

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

p q ¬p ¬q p→q ¬q→¬p
0 0 1 1 1 1
0 1 1 0 1 1
1 0 0 1 0 0
1 1 0 0 1 1

∴(p→q)⇔(¬q→¬p)

説明のベン図がーとか言ってるオチコボレは大学一年で落第

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

Steve Awodey 圏論 第2版に、
デカルト閉圏 カリー＝ハワード 直観主義が書いてあった
思えば、圏論は”矢印かいてナンボ”の世界だから
本質的に構成主義かもしれない。圏論で背理法は聞かない

(参考)
https://www.kyoritsu-pub.co.jp/book/b10003662.html
圏論 原著第2版 Steve Awodey 著・ 前原 和壽 著
発売日 2015/09/20
圏論が多分野に普及して30年を経た現在、誰もが読める圏論の本が必要だ――本書はこのモチベーションで執筆された。予備知識がほとんどない読者のために、例として半順序集合と半群がゼロから説明され、最後までそれらを用いて話が展開されている。これらのほかにも例が豊富に取り上げられている。なお、予備知識がほとんど必要ないとはいえ、数学的な厳密性は損なわれていない。すべての重要な命題と定理には完全な証明が付されている。本書は情報科学や論理学など、さまざまな分野へ役立てられるであろう。
(Steve Awodey :Category Theory　2nd edition、 Oxford University Press、 2010)

＜Steve Awodeyの講義動画＞
https://www.youtube.com/@p473r
p473r
https://youtu.be/ZKmodCApZwk?t=1
Category Theory Foundations, Lecture 1
p473r
2013/11/23 Oregon Programming Languages Summer School 2012
Steve Awodey - Category Theory Foundations, Lecture 1, Oregon Programming Languages Summer School 2012, University of Oregon
Homework excercises are available here: http://www.andrew.cmu.edu/user/awodey...

(p→q)⇔(¬q→¬p)は定理であって定理は証明するもの
説明するものではない　大学以上の数学では

とりあえずベン図について調べたら、集合が4つだと同じ楕円で線対称には描けるが、回転して一致するようには描けないらしい。
素数個の集合では回転して一致するようなベン図が描けるという話だと思う。
実用性が無いらしいから、それを下らないと表現するのなら、ある程度納得はできる。
さすがに言葉足らずではあると思うが…。

>ベン図をしっかり頭に叩き込もうね（＾＾
オチコボレ落第生が証明できない言い訳しても無駄

つづき

https://ja.wikipedia.org/wiki/%E9%9D%9E%E5%8F%A4%E5%85%B8%E8%AB%96%E7%90%86
非古典論理（non-classical logic(s)）は、古典論理におけるいくつかの仮定を否定、もしくは置き換えることによって構築された論理、あるいは、古典論理における仮定をすべて認めた上で新たな仮定を付け加えることによって構築された論理の総称である。

古典論理の拡張としての非古典論理
古典論理の拡張としての非古典論理では、基本的に、古典論理のすべての定理がその論理体系でも定理となる。
様相論理
時相論理（時制論理）
線形時相論理
義務論理（規範論理）

古典論理の代替としての非古典論理
古典論理の代替としての非古典論理は、基本的に、古典論理の定理のいくつかがその論理体系では定理でない。

直観論理
排中律を認めない。
多値論理
「真」、「偽」以外にも様々な真理値を取る論理。
適切さの論理
別名 : 相関論理、関連性の論理、関連性論理
「1+1=3なら宇宙人がいる」のような命題を真とは考えない論理。
線形論理
矛盾許容論理
Aと¬Aから⊥を導けない。
なお、古典論理や直観主義論理のシークエント計算による定式化において、構造規則を制限することによって得られる論理を部分構造論理とよび、線形論理、適切さの論理や、ウカシェヴィチの多値論理が含まれる[1]。
→「部分構造論理」を参照

https://ja.wikipedia.org/wiki/%E9%87%8F%E5%AD%90%E8%AB%96%E7%90%86
量子論理
(引用終り)
以上

簡単な論理式すら証明できないのにペタペタコピペしても無駄

>>110
ふっふ、ほっほ
文献読めない 数学イップスのオチコボレさん
これでも喰らえ！ｗ（＾＾

https://en.wikipedia.org/wiki/Reductio_ad_absurdum
Reductio ad absurdum
(google訳)
背理法
論理学において、reductio ad absurdum（ラテン語で「不条理への還元」）は、argumentum ad absurdum（ラテン語で「不条理への議論」）とも呼ばれ、アパゴジカルな議論、または矛盾による証明とも呼ばれ、反対の命題や議論の論理に従うと不条理や矛盾が生じることを示すことによって主張を確立しようとする議論の形式である。[ 1 ] [ 2 ] [ 3 ] [ 4 ]数学の証明ではかなり自由に使われているが、この種の非構成的な証明をすべての数学的思考の学派が受け入れているわけではない。[ 5 ]

この論証形式は古代ギリシャ哲学に由来し、歴史を通じて形式的な数学的・哲学的推論、そして議論において用いられてきた。数学では、この手法は背理法と呼​​ばれる。形式論理学では、この手法は「背理法（reductio ad absurdum ）」という推論規則によって表される。

より広義には、背理法とは、最初の仮定が証明すべき命題の否定ではない場合でも、矛盾にたどり着くことによって命題を確立するあらゆる形式の議論を指します。この一般的な意味では、背理法は間接証明、反対を仮定する証明[ 6 ]、および背理法[ 7 ]とも呼ばれます。

G・H・ハーディは背理法を「数学者の最も優れた武器の一つ」と表現し、「それはチェスのどんな策略よりもはるかに優れた策略だ。チェスプレイヤーはポーンや駒を犠牲にするかもしれないが、数学者はゲームそのものを提供するのだ」と述べている。[ 8 ]

正当化
古典論理では、命題¬¬P ⇒ Pの真理値表を調べることで、この原理が正当化される。真理値表は、この命題がトートロジーであることを示している。
略
この原理を正当化するもう一つの方法は、排中律からそれを導き出すことである。以下のようにする。¬¬Pを仮定し、 Pを証明しようとする。排中律によれば、P は成り立つか、成り立たないかのどちらかである。
1.Pが成り立つならば、もちろんPは成り立つ。
2.¬Pが成り立つ場合、 ¬Pと¬¬Pに矛盾律を適用して偽を導き、その後、爆発原理によりP を結論付けることができます。
いずれの場合も、我々はPを確立した。逆に、背理法を用いて排中律を導き出すことができることが分かった。

つづく

つづき

他の証明手法との関係
Refutation by contradiction
Proof by contradiction is similar to refutation by contradiction,[30][31] also known as proof of negation, which states that ¬P is proved as follows:
1.The proposition to be proved is ¬P.
2.Assume P.
3.Derive falsehood.
4.Conclude ¬P.

In contrast, proof by contradiction proceeds as follows:
1.The proposition to be proved is P.
2.Assume ¬P.
3.Derive falsehood.
4.Conclude P.
Formally these are not the same, as refutation by contradiction applies only when the proposition to be proved is negated, whereas proof by contradiction may be applied to any proposition whatsoever.[32] In classical logic, where
P and ¬¬P may be freely interchanged, the distinction is largely obscured. Thus in mathematical practice, both principles are referred to as "proof by contradiction".

Proof by contradiction in intuitionistic logic
In intuitionistic logic proof by contradiction is not generally valid, although some particular instances can be derived. In contrast, proof of negation and principle of noncontradiction are both intuitionistically valid.[33]
(引用終り)
以上

まーた訳も分からずペタペタ貼って懲りないサルだねえ

ハサミチョキチョキ
テープペタペタ
大好きな色クチュクチュ

>>112 補足
>Refutation by contradiction
>In contrast, proof by contradiction proceeds as follows:

下記 en.wikipediaでは √2の無理数証明は、
上記の ”Refutation by contradiction”で、”(and therefore are intuitionistically valid)”
だとある
後述の 仏語 Proof by contradictionでも同様で √2の無理数証明は
”There is therefore no proof by contradiction, despite appearances.
The reasoning presented is thus valid in both classical and intuitionistic logic.”
とある

国際的には √2の無理数証明は厳密には背理法でなく ”Refutation by contradiction”であって
”thus valid in both classical and intuitionistic logic”とあります
いやはや、背理法被害者の会の人、これ知ってるんかな？ （＾＾

(参考)
https://en.wikipedia.org/wiki/Reductio_ad_absurdum
より
Examples of refutations by contradiction
The following examples are commonly referred to as proofs by contradiction, but formally employ refutation by contradiction (and therefore are intuitionistically valid).[38]
（(google訳追加)以下の例は一般的に背理法による証明と呼ばれていますが、形式的には背理法による反駁を採用しています（したがって直観主義的に妥当です）。[ 38 ]）

Irrationality of the square root of 2
The classic proof that the square root of 2 is irrational is a refutation by contradiction.[39] Indeed, we set out to prove the negation ¬ ∃ a, b ∈ N.
a/b = √2 by assuming that there exist natural numbers a and b whose ratio is the square root of two, and derive a contradiction.

Assume that √2 is rational,[40] so it can be written as a fraction a/b in lowest terms, where a and b are integers with no common factors. This assumption allows us to apply a proof by contradiction.[41] Squaring both sides gives 2 = a²/b², which implies that a² = 2b².[42] Therefore, a² is even, and it follows that a must also be even. Let a = 2k for some integer k. Substituting back into the equation gives (2k)² = 2b², which simplifies to 4k² = 2b², or b² = 2k². Hence, b² is even, and therefore b must also be even. This shows that both a and b are even, which contradicts the assumption that a/b was in lowest terms. Therefore, the original assumption is false, and √2 is irrational.[40]

Proof by infinite descent
略

つつく

つづき

＜仏語（仏語ダメなので英訳スイッチ入れた）＞
https://fr.wikipedia.org/wiki/Raisonnement_par_l%27absurde
(google英訳)
Proof by contradiction

In logic and mathematics
In mathematical logic , we distinguish the rule of refutation [ref. needed] :
・p → False, therefore not( p ) , which can be taken as the definition of negation .
of the rule of reasoning by contradiction :
・not( p ) → False, therefore p is proof by contradiction.
Both classical and intuitionistic logic admit the first rule, but only classical logic admits the second rule, which involves the elimination of double negatives [citation needed] . Similarly, the law of excluded middle is rejected in intuitionistic logic . Therefore, no proof in intuitionistic logic can rely on proof by contradiction. In other words, any proposition provable in intuitionistic logic can be proven without using it. Conversely, a proposition demonstrable in classical logic but not demonstrable in intuitionistic logic requires proof by contradiction [citation needed] .

Examples and counter-examples
・Proof of the irrationality of √2 : We assume that √2 is rational. Therefore , there exist two integers a and b, which we can assume to be coprime , such that √2 =a/b
We then have 2b² = a² . If we take the remainders of both sides in the division by 2, we obtain a² = 0 mod 2 , so a is even and equal to 2a ' ( where a ' is an integer). We then have b² = 2a'² , which, by a comparable line of reasoning, leads to b being even . However , the fact that a and b are both even leads to a contradiction with a and b being coprime. The statement √2 is rational then leads to a contradiction, and therefore its negation is valid: √2 is irrational.
In this proof, we have only used the fact that if a proposition P leads to a contradiction, then not( P ) is true .
There is therefore no proof by contradiction, despite appearances.
The reasoning presented is thus valid in both classical and intuitionistic logic.
(引用終り)
以上

>>115
(引用開始)
下記 en.wikipediaでは √2の無理数証明は、
上記の ”Refutation by contradiction”で、”(and therefore are intuitionistically valid)”
だとある
後述の 仏語 Proof by contradictionでも同様で √2の無理数証明は
”There is therefore no proof by contradiction, despite appearances.
The reasoning presented is thus valid in both classical and intuitionistic logic.”
とある
国際的には √2の無理数証明は厳密には背理法でなく ”Refutation by contradiction”であって
”thus valid in both classical and intuitionistic logic”とあります
いやはや、背理法被害者の会の人、これ知ってるんかな？ （＾＾
(引用終り)

”Refutation by contradiction”
で
否定命題の背理法は、三重否定？
直観主義論理では、三重否定除去があって
¬¬¬p→¬p が 成立するからか・・

(参考)
https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9%E8%AB%96%E7%90%86
直観主義論理
古典論理において二重否定導入
p→¬¬p と二重否定除去はともに定理であるが、
直観主義論理においては、二重否定を導入することはできるが、除去することはできない。
ただし三重否定除去
¬¬¬p→¬p は定理である

>>71
>x = 1, 2, 3などの場合も証明しているわけなので
証明しては居ないでしょ

背理法は対偶証明法の一種か
対偶証明法は背理法の一種か

背理法は二つの論理的帰結関係 A1,・・・,An|=B と A1,・・・,An,¬B|=⊥ が互いに必要十分であることを用いた証明法。
対偶法は二つの論理的帰結関係 A1,・・・,An|=B と ¬B|=¬A1∨・・・∨¬An が互いに必要十分であることを用いた証明法。

>>119-120
>背理法は対偶証明法の一種か
>対偶証明法は背理法の一種か

下記のen.wikipedia Contraposition(対偶) が参考になるだろう
"この等価性は命題の証明を容易にするために使用できます"ご参照
背理法も同様に、命題の証明を容易にするために使用できます

https://en.wikipedia.org/wiki/Contraposition#Proof_by_contrapositive
Contraposition
(google訳)
対偶
直感的な説明
https://upload.wikimedia.org/wikipedia/commons/thumb/b/b0/Venn_A_subset_B.svg/500px-Venn_A_subset_B.svg.png
図示されたオイラー図では、Aに含まれるものは必ずBにも含まれます。したがって、「AのすべてがBに含まれる」は次のように解釈できます。
A→B
また、B（青色の領域）内にないものはA内にも存在できないことは明らかです。このことは次のように表現できます。
¬B→¬A
これは上記の命題の対偶である。したがって、次のように言える。
（A→B）↔（¬B→¬A）。
実際には、この等価性は命題の証明を容易にするために使用できます。

証明
単純な背理法による証明
Let:
（A→B）∧¬B
Aが真ならばBも真であり、Bは真ではないとされている。このとき、背理法を用いてAは真ではないことを示すことができる。なぜなら、Aが真であればBも真でなければならないからである（モーダス・ポネンスによる）。しかし、Bは真ではないとされているので、矛盾が生じる。
したがって、Aは真ではない（真か偽かの二値命題を扱っていると仮定した場合）。
（A→B）→（¬B→¬A）
同じプロセスを逆方向にも適用できます。その際、以下の前提から始めます。
（¬B→¬A）∧A
ここで、Bは真か偽かのどちらかであることがわかっています。Bが偽であれば、Aも偽です。しかし、Aは真であると与えられているので、Bが偽であるという仮定は矛盾を生じさせ、Bが偽ではないという状況はあり得ないことを意味します。したがって、Bは真でなければなりません。
（¬B→¬A）→（A→B）
証明された2つの命題を組み合わせると、条件文とその対偶との間の、求められていた論理的同値性が得られます。
（A→B）≡（¬B→¬A）

対偶の等価性に関するより厳密な証明
略

>>122 追加

背理法利用の大物で 下記 ワイルズによるフェルマーの最終定理の証明がある
『ワイルズは半安定楕円曲線に関してモジュラリティ定理を証明し、そこからフェルマーの最終定理が背理法で導かれることを明らかにした。』

これと下記望月氏IUT以外には、証明は知られていない
下記 望月氏のIUT５人論文は
abc予想を明示的に解決して 解の存在範囲を示し
値が小さいところを、コンピュータ数値計算で潰して
フェルマーの最終定理を証明している（まだ学会で認められずLEANで検証中）

素直に、間接証明の背理法が適する場面と
そうでない場面と どちらでも証明できる場面と
３つあることを認めたら良いと思うのだが・・

(参考)
https://ja.wikipedia.org/wiki/%E3%83%AF%E3%82%A4%E3%83%AB%E3%82%BA%E3%81%AB%E3%82%88%E3%82%8B%E3%83%95%E3%82%A7%E3%83%AB%E3%83%9E%E3%83%BC%E3%81%AE%E6%9C%80%E7%B5%82%E5%AE%9A%E7%90%86%E3%81%AE%E8%A8%BC%E6%98%8E
ワイルズによるフェルマーの最終定理の証明

ワイルズの証明の概要
ワイルズは半安定楕円曲線に関してモジュラリティ定理を証明し、そこからフェルマーの最終定理が背理法で導かれることを明らかにした。

証明は大きく2つの部分に分かれる。
略す

ワイルズの証明の数学的詳細
略す

https://ja.wikipedia.org/wiki/%E5%AE%87%E5%AE%99%E9%9A%9B%E3%82%BF%E3%82%A4%E3%83%92%E3%83%9F%E3%83%A5%E3%83%A9%E3%83%BC%E7%90%86%E8%AB%96
宇宙際タイヒミュラー理論
IUT関係者による研究
関連研究
2022年7月、楕円曲線の6等分点を用いて、論文中のディオファントス的不等式中の定数の数値を明示したもの（非明示的な「定数」が現れない）に変更した、ヴォイチェフ・ポロウスキ、南出新、星裕一郎、イヴァン・フェセンコ、望月新一らの査読論文が、東京工業大学が編集する数学論文誌Kodai Mathematical Journalに掲載された[51][52]。この結果により、宇宙際タイヒミュラー理論によるフェルマーの最終定理の新たな証明を得たとしている[53]。

誰も聞いてない背理法使用例をぺたぺた貼るオチコボレ憐れ

>>123
下記 鈴木 通夫先生の”有限単純群の分類”数学/34 巻 (1982)
背理法を使う
即ち 最小反例
『以下Gは分類定理にあげられた単純群のいずれとも同形でない最小位数の単純群と仮設する.
この仮設から矛盾を導くのが目的である』
という

背理法 分かり易いと思うけど・・（＾＾
まあ、背理法を使わない 分類定理の表現もあるんでしょうねぇ
（私には それを 考える気が全く起きないのですが・・ｗ）
追記
下記 田中康彦先生と 岩波 群論（下）鈴木通夫（多分大学の図書館なら読めるだろう）が詳しい
（後者の本は チラ見したｗ（＾＾）

(参考)
https://ja.wikipedia.org/wiki/%E6%9C%89%E9%99%90%E5%8D%98%E7%B4%94%E7%BE%A4%E3%81%AE%E5%88%86%E9%A1%9E
有限単純群の分類
(有限単純群の分類問題のあらすじ解説 [2])
出典
2. “P141 9. 有限単純群の分類問題について 田中康彦（大分大学）構成的ガロア逆問題と不変体の有理性問題（第27回整数論サマースクール報告集）2019年” (2019年9月6日).
https://niigata-u.repo.nii.ac.jp/records/33655
SS2019proceedings写真なし.pdf (7.8 MB)
https://niigata-u.repo.nii.ac.jp/record/33655/files/SS2019proceedings%E5%86%99%E7%9C%9F%E3%81%AA%E3%81%97.pdf
9. 有限単純群の分類問題について・・・・・・・・・・・・・・・141
田中康彦（大分大学）

外部リンク
https://www.jstage.jst.go.jp/article/sugaku1947/34/3/34_3_193/_article/-char/ja/
https://www.jstage.jst.go.jp/article/sugaku1947/34/3/34_3_193/_pdf/-char/ja
J-STAGEトップ/数学/34 巻 (1982) 3 号/
有限単純群の分類
鈴木 通夫
P204
§3.分類定理の証明
P205
以下Gは分類定理にあげられた単純群のいずれとも同形でない最小位数の単純群と仮設する.
この仮設から矛盾を導くのが目的である.
P208
さてこの段階で残っていた4つの散在単純群がすべて現われた.定理11により分類定理に対する最小の反例は定理9(3)の条件をみたすことがわかる.

定理12.非成分型の連結単純群Gがe(G)≧3かつ定理9の条件(3)をみたすことはできない.
ここにいたって分類定理に対する最小の反例の存在から矛盾が起り,分類定理が証明されたのである.
定理12の証明には可換部分群の弱閉包,2元体上の表現,特性核,いわゆるAschbacherブロックなどの多様な概念が必要で,[D],[SC]に証明の要点が述べられている

https://www.iwanami.co.jp/book/b266825.html
岩波 現代数学　 18
群論　（上）（下）（岩波オンデマンドブックス）
鈴木　通夫 著
この本の内容
有限群論で国際的に評価される著者自らが執筆した教科書．上巻で基本定理や方法，一般群論，下巻で有限群論を解説する．

>>124
ふっふ、ほっほ
数学文献イップス（下記）が さわぐ（＾＾

　ワイルズの>>123 フェルマーの最終定理の証明は
背理法による証明で いま公式に認められているのは これのみ（そのうち望月IUT）
　鈴木 通夫先生の”有限単純群の分類”の証明も 背理法によるものです

(google検索)
イップス 心理
AI による概要
イップスは、心理的な要因やプレッシャーが原因で、これまで無意識にできていた動作が突然できなくなる運動障害です。失敗への恐怖や「完璧にこなさなければ」という過度な緊張が脳に誤作動を引き起こし、筋肉の硬直や不随意運動をもたらします
イップスを引き起こす主な心理メカニズム
・失敗のトラウマ（フラッシュバック）過去の重大なミスや、その際に受けた強い叱責の記憶が無意識にフラッシュバックし、再び同じ失敗をする恐怖から体がすくんでしまいます。
・過度な競技不安とプレッシャー「ミスをしてはいけない」「結果を出さなければならない」という強いプレッシャーが自律神経を乱し、極度の緊張状態を生み出します
・意識の過剰（分析しすぎ）本来は無意識に行うべき動作（例：ボールを投げる、楽器を弾く）を、意識的にコントロールしようとしすぎることで、脳の指令と筋肉の動きにズレが生じます

イップスになりやすい性格的傾向
・完璧主義：ミスを極端に嫌い、理想のフォームや結果を常に追い求める人

また誰も聞いてないことをペタペタ貼ったり相手がイップスと妄想したり、オチコボレ憐れ

ホイップストロベリーケーキ

コピペ・連投・長文は
知能が低い証し

>>116 追加

中間値の定理の襲名に、背理法が必要とあるぞｗ
面白いなｗ（＾＾

https://fr.wikipedia.org/wiki/Raisonnement_par_l%27absurde
Raisonnement par l'absurde
(google英訳)
Proof by contradiction
Examples and counter-examples
・Proving the Intermediate Value Theorem :
even though proof by contradiction does not appear in the proof of this theorem, it nevertheless relies on the principle of excluded middle, the validity of which depends on proof by contradiction. The existence of the root asserted by the theorem is purely formal and not actual. This theorem is not accepted in constructive analysis unless stronger hypotheses are added [ 3 ] .
(google和訳)
中間値の定理の証明：
この定理の証明には背理法は用いられていないものの、排中律の原理に基づいている。排中律の妥当性は背理法によって証明される必要がある。定理が主張する根の存在は形式的なものであり、実際的なものではない。より強い仮定が加えられない限り、この定理は構成的解析では受け入れられない[3]。

https://ja.wikipedia.org/wiki/%E4%B8%AD%E9%96%93%E5%80%A4%E3%81%AE%E5%AE%9A%E7%90%86
中間値の定理

証明
#概要に述べた一般化された定理について証明する。必要な事実は
連結空間の連続像は連結である
ということだけである（この事実はここでは認めて話を進めることにする）。
証明[4][表示]
背理法によって示そう
略
存在型の定理
この種の定理は「存在」に関しては保証してくれるが、「具体的にどこにあるか」については分からない。具体的にどこにあるのか知りたい場合には別の考察が必要であるが、「存在」さえ確かめられれば、それでいい場合も多い[注 3]。
似たような存在型の定理に、ロルの定理や平均値の定理などがある。

https://en.wikipedia.org/wiki/Intermediate_value_theorem
Intermediate value theorem
Proof
The theorem depends on, and is equivalent to, the completeness of the real numbers.
In constructive mathematics
In constructive mathematics, the intermediate value theorem is not true.
（仏語）
https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_valeurs_interm%C3%A9diaires
Théorème des valeurs intermédiaires
(google英訳)
Demonstrations
The intermediate value theorem is one of the so-called existence theorems . However, there is no general constructive proof of its existence [ 7 ] .

指摘を理解できないバカ

>>130 追加

en.wikipedia を見ると
Intermediate value theorem（中間値の定理）
より
Proof version B が、背理法
Proof version A が、見かけ背理法ではないが 非構成部分は
”a consequence of the completeness property of the real numbers”
と、実数の完備性を使う

さらに In constructive mathematics
”構成的数学においては、中間値の定理は成り立たない。その代わりに、弱められた結論として、値は任意に小さい範囲内でのみ見つかる可能性がある、と述べる必要がある”
とありますね
つまり、中間値の定理自身は、構成的数学では不成立で それを弱めた定理になる
ということ

(参考)
https://en.wikipedia.org/wiki/Intermediate_value_theorem
Intermediate value theorem
中間値の定理
Proof
Proof version A
The theorem may be proven as a consequence of the completeness property of the real numbers as follows:[3]
略

Proof version B
(google訳)
略
矛盾を生じさせるために、次のように仮定してみましょう。
g(c)<0。
略
しかし、 x<cこれは、最小上界の最小性質に矛盾する。
つまり、 g(c)>0 不可能だ。
(注：背理法)

In constructive mathematics
In constructive mathematics, the intermediate value theorem is not true. Instead, the weakened conclusion one must take states that the value may only be found in some range which may be arbitrarily small.
（google訳：構成的数学においては、中間値の定理は成り立たない。その代わりに、弱められた結論として、値は任意に小さい範囲内でのみ見つかる可能性がある、と述べる必要がある。）
・Let a and b be real numbers and
f:[a,b]→R be a pointwise continuous function from the closed interval
[a,b] to the real line, and suppose that
f(a)<0 and 0<f(b). Then for every positive number
ε>0 there exists a point
x in the open interval
(a,b) such that
|f(x)|<ε.[15]

>>132 補足
>Proof version B が、背理法
>Proof version A が、見かけ背理法ではないが 非構成部分は
>”a consequence of the completeness property of the real numbers”
>と、実数の完備性を使う

いまの場合、古典論理では
背理法は、非構成的証明として機能していて
Proof version Bのような形で、非構成的証明を実行できるということかと
つまり、背理法は ある場面では 強力な証明手段とみることができる
（直接法では ムリかややこしい場面で、威力をはっきする）

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

>>130 誤変換訂正

中間値の定理の襲名に、背理法が必要とあるぞｗ
　↓
中間値の定理の証明に、背理法が必要とあるぞｗ

余談
　>>122の対角線論法で
”　なお、対角線論法はLawvereにより、
(不動点定理の形で)積閉圏へと一般化されています。
勿論、背理法は不要です。”
とか書いているが

パイオニアとして、世界で一番最初の証明を考えた人と
それを見て 別解・別証明を考えることとは、天と地の差があるということを認識しないと
そこをマゼコゼにしてしまうと、パイオニア精神が不足している 日本の凡庸な数学者が、
評論家的に 趣味的に 背理法を使わない別証明を考えて エッヘンとやってる

別にそれは個人の趣味としては良いが
それやってると、パイオニアにはなれない

と、オチコボレが申しております

>>136
勘違いしている人が多いが
教養で教える数学と
東大数学科で教える数学は違う

教養で教える数学は、
いまどきは数学以外の分野でいろんな数学が使われるから
その基礎部分を教える数学であって

東大数学科で教える数学は、
プロ数学者を養成するためのものだ

東京理科大の数学科が、前者だとすれば
できるだけ 背理法以外の証明も勉強しよう
という趣旨は分かるが

　>>41
”「私自身が、背理法のおかげで頭が腐った被害者であると実感しています。十数年前から現在もリハビリ中です。」(背理法被害者の会)”
は、明らかにいいすぎ

背理法が、数学の発展の中で
果たした役割を過小評価している

>>135 補足
　>>122の対角線論法で
”　なお、対角線論法はLawvereにより、
(不動点定理の形で)積閉圏へと一般化されています。
勿論、背理法は不要です。”

まあ、下記など
余談：なお 下記のだれも背理法不要とは言っていない

(参考)
(google検索)
対角線論法 不動点定理
AI による概要
「対角線論法」と「不動点定理」は、一見すると無関係に思えますが、実は数理論理学や計算機科学において「自己言及（自分自身について語ること）」を扱う際の表裏一体の概念です
対角線論法と不動点定理のつながり
・対角線論法: 集合の要素をリストアップし、それと対角線上になる要素を変更することで、「リストに漏れている新しい要素」を作り出す手法。カントールの集合論（実数の非可算性）やゲーデルの不完全性定理の証明に使われます。
・不動点定理: \(f(x) = x\) となる点（不動点）が存在することを主張する定理です
・本質的な共通点: 「対角線論法による新しい要素の構成」は、論理学や圏論の文脈では「不動点を作り出す操作」と完全に同じ構造（ローヴェアの不動点定理など）として定式化できます
具体的な応用例
1. ゲーデルの不完全性定理ゲーデルは、自身の論文でカントールの対角線論法に酷似した手法（対角化補題）を用いました。これにより、「自分自身が証明できないことを主張する命題」という自己言及的な数式を構成し、数学の無矛盾性をその内部の公理系からは証明できないことを示しました。
2. 計算機科学（不動点コンビネータ）ラムダ計算やプログラミング言語の関数型プログラミングにおいて、再帰処理（ループ構造）を実装するために「不動点コンビネータ（Yコンビネータなど）」が使われます。これは対角線論法の自己言及の構造を計算機上で具現化したものです
3. ラッセルのパラドックス「自分自身を要素として含まない集合全体の集合」を考えると矛盾が生じるという論理学のパラドックスです。これも対角線論法と同一の自己言及構造が引き起こす問題であり、この矛盾を回避するための枠組みが現代の集合論（ツェルメロ＝フレンケル集合論など）の基礎となっています。

さらに深掘りしたい場合は、以下のどのテーマに興味があるか教えてください：
・カントールの対角線論法の具体的な証明手順
・ゲーデルの不完全性定理と自己言及の仕組み

https://ja.wikipedia.org/wiki/%E5%AF%BE%E8%A7%92%E5%8C%96%E5%AE%9A%E7%90%86
対角化定理
歴史
対角化定理はカントールの対角線論法と類似しているため、「対角化」と呼ばれる
ルドルフ・カルナップ (1934)は、一般自己言及補題 を最初に証明した

https://www.kurims.kyoto-u.ac.jp/~hassei/index-j.html
長谷川 真人
講義資料 「自己言及の論理と計算」(2006年5月改訂；2007年8月追記)
https://www.kurims.kyoto-u.ac.jp/~hassei/selfref2006.pdf
自己言及の論理と計算∗長谷川真人
（ ∗京都大学数理解析研究所 数学入門公開講座（2002）
以下では，数理論理学と計算機科学の密接な関係を示す好例として，自己言及から生じる様々なパラドックスなどの数理論理学における問題，また自分自身を呼び出すような再帰的なプログラムやデータ構造に関する問題などについて，統一的な視点から考察します

訳も分からずペタペタ貼る病が治らないオチコボレ

まあな
人のスレで悪いが
自分のスレでもやっている
ここ5chは、おれのメモ帳
備忘録なのさｗ （＾＾

>>138 追加
下記は、旧ガロアすれでも紹介したので
覚えている
ペタペタ貼ると記憶に残る（＾＾

対角線論法に関する目次貼るね
（１投稿の容量制限で省いた部分な）

https://www.kurims.kyoto-u.ac.jp/~hassei/index-j.html
長谷川 真人
講義資料 「自己言及の論理と計算」(2006年5月改訂；2007年8月追記)
https://www.kurims.kyoto-u.ac.jp/~hassei/selfref2006.pdf
自己言及の論理と計算∗長谷川真人
（ ∗京都大学数理解析研究所 数学入門公開講座（2002）
以下では，数理論理学と計算機科学の密接な関係を示す好例として，自己言及から生じる様々なパラドックスなどの数理論理学における問題，また自分自身を呼び出すような再帰的なプログラムやデータ構造に関する問題などについて，統一的な視点から考察します

目次
I 自己言及と対角線論法
1 ラッセルの逆理
2 カントールの対角線論法
3 自己適用
4 停止性問題
5 対角線論法から不動点へ
6 不動点定理から具体例を見直す
II 矛盾したものを構成する
1 完備半順序集合と連続関数
2 最小不動点の発想
3 最初の試み
4 埋め込みと射影
5 なぜ失敗したか
6 正しい解の構成—逆極限法

記憶には残るが何一つ理解していない

目次が数学のすべての人がいるね

>>141-142
数学徒は、すぐに反例が示せる主張はしない方がいいだろう
数学センスを問われるからなｗ

記憶には残るが何一つ理解していない
　↓
何か少なくとも一つ以上は理解した

目次が数学のすべての人がいるね
　↓
それ以外にも 表題とか著者とかの記載あるよ！ｗｗｗ（＾＾

>>144 リンク訂正

>>141-142
　↓
>>142-143

算数のセンスを
問われるなｗｗ　（＾＾

屁理屈しか返せない憐れなオチコボレ

数学では、屁理屈であろうが
すべからく 理屈が通っていないといけないとしたもの
ヘリクツでも rigorous であるべし
その上で、“post-rigorous” stage ＝“big picture” by Terence Tao

https://rio2016.5ch.io/test/read.cgi/math/1781308317/31
＜“big picture”＞
https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/comment-page-1/
There’s more to mathematics than rigour and proofs Terence Tao
3. The “post-rigorous” stage, in which one has grown comfortable with all the rigorous foundations of one’s chosen field, and is now ready to revisit and refine one’s pre-rigorous intuition on the subject, but this time with the intuition solidly buttressed by rigorous theory. (For instance, in this stage one would be able to quickly and accurately perform computations in vector calculus by using analogies with scalar calculus, or informal and semi-rigorous use of infinitesimals, big-O notation, and so forth, and be able to convert all such calculations into a rigorous argument whenever required.) The emphasis is now on applications, intuition, and the “big picture”. This stage usually occupies the late graduate years and beyond.
https://terrytao.wordpress.com/career-advice/
Career advice Terence Tao

＜再録＞
　>>130より ”中間値の定理の証明に、背理法が必要”
（中間値の定理は、本質的に非構成的な定理であり、非構成部分を実数の完備性が担うと
　見かけは非背理法に見える証明が可能。そうでなければ、背理法証明が可能）
https://fr.wikipedia.org/wiki/Raisonnement_par_l%27absurde
Raisonnement par l'absurde
(google英訳)
Proof by contradiction
Examples and counter-examples
・Proving the Intermediate Value Theorem :
even though proof by contradiction does not appear in the proof of this theorem, it nevertheless relies on the principle of excluded middle, the validity of which depends on proof by contradiction. The existence of the root asserted by the theorem is purely formal and not actual. This theorem is not accepted in constructive analysis unless stronger hypotheses are added [ 3 ] .
(google和訳)
中間値の定理の証明：
この定理の証明には背理法は用いられていないものの、排中律の原理に基づいている。排中律の妥当性は背理法によって証明される必要がある。定理が主張する根の存在は形式的なものであり、実際的なものではない。より強い仮定が加えられない限り、この定理は構成的解析では受け入れられない

　>>132より 『Proof version B が、背理法
Proof version A が、見かけ背理法ではないが 非構成部分は
”a consequence of the completeness property of the real numbers”
と、実数の完備性を使う』
https://en.wikipedia.org/wiki/Intermediate_value_theorem
Intermediate value theorem
中間値の定理
Proof
Proof version A
The theorem may be proven as a consequence of the completeness property of the real numbers as follows:[3]
略
Proof version B
(google訳)
略
矛盾を生じさせるために、次のように仮定してみましょう。
g(c)<0。
略
しかし、 x<cこれは、最小上界の最小性質に矛盾する。
つまり、 g(c)>0 不可能だ。
(注：背理法)
In constructive mathematics
In constructive mathematics, the intermediate value theorem is not true. Instead, the weakened conclusion one must take states that the value may only be found in some range which may be arbitrarily small.
（google訳：構成的数学においては、中間値の定理は成り立たない。その代わりに、弱められた結論として、値は任意に小さい範囲内でのみ見つかる可能性がある、と述べる必要がある。）
・Let a and b be real numbers and
f:[a,b]→R be a pointwise continuous function from the closed interval
[a,b] to the real line, and suppose that
f(a)<0 and 0<f(b). Then for every positive number
ε>0 there exists a point
x in the open interval
(a,b) such that
|f(x)|<ε.[15]

また屁理屈

>>148 追加

ZFC公理系で、非構成的な公理がただ二つある
一つは 無限公理（無限集合は他の公理から構成できない）
もう一つは、言わずと知れた 選択公理
（下記 ”選択公理は選択集合の存在を主張するが 非構成的”）

実数に完備性を与えるには、選択公理による非構成的なコーシー列の存在を必要とする

https://rio2016.5ch.io/test/read.cgi/math/1780699023/173より
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
ツェルメロ＝フレンケル集合論
公理
ZFC公理系には、多くの同値な定式化が存在する。以下に示す公理は、Kunen (1980)（ケネス・キューネン）に従った
選択公理を除く下記の八つの公理でZFを定義できる。
（連番は筆者が付けた）
1）外延性の公理：任意の集合について、その集合と同じ元のみをもつ集合は、その集合自体の他に存在しない
2）正則性公理：略
3）分出公理図式：分出公理は、既出の集合から部分集合のみを構成できる
　ZFの公理の中で、この公理は置換公理と空集合の公理から導かれる
4）対の公理：任意の集合 xと y について、少なくとも xと y を元とする集合が存在する
5）和集合の公理：略
6）置換公理図式：置換公理は、定義可能な関数において集合の像も集合内にあると主張する
7）無限公理：略
8）冪べき集合公理：略
9）選択公理（または同値な命題）：任意の集合 X に対して、 X を整列する二項関係 R が存在する
これは R が、空でない X のどの部分集合も R のもとで最小元を持つような
X の全順序であることを意味する。
∀X ∃R[R well-orders X]
ZFの公理 (すなわち、前述の8つの公理および公理図式) の下で、選択公理は同値な主張をいくつか持つ。Kunenは選択公理に相当するものとして上記の主張を公理に設定した[6]が、これは通常整列可能定理と呼ばれるものである
（選択公理は選択集合の存在を主張するが、選択集合がどのように「構築」されるかについては言及しないため、非構成的であるとされる）

>>150
>実数に完備性を与えるには、選択公理による非構成的なコーシー列の存在を必要とする
有理コーシー列全体の集合の構成に選択公理は不要。
なんで口から出まかせに嘘デタラメ吐くかねえこのオチコボレは。

連投，長文，コピペは
頭が悪い

>>150
>ZFC公理系で、非構成的な公理がただ二つある
>一つは 無限公理
無限公理は帰納的集合の存在を主張する。帰納的集合は空集合と後者関数から生成できるすべての元 {},{{}},{{},{{}}},・・・ を持つ。
なぜこれが構成的でないのか？　また口から出まかせ？　懲りないオチコボレだねえ。

>>150
>ZFC公理系で、非構成的な公理がただ二つある
>一つは 無限公理（無限集合は他の公理から構成できない）
>もう一つは、言わずと知れた 選択公理
外延性の公理、正則性公理はいかなる集合も構成しない。
口から出まかせもほどほどにな。

コピペバカの吐く独自主張はことごとく間違えている。
>記憶には残るが何一つ理解していない
の証拠。

>>150 訂正

正確には
実数に完備性を与えるには、選択公理による非構成的なコーシー列の存在を必要とする
　↓
実数が完備距離空間であることを示すのに、選択公理による非構成的なコーシー列の存在を必要とする

だな
完備距離空間は下記ね
完備距離空間として考えると、p進距離とか別の距離を考えることができる
また、実数Rから複素数Cを考えるときも、完備距離空間として考えることができる
これが、デデキントカットに対する完備距離の優位性

(参考)
https://ja.wikipedia.org/wiki/%E5%AE%8C%E5%82%99%E8%B7%9D%E9%9B%A2%E7%A9%BA%E9%96%93
完備距離空間
、距離空間 M が完備（かんび、英: complete）またはコーシー空間（コーシーくうかん、英: Cauchy space）であるとは、M 内の任意のコーシー点列が M に属する極限を持つ（任意のコーシー点列が収束する）ことを言う。
直観的に言えば、空間が完備であるというのは（その内側や境界において）点を追いかけると「空間からはみ出してしまう」ということが起きないということである。例えば、有理数全体の成す集合 ℚ は完備でないが、これは例えば2 の正の平方根は、それに収束する有理コーシー数列が構成できるにも拘らず、有理数ではないので ℚ からははみ出してしまう（後述）。「こういった抜けを全て埋めてしまう」という考えは後述するように、空間の完備化 (completion) として常に可能である。
完備化
完備化の普遍性
「任意の完備距離空間 N と M から N への一様連続写像が与えられたとき、M′ から N への一様連続写像 f′ で f の延長となるものが一意に存在する」
という普遍性を持つ。空間 M′ は等距変換の違いを除いて、この普遍性によって決まり、M の完備化と呼ばれる。
M の完備化は M 内のコーシー列のある同値類集合として構成することができる。
略

>>153
赤ペン先生

無限公理は帰納的集合の存在を主張する。帰納的集合は空集合と後者関数から生成できるすべての元 {},{{}},{{},{{}}},・・・ を持つ。
　↓
無限公理は帰納的無限集合の存在を主張する。帰納的集合は空集合と後者関数から生成できるすべての元 {},{{}},{{},{{}}},・・・（可算無限） を含む。

だな。詳しくは 下記 Set-theoretic definition of natural numbers ご参照
要するに、帰納的定義だけでは、有限の範囲でいくらでも大きな自然数nが作れるが
しかし、無限集合としてのNは構成できない
従って、非構成的に なんらかの無限集合公理を与える必要があるのです■

(参考)
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers
Set-theoretic definition of natural numbers
Definition as von Neumann ordinals
In Zermelo–Fraenkel (ZF) set theory, the natural numbers are defined recursively by letting 0 = {} be the empty set and n + 1 (the successor function) = n ∪ {n} for each n. In this way n = {0, 1, …, n − 1} for each natural number n. This definition has the property that n is a set with n elements. The first few numbers defined this way are: (Goldrei 1996)
略
The set N of natural numbers is defined in this system as the smallest set containing 0 and closed under the successor function S defined by S(n) = n ∪ {n}. The structure ⟨N, 0, S⟩ is a model of the Peano axioms (Goldrei 1996). The existence of the set N is equivalent to the axiom of infinity in ZF set theory.

Frege and Russell
For enabling natural numbers to form a set, equinumerous classes are replaced by special sets, named cardinal. The simplest way to introduce cardinals is to add a primitive notion, Card(), and an axiom of cardinality to ZF set theory (without axiom of choice).[2]

>>156
コーシー実数がコーシー完備であることの選択公理を使わない証明。
https://ja.wikipedia.org/wiki/%E3%82%B3%E3%83%BC%E3%82%B7%E3%83%BC%E5%88%97#%E5%AE%9F%E6%95%B0%E3%81%AE%E6%A7%8B%E6%88%90

複素数体=R[x]/(x^2+1)　つまりRにx^2+1の根を添加した二次拡大体。

初歩の初歩から分かってないオチコボレの妄言は聞き飽きた。

>>157
君、帰納的集合は無限集合であることも知らんの？

>従って、非構成的に なんらかの無限集合公理を与える必要があるのです■
なんらかのじゃなく帰納的集合の存在を主張する無限公理。帰納的集合が持たなければならない元は明示的に定められているのだから構成的。君、頭悪いね。

名物 赤天先生

>赤ペン先生
大学1年の授業についていけず落第したオチコボレは赤ペンされる側だろｗ

青天井の優しさ

集合Xが元{}を持っていなければXは帰納的集合ではない。
「帰納的集合は”なんかほわ〜んとした無限集合”」とイメージして非構成的とほざくのはオチコボレが初歩の初歩から分かってないだけ。
実際、
>帰納的集合は空集合と後者関数から生成できるすべての元 {},{{}},{{},{{}}},・・・ を持つ。

ホワミル

オチコボレは初歩の初歩から分かってないから間違いだらけなのに重度NPD患者なので決して間違いを認めない
まずは病気治せ　数学はその後

補題　有限集合は帰納的集合である
って書いてある資料がある。

>>158
>コーシー実数がコーシー完備であることの選択公理を使わない証明。
>https://ja.wikipedia.org/wiki/%E3%82%B3%E3%83%BC%E3%82%B7%E3%83%BC%E5%88%97#%E5%AE%9F%E6%95%B0%E3%81%AE%E6%A7%8B%E6%88%90

ふっふ、ほっほ
1）それな ZFだけで証明したと謳ってないよね
2）実際、コーシー列に二種類 あることを認めようね
　一つは、構成可能なコーシー列 （例えば オイラー数 (Euler's number)e =1+1+1/2!+1/3!+・・ https://en.wikipedia.org/wiki/E_(mathematical_constant)）
　もう一つは、非構成可能なコーシー列
　非構成可能なコーシー列の存在を示すのに、(可算)選択公理を使う
　非構成可能なコーシー列の存在を示せないと 完備がいえない

>複素数体=R[x]/(x^2+1)　つまりRにx^2+1の根を添加した二次拡大体。

おっさんな
複素数C にL^2距離を導入して、距離空間にするんだよ
導入した距離を利用して 複素コーシー列を作る
(可算)選択公理を使って、非構成可能を含むコーシー列の複素数C内への収束を示すんだよ！

これだから、素人は・・（＾＾

背理法と排中律（下記）

https://ja.wikipedia.org/wiki/%E6%8E%92%E4%B8%AD%E5%BE%8B
排中律（英: Law of excluded middle、仏: Principe du tiers exclu）とは、論理学において、任意の命題 P に対し「P であるか、または P でない」という命題は常に成り立つという原理である。
直観主義論理においては排中律は公理として採用されておらず、また排中律は直観主義論理の定理ではない（すなわち、排中律は直観主義論理において証明できない）。ただし、排中律の二重否定 ¬¬(P ∨ ¬P) [注釈 1]や三重否定除去 ¬¬¬P → ¬P [注釈 2]などは直観主義論理においても証明可能であり、すなわち排中律が否定されているわけでもない。

例
排中律に依存した論証の例を次に示す。これは、よく知られた例である[7][8]。
『a と b ２つの無理数からなるabが有理数となる a 、 bが存在する』
√2 が無理数であることは知られている。そこで、次のような数を考える。
√2^√2
排中律に基づくと、明らかにこの数は有理数か無理数かのどちらかである。これが有理数なら証明が完了する。もし無理数なら、次のような数を考える。
a=√2^√2
および
b=√2
すると、
a^b=(√2^√2)^√2
=(√2)^(√2・√2)
=(√2)^2
=2
2 は明らかに有理数である。従って証明が完了する。
この論証において、「この数（√2^√2）は有理数か無理数かのどちらかである」という主張は排中律に基づいている。直観主義では、aが
√2であるのか
√2^√2 であるのか特定されていないような上記の論法、あるいは
√2^√2 について何らかの証拠（数・実数としての存在可能性、あるいは有理数であるか無理数であるかといった具体的な証明）がない限り、このような主張を認めない。この変形として、ある数が無理数（あるいは有理数）であることの証明や、ある数が有理数かどうかを判定する有限なアルゴリズムなどが考えられる。

無限に関する非構成的証明
上記の例は直観主義では許されない「非構成的; non-constructive」証明の例である。
「この証明は、定理を満足する a と b という数を特定せずに可能性だけで論じているため、非構成的である。実際には
a=√2^√2 は無理数だが[注釈 3]、これを簡単に示す証明は知られていない」(Davis 2000:220)　
（なお、上記の設題に関して別の数を用いれば、特定の構成的な証明を行うのは困難な事ではない。例えば
a=√2 及び
b=log2 (9)
は共に無理数であることは容易に証明でき、
a^b=3。これは直感主義で認められる証明方法の１つである[9]。）

Davis は「構成的」について「実際に一定の条件を満たす数学的実体が存在するという証明は、明示的に問題の実体を表す方法を提供する必要があるだろう」(p. 85) としている。そのような証明は全体の完全性の存在を前提としており、それは直観主義者にとっては、決して完全ではない「無限」に拡張することは許されない

つづく

つづき

古典数学では、「非構成的」あるいは「間接的」な存在証明があるが、直観主義者はそれを受け入れない。例えば、「P(n) が成り立つような n がある」ことを証明するとき、古典数学では全ての n について P(n) が成り立たないと仮定することで矛盾が生じることを示す。古典論理でも直観論理でも、帰謬法により「全ての n について P(n) が成り立たないということはない」ことが示される。古典論理はその結果を「P(n) が成り立つ n が存在する」に変換することを許すが、直観論理では総体として無限な自然数の集合が完全であって、P(n) となるような n が存在するということは言えない。なぜなら、直観主義では自然数が全体として完全であるとは考えないからである。[10] (Kleene 1952:49-50)

一般に、直観主義では有限な集合に関して排中律の適用を許すが、無限集合（例えば、自然数）に対しては許さない。したがって、「無限集合 D に関する全ての命題 P について、P であるかまたは P でないかのどちらかである」(Kleene 1952:48) という言い方は、直観主義では絶対できない。詳しくは、数学基礎論と直観主義を参照されたい。

排中律についての推定的反例として、嘘つきのパラドックスあるいはクワインのパラドックスがある。Graham Priest の dialetheism では、排中律を定理とするが、嘘つきのパラドックスは真でもあり偽でもあると説明する。この場合、排中律は真だが、真であるがゆえに選言は排他的ではなく、選言肢の一方が逆説的だったり、両者がともに真でありかつ偽であることもありうるとする。

注釈
2. 直観主義論理においても二重否定の導入 P → ¬¬P は真である。ここから、Pの三重否定とPは矛盾することが従うため、¬¬¬P ならばPでないことが成り立つ。
(引用終り)
以上

くっちゃらハピハピ

>>166
京大の資料か

>>167
>それな ZFだけで証明したと謳ってないよね
証明のどこで選択公理使ってると？　具体的な箇所を示して。
示せないなら黙ろうな　オチコボレの妄言は聞き飽きた。

>>168-169 補足
>三重否定除去 ¬¬¬P → ¬P [注釈 2]などは直観主義論理においても証明可能であり、
>注釈
>2. 直観主義論理においても二重否定の導入 P → ¬¬P は真である。ここから、Pの三重否定とPは矛盾することが従うため、¬¬¬P ならばPでないことが成り立つ。

下記が参考になるだろう

https://scrapbox.io/takker/%E4%B8%89%E9%87%8D%E5%90%A6%E5%AE%9A%E9%99%A4%E5%8E%BB
takker 2024-02-18
三重否定除去
¬¬¬P ⊢ ¬Pのこと。
一般的に呼ばれている名前はない
　名前がないと指し示しづらいので、[takker]が勝手につけておいた
[二重否定除去]とは違って、[直観論理]でも成立する

解釈
　この解釈を思いつけたら面白そうだ
証明
方針
P ⊢ ¬¬P と¬(¬¬ P)⇔ (¬¬P ⇒⊥)]を使うだけ
https://scrapbox.io/files/65d16b685a09250023130bf5.svg

注：”P ⊢ ¬¬P”は、二重否定の導入ですね(下記)
https://ja.wikipedia.org/wiki/%E4%BA%8C%E9%87%8D%E5%90%A6%E5%AE%9A%E3%81%AE%E9%99%A4%E5%8E%BB
二重否定の除去（にじゅうひていのじょきょ、英: double negation elimination）および二重否定の導入（にじゅうひていのどうにゅう、英: double negation introduction）は、いずれも推論の種類の一つである

二重否定の導入は直観主義論理でも定理であり、また
¬¬¬A⊢¬A も成立する。
素朴集合論でも、補集合が同様の性質を持つ。集合 A と集合 (A^C)^C は等価である（ここで、A^C は A の補集合を意味する）。

>>168
コピペ癖が治らない重度NPD患者は病院行け

オチコボレ、選択公理使ってる具体的な箇所を示せず
まーた口から出まかせに妄言吐いてるだけでしたとさ

>>172
>証明のどこで選択公理使ってると？　具体的な箇所を示して。

すでに述べた
　>>167より
『コーシー列に二種類 あることを認めようね
　一つは、構成可能なコーシー列 （例えば オイラー数 (Euler's number)e =1+1+1/2!+1/3!+・・ https://en.wikipedia.org/wiki/E_(mathematical_constant)）
　もう一つは、非構成可能なコーシー列
　非構成可能なコーシー列の存在を示すのに、(可算)選択公理を使う
　非構成可能なコーシー列の存在を示せないと 完備がいえない』

なお、下記が参考になるだろう
選択公理の能力は、出力できる非構成可能な列の長さで測れる
可算選択公理は実はDC(ω)と同値
任意の順序数 αについて DC(ℵα)⟺AC（フルパワー選択公理）

(参考)
https://ja.wikipedia.org/wiki/%E5%BE%93%E5%B1%9E%E9%81%B8%E6%8A%9E%E5%85%AC%E7%90%86
従属選択公理(英語: axiom of dependent choice; DCと略される)とは、選択公理(AC)の弱い形で、しかし実解析の大部分を行うのに十分な公理である。これはパウル・ベルナイスによって1942年の、解析学を実行するのに必要な集合論的公理を検討する逆数学の論文で導入された

従属選択公理とは、次の言明である
略
実のところ、x0 は X の好きな元を選ぶことができる。(これを見るには、x0 から始められる
R の有限鎖全体を考え、その中に右が左の延長であるという二項関係を考えてそこに従属選択公理を適用すれば有限鎖の無限列ができるので、それの和を取ればよい。)

使用例
このような公理が無いとしても、各 n について普通の帰納法によって最初の n 項を有限列としてとることはできる。従属選択公理が主張しているのは、その極限であるような可算無限列が取れるということである。

公理 DC はACの断片であって、超限帰納法の各ステップで選択をする必要があって、それまでの選択に独立した選択ができない場合に、可算長の列を構成するのに必要である。

従属選択公理の一般化としてさらに長い超限列の生成を認めるものを考えることができる
公理
DC(ℵα)
略す

この記法を採用すると、可算選択公理は実はDC(ω)と同値であり、実際に一般化になっていることがわかり、全ての順序数について上の命題が成立すると仮定すると選択公理が導ける[1]。

定理(ZF) ― 「任意の順序数 αについて DC(ℵα)⟺AC

>>176
おまえの独善持論なんて聞いてねーよサル
証明のどこで選択公理を使ってるか聞いてんだよ　言葉分かる？　サルだから分からない？

サルはヒト語の学習から　数学は100年早い

ヒト語すら解さぬサルが数学を解す訳が無い　サルは山へ帰れ　シッシ

来世は数学に転生するラノベ

数学者に転生