proof of principle of explosion using natural deduction

523 Views Asked by At

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$.

enter image description here

1

There are 1 best solutions below

0
On

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}$.