# First order logic FOL translation help!

I am allowed to use Prime$$(x)$$ and Even$$(x)$$, and quantifiers. I just wanted to make sure if I'm on the right track.

1. There is no greatest number: $$\forall x \exists y(x

2. Any number added to itself is even: $$\forall x \mathrm{Even}(x+x)$$

3. Every even number is the sum of two primes numbers: $$\forall x (\mathrm{Even}(x)) ⟹ \exists y \exists z(\mathrm{Prime}(y) \land \mathrm{Prime}(z) \land x = y+z)$$

4. No square number is prime: $$\lnot \exists x \mathrm{Prime}(x \cdot x)$$

5. The result of multiplying an odd number by itself is always odd.

I have no exact idea of how to approach this one. Would it be "for all the $$x$$'s that are not even, the result is not even when $$x$$ is multiplied by itself"?

• What exactly do you mean when you say $\forall x ⟶ R$?
– Nika
Nov 24 '19 at 22:06
• Welcome to math stack exchange! It might be useful for you to check out this link: math.stackexchange.com/tour . Your question, as it is, is not formatted with mathjax, making it harder to read: to understand how to use mathjax use this math.meta.stackexchange.com/questions/5020/…. Nov 24 '19 at 22:18
• I meant real numbers. I should have used the symbol ℝ ! Nov 24 '19 at 22:30
• Ah, ok. I assumed by $R$ you meant $\mathbb{R}$. But $\forall x ⟶ \mathbb{R}$ doesn't quite mean 'for all real numbers'. Typically the way to say that is $\forall x \in \mathbb{R}$, does that seem familiar?
– Nika
Nov 24 '19 at 22:36

The consequent in ($$3$$) has a free variable, namely $$x$$. This can be fixed by moving the parenthesis at the end of the antecedent to the end of the entire expression, so:
$$\forall x (\mathrm{Even}(x)) ⟹ \exists y \exists z(\mathrm{Prime}(y) \land \mathrm{Prime}(z) \land x = y+z)$$
$$\forall x (\mathrm{Even}(x) ⟹ \exists y \exists z(\mathrm{Prime}(y) \land \mathrm{Prime}(z) \land x = y+z))$$ So that the universal quantifier can quantify over the whole expression.
For ($$5$$), the way you phrase it in English makes it somewhat unclear what you mean for it to say. Particularly with the word 'result'. Try:
$$\forall x (\lnot \mathrm{Even}(x) \implies \lnot \mathrm{Even}(x \cdot x))$$