背理法不要論ってどうなん?
■ このスレッドは過去ログ倉庫に格納されています
>>407
背理法抜きで構成的に証明するのは遥かに難しい >>409
間違いではないよ
直観主義論理の採用しなかつたこととは何かということと
否定の定義はなんとされているかを調べてごらん >>410
恐らく無理じゃないかな
超越数の定義が代数的数ではないことで
代数的数であると仮定して矛盾することが定義だから
これも背理法だと思い込んでると
背理法は使わざるを得ないことになる ¬PとPから人が出る
すなわち
¬PからP→人が出て
P→人から¬Pが出る
というのは
直観主義論理より弱い最小論理でも採用してる公理 >>412
407は¬(AかつB)から(¬Aまたは¬B)を導いているから
直観主義論理では無効な議論だと思うけど >>414
「a、bが超越数ならばa+bまたはabは超越数」の証明ならば背理法は不要
πやeの超越性を前提にした上の話 >>416
背理法が不要というのは直観主義論理で
証明できるという意味? >>407
Π+eとΠeのどちらかは超越数である。
まず、Π+e,とΠ-eのどちらかは超越数である。
何故ならば、Πは超越数かつΠ = {(Π+e)+(Π-e)}/2かつ代数的数全体は体なので。
Π+eが超越数とすると、「Π+eとΠeのどちらかは超越数である」は真。
Π-eが超越数とすると、(Π-e)^2 = (π+e)^2-4πeかつ代数的数全体は体であることより「Π+eとΠeのどちらかは超越数である」は真。
よってΠ+eとΠeのどちらかは超越数である。 >>420
解析学のいくつかの評価式については
背理法以外の証明は知られていない。 背理法を他の同等の推論に置き換えるという意味だから
古典論理の否定ではないね
その程度の日本語も読めない馬鹿には数学は無理だから諦めろ >>425
どれ?
FOURIER INTEGRAL OPERATORS ってやつ? 名著「非圧縮性粘性流の数学的理論」の第89ページの証明中、
「そうでなかったと仮定すると」で始まった文章が
「矛盾する」で終わっていない。
これは「見かけの背理法」か? >>430
bounded arithmeticという分野がその辺りを研究している 無矛盾であることが証明された系、または無矛盾であることが証明不可能であることが証明された系でしか背理法は使えないのでは?
矛盾を導出したとして、その原因が「仮定」にあるのか系自体にあるのか判別できないから >>433
背理法は偽の命題を導いてその仮定が偽だとする論法
理論の無矛盾性なんて関係ない
つまり、もし偽の命題を導いてその仮定が偽であるかどうか知りたいならそれを証明の中で用いているか調べさえすればいい 中学生のときに以下のような妄想をした。
命題の論理をつなげて公理から定理、定理、定理とどんどん論理の網を
広げて行く際に、まるで複素関数論の解析接続のように、論理の網を
どんどんと進めていくときに、その経路によって結果に違いが出る
ことが起こらないのかなと。例えばy=√xのような代数函数の
リーマン面は原点と無限円点以外では二価になっていて、そのことを
しらなければ、x=1のときy=1から接続して原点の周りを回ってくると
x=1でy=−1になるので、よって1=−1だ、みたいな間違った結果を
導くけれども、それに類したことが起こらないのかという感じの妄想だ。
つまり、命題を証明する手段の網目をつなぐときの経路によって
異なる結果が得られても良いのではないだろうか、それは別のリーマン面の
シートに入り込んだようなものだと考えれば矛盾ではないと。
そういう妄想を抱いたのだ。 >>434
矛盾が導出された理由が追加した仮定にあるのか系自体にあるのかが証明できないので仮定が偽である証明にはならない 延々とバグで紛れ込んだ裏面が続く悪夢的コンピューターゲーム。 排中律を証明できれば背理法を使ってもいいと思う。YESかNOか2択しかないっていう状況自体をまず証明してその上で背理法を使う。
これなら問題ないはず。 ある命題が「正しい」か「正しくない」か「決定不能」であるかの
3種類の"状態"があると思いますが、決定する手順が存在しないで
決定不能であっても、もしもたまたま成立することを示す例が
見付かれば「正しい」になるし、成立しないことを示す例が
見付かれば「正しくない」になるでしょう。
しかしたとえば、平面幾何で平行線公理を除いた体系を考えて、
その中で「平行線公理」を普通の命題のように考えて、
それが正しいか正しくないかを決定しようとしても、
正しいあるいは正しくないという証明はできないはずです。
つまりそのような「決定不能」の場合には、どれだけ成立例
あるいは反例をさがしたとしても、見付かるということは
あり得ませんね。
そうなると、正しいか、正しくないかの二通りだというのは
無理があるのではないでしょうか? 排中律は成り立つのでしょうか? よく知らないけど直観主義論理はそういった違和感から産み出さたのかな? ある程度複雑な体系はその中では真偽を決定出来ない命題が存在する、
とゲーデルがのたまっているそうだから排中律は成り立たないのではないだろうか?
決定できない命題を1つをとり、それを肯定するあるいは否定する命題を公理系に
新たに付け加えたとしても、その拡大された体系の中にも真偽を決定出来ない命題が
存在する,そこでその決定出来なかった命題をまた1つとり、それを肯定あるいは
否定する命題を再度公理系に新たに付け加えたとしても、その拡大された体系の
中には、。。。。。いくらやってもキリがないことになる。
こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの? 排中律は証明すべきものではないでしょう。
公理として認めてスタートするか、
認めないとするかを選べばいいだけ。
悩む時間があるなら、どっちかに決めて、
数学を始めた方が有意義。 決定不能な命題は真であると仮定しても偽であると仮定しても矛盾を導けないので気にする必要はない >こんなことでは安心して夜も寝られない。それでも排中律は成り立つと言えるの?
君は排中律の意味が全く理解できていない。
すでにコメントにあるが、決定不能な命題がその理論に存在しても排中律には何の影響も与えない。
理論Tに対して、その理論で決定不能な命題をAとする。
TからはAも¬Aもどちらも証明できないということは、
(1)TにAを加えたT+A
(2)Tに¬Aを加えたT+¬A
という二つの新しい理論が考えられ、そのどちらも矛盾しない。
しかし、排中律が成り立つということは(1)かつ(2)を考えると「Aかつ¬A」となって矛盾する。
ただこれだけのことだ。 >長〜い背理法ってウザい
証明の長さに背理法か否かは全く関係がない.
長い証明はうざいかもしれないが,現状その証明しかないのならそれを理解するしかない. >基礎論バカはまじ不要
>数学バカはもっと不要
確かにバカは不要かもしれんな.
しかし,基礎論や数学に通じている人間は総じてバカではない.
これは他の理学の研究者などでも同じこと.
だから,そんな人間はこの世にほぼいないだろうな.
最もこの世に必要ない連中は,何も学ばずに思い込みで何らかの分野をバカ呼ばわりする本物のバカだけだろう. >ZFCなら排中律を証明できる
この事実だけなら確か1950年あたりには既に知られているはず.
直感主義論理で解析を実行しようという数学もあるけど,その場合の集合論では選択公理は入れてはいけない.
「Z+選択公理」を集合論の前提にしてしまうと,論理が直観主義論理でも集合に関する全ての事柄で排中律が成り立ってしまうから,せっかく直観主義論理でやったら古典論理とどう違うのかを考えているのに,古典論理でやったのと区別がつかなくなる.
同じ理由で(普通の)正則性公理を仮定しても排中律が出る.
直観主義的集合論でも選択公理や正則性公理(基礎の公理)の名前は出てくるが,それは通常のZFCのそれらより弱い形のもので別物だ. >>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’)を自由に扱って良い古典論理の場合の事をさす. >>452
希少だが,声がでかいからバカが目立つ.
数学や基礎論に親でも殺されたのかというぐらいにヘイトがあるから真正のバカはすぐ分かる. >>455
基礎論(この場合は証明論)に関する話題で基礎論を排除しようという奴らこそがキチガイ。
料理教室で「料理の先生煩い」と吠えるDQN猿と一緒。 >>453
話の前後関係しらんけど
> 自然演繹(推論)における「否定の導入」という推論規則が別名背理法なんだよ
これは違うだろ
背理法は¬P→⊥からPを結論する
否定の導入はP→⊥から¬Pを結論する ■ このスレッドは過去ログ倉庫に格納されています