# Sequent calculus, how to prove double negation introduction and conjunction

I want to prove double negation introduction in sequent calculus using the most basic rule set.

That is what I want to prove: from the sequent $$\Gamma \rightarrow\Phi,$$ the sequent $$\Gamma \rightarrow\neg\neg\Phi$$ is derivable.

How is this accomplished? It's seems much more difficult than in natural deduction. I think I may be able to prove the conjunction myself once I have this result.

• Do you have the negation sign as primitive or it is defined in terms of $\supset$ and $\bot$ ? – Mauro ALLEGRANZA Feb 13 '17 at 8:18

With $\lnot$ as primitive, we have to use $\text {L-} \lnot$ followed by : $\text {R-} \lnot$:
With $\lnot A$ defined as $A \supset \bot$, we have to use $\text {L-} \supset$ followed by : $\text {R-} \supset$: