$(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$ Consider the logical formula $(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$ where x does not appear free in p. 
This formula is not derivable in intuitionistic logic, but it is in classical logic.


*

*What kind of logical system do we get if we add this formula to intuitionistic logic? In particular, how far do we land from classical logic?

*Any intuition on why this benign looking formula is not derivable in a constructive logic?
Thanks for any answers and pointers to the literature.


JL Lenard
 A: The answer to your first question depends on what sort of domain the variable $x$ can range over.  Here's a specific answer in the most generous case, where we're dealing with the intuitionistic internal logic of topoi (also known as intuitionistic type theory).  In this situation, your benign-looking formula implies the law of the excluded middle, so it brings us all the way to classical logic.  To see this, consider an arbitrary proposition $p$.  Form a subset $S$ of a one-element set $\{a\}$ by  putting $a$ into $S$ if and only if $p$.  Let $q(x)$ be the identically false predicate on this set $S$, and, accordingly, let the variable $x$ in your formula range over $S$.  Then the antecedent in your formula, $(\forall x)\,(p\lor q(x))$, is true, because if there's any $x$ at all (in $S$ of course), then $p$ is true.  So your formula would allow me to infer that $p\lor(\forall x)\,q(x)$.  But $(\forall x)\,q(x)$ says (since $q(x)$ is simply false) that there isn't any $x$ (in $S$, of course), which means, by definition of $S$, that $p$ is false.  So we get that $p$ is true or false.  
I don't know how strong your formula would be in a weaker context than type theory.  It can fail in a two-world Kripke model, but that requires having the domain over which $x$ ranges change from the one world to the other.  Kripke models with constant domain always satisfy your formula (unless I've made a mistake).
Either the two-world Kripke model or the proof in the first paragraph above suggests the following intuition for what's going on.  Suppose $p$ is a proposition that hasn't yet been proved or disproved (say, Goldbach's conjecture).  The assumption, $(\forall x)\,(p\lor q(x))$, requires $q(x)$ to be true for all $x$'s as long as $p$ remains unproved.  For all these $x$'s, $q(x)$ will remain true, even if somebody proves $p$.  But, when and if $p$ gets proved, a new element might enter the domain (over which $x$ ranges) and $q$ might not hold for this new element.  $(\forall x)\,(p\lor q(x))$ would still be correct, because the counterexample for $q(x)$ appeared only when $p$ became true.  But we can't assert $p\lor(\forall x)\,q(x)$ because the first disjunct is justified only when $p$ is proved and the second only if we know that no counterexample to $q(x)$ will ever appear.  If we don't know whether $p$ will be proved or not, then we can't assert either disjunct, so we (being intuitionists) can't assert the disjunction.
