このサイトは学部では早稲田で物理を, 修士では東大で数学を専攻し, 今も非アカデミックの立場で数学や物理と向き合っている一市民の奮闘の記録です. 運営者情報および運営理念についてはこちらをご覧ください.

理系のための総合語学・リベラルアーツの視点から数学・物理・プログラミング・語学 (特に英語) の情報を発信しています. コンテンツアーカイブに見やすくまとめているのでぜひご覧ください.

どこまでどう引用していいものかわからないがとりあえず記録.
結城浩さんのサイトから.

• 背理法のお話

これがフェイスブックで次のように引用されていた.

高校生に背理法の説明をするのに「sqrt(2)は無理数」は定番で、避ける方法も思いつきませんが、もやもやしちゃうんですよね。背理法の形式で書いているだけで、実は否定導入ですから。どうしたものか、ずっと悩んでいます。
次回、ミルカさんが中間値の定理とか証明に背理法が本質的に必要なものの話をしてくれるのを期待します。ちなみに、「証明に背理法が本質的に必要」の定義は「古典数学で証明できてBishop流構成的数学で証明できない」でいいですよね。

これに対して次のようなやりとりがあった.

そういう話はどんな本とか読むときちんとした記述があるのでしょうか？
論理系統の話、初等的な範囲で問題が色々あるっぽいのにそれを説明している記述になかなか巡り会えないので困っています。
基礎論やら数理論理をゴリゴリやるのも大変で。

これへのコメント.

そういえば、構成的証明についてまとめた本は思い当たりません。ほしいですね。

さらにコメント.

http://ameblo.jp/metameta7/entry-11526220719.html
8番目のwd0さんのコメント（の下から5行目を「狭義の排中律」から「狭義の背理法」に直したもの）を読むだけでずいぶん前に進めますね。

コメントも引用しておこう.

まず明快なコメントを.

結論から言えば、安部さんは「背理法を使わない」の定義を明確に定義せずに曖昧な主張をしているために、トンデモな議論になっています。
Ｐを証明するために、￢Ｐを仮定して矛盾を導く。
￢Ｐを証明するために、Ｐを仮定して矛盾を導く。
狭義には前者のみが背理法です。後者は否定導入と呼ばれます。

参考のため以降の部分も引用.

高校数学は、狭義の背理法と否定導入をあわせたものを背理法と呼ぶ立場です。高校数学ではそれで困らないのでしょう。

数理論理学では、背理法と否定導入は性質が大きく異なるので、広義の背理法としてまとめて扱うことに何の利点もありません。したがって、通常はそうしません。

構成的論理（別名：直観主義論理）では狭義の背理法は使えませんが、否定導入は許されます。古典論理（通常の数学で用いる論理）で証明できるが、構成的論理では証明できない定理は掃いて捨てるほどあります。

古典論理は構成的論理＋狭義の背理法と同値であることが知られています。さらに、構成的論理＋排中律とも構成的論理＋二重否定除去とも同値であることが知られています。

狭義の背理法は使ってはならないが排中律か二重否定除去は使って良いとするなら、「背理法で証明できることは背理法を使わないで証明できる」は真です。排中律か二重否定除去を使うように書き換えればよいのですから。

狭義の排中律と同値なものも背理法の変種とみなして使ってはよくないとするなら、上記の主張は偽です。古典論理で証明できて構成的論理で証明できないすべての定理が反例となります。中間値の定理もその一例です。

広義の背理法（およびそれと同値なものすべて）を使用不可とするなら、それは構成的論理よりもさらに弱い論理となります。当然、上記の主張は偽となります。

つまり、安部さんの主張は「背理法を使う」を明確に定義しない限り、ナンセンスということです。

今日も脱背理法は厳しい.