George McNulty mcnulty at math.sc.edu
Tue Feb 6 01:06:20 EST 2007

```The answer is still the same.  There is a finite set \Sigma
of identities in just one operation symbol which is binary
such that the set of identities which are logical consequences
of \Sigma form a nonrecursive set.  It is also possible to do
this with two unary operation symbols. On the other hand, it
cannot be done with just one unary operation symbol (even
expanded by finitely many constant symbols).  The proofs
of the undecidability results ultimately get back to the
Halting Problem via the 1947 Post-Markov construction of a finitely
presented semigroup with an unsolvable word problem.  One place
where the details are worked out is the following paper of
Mal'cev:

A. I. Mal'cev, Identical relations on varieties of quasigroups
(Russian) Mat. Sb. vol 69 (1966) pp. 3--12 (Translation:
American Matheamtical Society Translations, series 2 vol. 82
(1968) pp. 225--235)

More difficult is the result of Vadim Murskii that there is
a finite set \Gamma of identities (in just one operation symbol, that one
being binary) which includes the associative law (that is: a set of
semigroup equations) which also axiomatizes an undecidable
equational theory. The reference here is

V. L. Murskii, Some examples of varieties of semigroups (Russian)
Mat. Zametki, vol. 3 (1968) pp. 663--670.

As I mentioned in my earlier message, perhaps the most striking result
in this direction is that of Ralph Freese that the equational theory
of modular lattices is undecidable.  This theory is axiomatized by
a finite set of identities, but unlike the results above, this is the
equational theory of a class of algebras of significant mathematical
interest in their own right.

George McNulty

> Thanks to all who replied to my inquiry about identities.
>
> It turns out that my friend is asking a more difficult question. He
> asks whether there is an algorithm to determine whether a given
> equation follows from a given finite set of such equations if THE
> OPERATIONS ARE RESTRICTED TO A SINGLE BINARY OPERATION. Constants and
> unary operations are not permitted.
>
> Martin
>
>
>                            Martin Davis
>                     Visiting Scholar UC Berkeley
>                       Professor Emeritus, NYU
>                           martin at eipye.com
>                           (Add 1 and get 0)
>                         http://www.eipye.com
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

```