Is subtraction term-definable from addition in the reals? In the structure $(\mathbb{R};-)$, where $-$ is binary subtraction, addition is a term function in it, like this: $x+y=x-((y-y)-y)$. I want to know if subtraction is a term function in the structure $(\mathbb{R};+)$. I know that it is definable from addition by a first-order formula, but I want to know if it is definable by a term function. I believe it is not, but how does one prove that it is not?
 A: I believe it is not, but how does one prove that it is not?
Suppose that $f$ is a $k$-ary operation on a set $A$ and $\mathcal F$ is a set of operations on $A$. Then $f$ is expressible as a composition of operations from $\mathcal F$ if and only if every relation on $A$ of arity $|A|^k$ that is closed under $\mathcal F$ is also closed under $f$. Therefore, to show that $f$ is not expressible as a composition of the operations in $\mathcal F$, it is enough to exhibit some relation closed under $\mathcal F$ and not closed under $f$.
In this case, where $f = -$ and $\mathcal F = \{+\}$, choose the unary relation $(0,\infty)$ of positive reals. It is closed under $+$ but not $-$, so $-$ cannot be expressed as a term in $+$.


EDIT Oct 15.
Let me respond to a comment. I will leave my answer
unchanged, but append more explanation here.

Theorem.
 Suppose that $f$ is a $k$-ary operation on a set $A$ and $\mathcal F$ is a set of operations on $A$. Then $f$ is expressible as a composition of operations from $\mathcal F$ if and only if every relation on $A$ of arity $|A|^k$ that is closed under $\mathcal F$ is also closed under $f$. 
Before proving this, let me clarify with an example what I mean when I say that $f$ is expressible as a composition of operations from $\mathcal F$. Let $\mathcal F = \{+\}$, and let me write down operations in the variables $X=\{x_0, x_1,x_2,\ldots\}$ that are expressible as compositions of operations in $\mathcal F$:

Operations with $0$-occurrences of $+$:    $x_i$.
Operations with $1$-occurrences of $+$:    $x_i+x_j$.
Operations with $2$-occurrences of $+$:    $(x_i+x_j)+x_k, \;\;x_i+(x_j+x_k)$.
The important point is that I allow operations with zero occurrences of operation symbols. Syntactically, these are just variables. Semantically, they are projections: the variable $x_2$, considered as a $k$-ary operation, accepts $(a_0,a_1,a_2,\ldots,a_{k-1})\in A^k$ and returns $a_2$.

Proof of theorem.
($\Rightarrow$)
For any relation $R\subseteq A^n$ on $A$, the set of operations
on $A$ that preserve $R$ is closed under composition.
Therefore, if the operations in $\mathcal F$ preserve $R$ and
$f$ is expressible as a composition
of operations from $\mathcal F$, it follows that $f$ must preserve $R$.
($\Leftarrow$)
For any operation $t\colon A^k\to A$ of arity $k$ on $A$
let $G(t) = (t({\bf a}))_{{\bf a}\in A^k}$ be its graph.
This graph is a tuple indexed by by the set $A^k$.
For an element ${\bf a}\in A^k$ of the index set,
the ${\bf a}$-coordinate value of $G(t)$
is $t({\bf a})$.
Suppose that $\mathcal F$ is a set of operations on $A$
and that $\langle {\mathcal F}\rangle$ is the
composition-closure of $\mathcal F$ (the collection of all
operations expressible as composition of operations in $\mathcal F$).
Let $R$ be the relation that consists of the graphs of $k$-ary operations
in $\langle {\mathcal F}\rangle$.
Claim. $R$ is closed under $\mathcal F$.
Choose any $h\in {\mathcal F}$ of arity $m$ and choose
$m$ tuples from $R$: $G(t_0), G(t_1),\ldots, G(t_{m-1})$.
It is enough to see that
$h(G(t_0), G(t_1),\ldots, G(t_{m-1})) = G(h(t_0,\ldots,t_{m-1}))\in R$.
One may see this by noting that both
$h(G(t_0), G(t_1),\ldots, G(t_{m-1}))$ and $G(h(t_0,\ldots,t_{m-1}))$
have the same ${\bf a}$-coordinate for every ${\bf a}\in A^k$, namely
$h(t_0({\bf a}),t_1({\bf a}),\ldots,t_{m-1}({\bf a}))$.
Claim. If $R$ is closed under $f$, then $f\in \langle {\mathcal F}\rangle$.
Apply $f$ to $G(x_0), G(x_1),\ldots, G(x_{k-1})\in R$:
$$
f(G(x_0), G(x_1),\ldots, G(x_{k-1})) = G(f(x_0,\ldots,x_{k-1}))=G(f)\in R.
$$
If $G(f)\in R$, then, according to the definition of $R$,
$G(f)=G(t)$ for some $t\in \langle {\mathcal F}\rangle$,
so $f=t\in \langle {\mathcal F}\rangle$.
The two claims show that if
every relation on $A$ of arity $|A|^k$
that is closed under $\mathcal F$ is also closed under $f$,
then $f\in \langle {\mathcal F}\rangle$. \\\
