1
$\begingroup$

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

$\endgroup$
4
  • 2
    $\begingroup$ 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? $\endgroup$ Feb 2, 2022 at 5:54
  • $\begingroup$ $\Sigma, \neg A \vdash B$ and $\Sigma, \neg A \vdash \neg B$, infer $\Sigma\vdash A$ $\endgroup$
    – KOMAX233
    Feb 2, 2022 at 6:02
  • 1
    $\begingroup$ 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$. $\endgroup$ Feb 2, 2022 at 6:12
  • $\begingroup$ @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? $\endgroup$ Feb 2, 2022 at 16:55

1 Answer 1

4
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .