背理法不要論ってどうなん？

背理法不要論ってどうなん？ at MATH

436:１３２人目の素数さん
22/12/24 09:07:45.43 6P5AjeCt.net
矛盾とは何を指すのかという妄想は湧かなかった？

437:１３２人目の素数さん
22/12/24 09:25:24.79 OdkKx1mA.net
>>434
矛盾が導出された理由が追加した仮定にあるのか系自体にあるのかが証明できないので仮定が偽である証明にはならない

438:１３２人目の素数さん
22/12/24 19:18:29.62 QubhUbIE.net
延々とバグで紛れ込んだ裏面が続く悪夢的コンピューターゲーム。

439:１３２人目の素数さん
23/01/01 10:07:26.27 W1uGFZgv.net
排中律を証明できれば背理法を使ってもいいと思う。YESかNOか2択しかないっていう状況自体をまず証明してその上で背理法を使う。
これなら問題ないはず。

440:１３２人目の素数さん
23/01/02 11:01:19.68 Tjm8RrUz.net
ある命題が「正しい」か「正しくない」か「決定不能」であるかの
3種類の"状態"があると思いますが、決定する手順が存在しないで
決定不能であっても、もしもたまたま成立することを示す例が
見付かれば「正しい」になるし、成立しないことを示す例が
見付かれば「正しくない」になるでしょう。
しかしたとえば、平面幾何で平行線公理を除いた体系を考えて、
その中で「平行線公理」を普通の命題のように考えて、
それが正しいか正しくないかを決定しようとしても、
正しいあるいは正しくないという証明はできないはずです。
つまりそのような「決定不能」の場合には、どれだけ成立例
あるいは反例をさがしたとしても、見付かるということは
あり得ませんね。
そうなると、正しいか、正しくないかの二通りだというのは
無理があるのではないでしょうか？　排中律は成り立つのでしょうか？

441:１３２人目の素数さん
23/01/02 12:13:58.59 g8sppIUg.net
よく知らないけど直観主義論理はそういった違和感から産み出さたのかな？

442:１３２人目の素数さん
23/01/09 20:07:44.17 afxohR47.net
ある程度複雑な体系はその中では真偽を決定出来ない命題が存在する、
とゲーデルがのたまっているそうだから排中律は成り立たないのではないだろうか？
決定できない命題を1つをとり、それを肯定するあるいは否定する命題を公理系に
新たに付け加えたとしても、その拡大された体系の中にも真偽を決定出来ない命題が
存在する，そこでその決定出来なかった命題をまた1つとり、それを肯定あるいは
否定する命題を再度公理系に新たに付け加えたとしても、その拡大された体系の
中には、。。。。。いくらやってもキリがないことになる。
　こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの？　

443:１３２人目の素数さん
23/01/10 22:35:57.38 sWivYE4V.net
排中律は証明すべきものではないでしょう。
公理として認めてスタートするか、
認めないとするかを選べばいいだけ。
悩む時間があるなら、どっちかに決めて、
数学を始めた方が有意義。

444:１３２人目の素数さん
23/01/20 09:41:28.41 A5vIrXQO.net
決定不能な命題は真であると仮定しても偽であると仮定しても矛盾を導けないので気にする必要はない

445:１３２人目の素数さん
23/04/01 10:48:43.51 1/gRl0so.net
＞こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの？
君は排中律の意味が全く理解できていない。
すでにコメントにあるが、決定不能な命題がその理論に存在しても排中律には何の影響も与えない。
理論Tに対して、その理論で決定不能な命題をAとする。
TからはAも￢Aもどちらも証明できないということは、
（1）TにAを加えたT+A
（2）Tに￢Aを加えたT+￢A
という二つの新しい理論が考えられ、そのどちらも矛盾しない。
しかし、排中律が成り立つということは（1）かつ（2）を考えると「Aかつ￢A」となって矛盾する。
ただこれだけのことだ。

446:１３２人目の素数さん
23/04/01 11:16:51.79 SFuGsu5u.net
長～い背理法ってウザい

447:１３２人目の素数さん
23/04/01 13:09:41.82 0oPYJmC1.net
基礎論バカはまじ不要

448:１３２人目の素数さん
23/04/01 13:23:54.15 7ziiEkiM.net
数学バカはもっと不要

449:１３２人目の素数さん
23/04/02 15:03:00.34 icxGHFsq.net
>長～い背理法ってウザい
証明の長さに背理法か否かは全く関係がない．
長い証明はうざいかもしれないが，現状その証明しかないのならそれを理解するしかない．

450:１３２人目の素数さん
23/04/02 15:05:58.84 icxGHFsq.net
>基礎論バカはまじ不要
>数学バカはもっと不要
確かにバカは不要かもしれんな．
しかし，基礎論や数学に通じている人間は総じてバカではない．
これは他の理学の研究者などでも同じこと．
だから，そんな人間はこの世にほぼいないだろうな．
最もこの世に必要ない連中は，何も学ばずに思い込みで何らかの分野をバカ呼ばわりする本物のバカだけだろう．

451:１３２人目の素数さん
23/04/02 15:42:32.72 icxGHFsq.net
>ZFCなら排中律を証明できる
この事実だけなら確か1950年あたりには既に知られているはず．
直感主義論理で解析を実行しようという数学もあるけど，その場合の集合論では選択公理は入れてはいけない．
「Z＋選択公理」を集合論の前提にしてしまうと，論理が直観主義論理でも集合に関する全ての事柄で排中律が成り立ってしまうから，せっかく直観主義論理でやったら古典論理とどう違うのかを考えているのに，古典論理でやったのと区別がつかなくなる．
同じ理由で（普通の）正則性公理を仮定しても排中律が出る．
直観主義的集合論でも選択公理や正則性公理（基礎の公理）の名前は出てくるが，それは通常のZFCのそれらより弱い形のもので別物だ．

452:１３２人目の素数さん
23/04/02 15:42:46.97 SX50VDhd.net
本物のバカは希少種

453:１３２人目の素数さん
23/04/02 16:08:53.38 icxGHFsq.net
>>411
>直観主義論理の採用しなかつたこととは何かということと
自然演繹（推論）における「否定の導入」という推論規則が別名背理法なんだよ．
そして，背理法の原理はそのままこの否定の導入でもある．
演繹定理があるから否定の導入の推論規則は「公理」の形に書き換えることもできるから，やる意味はないが「対偶の公理」のように「背理法の公理」とすることもできる．
古典論理はこの「否定の導入」だけでなく「排中律」つまり実質は「二重否定の除去」に相当する否定の特徴づけが加えてある．
直観主義論理には否定に関しては「否定の導入」しかない．
理論Γと命題Aを仮定して，それがΓと矛盾する事を示して，¬Aを結論づける論法が背理法（否定の導入に対応）だ．
(1)．Γ,A ⊢ P(B,C,D,…）⇛⊥(矛盾)，よって¬A
対して，最初の仮定をAから¬Aに置き換えたものが
(2)．Γ,¬A ⊢ P(B,C,D,…）⇛⊥(矛盾)，よって¬(¬A)
となる．直観主義論理だと最後の¬(¬A)はAと同じと言い切れないが，古典論理ならおなじになる．
(2’)．Γ,¬A ⊢ P(B,C,D,…）⇛⊥(矛盾)，よってA
そして背理法とは，なんの断りもなければ，(1)，(2’)を自由に扱って良い古典論理の場合の事をさす．

454:１３２人目の素数さん
23/04/02 16:11:57.27 icxGHFsq.net
>>452
希少だが，声がでかいからバカが目立つ．
数学や基礎論に親でも殺されたのかというぐらいにヘイトがあるから真正のバカはすぐ分かる．

455:１３２人目の素数さん
23/04/02 18:03:14.26 qCWehNrF.net
声がデカいのはどう見ても基礎カスだろうが

456:１３２人目の素数さん
23/04/02 19:58:04.00 qCWehNrF.net
スレ見渡したけど、クソスレだった．．．