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?