Translation to predicate logic

Question

We have a statement to be translated into first order logic (not caring whether it is true or false in the real world):
There does not exist an even prime number which is the square of a prime number.

I have trouble translating this sentence to first order logic. These were my steps:

$\forall y \neg \exists x ((prime(2*x) \land prime(y)) \implies (2*x=y*y))$
So, for all prime numbers y, there does not exist an even prime number that is equal to the square of the prime number y. So far, it should be correct.

$\forall y \neg \exists x (\neg(prime(2*x) \land prime(y)) \lor (2*x=y*y))$
Using laws for implication transformation, I changed the expression.

$\forall y \neg \exists x (\neg prime(2*x) \lor \neg prime(y) \lor (2*x=y*y))$
Using De Morgan laws, I changed the expression again.

Now, I can change the negation of "there exist" to "for all" by negating the inside of the brackets:
$\forall y \forall x (prime(2*x) \land prime(y) \land \neg (2*x=y*y))$

This, however, is not correct, but I can't find the mistake in my reasoning. I would really appreciate if someone could point me the right way. Thank you.

Answer 1

There does not exist an even prime number which is the square of a prime number.

First we should clarify what is meant by "even prime number". Below are two possible predicate definitions:

1. $\mbox{evenPrime}(x)\equiv x=2$
2. $\mbox{evenPrime}(x)\equiv (2\mid x\land\mbox{prime}(0.5 x))\lor x=2$

So now we can translate the above statement as the following $$\forall x\lnot\exists y(\mbox{evenPrime}(y)\land \mbox{prime}(x)\land y=x^2)$$ If you apply the first definition of $\mbox{evenPrime}$, then the statement is true.

If you apply the second definition of $\mbox{evenPrime}$, then the statement is false.