背理法はいりほう

背理法はいりほう（はいりほう、英えい: 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$ を結論けつろんすることは、認みとめられる。