背理法と対偶って違うの？ (117ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
38: １３２人目の素数さん [sage] 2024/11/13(水)12:07 ID:0yIDnyuw(1/3)
直観主義論理と背理法
下記が分かり易い
mathlog.info/articles/3000
E 自己紹介・記録 2022年2月15日
私が直観主義論理を擁立するたった1つの理由
本題に入る前に
最初に明確にしておきたいのですが、私は古典論理における背理法や排中律の正しさを疑っているわけでは全くありません。
直観主義論理を擁護するとしたらこの路線かなあと思いましたので記事にしてみました。
古典論理とは？
略
直観主義論理
そこで現れるのが直観主義論理です。
直観主義論理では「命題とは真であるか偽であるかが定まるものである」という真理値としての命題の定義を捨て、その代わりに「命題とはそれが真であるかどうかを判断できるものであり、命題が真であるとはその証明を実際に構成して説明できることである」というように定義します。
もちろん、この後には証明の構成とは何か？という説明が必要ですが今回は割愛します。
これにより何が変わるかと言うと、命題には真偽を定めなければならないという古典論理の制約が無くなるため、自由変数命題も命題として扱うことができるようになります。つまり、"自由変数命題が真である"ということを議論できるようになります。
そして、自由変数命題の証明とはまさしく自由変数証明のことです。
このように、構成の観点から普段私たちが数学をする際に行っている無限の領域に対する量化を正当化することができます。
ただし、古典論理を捨てる代償もあり、直観主義論理の命題の定義では「命題の真偽が定まる」とは限らなくなってしまうため、特に命題の否定の意味が古典論理から大きく変わってしまいます。
これにより、古典論理では"命題の定義より明らか"であった排中律であったり背理法であったりが一般には成り立たなくなる……というのは有名な話です。
しかし、排中律を捨てるか無限領域での量化を捨てるかを選ぶとすれば私は前者を選ぶでしょう。
(引用終り)
39: １３２人目の素数さん [sage] 2024/11/13(水)12:08 ID:0yIDnyuw(2/3)
下記は、かなり荒っぽい説明ですが
ゆえに分かり易い説明で、参考になります
『集合論のパラドックスです。例えばXを自分自身を元として含まない集合の集合としましょう。さてX∈Xでしょうか。X∈XとするとXの定義からXの元ではありません。一方X∈Xではないとすると、X∈Xのはずです。いずれにしても矛盾が導かれます。』
これに対する直観主義（構成主義）は
『排中律（任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する』です
note.com/yoriyuki/n/n456e260e4b1f
数学基礎論論争は結局どうなったか 筆の滑り 2020年5月17日
数学に関心のある人なら、20世紀の初めに「数学基礎論論争」があったことをぼんやりとは聞いたことがあると思います。数学基礎論論争が結局どうなったかについて書きます。
目次
数学基礎論論争とは
論理主義
形式主義
直観主義（構成主義）
その後どうなったか
数学基礎論論争とは
19世紀を通じて数学は厳密化の道をたどってきました。たとえばフーリエ級数の収束については多くの誤った「証明」がなされ、最終的に「測度0上の除外点を除いて収束する」という条件にたどりついたのは20世紀になってからです。そして「測度」という概念を定式化するには集合論が不可欠です。
そこで集合論を厳密に公理的に取り扱う試みが行われましたが、ここで表面化したのが集合論のパラドックスです。例えばXを自分自身を元として含まない集合の集合としましょう。さてX∈Xでしょうか。X∈XとするとXの定義からXの元ではありません。一方X∈Xではないとすると、X∈Xのはずです。いずれにしても矛盾が導かれます。
このようなパラドックスにどう対応するかという問題を契機にして、数学をどのように行うべきか関する論争が行われました。これを数学基礎論論争といいます。数学の危機とも呼ばれます。
ただし、この「危機」の最中にも数学は普通に発展していました。したがって「危機」というのは誇張だという考えもあります。また、現代から見ると何を論争しているかよくわからないところがあります。個人的な誤解にもとづく争いであったと考える人もいるようです（ファン・ダーレンとか）。また、単に集合論のパラドックスの解決を目指したものではなく、無矛盾性や数学の確実性を担保することだけがゴールでもありませんでした。
形式主義
形式主義はヒルベルトが唱えた立場とされています。
略
形式主義は失敗したということになっています。ゲーデルの不完全性定理より、Tの中に含まれる手段ではTの無矛盾性を示すことはできません。有限的な理論がTに含まれていると考えれば、Tの無矛盾性を有限的に示すことはできません。
ただ、個人的にはこの結論は性急だと思っています。Tに含まれない有限的な原理を想定することが可能だからです。例えば、順序数解析では自然数上のある種の順序について帰納法が可能であることから、いろいろな数学体系の無矛盾性を示しています。
つづく
40: １３２人目の素数さん [sage] 2024/11/13(水)12:09 ID:0yIDnyuw(3/3)
つづき
直観主義（構成主義）
直観主義数学とは、オランダの数学者ブラウアー(1881-1966)によって提唱された立場です。直観主義数学は排中律（任意の命題Pについて「PであるかPでないかどちらかである」とする主張)を否定する数学と紹介されることがありますが、排中律を否定するのはその主張の一部であって、他の古典数学の主張も否定されたり、古典数学とは相容れない独自の主張がなされることもあります。また、気まぐれに排中律を否定しているわけではなく、その背景には理由付けが存在します。
直観主義数学は大雑把に言って「具体的に操作可能なもの」だけが数学の対象だと考えます。そして、何かが存在すると主張することはそれを「構成」することだと考えます。また、「証明」自体も数学の対象です。ただし、数学の証明とは形式論理の推論の並びではなく、ある数学的命題の正しさを「構成」する「直観」です。
略
新しい数学の基礎として注目されているホモトピー型理論は直観主義型理論にUnivalent axiomという公理を追加したものになっています。また、古典的な数学をある程度直観主義の数学で解釈することが可能です。なので真っ向から対立するものだ、と考える必要はないことを付け加えておきます。
その後どうなったか
集合論のパラドックスについては、矛盾を含まないだろうと思われるZFCという小公理系が整備されて、あまり問題にならなくなりました。一方で、数学基礎論論争をきっかけに始まった数学の基礎についての研究は、数理論理学という形で（数学の基礎とはもはやあまり関係はなく）発展しています。また、集合論は圏論を扱うのがやや不便なので圏論そのものを基礎に据える考えや、直観主義の立場にたったホモトピー型理論などが新しい数学の基礎として研究されています。
(引用終り)
以上
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.941s*