# $(\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.

1. 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?
2. 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

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.