Is the following argument valid in intuitionistic first-order logic? Let $P$ be a predicate, $R$ be a binary relation and $a, b, c$ be three individuals. We have the following premises:


*

*$P(a)$

*$\neg P(c)$

*$R(a, b)$

*$R(b, c)$


The statement $\exists x \exists y (R(x,y) \land P(x) \land \neg P(y))$ is a consequence of the four premises in classical first-order logic, as can be seen by the law of the excluded middle. However, in intuitionistic first-order logic,
we can no longer appeal to the law of the excluded middle. Is the argument still valid in intuitionistic first order logic, however?
I was motivated to ask this question by the following logic puzzle: "Persons A, B, and C are standing in a line. Person A is looking at Person B. Person B is looking at Person C. Person A is married. Person C is unmarried. Is a married person looking at an unmarried person? 1.Yes 2.No 3.Not enough information"
 A: No. Here's a countermodel. Let the poset be $\{w_0,w_1\}$ with $w_0<w_1$. Then let $\neg P(b)$ in world $w_0$ and $P(b)$ in world $w_1$. The only constraint that the Kripke semantics requires beyond $\exists x, y.R(x,y) \land P(x) \land \neg P(y)$ being true in all worlds is that for the chosen $y$, $P(y)$ is false in all worlds. So, while we have $$w_1\Vdash\exists x, y.R(x,y) \land P(x) \land \neg P(y)$$ by picking $x=b$ and $y=c$, we don't have $$w_0\Vdash\exists x, y.R(x,y) \land P(x) \land \neg P(y)$$ picking $x=a$ and $y=b$ since this would require $\neg P(b)$ in $w_1$ as well as in $w_0$. You can verify that any other choices for the existentially quantified variables won't work just as in the classical case.
A: Assume that every element is equal to either $a$, $b$ or $c$ and $a$, $b$, $c$ are all different. Now assume that $R(x,y)\land P(x)\land \lnot P(y)$ holds. Notice that our equality is decidable under our assumption and $x\neq c$, $y\neq a$.
Hence there are four possibilities: $(x,y) = (a,b),\, (a,c),\, (b,b),\, (b,c)$. We know that $x\neq y$ so $(x,y)$ can't be $(b,b)$. Therefore we have either 


*

*$R(a,c)$ (if $(x,y)=(a,c)$), 

*$\lnot P(b)$ (if $(x,y)=(a,b)$) or

*$P(b)$ (if $(x,y)=(b,c)$).


Therefore, if $R(a,c)$ fails then $P(b)\lor \lnot P(b)$, which is not pleasurable.

We can give a Kripke semantics which satisfies your assumption but not your conclusion. 
Consider the Kripke frame $P=\{p,q,r\}$ with order $\le$ such that $p<q$, $p<r$ and $q$ and $r$ are incomparable. Let define


*

*$M_p=M_q=M_r = \{a,b,c\}$,

*$P_p = P_q = \{a\}$, $P_r=\{a,b\}$ and

*$R_p = R_q = R_r = \{(a,b), (b,c)\}$.


Then we have $p\Vdash P(a)\land \lnot P(c)\land R(a,b)\land R(b,c)$. However $p \not\Vdash P(b)\lor \lnot P(b)$ and $p\Vdash \lnot R(a,c)$. Hence by my above argument we have $p$ does not force your statement.
A: I see.   Indeed $\neg P(b)\vee P(b)$ and the premises would infer $\big(R(a,b)\wedge P(a)\wedge \neg P(b)\big)$ $\lor$ $\big(R(b,c)\wedge P(b)\wedge \neg P(c)\big)$, and thus $\exists x~\exists y~(R(x,y)\wedge P(x)\wedge\neg P(y))$.
But no, it does not look like you can get there without accepting the Law of Excluded Middle.
