# Double negation in sequent calculus

Kind of related to this post.

I wonder if it is possible to derive $$\Phi\vdash\Delta$$ from $$\lnot\lnot\Phi\vdash\Delta$$ using standard sequent calculus elimination rules. I am not sure where to start. Applying $$\lnot$$R rule to $$\lnot\lnot\Phi\vdash\Delta$$ will result in $$\vdash\Delta,\lnot\lnot\lnot\Phi$$, which makes the problem worse.

• What do you mean by elimination rule? Mar 2 at 6:04
• @Taroccoesbrocco sorry, I mean inference rules Mar 2 at 6:09

If $$\neg\neg \Phi \vdash \Delta$$ is derivable in the usual classical sequent calculus LK, then so is $$\Phi \vdash \Delta$$.
We know this because $$\Phi \vdash \neg\neg \Phi$$ is derivable simply by invoking $$\neg L$$ and $$\neg R$$ rules. With this we can just use
$$\frac{\Phi \vdash \neg\neg\Phi \:\:\: \neg\neg\Phi \vdash \Delta}{\Phi \vdash \Delta} \text{cut}$$
However, there is no single schematic derivation that has the conclusion $$\Phi \vdash \Delta$$ at its root, and proceeds upward through $$\neg\neg\Phi \vdash \Delta$$ without invoking the cut rule.
We know this because cut-free proofs have to satisfy the subformula property, and in general $$\neg\neg \Phi$$ need not be a subformula of $$\Phi, \Delta$$. For example, $$\bot \vdash \top$$ clearly has no cut-free proof in which the sequent $$\neg\neg \bot\vdash \top$$ makes an appearance.
• @RobArthan: Sure, and the question is whether it is a subformula of one of the formulas that occur in the sequent (the $\Phi,\Delta$); which it may be, e.g. if $\Delta$ is $\neg\neg\Phi$ itself. Mar 2 at 22:07