Is the equational theory of sine and cosine trivial? Consider the algebraic structure $(\mathbb{R}; \sin, \cos)$. I conjecture that the only equations that hold in that structure are of the form $t=t$, for some term $t$. Is this true? If so, can someone give me a proof that it is true.
 A: I don't know the answer, but let me make some comments.
We are working in the language of two unary function symbols $c$ and $s$. Say that a term has weight zero if it is a variable. If a term $T$ has the form $ct$ or $st$ for some term $t$, say that the weight of $T$ is one more than the weight of $t$. So, for example, the terms involving the variable $x$ which have weight at most $2$ are $\{x,c(x), s(x), cc(x), sc(x), cs(x), ss(x)\}$. Say that an equation $u=t$ has weight at most $k$ if both $u$ and $t$ have weight at most $k$. 
Let $\mathbb R$ be the structure with universe equal to the real numbers and unary functions $c^{\mathbb R}(x) = \cos(x), s^{\mathbb R}(x) = \sin(x)$.
Claim. Each term in this language involves a single variable. $\Box$ 
Claim. If $\mathbb R$ satisfies a nontrivial identity, then the same variable is involved on both sides of the identity.
Reason. Else $\mathbb R\models u(x)=t(y)$ for some $u$ and $t$ and $x\neq y$. By replacing $y$ with some $z\neq y$ we get $\mathbb R\models u(x)=t(z)$. By symmetry+transitivity we get $\mathbb R\models t(y)=u(x)=t(z)$ or $\mathbb R\models t(y)=t(z)$, $z\neq y$, which implies that the term operation $t^{\mathbb R}$ is constant. But $t^{\mathbb R}$ is a composition of $\sin$ and $\cos$, which both map $[0,1]$ injectively into itself, so it is impossible that $t^{\mathbb R}$ is constant. $\Box$ 
Claim. If $\mathbb R\models u(x)=t(x)$ and $u=t$ has weight at most $2$, then $u(x)=t(x)$ is trivial. 
Reason. Substitute $x=1\in \mathbb R$ into the $7$ terms involving $x$ which have weight at most $2$, namely into the terms in the set $\{x,c(x), s(x), cc(x), sc(x), cs(x), ss(x)\}$. You obtain a set of $7$ different values
$$\{0.514395258523549, 0.540302305868140, 0.666366745392880, 0.745624141665558, 0.841470984807897, 0.857553215846393,1\}.$$
This shows that $u^{\mathbb R}(1)\neq t^{\mathbb R}(1)$ whenever $u$ and $t$ are different terms of weight at most $2$. $\Box$ 
Claim. If $\mathbb R\models u(x)=t(x)$ and $u=t$ has weight at most $20$, then $u(x)=t(x)$ is trivial. 
Reason. This is done exactly like the weight 2 case. Substitute $x=1\in \mathbb R$ into the $2^{20+1}-1=2097151$ terms involving $x$ which have weight at most $20$. You will find that you get $2097151$ distinct numbers as your result, so $\mathbb R$ satisfies no nontrivial identity of weight at most $20$. $\Box$
I used the following lines of Maple to perform the preceding computation.
$\texttt{Digits:=15:}$
$\texttt{L[0]:=[1]: U[0]:={1}:}$
$\texttt{for i from 0 to 19 do}$
$\texttt{L[i+1]:=[op((evalf@sin)~(L[i])),op((evalf@cos)~(L[i]))]:}$
$\texttt{U[i+1]:=U[i]union{op(L[i+1])} od:}$
$\texttt{nops(U[20]);}$
In this code, $L[k]$ is a complete, irredundant list of the $2^k$ term operations, induced by terms of weight exactly $k$, evaluated at $x=1$. $U[k]$ is the accumulated set of list values, which means that $U[20]$ is the set of values obtained by evaluating terms of weight at most $20$ at the real number $x=1$. The last line computes the size of $U[20]$, which turns out to be $2097151$ --- the same as the number of terms of weight at most $20$. 
I did not analyze the roundoff error. I did vary the choice for Digits and saw that the outcome is unreliable when Digits is small, but seems to stabilize at the expected value as you gradually increase the value for Digits. (Digits is the environment variable that controls the number of digits Maple uses when calculating with floating point numbers.)
To alter the code to explore further, change the $19$ in the 3rd line to some $n$ and change the $20$ in the last line to $n+1$ to see if $\mathbb R$ satisfies nontrivial identities of weight at most $n+1$.
