背理法

背理法（はいりほう、英: proof by contradiction, reduction to the absurd, indirect proof, apagogical argument など、羅: reductio ad absurdum, RAA）とは、ある命題 $P$ を証明したいときに、 $P$ が偽であることを仮定して、そこから矛盾を導くことによって、 $P$ が偽であるという仮定が誤り、つまり $P$ は真であると結論付けることである^[1]。帰謬法（きびゅうほう）とも言う。

$P$ を仮定すると、矛盾 $⊥$ が導けることにより、 $P$ の否定 $\neg P$ を結論付けることは否定の導入などと呼ばれる^[2]。

{\cfrac {\displaystyle {[P] \atop \bot }}{\neg P}}

これに対して $\neg P$ を仮定すると矛盾 $⊥$ が導けることにより $P$ を結論付けることを狭義の背理法あるいは否定の除去ということがある。

{\cfrac {\displaystyle {[\neg P] \atop \bot }}{P}}

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