Learning to translate natural-language phrases to formal logic

Question

In natural language, we often use phrases like:

1. "fix arbitrary"
2. "such that"
3. "we have"

In general, how to translate those phrases into formal logic?

One example condition is:

Fix arbitrary $x,y$. For all $f\in A$ such that $f(x)=0$, we always have $f(y)\geq0$, or we always have $f(y)\leq 0$.

Answer 1

1. "fix arbitrary"

for each

• Fix an arbitrary $x$ (or:  arbitrarily fix $x$);  then $P(x)$ is true.
  In other words:  $P(a)$ is true; $P(b)$ is true; $P(c)$ is true; etc. $$\forall x\;P(x).$$ Literally:  For each $x,\:P(x)$ is true.

2. "such that"

• For each $x$ such that $P(x)$ is true, $Q(x)$ is true. $$\forall x\;\big(P(x)\implies Q(x)\big).$$ Literally:  For each $x,\,$ if $P(x)$ is true, then $Q(x)$ is true.
• There is some $x$ such that $P(x)$ is true. $$\exists x\;P(x).$$ Literally:  For some $x,\,P(x)$ is true.

3. "we have"

• We have $P(x)$ being true.
  (or:  We have that $P(x)$ is true.) $$P(x).$$ More crisply:  $P(x)$ is true.

---

Fix arbitrary $x,y$. For all $f\in A$ such that $f(x)=0$, we always have $f(y)\geq0$, or we always have $f(y)\leq 0.$

$$∀x\;∀y\;∀f{\in}A\;\Big(f(x)=0\implies f(y)\ge0\;∨\;f(y)\le0 \Big);\tag1$$ more plainly:  for each $f,x$ and $y$ for which $f$ is in $A$ and $f(x)$ equals zero, $f(y)$ is either nonnegative or nonpositive.

Equivalently: $$∀f{\in}A\;\Big(∃x\;f(x)=0\implies ∀y\;f(y)\ge0\;∨\;∀z\;f(z)\le0 \Big),\tag2$$ i.e.,  every function in $A$ that has a root is either identically nonnegative or identically nonpositive,
i.e.,  every function in set $A$ that has a root never crosses (cuts through) the $x$-axis.

(Observe that formalisation (1) is the most succinct, while verbalisation (2) is the easiest to understand.)