As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $\exists x:P(x)$ only by constructing an explicit such object $x$, right? So for instance one can't do this:
first assume that $\exists x: P(x)$ is false, then this leads to …, which is a contradiction; therefore $\exists x: P(x)$.
Having this main idea of constructive logic in mind I would define constructive logic (= intuitionistic logic?) to be logic without the rule $\neg\neg\exists x P(x)\implies\exists xP(x)$. But this seems to contradict the slogan "constructive logic is classical logic without law of excluded middle (and therefore – because these two happen to be equivalent – without double negation elimination)". I'm assuming this is the "correct" definition of constructive logic. So constructive logic is classical logic without $\neg\neg A\implies A$.
My question is already in the title: How strong is classical logic without $\neg\neg\exists x P(x)\implies\exists xP(x)$? Is it strictly stronger than constructive logic; and is it strictly weaker than classical logic?
Another question I have is this (but it's quite "soft"): Why does one define constructive logic as the logic without $\neg\neg A\implies A$ rather than logic without $\neg\neg\exists x P(x)\implies\exists xP(x)$? Isn't using the rule $\neg\neg A\implies A$ for an existential $A$ what makes a proof non-constructive?
As said in the comments section, in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" the statement "$¬¬A ⟹ A$" where $A$ is $(∃xP(x))∨(Q∧¬Q)$ ($Q$ can be any statement, such as $∃x.x=x$) is still true. Now if $¬¬∃xP(x)$ then $¬¬((∃xP(x))∨(Q∧¬Q))$; because if $¬((∃xP(x))∨(Q∧¬Q))$, then $¬(∃xP(x))$. Also, if $(∃xP(x))∨(Q∧¬Q)$, then by case analysis $∃xP(x)$.
Thus we have proven in "logic without $¬¬∃xP(x) ⟹ ∃xP(x)$" that $¬¬∃xP(x) ⟹ ∃xP(x)$. Therefore, this logic is equivalent to classical logic.