A question about intuitionistic logic

Question

I find it hard to understand the following formula in intuitionistic logic, where $P\neq\perp$ and $P\not\leftrightarrow(\neg\neg\exists xQ(x)\rightarrow\exists xQ(x))$: $$P\rightarrow(\neg\neg\exists xQ(x)\rightarrow\exists xQ(x))\quad\quad(*)$$ Intuitively, it says that from $P$, infer $\neg\neg\exists xQ(x)\rightarrow\exists Q(x)$. Clearly, the consequent $\neg\neg\exists xQ(x)\rightarrow\exists xQ(x)$ does not hold in intuitionistic logic. So, my question is under what conditions, this formula is true. The only way I can come up with is that $(*)$ holds if $P\rightarrow\exists xQ(x)$. But is that the only way to derive $(*)$? If that's the only way, can we infer $P\rightarrow\exists xQ(x)$ from $(*)$? This looks quite odd. So, is there any other way to derive $(*)$ and what can we infer from $(*)$? Thanks in advance!

Answer 1

We definitely do not need $P \to \exists x Q(x)$ for this. For example, we could have that $P$ is $R \wedge (\neg \neg \exists x Q(x) \to \exists x Q(x))$, where $R$ is some new propositional symbol. So $(*)$ trivially holds. Then it is easy to see that $P \to \exists x Q(x)$ cannot be derived from $(*)$. Just consider a model where $R$ is true and $\forall x \neg Q(x)$ holds.

I do not think we can say much more in general than that. Because in the above example, once we would also add the axiom that $R$ is always true, we just get that $P$ is equivalent to $\neg \neg \exists x Q(x) \to \exists x Q(x)$ and $R$ has no real function. So no information is gained from $(*)$.