Statement of "proof by contradiction"

Question

Wikipedia states:

In mathematical logic, the proof by contradiction is represented as "if $S \cup \{ P \} \vdash \mathbb{F}$ then $S \vdash \neg P$" or "if $S \cup \{ \neg P \} \vdash \mathbb{F}$ then $S \vdash P$".

Is it true? Are the two really the same? I think it is impossible for one to deduce the "law of excluded middle" from the the second representation, but possible to do so using the first. Am I wrong?

Law of excluded middle states that "Everything is either true or false". I know how to use the first statement of RAA (proof by contradiction) to prove this law, but is it possible to do so using the second statement?

Why I claim it to be impossible, you ask? Because in the natural system of deduction, RAA is the only way to introduce a $\neg$ to the right-hand side. Replacing the first form, with the second, I see no way of introducing $\neg$ to right-hand side.

Answer 1

The two formulations are easily equivalent if $\vdash \neg\neg P\leftrightarrow P$, as is the case in classical logic but not in intuitionistic logic.

In intuitionistic logic they are not the same. Indeed, the inference $$ \tag{1} \frac{S,P\vdash \bot}{S\vdash \neg P}$$ is intuitionistically valid (and is the canonical way of establishing $\neg P$ intuitionistically), whereas $$ \tag{2} \frac{S,\neg P\vdash \bot}{S\vdash P} $$ is not intuitionistically valid. Adding the latter rule to intuitionistic logic will produce classical logic.

The law of excluded middle is, of course, another example of something that is classically but not intuitionistically valid. Therefore it cannot be proved using only (1) (and other intuitionistically valid rules).

The law of excluded middle can be proved using (2) -- namely, $\neg(A\lor \neg A)\vdash \bot$ is intuitionistically valid, and one application of (2) will then conclude $A\lor \neg A$.

To reach a contradiction from $\neg(A\lor \neg A)$, use the fact that $\neg(P\lor Q)\vdash \neg P$ intuitionistically to conclude first $\neg A$ and then $\neg\neg A$, which contradict each other.

Answer 2

The "common" approach to intuitionistic and classical logic with Natural Deduction is to assume $\bot$ (the falsum) as primitive and define $\lnot A$ as an abbreviation for $A \to \bot$.

In this way, from the rules for $\to$ :

$$\frac {A \, \, A \to B} B \, \, (\to E)$$

$$\frac {A \vdash B} {A \to B} \, \, (\to I)$$

we can derive the rules for $\lnot$ :

$$\frac {A \, \, \lnot A } \bot \, \, (\lnot E)$$

$$\frac {A \vdash \bot} {\lnot A} \, \, (\lnot I)$$

Up to now, the rules are both classicaly and intuitionistically valid.

In addition, classical logic adds one more rule :

$$\frac {\lnot A \vdash \bot } A$$

called Double negation, or Rule of indirect proof or Reductio ad absurdum.

With it, we can prove Excluded Middle :

$$\frac { } {\lnot A \lor A}$$

---

Proof of : $A \lor \lnot A$.

1) $A$ --- assumed [a]

2) $A \lor \lnot A$ --- from 1) by $\lor$-I

3) $\lnot (A \lor \lnot A)$ --- assumed [b]

4) $\bot$ --- from 2) and 3) by $\lnot$-E

5) $\lnot A$ --- from 1) and 4) by $\lnot$-I, discharging assumption [a]

6) $A \lor \lnot A$ --- from 5) by $\lor$-I

7) $\bot$ --- from 3) and 6) by $\lnot$-E

8) $A \lor \lnot A$ --- from 3) and 7) by DN, discharging [b] : this is the crucial step that is intuitionistically not valid.