1
$\begingroup$

Which natural deduction rule allows to derive any consequence from a contradiction in a conditional proof?

enter image description here

$\endgroup$
4
  • 1
    $\begingroup$ You've asked several questions about formal logic proofs and yet your proofs always follow some 'home-made' format ... I would highly recommend using some software for this; they typically have built-in checking, and so you learn the rules really quickly! Search for the Open Logic Project $\endgroup$ – Bram28 Jan 2 '20 at 19:25
  • 2
    $\begingroup$ Here is a pretty nice online Fitch-based interface $\endgroup$ – Bram28 Jan 2 '20 at 19:52
  • 1
    $\begingroup$ Alternatively, this one $\endgroup$ – Quelklef Jan 3 '20 at 3:49
  • $\begingroup$ Contradiction Elimination. You can deduce anything from a contradiction. $\endgroup$ – Adrian Keister Feb 24 '20 at 14:59
7
$\begingroup$

It is the principle of explosion, also known as ex falso quodlibert: from contradiction, anything follows.

In natural deduction, it says that if $\mathcal{D}$ is a derivation with conclusion $\bot$ then, for every formula $\varphi$, $$\dfrac{\genfrac{}{}{0pt}{}{\ \ \vdots \mathcal{D}}{\bot}}{\varphi}\scriptstyle\text{efq}$$ is a derivation with conclusion $\varphi$ and the same hypotheses as $\mathcal{D}$. For a reference, see here (p. 3)


Note that this rule can be used everywhere (not only in a conditional proof). Moreover, unlike the principle of reductio ad absurdum, ex falso quodlibet is accepted not only in classical logic but also in more constructive logics such as intuitionistic logic.

$\endgroup$
3
$\begingroup$

In a typical Fitch system, this is the rule of $\bot \text{Elim}$:

$$\bot$$

$$\therefore \varphi$$

Here, by the way, is your whole proof in Fitch:

enter image description here

$\endgroup$