Sequent calculus, how to prove double negation introduction and conjunction

Question

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.

Answer 1

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

\begin{align} {\cfrac{{\cfrac{\Gamma \to \Delta, A }{\lnot A, \Gamma \to \Delta} \text {L-} \lnot}}{\Gamma \to \Delta, \lnot \lnot A }\text {R-} \lnot} \end{align}

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

\begin{align} {\cfrac{\cfrac{{\cfrac{\Gamma \to \Delta, A \quad \quad \bot, \Gamma \to \Delta }{A \supset \bot, \Gamma \to \Delta} \text {L-} \supset}}{A \supset \bot, \Gamma \to \Delta, \bot}\text {R-W}}{\Gamma \to \Delta, (A \supset \bot) \supset \bot }\text {R-} \supset} \end{align}

Note : the top-right sequent is:

\begin{align} {\cfrac{ }{\bot, \Gamma \to \Delta} \text {L-} \bot} \end{align}