# Learning to translate natural-language phrases to formal logic

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

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

• This is very concise! In the first formal logic statement, is it possible to have: $g(0)=h(0)=0$ and $g(1)>1$, and $h(1)<1$ simultaneously hold? May 28 at 7:35
• Re: the new plain statement. I guess when we say a function $f$ is nonnegative, it usually mean that $f(\mathbb R)\geq 0$? Will people confuse "$f(y)$ is nonnegative" with "$f$ is nonnegative"? May 28 at 7:37
• 1. Yes. $\quad$ 2. Not technically: $f$ being identically nonnegative means that for each $x$ in $f$'s domain (in real analysis, this is some subset of $\mathbb R),\;f(x)≥0.\quad$ 3. "$f(y)$ is nonneg" is an incomplete sentence: the reader is left wondering whether you mean that $f$ is identically nonneg, or that $f$ is nonneg somewhere, and if the latter, whether that nonneg location is unknown or has been specified. May 28 at 8:28
• Very helpful! So it seems like "for all constant", "fix arbitrary constant" and "fix a constant" all have the same meaning? If so, why do people often use “fix a constant” instead of "for all"? May 28 at 14:20
• Writing style! Alternatively, maybe think of “For all $x,$ blah blah.” as the theorem statement, and “Let us arbitrarily fix $x.$ blah blah. more blah blah.” as its proof. Personally, I might write “Let $x\in X$ (i.e., let $x$ be an arbitrary element of set $X)$, and suppose that $P(x).$ Then blah blah blah.” $\quad$ P.S. The comments at the top of Using “we have” in maths papers cracked me up; this response is particularly eloquent. May 28 at 23:40