Proof negation in Gentzen system

Question

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →):

$${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] {\Gamma,\varphi\vdash\Delta\over \Gamma\vdash\Delta\lnot\varphi}\ R\lnot $$

I’m trying to proof:

$${\Gamma,\lnot\lnot q\vdash\Delta\over \Gamma,q\vdash \Delta}$$

However, I did not manage to this with the provided rules.

Does anyone have an idea of how to start? Are there any other rule for negation in the Gentzen system that could be used here?

Answer 1

We start a left branch with :

$$\frac{A \vdash A}{\lnot A, A \vdash}$$ by $\lnot$-left;

then :

$$\frac{\lnot A, A \vdash}{A \vdash \lnot \lnot A}$$ by $\lnot$-right.

Now we apply the Cut rule (where the cut-formula $\psi$ is $\lnot \lnot A$ ) :

$$\frac {A \vdash \lnot \lnot A \quad \quad \Gamma, \lnot \lnot A \vdash \Delta } {\Gamma, A \vdash \Delta }$$

If we "merge" the derivation from the Axiom of the left top sequent, we obtain the "derived rule" :

$$\frac {\Gamma, \lnot \lnot A \vdash \Delta } {\Gamma, A \vdash \Delta }$$