the Richardson theorem and the base identities problem 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.
 A: Note: I'm not actually familiar with either problem that you ask about, so I'm going by your description.
Recursive base of identities means there is a computer program P such that given an identity I, running P will tell you in a finite amount of time whether I is in the base or not.  P is called a "decision procedure".
Richardson problem being undecidable means something like: given an arbitrary program (Turing machine) P, you can encode the halting problem for P an an expression in $\mathcal R$.  That is you can write down a formula that is identically zero if and only if P halts.  Since the halting problem is undecidable, there is no decision procedure for telling if such a formula in $\mathcal R$ is identically zero.  That's sort of like Hilbert's tenth problem, where you can encode an arbitary program P as a set of diophantine equations, that has a solution iff P halts.  Again since the halting problem is undecidable, there is no algorithm to tell whether an arbitrary diophantine system has a solution.
I think the absolute value function being available in $\mathcal R$ may have something to do with the undecidability.  In symbolic algebra, the Risch algorithm is a finite procedure for telling whether a given expression made from elementary functions and composition has a closed-form indefinite integral.  But I seem to remember that if you add the absolute value function, the problem becomes undecidable.
A: Sergei, this is a reply to your comment asking about enumerating formulas in $\mathcal R$.  Sorry to post it as a separate answer but I no longer have the browser cookie to post it as a followup comment.
You don't need a particular standardized enumeration, but just some computable mapping between formulas and natural numbers so that each formula gets a unique number.  Such a numbering scheme is traditionally called a "Gödel numbering" and the numbers are called "Gödel numbers" because the idea was (I think) introduced in Gödel's landmark paper (1931) about the incompleteness theorem.
A simple Gödel numbering scheme (similar to the one Gödel used) is like this: say the formulas are written in an "alphabet" whose "letters" are $\{\sigma_1,\sigma_2,\ldots\}$.  Treat those as natural numbers the obvious way (i.e. $\sigma_k\mapsto k$).  So a formula F might be written as $(F_1,F_2,\ldots F_n)$ where the $F_i$ are natural numbers.  Then let
$$N_F=2^{F_1}\cdot 3^{F_2} \cdot 5^{F_3} \cdots p_n^{F_n}$$ 
where $p_i$ is the $i$'th prime number.  That is the Gödel number for F (under this particular scheme).  It's pretty easy to see how to convert a formula to a number and back.  Some numbers won't correspond to valid formulas so treat them as identically zero, for example.
Maybe you should read an introductory book on logic, if you want more clarity about this stuff.  There are some other threads suggesting them.
A: I am not a professional logician, but I have studied mathematical logic, and in past work I used the rough notion (as have many before me) that if you can write a Pascal program to decide correctly the yes or no answer to a problem given the finite set of parameters as input, then the problem or issue is decidable.  Otherwise it isn't.  Taken at this level, I see both uses of decidability as the same.  In one, there is a finite specification which can be used to test whether an identity is in the one set, in the other there is no such program to test whether an equation/identity is in the other set.
(There are technical arguments to be made as to which machine model, complexity, degree of undecidability if one looks at e.g. Turing equivalent degrees, and so on.  I am setting aside all these complexities and ways to distinguish the two uses of decidability, since they seem to me irrelevant to the basic intent of your question.)
I can see both problems as problems of clone theory.  Again roughly, the first problem talks about whether there are a finite number of relations in the generators in addition to the general relations for a clone that can be used to describe the collection of equivalence classes of terms (there are not, but there is a recursive set of such relations).  The second talks about whether the set of terms in the clone equivalent to the term 0 is describable by a computer program; according to Richardson, it is not.  There are other ways to recast the problems to see some similarities and highlight the differences; it depends on just what you want to see.
EDIT: Another view of many issues of decidability is this one, borrowed and simplified from one used in complexity studies in computer science.  If you have a decision or labelling
problem, where you have a set S of instances and for each instance you want to say
"yes, instance I has property P" or "no, I does not have P", you take a somewhat
Platonist viewpoint and say " I will group those instance which have P into this subset
R", and then you end up with two sets, S and a proper subset R.  Then you shift to a
constructivist mode and ask "Is there a way I can tell quickly, or even mechanically, when
a member of S is also a member of R or not?"  Then you switch to programmer/computer
scientist mode and say "Let's see if I can either a) write a program to determine if
an instance is a member of R, or b) translate the domain to one where I can encode
the halting problem, so that determining membership in R solves the halting problem" .
If the set R is recursive inside S, then a) is possible in theory, but may be difficult or impossible in practice, depending on the complexity of the set R.  If the set R is not recursive in S, then b) may or may not be possible, but is usually the first step
one tries.
How does one show R recursive in S or not? One takes an encoding, which is an
injective and computable map from S into the natural numbers (or computably functional
equivalent), and then sees if the image of R under this map is a recursive subset of
the natural numbers.  So this and the previous paragraph are a long winded way of
saying that most issues of decidability involve coding the problem up in a way as
to move the question into the realm of subsets of natural numbers, and using recursion
theory or diagonalization or something to determine the status of the image set.  For
me, I picture the set of identities or the set of terms as a set of numbers, each number colored with label or term or identity it represents, and I picture the subset with
property P as a subset of integers which may or may not be a recursive subset.  The
set of identities satisfied by the real numbers with exponentiation , addition and
multiplication is a set which has a logically equivalent, recursive, and non finite
subset.  The set of terms in the Richardson theorem which are equivalent to 0 is a
nonrecursive subset of the set of all terms used in the context of the theorem.  END EDIT
Gerhard "Ask Me About System Design" Paseman, 2012.05.11
