7
$\begingroup$

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?

Improve this question
$\endgroup$
14
  • $\begingroup$ Ricky, I think you need to restate the question without multisorted logic: There is no quantification over "sorts"! For example, how about the simpler question: "Is the theory of all $n\times n$ matrix rings with complex coefficients decidable?" $\endgroup$
    – Sidney Raffer
    Commented Jul 30, 2010 at 3:22
  • $\begingroup$ What there is, is quantification within "sorts". The answer to the simpler question is yes by interpreting in a real ordered field. $\endgroup$
    – user5810
    Commented Jul 30, 2010 at 3:34
  • 3
    $\begingroup$ A related question would be whether there is a 0-1 law for your 4-sorted statements as the dimension increases. In other words, is it true that for every statement about matrices, vectors & scalars, the truth is the same in all sufficiently high dimensions? A simple example: matrix multiplication is commutative in dimension 1, but not in all higher dimensions. Do you know if such a phenomenon holds for all statements? $\endgroup$
    – Joel David Hamkins
    Commented Jul 30, 2010 at 3:57
  • 1
    $\begingroup$ The scalars 0 and 1 are definable, as is any algebraic number, so they don't have to be in the language, but you can freely use them anyway. The same for the identity matrix and the 0 matrix. $\endgroup$
    – Joel David Hamkins
    Commented Aug 2, 2010 at 1:03
  • 3
    $\begingroup$ The question is undecideable: see the answers for this Math Overflow question: mathoverflow.net/questions/34186/… $\endgroup$
    – Peter Shor
    Commented Aug 2, 2010 at 21:40

3 Answers 3

Reset to default
2
$\begingroup$

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, https://www.ima.umn.edu/sites/default/files/2165.pdf (Wayback Machine).

Improve this answer
$\endgroup$
2
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ "this algorithm is uniform in n, and so you get a full decision procedure for the multi-sorted logic." How does this follow? I see that we have an algorithm to take a sentence and n, and determine whether the sentence is true for n, but what I'm looking for is an algorithm to take a sentence and determine whether it is [true for all n]. $\endgroup$
    – user5810
    Commented Jul 30, 2010 at 3:08
  • $\begingroup$ I see. I had interpreted your question as to whether or not you could decide the truth of any particular sentence in the multi-sorted logic. But you want to determine whether an unsorted statement holds true for each sort. $\endgroup$
    – Joel David Hamkins
    Commented Jul 30, 2010 at 3:14
  • $\begingroup$ Actually, could you clarify your precise question? You seem to have a handful of sorts for each $n$: matrices, col vectors, row vectors, scalars. So the sentences that you want to decide should each have quantifiers and variables over matrices, scalars, column vectors and row vectors, of unspecified size? But then you want to decide which such sentences are true regardless of the dimension? $\endgroup$
    – Joel David Hamkins
    Commented Jul 30, 2010 at 3:25
  • $\begingroup$ Correct. (editing question now) $\endgroup$
    – user5810
    Commented Jul 30, 2010 at 3:29
  • 1
    $\begingroup$ This answer was answering the version of the question where you have different sorts for each n. But the OP intends to have only four sorts, and wants to know whether the statement holds in all dimensions. $\endgroup$
    – Joel David Hamkins
    Commented Aug 30, 2010 at 15:52
1
$\begingroup$

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)∧(∀X1…∀Xn.(P1(X1,…,Xn)=I∧…∧Pm(X1,…,Xn)=I→Q(X1,…,Xn)=I)))

where I, X, X1, …, Xn are matrix variables and P1(X1,…,Xn), …, Pm(X1,…,Xn), Q(X1,…,Xn) are products of one or more variables in X1, …, Xn 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. Link

Improve this answer
$\endgroup$

You must log in to answer this question.