2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I don't think you can intuitionistically go from $\exists x A(x)\vee\exists x B(x)$ to $\exists x(A(x)\vee B(x))$; are you sure of that step? $\endgroup$ – Steven Stadnicki Feb 3 '15 at 2:43
  • $\begingroup$ @StevenStadnicki Although I did not claim such a step intuitionistically (the derivation in the first part is classical), the equivalence you've pointed out is indeed intuitionistically true in both directions. (Just note that $\exists x A\to\exists x(A\lor B)$ and $\exists x B\to\exists x(A\lor B)$, and in the reverse direction note that $(A\lor B)\to(\exists x A\lor\exists x B)$.) $\endgroup$ – Mario Carneiro Feb 3 '15 at 2:53
  • $\begingroup$ As models have always at least one element, $\forall x\,P(x)\implies\exists x\,P(x)$ is universally valid. (It would be false in the empty set.) But it is not a tautology. $\endgroup$ – Olórin Feb 3 '15 at 3:45
  • $\begingroup$ It seems to me that there are two problems : i) $p \rightarrow q \vdash \lnot p \lor q$ does not holds intuitionistically; ii) $\lnot \forall x P \vdash \exists x \lnot P$ does not holds intuitionistically. Are you able to prove it with Natural Deduction ? $\endgroup$ – Mauro ALLEGRANZA Feb 3 '15 at 8:29
  • $\begingroup$ @MauroALLEGRANZA Of course, assuming you mean the kind that is equivalent to classical logic, and of course not, if you mean intuitionistic natural deduction (because that would give me an answer to this question). I have no issue with viewing this as a deduction if you prefer to show it that way, the approaches are effectively equivalent. The weird part is that Kripke claims a completeness theorem for his model, so the proof above should show (non-constructively, possibly) that there is a proof of this statement in IL. $\endgroup$ – Mario Carneiro Feb 3 '15 at 16:32
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.