I have a question regarding First Order Logic. I have to express the property "x is a Prime" in First Order logic. So far I have the following solution:
$\forall x\;Prime(x) \leftrightarrow \neg \exists y, z \;y \times z = x \land (y > 1 \land z > 1)$
I think that it is right but I am not 100% sure. My reason for putting a bidirectional there is that
$\forall x\;\neg \exists y,z\;y \times z = x \land (y > 1 \land z > 1) \to Prime(x)$
is also true. But it feels weird as we mostly use $\to$ with a universal quantifier.
Same goes for the formula:
$\forall x\;Even(x) \leftrightarrow \exists y\;y + y = x$ (x is even)
EDIT
After thinking a lot about it again and taking into account the comments below, I came up with this:
PROBABLY RIGHT:
$\forall x\; Prime(x) \leftrightarrow x \neq 0 \land x \neq 1 \land \neg \exists y, z [(y \times z = x) \land y \neq x \land z \neq x]$ P.S.
One has to be careful here. To express that $x$ is even, simply use $$\tag1 \exists y\; y+y=x.$$ This allows us to extend the language by a unary predicate $\operatorname{even}(x)$, which we define thus: $$ \operatorname{even}(x)\ :\leftrightarrow\ \exists y\; y+y=x$$ (or possibly with other symbols such as $\equiv$, but it should at least be distinguished from the biconditional), by which we can eliminate $\operatorname{even}()$ from any statement, and which makes $$\tag2\forall x \operatorname{even}(x)\leftrightarrow\exists y\; y+y=x$$ (somewhat trivially) true. So to repeat, the statement that $x$ is even is not expressed by $(2)$, but rather by $(1)$.
That being said, your definition of $\operatorname{Prime}(x)$ would make $1$ and $0$ primes, so you should also double check the condition itself.