Decidability of matrix algebra - MathOverflow

Decidability of matrix algebra

2010-07-30T02:03:26Z

Take multi-sorted first-order logic with equality, complex scalars, 1xn vectors, nx1 vectors, nxn matrices, addition and multiplication for each pair of sorts they make sense for, and hermitian transpose (which is conjugation on scalars). Is it decidable what sentences are [true for all n]? (there are 4 sorts, what sentences are true simultaneously for all n)

(For each particular n, it is decidable by interpreting in a real ordered field.)

What if we also add real scalars and ≤ for them?

Answer by Joel David Hamkins for Decidability of matrix algebra

2010-07-30T02:53:41Z

If you want to determine truth in this language with real or complex entries, then Yes. All this is expressible in the language of real-closed fields, simply by using components, and is therefore expressible in the complete theory of $\langle\mathbb{R},+,\cdot,0,1,\lt\rangle$, which is decidable by Tarski's theorem on real-closed fields. For example, quantifying over $n\times 1$ vectors is just $n$ quantifiers over reals (or $2n$ if you want complex numbers).

You mentioned that for each particular $n$, it is decidable by interpreting in the real-closed field, but my point is that this algorithm is uniform in $n$, and so you get a full decision procedure for the multi-sorted logic. That is, given a sentence in the multi-sorted language, we can tell which sorts are quantified over, and so we know how to translate it into a question about real-closed fields, which we can then answer. (I assume that you use a set-up as usual in the multi-sorted logic where each sort gets its own variables and quantifiers.)

If you intend to interpret it over the rationals, then No, since even the $1$-dimensional ring theory of $\langle\mathbb{Q},+,\cdot,0,1,\lt\rangle$ is not decidable, as the integers are definable there, and so you can express the halting problem.

Answer by Tsuyoshi Ito for Decidability of matrix algebra

2010-07-30T18:15:45Z

The second problem (where real scalar variables and the comparison relation are also allowed) is equivalent to the first problem. Here is a standard argument showing this:

A complex scalar variable z can be restricted to real values by requiring $z=\bar{z}$.
The comparison x≤y can be replaced by $\exists z.\ x+z\bar{z}=y$, where z is a fresh complex scalar variable.

Back to the original question, the following paper may be related (or even answer your question) but I do not have enough knowledge to understand the content completely. Mihai Putinar: Undecidability in a Free *-Algebra, preprint, April 2007, http://www.ima.umn.edu/preprints/apr2007/2165.pdf.

Answer by Tsuyoshi Ito for Decidability of matrix algebra

2010-08-30T14:33:48Z

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₁…∀X_n.(P₁(X₁,…,X_n)=I∧…∧P_m(X₁,…,X_n)=I→Q(X₁,…,X_n)=I)))

where I, X, X₁, …, X_n are matrix variables and P₁(X₁,…,X_n), …, P_m(X₁,…,X_n), Q(X₁,…,X_n) are products of one or more variables in X₁, …, 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/