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 labellingproblem, 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 somewhatPlatonist viewpoint and say " I will group those instance which have P into this subsetR", and then you end up with two sets, S and a proper subset R. Then you shift to aconstructivist mode and ask "Is there a way I can tell quickly, or even mechanically, whena member of S is also a member of R or not?" Then you switch to programmer/computerscientist mode and say "Let's see if I can either a) write a program to determine ifan instance is a member of R, or b) translate the domain to one where I can encodethe 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 stepone tries.
How does one show R recursive in S or not? One takes an encoding, which is aninjective and computable map from S into the natural numbers (or computably functionalequivalent), and then sees if the image of R under this map is a recursive subset ofthe natural numbers. So this and the previous paragraph are a long winded way ofsaying that most issues of decidability involve coding the problem up in a way asto move the question into the realm of subsets of natural numbers, and using recursiontheory or diagonalization or something to determine the status of the image set. Forme, 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 withproperty P as a subset of integers which may or may not be a recursive subset. Theset of identities satisfied by the real numbers with exponentiation , addition andmultiplication is a set which has a logically equivalent, recursive, and non finitesubset. The set of terms in the Richardson theorem which are equivalent to 0 is anonrecursive subset of the set of all terms used in the context of the theorem. END EDIT
