The Church-Theorem via matrix mortality

The Church-Theorem via matrix mortality#

We give another short proof of Theorem 17, this time using our work on matrix mortality.

Commutative rings with unit#

We us a first-order signature in this section has symbols \(0\), \(1\), \(-\), \(+\), and \(\times\). The symbol \(-\) is unary. The set \(Ax\) of axioms are those of commutative rings with unit. As usual, we elide the multiplication sign \(\times\), and we omit all the parentheses on repeated additions. (For example, we would write \(1+1+1\) instead of \(1 + (1+ 1)\).) What we need to know about this set is that (1) the integers \(\mathbb{Z}\) with the usual operations is a model of it, and a lemma stated below.

Definition

A numeral is a term of the form \(0\), \(1\), \(1+1\), \(\ldots\), or its negative \(-(1 + \cdots+ 1)\). For each integer \(n\) we have a corresponding numeral \(\underline{n}\). For example, \(\underline{-3}\) is \(-(1+ 1 + 1)\). Every numeral is of the form \(\underline{m}\) for some integer \(m\).

Lemma 13

For all integers \(n\) and \(m\):

  1. \(\underline{n} + \underline{m} = \underline{n+m}\).

  2. \(\underline{n} \times \underline{m} =\underline{n\times m}\).

Add a \(9\)-place relation symbol \(R\)#

We add a relation symbol \(R\) to our signature. The \(9\) comes from \(3\times 3\) matrices, and since we are thinking of matrices, we use subscripts on variables as a reminder. So we write

\[ R(x_{1,1}, x_{1,2}, x_{1,3}, x_{2,1}, x_{2,2}, x_{2,3}, x_{3,1}, x_{3,2}, x_{3,3}) \]

rather than \(R(x_1, \ldots, x_9)\). Moreover, if \(M = (m_{ij})\) is \(3\times 3\) matrix of integers, we write \(R(M)\) to mean

\[ R(\underline{m_{1,1}},\underline{m_{1,2}}, \underline{m_{1,3}}, \underline{m_{2,1}},\underline{m_{2,2}}, \underline{m_{2,3}}, \underline{m_{3,1}},\underline{m_{3,2}}, \underline{m_{3,3}}) \]

This is a first-order sentence in the language of our signature. The idea of \(R(M)\) is that it should mean that \(M\) is obtainable as a finite product of elements of a given finite set \(\mathcal{S}\) of matrices. But we are getting ahead of ourselves here, since we have not mentioned our overall strategy in this proof. Here it is: we are going to associate to each finite set \(\mathcal{S}\) of \(3\times 3\) integer matrices a sentence \(\varphi_{{\mathcal S}}\) in our signature, and we shall arrange in Lemma 14 that \(\varphi_{{\mathcal S}}\) is provable in first-order logic if and only if some finite product of elements of \(\mathcal{S}\) is the zero matrix. As before, we allow repeats in the product. To simplify things a touch, we regard the empty product as the identity matrix.

The sentence \(\varphi_{{\mathcal S}}\) is \(Ax_{\mathcal{S}} \to R(0_3)\), where \(Ax_{\mathcal{S}}\) is the conjunction of the sentences which we have seen so far, together with some additional sentence pertaining to a given set \(\mathcal{S}\). Whenever \(M = (m_{i,j})\) is a matrix in \(\mathcal{S}\), we also add

\[\begin{split} \begin{array}{lll} (\forall x_{1,1}) \cdots (\forall x_{3,3})& & R(x_{1,1}, x_{1,2}, x_{1,3}, x_{2,1}, x_{2,2}, x_{2,3}, x_{3,1}, x_{3,2}, x_{3,3}) \\ & \rightarrow & R\bigl(x_{1,1} \underline{m_{1,1}} + x_{1,2} \underline{m_{2,1}} + x_{1,3} \underline{m_{3,1}},\\ & & \quad x_{1,1} \underline{m_{1,2}} + x_{1,2} \underline{m_{2,2}} + x_{1,3} \underline{m_{3,2}},\\ & & \qquad \vdots \\ & & \quad x_{3,1} \underline{m_{1,3}} + x_{3,2} \underline{m_{2,3}} + x_{3,3} \underline{m_{3,3}} \bigr) \end{array} \end{split}\]

In our shorthand notation, the first axiom is \(R(I_3)\), where \(I_3\) is the \(3\times 3\) identity matrix. Our remaining axioms imply that if \(R(M_1)\) and \(M_2\in \mathcal{S}\), then \(R(M_1\times M_2)\). In other words, the interpretation of \(R\), considered as a set of matrices, is closed under multiplication by elements of \(\mathcal{S}\).

Let \(Ax_{\mathcal{S}}\) be the conjunction of the finite set of axioms mentioned above. We have a model \(\mathbb{Z} \models Ax_{\mathcal{S}}\), where for \(R\) we specify that \(R(M)\) iff \(M\) is a product of elements of \(\mathcal{S}\).

Lemma 14

For all finite sets \(\mathcal{S}\) of matrices, the following are equivalent:

  1. Some finite product from \(\mathcal{S}\) is the \(3\times 3\) zero matrix \(0_3\).

  2. In first order logic, \(\vdash Ax_{\mathcal{S}} \to R(0_3)\).

Proof. (2)\(\Rightarrow\)(1) is immediate from the observation that \(\mathbb{Z}\) from above is a model of \(Ax_{\mathcal{S}}\). Again, the interpretation of \(R\) corresponds to the matrices which are obtainable as finite products from \(\mathcal{S}\). So to say that \(R(0_3)\) is to say that the zero matrix is obtainable.

As for (1)\(\Rightarrow\)(2), we show by induction on \(i\geq 0\) that if the matrix \(M\) is a product of \(i\) members of \(\mathcal{S}\), then \(\vdash Ax_{\mathcal{S}} \rightarrow R(M)\). Point (2) follows immediately from this fact and (1).

Lemma 14 implies the Church-Turing Theorem, Theorem 17, in view of the undecidability of matrix mortality.

Contents