Is $\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$ intuitionistic derviable?

Question

Is the following a rule which is derivable in intuitionistic logic:

$\neg \neg \forall \neg \neg A \leftrightarrow \forall \neg \neg A$

I thought that I read it somewhere,... hope that someone can help me.

Thank you in advance.

Answer 1

The right to left is trivial, because $p \to \lnot \lnot p$ holds intuitionistically.

For the left to right:

1) $\lnot \lnot \forall x \lnot \lnot A$ --- premise

2) $\lnot A$ --- assumed [a]

3) $\forall x \lnot \lnot A$ --- assumed [b]

4) $\lnot \lnot A$ --- from 3) by $\forall$-elim

5) $\bot$ --- from 2) and 4) by $\to$-elim

6) $\lnot \forall x \lnot \lnot A$ --- from 3) by $\to$-intro, discharging [b]

7) $\bot$ --- from 1) and 6) by $\to$-elim

8) $\lnot \lnot A$ --- from 2) and 7) by $\to$-intro, discharging [a]

9) $\forall x \lnot \lnot A$ --- from 8) by $\forall$-intro.