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
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.