[過去ﾛｸﾞ] 背理法不要論ってどうなん？ (459ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
440: 2023/01/02(月)11:01 ID:Tjm8RrUz(1) AAS
ある命題が「正しい」か「正しくない」か「決定不能」であるかの
3種類の"状態"があると思いますが、決定する手順が存在しないで
決定不能であっても、もしもたまたま成立することを示す例が
見付かれば「正しい」になるし、成立しないことを示す例が
見付かれば「正しくない」になるでしょう。
しかしたとえば、平面幾何で平行線公理を除いた体系を考えて、
その中で「平行線公理」を普通の命題のように考えて、
それが正しいか正しくないかを決定しようとしても、
正しいあるいは正しくないという証明はできないはずです。
つまりそのような「決定不能」の場合には、どれだけ成立例
省4
441: 2023/01/02(月)12:13 ID:g8sppIUg(1) AAS
よく知らないけど直観主義論理はそういった違和感から産み出さたのかな？
442: 2023/01/09(月)20:07 ID:afxohR47(1) AAS
ある程度複雑な体系はその中では真偽を決定出来ない命題が存在する、
とゲーデルがのたまっているそうだから排中律は成り立たないのではないだろうか？
決定できない命題を1つをとり、それを肯定するあるいは否定する命題を公理系に
新たに付け加えたとしても、その拡大された体系の中にも真偽を決定出来ない命題が
存在する，そこでその決定出来なかった命題をまた1つとり、それを肯定あるいは
否定する命題を再度公理系に新たに付け加えたとしても、その拡大された体系の
中には、。。。。。いくらやってもキリがないことになる。
こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの？
443: 2023/01/10(火)22:35 ID:sWivYE4V(1) AAS
排中律は証明すべきものではないでしょう。
公理として認めてスタートするか、
認めないとするかを選べばいいだけ。
悩む時間があるなら、どっちかに決めて、
数学を始めた方が有意義。
444: 2023/01/20(金)09:41 ID:A5vIrXQO(1) AAS
決定不能な命題は真であると仮定しても偽であると仮定しても矛盾を導けないので気にする必要はない
445: 2023/04/01(土)10:48 ID:1/gRl0so(1) AAS
＞こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの？
君は排中律の意味が全く理解できていない。
すでにコメントにあるが、決定不能な命題がその理論に存在しても排中律には何の影響も与えない。
理論Tに対して、その理論で決定不能な命題をAとする。
TからはAも¬Aもどちらも証明できないということは、
（1）TにAを加えたT+A
（2）Tに¬Aを加えたT+¬A
という二つの新しい理論が考えられ、そのどちらも矛盾しない。
しかし、排中律が成り立つということは（1）かつ（2）を考えると「Aかつ¬A」となって矛盾する。
ただこれだけのことだ。
446: 2023/04/01(土)11:16 ID:SFuGsu5u(1) AAS
長～い背理法ってウザい
447: 2023/04/01(土)13:09 ID:0oPYJmC1(1) AAS
基礎論バカはまじ不要
448: 2023/04/01(土)13:23 ID:7ziiEkiM(1) AAS
数学バカはもっと不要
449: 2023/04/02(日)15:03 ID:icxGHFsq(1/5) AAS
>長〜い背理法ってウザい
証明の長さに背理法か否かは全く関係がない．
長い証明はうざいかもしれないが，現状その証明しかないのならそれを理解するしかない．
450: 2023/04/02(日)15:05 ID:icxGHFsq(2/5) AAS
>基礎論バカはまじ不要
>数学バカはもっと不要
確かにバカは不要かもしれんな．
しかし，基礎論や数学に通じている人間は総じてバカではない．
これは他の理学の研究者などでも同じこと．
だから，そんな人間はこの世にほぼいないだろうな．
最もこの世に必要ない連中は，何も学ばずに思い込みで何らかの分野をバカ呼ばわりする本物のバカだけだろう．
451: 2023/04/02(日)15:42 ID:icxGHFsq(3/5) AAS
>ZFCなら排中律を証明できる
この事実だけなら確か1950年あたりには既に知られているはず．
直感主義論理で解析を実行しようという数学もあるけど，その場合の集合論では選択公理は入れてはいけない．
「Z＋選択公理」を集合論の前提にしてしまうと，論理が直観主義論理でも集合に関する全ての事柄で排中律が成り立ってしまうから，せっかく直観主義論理でやったら古典論理とどう違うのかを考えているのに，古典論理でやったのと区別がつかなくなる．
同じ理由で（普通の）正則性公理を仮定しても排中律が出る．
直観主義的集合論でも選択公理や正則性公理（基礎の公理）の名前は出てくるが，それは通常のZFCのそれらより弱い形のもので別物だ．
452(1): 2023/04/02(日)15:42 ID:SX50VDhd(1) AAS
本物のバカは希少種
453(1): 2023/04/02(日)16:08 ID:icxGHFsq(4/5) AAS
>>411
>直観主義論理の採用しなかつたこととは何かということと
自然演繹（推論）における「否定の導入」という推論規則が別名背理法なんだよ．
そして，背理法の原理はそのままこの否定の導入でもある．
演繹定理があるから否定の導入の推論規則は「公理」の形に書き換えることもできるから，やる意味はないが「対偶の公理」のように「背理法の公理」とすることもできる．
古典論理はこの「否定の導入」だけでなく「排中律」つまり実質は「二重否定の除去」に相当する否定の特徴づけが加えてある．
直観主義論理には否定に関しては「否定の導入」しかない．
理論Γと命題Aを仮定して，それがΓと矛盾する事を示して，¬Aを結論づける論法が背理法（否定の導入に対応）だ．
(1)．Γ,A ⊢ P(B,C,D,…）⇛⊥(矛盾)，よって¬A
対して，最初の仮定をAから¬Aに置き換えたものが
省4
454: 2023/04/02(日)16:11 ID:icxGHFsq(5/5) AAS
>>452
希少だが，声がでかいからバカが目立つ．
数学や基礎論に親でも殺されたのかというぐらいにヘイトがあるから真正のバカはすぐ分かる．
455(1): 2023/04/02(日)18:03 ID:qCWehNrF(1/2) AAS
声がデカいのはどう見ても基礎カスだろうが
456: 2023/04/02(日)19:58 ID:qCWehNrF(2/2) AAS
スレ見渡したけど、クソスレだった．．．
457: 2023/04/24(月)12:44 ID:jbDWs/M5(1) AAS
>>455
基礎論（この場合は証明論）に関する話題で基礎論を排除しようという奴らこそがキチガイ。
料理教室で「料理の先生煩い」と吠えるDQN猿と一緒。
458: 2023/04/26(水)08:51 ID:KQBwQ7v3(1) AAS
ブヒブヒブヒｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ
459: 2023/05/09(火)13:33 ID:WePDQ/me(1) AAS
>>453
話の前後関係しらんけど
> 自然演繹（推論）における「否定の導入」という推論規則が別名背理法なんだよ
これは違うだろ
背理法は¬P→⊥からPを結論する
否定の導入はP→⊥から¬Pを結論する
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.336s*