Statement of “proof by contradiction”

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.

• The second version is non-constructive, yes. I mean this point is adressed at the bottom of the Wikipedia subsection you quoted from, here. – Nikolaj-K Feb 20 '15 at 12:40
• The two are equivalent from the point of view of classical logic, where the Law of Double Negation : $\lnot \lnot P \vdash P$ holds. In intuitionistic logic where it does not hold, the two rules are nor more equivalent. – Mauro ALLEGRANZA Feb 20 '15 at 12:42
• So, you guys would agree that using the second one instead of the first makes the system incomplete, unless law of double negation is taken as a rule. Right? – Untitled Feb 20 '15 at 12:45
• What you can say for the second statement works just like the first $S \cup \{ (\neg P) \} \vdash \mathbb{F}$ then $S\vdash \lnot (\lnot P)$. Then, if you accept double negation, $\lnot \lnot P \equiv P$. If not, we conclude simply $\lnot (\lnot P)$. – Namaste Feb 20 '15 at 12:53
• Yes, incomplete according to the "standard" classical semantics (truth-tables)... Double Negation and Law of Excluded Middle are equivalent, and thus both are rejected in intuitionistic logic. – Mauro ALLEGRANZA Feb 20 '15 at 12:54

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.

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.