背理法

テンプレート:Redirect テンプレート:出典の明記 背理法（はいりほう、テンプレート:Lang-en-short など、テンプレート:Lang-la-short）とは、ある命題テンプレート:Mvar を証明したいときに、テンプレート:Mvar が偽であることを仮定して、そこから矛盾を導くことによって、テンプレート:Mvar が偽であるという仮定が誤り、つまりテンプレート:Mvar は真であると結論付けることであるテンプレート:Sfn。帰謬法（きびゅうほう）とも言う。

\frac{\binom{[P]}{⊥}}{\neg P}

これに対してテンプレート:Math を仮定すると矛盾テンプレート:Math が導けることによりテンプレート:Mvar を結論付けることを狭義の背理法あるいは否定の除去ということがある。

\frac{\binom{[\neg P]}{⊥}}{P}

否定の導入と狭義の背理法をあわせて広義の背理法ということもある。一般的に、背理法と言った場合は広義の背理法を指す。否定の導入により、テンプレート:Math から矛盾が導けた場合、テンプレート:Math を結論できるが、いわゆる古典論理では推論規則として二重否定の除去が認められているため、結局テンプレート:Mvar が結論できることになる。排中律や二重否定の除去が成り立たない直観論理では、狭義の背理法による証明は成立しないがテンプレート:Sfn、否定の導入や、テンプレート:Math からテンプレート:Math を結論することは、認められる。

背理法を使って証明される有名な定理には、2の平方根 $\sqrt{2}$ が無理数であること、素数が無限に存在すること、中間値の定理，ハイネ・カントールの定理などがある。

しかし例えば、 $\sqrt{2}$ が無理数である（すなわち有理数でない）ことの証明は、狭義の背理法ではなく否定の導入によって証明することができる。

脚注