# If the move is correct, which rule allows to go from line 4 to line 5 of this derivation? ( a question on the use of “ falsum” in natural deduction) [closed]

Which natural deduction rule allows to derive any consequence from a contradiction in a conditional proof? • 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 – Bram28 Jan 2 '20 at 19:25
• Here is a pretty nice online Fitch-based interface – Bram28 Jan 2 '20 at 19:52
• Alternatively, this one – Quelklef Jan 3 '20 at 3:49
• Contradiction Elimination. You can deduce anything from a contradiction. – Adrian Keister Feb 24 '20 at 14:59

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.

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: 