Does sine interact equationally with addition alone? $\DeclareMathOperator\Eq{Eq}\DeclareMathOperator\Th{Th}$Originally asked at MSE 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 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.
 A: 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 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$.
