This should be a comment but is too long. The decidability of the question whether a finite set R of relations implies some other relation r=1 in all linear grous is the same as asking if R implies r=1 in all finite groups because of Malcev's theorem on residual finiteness of linear groups. A beautiful theorem of Slobodoskoii says this latter problem is undecidable. A consequence is that the first order theory for modules over an algebra of wild representation type is undecidable.