$\DeclareMathOperator\Eq{Eq}\DeclareMathOperator\Th{Th}$*Originally [asked at MSE](https://math.stackexchange.com/questions/4164632/does-sine-equationally-interact-with-addition-or-with-multiplication) without success:*


For a structure $\mathcal{A}$ whose signature only contains function and constant symbols, let $\Eq(\mathcal{A})$ be the equational theory of $\mathcal{A}$ — that is, the set of all universal closures of atomic formulas which are satisfied by $\mathcal{A}$. Via trigonometric identities like the double angle identity, [we have](https://math.stackexchange.com/a/4164504/28111) that $\Eq(\mathbb{R};+,\times,\sin)$ does *not* "reduce" to $\Eq(\mathbb{R};+,\times)$; formally, we have $\Eq(\mathbb{R};+,\times)\not\models \Eq(\mathbb{R};+,\times,\sin)$.


Notably, all such examples I know crucially involve all three operations available. I'm curious whether this is necessary. Since this question seems harder than I originally suspected, I'll focus on addition specifically:



> 
> Does $\Eq(\mathbb{R};+)\models \Eq(\mathbb{R};+,\sin)$?
> 
> 
> 


I suspect that the answer is **yes**; in a sense this would amount to saying that trigonometric identities have to use multiple arithmetic operations, which matches at least my experience. However, I don't see how to prove this.


Note that $\Eq(\mathcal{A})$ is generally *far* less informative than $\Th(\mathcal{A})$. For example, suppose $f:\mathbb{R}\rightarrow\mathbb{R}$ is "sufficiently wild." Then $\Th(\mathbb{R};f)$ will be nontrivial (e.g. it will say "$f$ is not injective") but no nontrivial equation will hold in $(\mathbb{R};f)$ so $\emptyset\models \Eq(\mathbb{R};f)$. So the relative tameness of $(\mathbb{R};+)$ from the "coarse" perspective of first-order logic can't help us here.



Does sine interact equationally with addition alone?
Here is the outline of a proof that $Eq(\mathbb{R},+)$ proves all the equalities in both $Eq(\mathbb{R},+,\sin)$ and $Eq(\mathbb{R},+,\exp)$.


**Step 1, defining $<$:**


For any term $t$ in $L(+,\sin)$, define a real function $t\_R$ by $$t\_R(r\_1,\ldots r\_n)=\sup(\{|t(z\_1,\ldots,z\_n)|: z\_1,\ldots,z\_n \in \mathbb{C}, |z\_1|=r\_1, \cdots, |z\_n|=r\_n\})$$


Then for terms $t$ and $u$ in $L(+,\sin)$, define $t<u$ iff
$$\mathbb{R}\models Qr\_1 \ldots Qr\_n\, t\_R<u\_R$$
where $Q$ is the quantifier "for all sufficiently large" and $n$ is the largest index of a primitive variable which appears in $t+u$.


Similary, for terms $t$ and $u$ in $L(+,\exp)$, define $t<u$ iff
$$\mathbb{R}\models Qx\_1 \ldots Qx\_n\, t<u$$


**Step 2, determining $<$:**


I claim that for the definitions above:


* $t<x\_i$ iff all the primitive variables appearing in $t$ have indices less than $i$.
* $\sin(t)<\sin(u)$ iff $t<u$
* $\exp(t)<\exp(u)$ iff $t<u$
* if $m>1$, then $\sum\_{i=1}^m t\_i<\sin(u)$ iff $t\_i < \sin(u)$ for all $i\le m$.
* if $m>1$, then $\sum\_{i=1}^m t\_i<\exp(u)$ iff $t\_i < \exp(u)$ for all $i\le m$.
* if $m\ge 1$, $n>1$ with $t\_1 \ge \cdots \ge t\_m$ and $u\_1 \ge \cdots \ge u\_n$, and none of the $t$'s and $u$'s are sums, then $\sum\_{i=1}^m t\_i<\sum\_{j=1}^n u\_j$ iff either $t\_k < u\_k$ at the first index $k$ where the $t$'s and $u$'s differ, or $m<n$ and $t\_k=u\_k$ for all $k\le m$.


Furthermore, this provides a recursive algorithm for determining whether $t<u$ for any terms $t$ and $u$ in the same one of the languages above.


**Step 3, normalizing $<$:**


For any term $t$ in the language, we get a normal form $N(t)$ by repeatedly applying the following rules:


* if $a<b$, replace $a+b \rightarrow b+a$
* if $a<b$, replace $a+(b+c) \rightarrow b+(a+c)$
* always replace $(a+b)+c \rightarrow a+(b+c)$


I claim that $t<u$ iff $N(t)$ is smaller than $N(u)$ in the first part that differs.


Now, lexicographically, for any terms $t$ and $u$, either $N(t)<N(u)$ or $N(t)=N(u)$ or $N(t)>N(u)$. In the first and last cases, $t$ and $u$ are not equal over $\mathbb{R}$; for $\sin$ the definition of $<$ tells us that they are different over $\mathbb{C}$, and then the [identity theorem](https://en.wikipedia.org/wiki/Identity_theorem) tells us that they are also different over $\mathbb{R}$. In the middle case, $Eq(\mathbb{R},+)$ is enough to establish $t=N(t)=N(u)=u$.


