[過去ﾛｸﾞ]
現代数学の系譜 工学物理雑談 古典ガロア理論も読む62 (1002ﾚｽ)
現代数学の系譜 工学物理雑談 古典ガロア理論も読む62 http://rio2016.5ch.net/test/read.cgi/math/1551963737/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制
です｡10分ほどで解除するので､
他のﾌﾞﾗｳｻﾞ
へ避難してください｡
687: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [sage] 2019/03/22(金) 11:11:04.12 ID:WSdp8+VY >>679-684 おっちゃん、どうも、スレ主です。 R大 ”背理法被害者の会”の被害者かね？（＾＾ 直観主義論理の抜粋は、下記だが ”背理法被害者の会”の主張は、直観主義論理の記述（下記） 「直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。」 と類似しているね だけど、「背理法を使わない意味と直観主義論理との関係」がしっかり論じられていないみたいだから、 ”背理法被害者の会”の被害者が量産されている印象がある。外しているかも知れないがね（＾＾ https://ja.wikipedia.org/wiki/%E7%9B%B4%E8%A6%B3%E4%B8%BB%E7%BE%A9%E8%AB%96%E7%90%86 直観主義論理 直観主義論理または直観論理（英: intuitionistic logic）、あるいは構成的論理（英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念が構成的証明の概念に置き換わっている点で古典論理とは異なる。 直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。 証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。 直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。 形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。 つづき http://rio2016.5ch.net/test/read.cgi/math/1551963737/687
688: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [sage] 2019/03/22(金) 11:11:55.25 ID:WSdp8+VY >>687 つづく 古典論理との関係 古典論理の体系は次のどれかを公理に追加することによって得られる： ・排中律 ・二重否定除去 ・パースの法則 別の関係性としてはゲーデル＝ゲンツェン変換によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。 またグリベンコの定理によれば、命題論理式が古典論理で証明可能であることと、それを二重否定したものが直観主義論理で証明可能であることとは同値である。したがって直観主義論理は古典論理を構成的意味論の観点から拡大したものと見做すことができる。 意味論 ハイティング代数意味論 他の論理との関係 直観主義論理は双対性によって矛盾許容論理の一種であり、ブラジリアン論理、反直観主義論理、双対直観主義論理などと呼ばれる論理と対応している。[3] 直観主義論理から爆発原理を取り除いたものは最小論理として知られる。 多値論理との関係 クルト・ゲーデルは1932年に直観主義論理が多値論理ではないことを証明した。（#ハイティング代数意味論は直観主義論理の"無限多値論理"としての解釈の一種と見られる。） 様相論理との関係 直観主義命題論理の論理式は次のように様相命題論理S4の論理式に翻訳できる： ラムダ計算 カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。[5] (引用終わり) 以上 http://rio2016.5ch.net/test/read.cgi/math/1551963737/688
691: １３２人目の素数さん [sage] 2019/03/22(金) 11:58:44.84 ID:h6pRN5t+ >>687 >R大 ”背理法被害者の会”の被害者かね？（＾＾ >直観主義論理の抜粋は、下記だが 教育とかには余り関心がないのでよく分からんが、それを提唱していた教授のサイトを読むと、 何やら教育では排中律を適用した証明するより、排中律を用いない証明の方が短くなって、 生徒(や学生)が理解し易くなるという。だが、研究段階ではその教授も排中律も認めるようになるとのこと。 数学教育についてそのようなことを書いているような、数学教育に熱心な人だったようだ。 そのサイトによると、その教授は数理論理やシンプレクティック幾何が専門らしい。 隅々までサイトを調べていないだけかも知れない可能性はあるが、 不思議なことにサイトでは明確に業績の論文を挙げて明示してはいなかった。 まあ、幾何と数理論理を研究分野として兼任することは、余りよい選択肢とは思えんが。 幾何では未だに直観が欠かせない。それに対し、数理論理は証明自体などや数学の論理について研究する。 全く違う分野になる。まあ、”背理法被害者の会”の犠牲者は決して少なくはないだろうし、 私はその ”背理法被害者の会”の考え方は全く支持していない。 http://rio2016.5ch.net/test/read.cgi/math/1551963737/691
692: １３２人目の素数さん [sage] 2019/03/22(金) 12:05:44.22 ID:h6pRN5t+ >>687 全く不可解なのが、話によると大学の数学科の講義でも排中律を用いなかったらしいということ。 この行為は全く不可解でならない。わざわざそのような形の講義をすることに何のメリットも見当たらない。 http://rio2016.5ch.net/test/read.cgi/math/1551963737/692
694: 現代数学の系譜 雑談 古典ガロア理論も読む ◆e.a0E5TtKE [sage] 2019/03/22(金) 12:28:03.88 ID:WSdp8+VY >>691-692 おっちゃん、どうも、スレ主です。 同意だね http://www.ma.kagu.tus.ac.jp/~abe/sub3.html 東京理科大学理学部第一部数学科 教授 安部直人 2012年11月16日 02時56分7 (抜粋) 「背理法では途中に正しくない主張や空論や矛盾が必ず現れる」 のに比して 「対偶法では途中に正しくない主張や空論や矛盾は現われない」 ので、対偶法では直接法と同じに証明は完全理解が可能です。 「背理法を用いて証明される命題は、背理法を用いず証明できる」 ことが分かります。 (数学基礎論入門、前原昭二著、朝倉書店、１９７７年) 背理法は、正しくない中間結果(他へ使えず、理解納得できない)も覚えることになり、丸暗記すると大変危険です。また、背理法に慣れてしまうと、中間結果の数学的意味を (考えても無駄と無意識に悟り)考えない習慣がついて、誤った数学的主張に対して鈍感になります。 (引用終わり) これ、上記（>>687）直観主義論理で （>>687） 「直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。」 (>>688) 「ゲーデル＝ゲンツェン変換によるものがある。これは古典一階述語論理が直観主義一階述語論理に埋め込めることを示す。すなわち一階述語論理式が古典論理で証明可能であることと、それをゲーデル・ゲンツェン変換したものが直観主義論理で証明可能であることとが同値となる。」 に対応するだろう http://rio2016.5ch.net/test/read.cgi/math/1551963737/694
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.044s