# proof of principle of explosion using natural deduction

That is, I am asked to prove the sequent $$A, \neg A \vdash B$$ using natural deduction.

The inference rules I am allowed to use are: reflexivity, +, $$\neg$$-elimination, $$\vee/\wedge/\to / \leftrightarrow$$ -introduction/elimination, see the image below for their definition.

I get stuck because I don't see how a new formula (in the case of the sequent $$A, \neg A \vdash B$$, the formula $$B$$) can be formed without being on the LHS of the turnstile $$\vdash$$.

• That essentially is the rule for $\neg$ elimination as I’ve seen it, unless you’re using some variant. What exactly is the $\neg$ elimination rule? Feb 2, 2022 at 5:54
• $\Sigma, \neg A \vdash B$ and $\Sigma, \neg A \vdash \neg B$, infer $\Sigma\vdash A$ Feb 2, 2022 at 6:02
• Oh, the rule you’re referring to is typically called proof by contradiction. Apply your rule with $\Sigma \to A, \neg A$; $A \to B$; and $B \to A$. Feb 2, 2022 at 6:12
• @MarkSaving - I am not totally sure to understand what you mean. Intuitively, you are right, but formally I don' t understand what you are suggesting. Do you use $\to$ for $\vdash$? What does ";" mean? Feb 2, 2022 at 16:55

According to the list of rules you posted here, it is possible to derive a sequent where a formula on the right-hand side of the turnstile $$\vdash$$ does not occur (not even as a subformula) on the left-hand side of $$\vdash$$. This is because of the rule $$\lnot_\text{elim}$$, which moves a formula from the left-hand side to the right-hand side of $$\vdash$$ (technically, this operation is called discharging), and of the rule $$+$$, which adds whatever formula on the left-hand side of $$\vdash$$.
The rules $$\lnot_\text{elim}$$ and $$+$$ are exactly the two rules needed to prove the principle of explosion! Indeed, a derivation of the sequent $$A, \lnot A \vdash B$$ is the following:
\begin{align} \dfrac{\dfrac{\dfrac{}{\dfrac{A \vdash A}{A, \lnot A \vdash A}+}{}^\text{refl}}{A, \lnot A, \lnot B \vdash A}+ \qquad \dfrac{\dfrac{}{\dfrac{\lnot A \vdash \lnot A}{A, \lnot A \vdash \lnot A}+}{}^\text{refl}}{A, \lnot A, \lnot B \vdash \lnot A}+}{A, \lnot A \vdash B}\lnot_\text{elim} \end{align}
The intuition is that the sequent $$A, \lnot A \vdash B$$ expresses the principle of explosion (aka ex falso quodlibet), that is, once a contradiction has been asserted ($$A, \lnot A$$), any proposition ($$B$$) can be inferred from it. Roughly, the principle of explosion can be considered as a "weak form" (or a consequence) of the proof by contradiction technique (aka reductio ad absurdum), which in your formal system is represented by the rule $$\lnot_\text{elim}$$. So, it is natural to use that inference rule to derive the sequent $$A, \lnot A \vdash B$$. The rules $$+$$ (aka weakening) are just needed to have the right premises for $$\lnot_\text{elim}$$.