In the fields related to school mathematics there is some acitivity on proving (or disproving) deducibility/decidability for some classes of school identities. In particular,
1) In logic they considered not long ago the base identities problem (this term is the translation from Russian, I am not sure that it is correct). The problem was the following. Let $N$ be the set of positive integers, and $\mathcal K$ a class of all functions from $N^k$ into $N$ ($k$ runs over $N$) which can be represented as compositions of usual algebraic operations $x+y$, $x\cdot y$ and $x^y$. Let us call a base of identities in $\mathcal K$ a set $B$ of identities for functions in ${\mathcal K}$, such that any identity for functions in $\mathcal K$ can be deduced from $B$. The question was, does there exist a finite base of identities for ${\mathcal K}$? This question appeared when A.Wilkie gave a counterexample for the Tarski high school algebra problem (where a list of identities was suggested by Tarski, and the question was whether this list is a base). In 1980-es R.Gurevich proved that there is no finite base of identities, so the problem of base identities is solved in negative. At the same time, as far as I understand, R.Gurevich proved that instead of finite base of identities, there exists a recursive base of identities, and as far as I understand this is an example of what logicians call decidability.
2) In computer algebra there is the so-called Richardson theorem, which states that if $\mathcal R$ is a class of expressions generated by
-- the rational numbers and the two real numbers $\pi$ and $ln 2$,
-- the variable $x$,
-- the operations of addition, multiplication, and composition, and
-- the sine, exponential, and absolute value functions,
then for $F\in {\mathcal R}$ the predicate $F=0$ is recursively undecidable.
My question is whether these two fields are related to each other? Is decidability for Richardson the same as decidability for logicians? If yes, then which exactly logical system does Richardson mean?
I am not a specialist here, I am interested in this because I write a textbook on mathematical analysis (I am sorry, this happens sometimes with mathematicians), and when describing elementary functions I faced a problem analogous to the base identities problem above, but the difference is that the list of operations (and elementary functions) is wider (for example, both $x-y$ and $x^y$ are included), and as a corollary the arising functions are defined not everywhere on $R$ (one can look at the details at page 197 in the draft of the first volume of my textbook -- unfortunately, it is in Russian).
This is strange, but I can't find anyone who could explain me this. I asked this question in sci.math.research some time ago, but the problem of overcoming the Kevin Buzzard resistance turned out to be undecidable for me there. So I would be much obliged to MO if my question will hang here for some time so that, perhaps, some specialitsts in logic could clarify me something.