Learning to translate natural-language phrases to formal logic In natural language, we often use phrases like:

*

*"fix arbitrary"

*"such that"

*"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$.

 A: 

*

*"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.




*"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.




*"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.)
