背理法は、ある命題 P を証明したいときに、まずその命題 P の否定である ¬P を仮定します。そして、その仮定 ¬P から論理的に矛盾（Q∧¬Q の形、あるいは単に ⊥（ボトム、矛盾を表す記号）と書かれます）を導き出します。矛盾が導かれたということは、最初の仮定 ¬P が誤っていた（偽であった）ことを意味します。したがって、¬P が偽である以上、その否定である P（すなわち ¬(¬P)）が真である、と結論付ける推論方法です。
この推論の構造は、以下のように論理記号で表すことができます。
- 証明したい命題: P
- 背理法の仮定: ¬P を仮定する。
- 矛盾の導出: 仮定 ¬P から出発し、推論を進めていくと、ある命題 Q とその否定 ¬Q が同時に成り立つという形（Q∧¬Q）、あるいは単に矛盾 ⊥ が導かれることを示します。これは、次のように書けます。¬P⊢(Q∧¬Q)または¬P⊢⊥（ここで、⊢ は「～から（論理的に）導出される」という意味の記号です。）
- 矛盾からの結論: ¬P を仮定すると矛盾が生じるので、¬P は偽でなければなりません。(¬P→(Q∧¬Q))あるいは(¬P→⊥)この含意文が真であることから、前件である ¬P は偽であると結論づけられます（後件である Q∧¬Q や ⊥ は定義上、偽であるため、この含意文全体が真となるためには、前件 ¬P が偽でなければならない、というモーダストーレンスに近い考え方です）。
- 最終的な結論: ¬P が偽であるため、P が真であると結論します。これは、古典論理における二重否定の除去（¬¬P↔P）という法則に基づいています。つまり、(¬P→⊥)→P という推論規則として定式化できます。
したがって、背理法全体の論理構造を一つの論理式として表現するならば、次のようになります。
(¬P→(Q∧¬Q))→P
あるいは、矛盾を ⊥ で表すなら、
(¬P→⊥)→P
これが背理法の論理記号による表現です。
補足:
- 矛盾律 ¬(Q∧¬Q) は、古典論理において常に真である（トートロジー）と考えられています。背理法は、この矛盾律を暗黙の前提として用いています。
- 直観主義論理など、一部の非古典論理では、(¬P→⊥)→P という形の二重否定除去を無制限には認めないため、背理法の適用範囲が古典論理よりも限定的になる場合があります。ただし、命題の否定 ¬P を証明するために、P を仮定して矛盾を導く推論（¬導入：(P→⊥)→¬P）は直観主義論理でも一般に認められます。
