1
$\begingroup$

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.

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

1 Answer 1

4
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ @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. $\endgroup$
    – Z. A. K.
    Mar 2 at 22:07
  • $\begingroup$ Whoops! I misread your answer. I'll hoover up my spurious comment. $\endgroup$
    – Rob Arthan
    Mar 2 at 23:42

You must log in to answer this question.

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