Show that for propositional logic $\vdash_i \neg \varphi \Leftrightarrow \vdash_c \neg \varphi$.

Question

As the title says, where $\vdash_i$ is derivations in Intuitionistic logic and $\vdash_c$ is derivations in Classical logic.

I am allowed to use a corollary that states that $\vdash_i \varphi \Leftrightarrow \vdash_c \varphi$ holds for all negative formulas, i.e. those which have all their atoms negated and contain only the connectives $\bot, \wedge, \vee, \to, \leftrightarrow$. I am also allowed to use Glivenko’s theorem. The problem is from van Dalen’s Logic and Structure.

I’m allowed to use elimination and introduction rules for all the above connectives, but I’m not allowed to used RAA (reductio) for the Intuitionistic derivations. Gentzen style derivations.

The problem is that I can’t quite see how to get started. I would appreciate some hints. Please don’t give me the full answer though, I’d like to find that on my own. Thanks!

Answer 1

By Glivenko's Th (6.2.10):

$⊢_c \varphi \ ⇔ \ ⊢_i ¬¬ \varphi$.

The result follows proving (by Natural Deduction) the intuitionistically valid:

$⊢_i ¬ \varphi ↔ ¬¬¬ \varphi$.