背理法（はいりほう、、）とは、ある命題 "P" を証明したいときに、"P" が偽であると仮定して、そこから矛盾を導くことにより、"P" が偽であるという仮定が誤り、つまり "P" は真であると結論付けることである。帰謬法（きびゅうほう）とも言う。"P" を仮定すると、矛盾が導けることにより、"P" の否定 ¬"P" を結論付けることは否定の導入などと呼ばれる。これに対して ¬"P" を仮定すると矛盾が導けることにより "P" を結論付けることを狭義の背理法あるいは否定の除去ということがある。否定の導入と狭義の背理法をあわせて広義の背理法ということもある。一般的には、背理法と言った場合広義の背理法を指す。否定の導入により、¬"P" から矛盾が導けた場合、¬¬"P" を結論できるが、いわゆる古典論理では推論規則として二重否定の除去が認められているため、結局 "P" が結論できることになる。排中律や二重否定の除去が成り立たない直観論理では、狭義の背理法による証明は成立しないが、否定の導入や、¬¬¬"P" から ¬"P" を結論することは、認められる。背理法を使って証明される有名な定理には、formula_1 が無理数であること、素数が無限に存在すること、中間値の定理，ハイネ・カントールの定理などがあり、無限を相手にした証明には基本的に背理法のスタイルを取らざるを得ないものが多くある。しかし例えば、formula_1 が無理数である（すなわち有理数でない）ことの証明は、狭義の背理法ではなく否定の導入によって証明することができる。背理法の証明において仮定に矛盾する結論を導く場合は，容易に非背理法証明に直すことができる．たとえば，ハイネ・カントールの定理：「有界閉集合上の連続関数は一様連続である」は，有界閉集合上の連続関数 "f" は一様連続でないと仮定して議論を進め， "f" が連続でないことを導いて矛盾を出すが，これは連続性を仮定せず「有界閉集合上の関数 "f" が一様連続でない」と仮定し，連続でないことを示すことによって，対偶としてハイネ・カントールの定理が直接証明できる（((P かつ Q)⇒R) ⇔ ((P かつ ￢R)⇒￢Q) ということを用いる）．

出典:wikipedia