Is this formula provable in intuitionistic first-order logic? I know that in classical first-order logic, the formula $(\exists x)( \exists y) x \neq y \rightarrow (\forall x)(\exists y) x \neq y$ is a theorem. Is it also a theorem of intuitionistic first-order logic? If so, what is the proof? I am asking because to prove the theorem in classical logic, you have to do a proof by cases of an excluded middle disjunction, that is, a disjunction of a formula with its negation.
 A: It is not provable.
Given a proposition $P$, form the set generated by three elements $a,b,c$ such that $P → a = b$ and $¬P → a = c$. Call it $Q$.
It is still the case that $b \neq c$, so $∃x \in Q. ∃y \in Q. x \neq y$.
Now, instantiate $∀x. ∃y. x \neq y$ with $x = a$:

*

*$y$ can't be $a$, obviously

*If $y = b$, then we can conclude $¬P$, because $P → a = b$

*If $y = c$, then we can conclude $¬¬P$, because $¬P → a = c$
So, the conclusion allows us to deduce $¬P ∨ ¬¬P$, for an arbitrary $P$, which is not an intuitionistic theorem.
Here is a computer formalization of the argument.
A: For a concrete model in which the statement does not hold, consider the poset category consisting of elements $0,1,1'$ where $0 \le 1$ and $0 \le 1'$:
  /->  1
0
  \->  1'

We will now form a presheaf $F$ of sets on this category: $F(0) := \{ a, b, c \}$, $F(1) := \{ a, b \}$, $F(1') := \{ a, b \}$.  The restriction maps (other than the trivial ones on identity morphisms) will be $F(0\to 1) : a \mapsto a, b \mapsto b, c \mapsto a$ and $F(0\to 1') : a \mapsto a, b \mapsto b, c \mapsto b$.
If you trace through the definitions, then you see $0 \Vdash a \ne b$, so $0 \Vdash (\exists x) (\exists y) x\ne y$.  However, $1 \Vdash a = a$, so $0 \not\Vdash c \ne a$; and similarly, $1' \Vdash b = b$, so $0\not\Vdash c \ne b$.  And clearly, $0\not\Vdash c\ne c$.  Therefore, $0 \not\Vdash (\exists y) c\ne y$, so $0 \not\Vdash (\forall x) (\exists y) x \ne y$.
(If I understand correctly, this is technically not quite a Kripke frame, since Kripke frames require the restriction maps to be inclusion maps.  It is fairly close to a Kripke frame, though, which is why I felt comfortable using the notation from the theory.)
