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