What lets the Square of Opposition fail in Intuitionistic Logic? See moderator's note in the comments.
I just came across the following. In intuitionistic logic
and classical logic we have the following consequences:
∃x¬φ → ¬∀xφ  
∀x¬φ → ¬∃xφ  
¬∃xφ → ∀x¬φ

But the following consequence is only generally valid
in classical logic but not in intuitionistic logic:
¬∀xφ → ∃x¬φ                         (Q)

Are there intermediate logics where the last consequence
doesn't fail? I mean a logic where φ v ¬φ doesn't hold
in general but (Q) does.
Bye
 A: As Emil pointed out in a comment, the answer to this question will depend on what else is available in your intuitionistic logic.  If that background logic is strong enough, then (Q) will imply the law of the excluded middle.  Specifically, suppose we're working in a higher-order intuitionistic logic (also called intuitionistic type theory) such as arises as the internal logic of topoi, and suppose we adjoin (Q) as a general principle, i.e., with arbitrary formulas $\phi$ and with the variable $x$ ranging over an arbitrary type.  Then we get classical logic, in the form $(\neg\neg\alpha)\to\alpha$ (which is known to imply the law of the excluded middle) as follows.  
Given $\alpha$, let $A=\{x\in1:\alpha\}$.  That is, $A$ is the subset of the singleton 1 that contains the unique element of 1 iff $\alpha$ is true.  Then, for any formula $\phi$, we have that $(\exists x\in A)\,\phi$ is equivalent to $\alpha\land\phi$ and that $(\forall x\in A)\,\phi$ is equivalent to $\alpha\to\phi$.  In particular, if we apply (Q) with $\bot$ (the always false proposition) in the role of $\phi$ and with the quantifiers ranging over $A$, then the left side of (Q) is equivalent to $\neg(\alpha\to\bot)$ and thus to $\neg\neg\alpha$, while the right side of $Q$ becomes equivalent to $\alpha\land\neg\bot$ and thus to $\alpha$.  So this particular instantiation of (Q) says $(\neg\neg\alpha)\to\alpha$.
A: I'm not sure if there's a system short of classical logic where (Q) holds for all formulas, however the principle
$$\forall x(\phi\vee\neg\phi)\rightarrow(\neg \forall x\neg\phi\rightarrow\exists x\phi)$$
(or sometimes
$$\forall x(\phi\vee\neg\phi)\rightarrow(\neg \neg\exists x\phi\rightarrow\exists x\phi)$$
instead)
is Markov's principle, and there's a great deal of work on constructive logics with Markov's principle.
