※素の直観主義論理が前提です。
nLab の double-negation shift に排中律との等価性が述べられています。
これに関して、命題の量化等を許して確認してみます。
$$ (\forall x. \lnot \lnot Q(x)) \implies \lnot \lnot \forall x. Q(x) $$
これは直観主義論理とは独立した命題だそうです。
二重否定のことを"反証不可能"と読むことにすると、『任意の$x$について、$Q(x)$が反証不可能であるならば、「すべての$x$について、$Q(x)$が構成的に実証可能である」は反証不可能である』と読めます。
直観主義論理ではこれが成り立つとは限らないということは、無限領域の量化で反証不可能性を実証可能性に昇華するのは論理の飛躍がある、少なくとも反証の余地があるということでしょう。
どのような反証の余地があるのかは、排中律と比較すると分かりやすくなります。
$$ \lnot \lnot (\forall P. P \lor \lnot P) \implies (\forall Q. ((\forall x. \lnot \lnot Q(x) ) \implies \lnot \lnot \forall x. Q(x) ) ) $$
$$ \lnot \lnot (\forall P. P \lor \lnot P) \tag{A} $$
が成り立ち、任意の$Q$について
$$ \forall x. \lnot \lnot Q(x) \tag{B} $$
が成り立つときに
$$ \lnot \forall x. Q(x) \tag{C} $$
の成立を仮定して矛盾を導けばよい。
つまり、$(A), (B), (C)$の仮定の下で
$$ \forall P. P \lor \lnot P \tag{D} $$
を仮定して
$$ \forall x. Q(x) \tag{E} $$
が成り立つことを示せばよい。
※$(D)$の仮定の下で$(E)$が成り立つとき、これは$(C)$に矛盾する。したがって$\lnot (D)$であるが、これは$(A)$に矛盾する。
排中律と二重否定の除去規則は同値であるので、$(D)$により、
$$ \forall P. \lnot \lnot P \implies P \tag{F} $$
が成り立つ。
最後に、$(B), (F)$の仮定の下で$(E)$が成り立つことを示す。
$(B)$により、すべての$x$に対して$\lnot \lnot Q(x)$が成り立つ。
このとき、$(F)$により$Q(x)$が成り立つ。つまり$(E)$が成り立つ。$\square$
こちらは二重否定シフトの階層を1段階挙げる必要があります。
（この意味で二重否定シフトと排中律の二重否定が"同値"であるとは言いづらい）
$$ (\forall \mathcal{F}. ((\forall P. \lnot \lnot \mathcal{F}(P)) \implies \lnot \lnot \forall P. \mathcal{F}(P))) \implies \lnot \lnot (\forall P. P \lor \lnot P) $$
任意の$\mathcal{F}$について
$$ (\forall P. \lnot \lnot \mathcal{F}(P)) \implies \lnot \lnot \forall P. \mathcal{F}(P) \tag{A} $$
が成り立つときに
$$ \lnot (\forall P. P \lor \lnot P) \tag{B} $$
の成立を仮定して矛盾を導けばよい。
ここで$\mathcal{F}$は任意なので
$$ \mathcal{F}(P) = P \lor \lnot P $$
とすると、$(A)$は
$$ (\forall P. \lnot \lnot (P \lor \lnot P)) \implies \lnot \lnot \forall P. P \lor \lnot P $$
となる。
ここで、$\forall P. \lnot \lnot (P \lor \lnot P)$は直観主義論理でも成り立つので、$\lnot \lnot \forall P. P \lor \lnot P$も成り立つ。
しかし、これは$(B)$に矛盾する。$\square$