[FOM] About identities

[George McNulty]

Here is some more information about undecidable equational theories.

In addition to the work of A.I. Mal'cev I mentioned before, I should also
mention that a finite set of identities in just one binary operation symbol
whose equational consequences form a nonrecursive set was constructed by
Peter Perkins in his 1966 doctoral dissertation at Berkeley written under
the direction of Dana Scott. The methods of Mal'cev and Perkins are pretty
much the same.  The results were obtained independently. Perkins eventually
published this part of his dissertation in the Notre Dame journal in 1974(?).

Harvey Friedman's observation about a single equation axiomatizing an
undecidable equational theory is also correct, but the attribution to Ralph
McKenzie may not be correct (although it might be).  Lacking conjunction, it
is not generally true in equational logic that a finite set of equations is
logically equivalent to a single equation.  However, in the mid-1960's
Tarski and, independently a collaboration between McKenzie and Gratzer, found
that any finite set of equations which includes to equational axioms for
rings with unit is logically equivalent to a single equation. So to achieve
a single equation which axiomatizes an undecidable equational theory one
need only come up with some finite set which includes enough ring theory
and which gives an undecidable equational theory.  Tarski already had such
a theory on hand in the mid-1940's.  If you want to get down to just a
single binary operation, then it is easy to employ the devices invented 
by Mal'cev and Perkins to wind up with a single equation in just one
binary operation which axiomatizes an undecidable equational theory.

Tarski's route to this result is actually very interesting but also fairly
involved.  A more (?) direct route is possible. In 1973 Angus MacIntyre
found a finitely presented division ring with an unsolvable word problem.
So one could start with a finite set of equations (using new constants to
name the generators) that present MacIntyre's ring. Apply the one equation
collapse of Tarski and Gratzer-McKenzie to get one equation in a bunch of
operations including the new constants.  Final apply the devices of Mal'cev
and Perkins to get a single equation in just one binary operation.

Tarksi's route actually gives more.  He provided a method for emulating 
set theory (or say some rich enough finitely axiomatizable consistent 
undecidable part) as an equational theory of relation algebras (with an
additional constant.  Relation algebras, in essence, have a reduct to
Boolean rings so enough ring theory is available.  Because Tarski's method
provides a faithful enough emulation of first order logic, we get a
way to apply some of the methods of Tarski-Mostowski-Robinson and the
later methods of Ershov, Taimonov, Taiclin in the equational setting.
For more details on these results, see sections 8.5 and 8.6 of 

   Alfred Tarski and Steven Givant, A Formalization of Set Theory without
   Variables, Amer. Math. Soc., Colloquium Publications vol. 41  1987.

Section 8.7 provides extensive historical background.

Another interesting related result is that the equational theory of 
the field of real numbers expanded by the sine function and the
absolute value function is undecidable. (The equational theory of
an algebra is just the set of all identities true in the algebra.)
This was proven by Matiyasevich (see his 1993 monograph) based on
work done by Daniel Richardson in 1968, where a similar result in a
much expanded language is deduced from the Davis-Putnam-Robinson
result that Hilbert's 10th Problem has a negative solution if exponential
Diophantine equations are considered.

George F. McNulty