I wonder how hard identity testing (similar to polynomial identity testing) can be for a free algebra. I thought that in a certain sense, the problem should always be semi-decidable, because the free algebra is defined with respect to the identities which follow from the given set of equational axioms. So how do I have to interpret the following statement from Equational and universal Horn theory of modular lattices:
The free modular lattice on 4 or more generators has an unsolvabe word problem.
Are they talking about the same identity testing problem I'm interested in? Do they use "unsolvable" instead of "semi-decidable", because the semi-decidability is obviously already part of the definition? Or does unsolvable quite generally just means that one of the two directions is not decidable?
Yes this theorem states that, for any fixed $n$ at least 4, the equational theory of modular lattices in $n$ generators is not computable. Here a lattice is viewed as an algebra with two binary operations, not as a relational structure. Ralph Freese