Although Peter Shor gave a proof of the undecidability (as he stated in a comment to the current question), here is another proof. An advantage of this proof is that it gives the undecidability of a very restricted version of the problem.

In an answer to my question, Agol told me that the following problem (which I called the Finite-Dimensional Word Problem for Groups (FWP) in the question) is undecidable by a result of Slobodskoi [Slo81].

*Instance*: A finite presentation of a group G and an element w of G as a product of generators and their inverses.

*Question*: Does every matrix representation of G map w to the identity matrix?

(The result in [Slo81] does not literally talk about this problem, but the result there implies the undecidability of this problem. See the answer by Agol linked above and also the discussion linked from my question.)

This problem can be easily translated into a special case of the current problem, which shows that the problem in question is undecidable even if we only allow a sentence of the form:

∃I.((∀X.IX=X)∧(∀X.XI=X)∧(∀X_{1}…∀X_{n}.(P_{1}(X_{1},…,X_{n})=I∧…∧P_{m}(X_{1},…,X_{n})=I→Q(X_{1},…,X_{n})=I)))

where I, X, X_{1}, …, X_{n} are matrix variables and P_{1}(X_{1},…,X_{n}), …, P_{m}(X_{1},…,X_{n}), Q(X_{1},…,X_{n}) are products of one or more variables in X_{1}, …, X_{n} in some order with repetitions allowed. In particular, the problem is undecidable even if we do not allow scalar variables, vector variables, addition or conjugate transpose!

References

[Slo81] A. M. Slobodskoi. Unsolvability of the universal theory of finite groups. *Algebra and Logic*, 20(2):139–156, March 1981. http://www.springerlink.com/content/x880g1x17754hq83/