Intuitionistic proof of $(\exists x P(x)\to\exists x Q(x))\to\exists x(P(x)\to Q(x))$

Question

This one is throwing me for a loop. My gut tells me that this isn't intuitionistically valid, although it is classically valid, since you have

$$\forall x\,P(x)\implies\exists x\,P(x)$$ \begin{align} (\exists x\,P(x)\to\exists x\,Q(x))\implies&(\forall x\,P(x)\to\exists x\,Q(x))\\ \iff&(\exists x\,\neg P(x)\vee\exists x\,Q(x))\\ \iff&\exists x\,(\neg P(x)\vee Q(x))\\ \iff&\exists x\,(P(x)\to Q(x)). \end{align}

But the Kripke semantics seem to work out, since the provability of the statement in a world $u$ under the arbitrary assignment $e$ is defined as

$$u\Vdash((\exists x P(x)\to\exists x Q(x))\to\exists x(P(x)\to Q(x))[e]$$ $$\forall w\ge u\,(\forall t\ge w\,((t\Vdash\exists x P(x)[e])\to(t\Vdash\exists x Q(x)[e]))\to(w\Vdash\exists x(P(x)\to Q(x))[e]))$$ $$\forall w\ge u\,(\forall t\ge w\,(\exists x\in M_t\,P(x)\to\exists x\in M_t\,Q(x))\to\exists x\in M_w\,(P(x)\to Q(x)))$$

and setting $t=w$ on the left yields $$(\exists x\in M_w\,P(x)\to\exists x\in M_w\,Q(x))\to\exists x\in M_w\,(P(x)\to Q(x))$$ which (since this expression is in classical logic) is the same theorem as proven above.

Regarding proof avenues, the only simplification I can see turns the original expression into $\forall x\,(P(x)\to\exists x\,Q(x))\to\exists x\,(P(x)\to Q(x))$, after which none of the quantifiers are in a good position to admit additional simplification.

Answer 1

The evaluation of the Kripke model was done incorrectly. The last line was

$$\forall w\ge u\,(\forall t\ge w\,(\exists x\in M_t\,P_t(x)\to\exists x\in M_t\,Q_t(x))\to\exists x\in M_w\,(P_w(x)\to Q_w(x)))$$

when it should be

$$\forall w\ge u\,(\forall t\ge w\,(\exists x\in M_t\,P_t(x)\to\exists x\in M_t\,Q_t(x))\to\exists x\in M_w\,\forall t\ge w\,(P_t(x)\to Q_t(x)))$$

because implication is evaluated in all reachable worlds. Since the functions $P_w(x)$ on different worlds $w$ are truth-preserving but not falsity-preserving (i.e. they satisfy $u\le w\to(P_u(x)\to P_w(x))$, not $u\le w\to(P_u(x)\leftrightarrow P_w(x))$), $\forall t\ge w\,(P_t(x)\to Q_t(x))$ and $(P_w(x)\to Q_w(x))$ are not equivalent. From this fact it is not hard to come up with a counterexample:

There are two frames, $w$ and $u$ with $w<u$.

In $w$ the universe is $\{\mathtt a\}$ and all predicates are false.

In $u$ the universe is $\{\mathtt a,\mathtt b\}$, and $P(\mathtt a)$ and $Q(\mathtt b)$ are true.

Then both frames satisfy $(\exists x\,P(x)\to\exists x\,Q(x))$. But $\exists x\,(P(x)\to Q(x))$ is false in $w$, because it can only be true if $P(\mathtt a)\to Q(\mathtt a)$ is true in all worlds accessible from $w$, and it is false in $u$. Thus the original statement is not intuitionistically valid.

Answer 2

I'm quite sure it doesn't hold intuitionistically. Imagine the Heyting algebra containing $\bot$, $\top$ and four other elements, namely two incomparable elements $V$ and $M$ together with $V \wedge M$ and $V \vee M$. Assume a universe of discourse with precisely two elements $a$ and $b$, and let the truth value of $P(a)$ and $P(b)$ be $V \vee M$, while letting the truth value of $Q(a)$ be $V$ and the truth value of $Q(b)$ be $M$. Then in that model the truth value of $\exists{x} P(x) \rightarrow \exists{x} Q(x)$ is the truth value of $V \vee M \rightarrow V \vee M$, i.e., $\top$. On the other hand, there the truth value of $\exists x(P(x) \rightarrow Q(x))$ is the truth value of $((V \vee M) \rightarrow M) \vee ((V \vee M) \rightarrow V)$, which is the truth value $V \vee M$.

The Heyting algebra I mention is actually important, I think, as the algebra of truth values if you want to allow both assertable, very silly atomic statements (corresponding to V) and unassertable, moderately silly atomic statements (corresponding to M), as I am doing in my research. If you throw away the truth value $\bot$ from the six-element Heyting algebra I mentioned (so $V \wedge M$ becomes the smallest element), you'd get a five-element Heyting algebra that also would work to give a counterexample, but the latter mostly seems less natural to me.