show/hide this revision's text 2 added 71 characters in body

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?

show/hide this revision's text 1

Decidability of matrix algebra

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]?

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

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