The Church-Theorem via matrix mortality

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

Rings with unit

The first-order signature in this section has symbols \(0\), \(1\), \(-\), \(+\), \(\times\), and an extra relation symbol \(R\). The symbol \(-\) is unary. Let \(\Rings\) be the axioms of ring theory with a unit:

\[\begin{split} \begin{array}{lcl} x + y & = & y + x \\ x + (y + z ) & = & (x + y) + z \\ x + 0 & = & x \\ x + (-x) & = & 0 \\ \end{array} \qquad\qquad \begin{array}{lcl} %x \times y & = & y \times x \\ x \times (y \times z ) & = & (x \times y) \times z \\ x \times 1 &=& x \\ x \times (y+z) & = & (x \times y) + (x \times z)\\ \quad \\ \end{array} \end{split}\]

We let \(\Rings\) be the sentence obtained by putting universal quantifiers \(\forall\) in front of the sentences above and then taking the conjunction \(\andd\). So it would be

\[ (\forall x)(\forall y)(x + y = y + x) \andd\cdots \andd (\forall x)(\forall y)(\forall z) (x \times (y+z) = (x \times y) + (x \times z)). \]

The main thing about rings that we need to know is that the integers \(\mathbb{Z}\) with the usual operations is a ring. As usual, we sometimes 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)\).)

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\)

The signature in this section also includes a \(9\)-place relation symbol \(R\). 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 15 that \(\varphi_{{\mathcal S}}\to 0_3\) 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 \(I_3\) the identity matrix.

Whenever \(M = (m_{i,j})\) is an integer matrix, let \(\psi_{M}\) be

\[\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}\]

Finally, for each finite set \(\mathcal{S}\) of matrices, let the sentence \(\varphi_{{\mathcal S}}\) be

\[ \Rings \andd \bigwedge_{M\in \mathcal{S}} \psi_{M} \andd R(I_3) \]

Notice that for all finite sets \(\mathcal{S}\) of matrices, \(\varphi_{{\mathcal S}}\) is a sentence of first-order logic, and the map \(\mathcal{S}\mapsto \varphi_{\mathcal{S}}\) is computable. For each finite set \(\mathcal{S}\), we have a model \(\mathbb{Z}_{\mathcal{S}}\) which satisfies \(\varphi_{\mathcal{S}}\). where we interpret \(R\) in the natural way: \(R(M)\) iff \(M\) is a product of elements of \(\mathcal{S}\). The main point to check is that \(\mathbb{Z}_{\mathcal{S}}\models \psi_M\) for all \(M\in \mathcal{S}\).

Lemma 14

If \(M_1\) is any \(3\times 3\) matrix and \(M_2\in \mathcal{S}\), then \(\proves \psi_{M_2} \andd R(M_1)\iif R(M_1\times M_2)\).

The main lemma

Lemma 15

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

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

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

Proof. (2)\(\Rightarrow\)(1). Fix \(\mathcal{S}\), and assume (2). Recall that \(\mathbb{Z}_{\mathcal{S}}\models \varphi_{\mathcal{S}}\). It follows that \(\mathbb{Z}_{\mathcal{S}}\models R(0_3) \).
The interpretation of \(R\) corresponds to the set of 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 fix \(\mathcal{S}\) and show by induction on \(i\geq 0\) that if the matrix \(M\) is a product of a sequence of \(i\) members of \(\mathcal{S}\), then \(\vdash \phi_{\mathcal{S}}\iif R(M)\).

Point (2) follows immediately from this fact and (1).

For \(i = 0\), the product of the empty sequence is \(I_3\). One of the conjuncts of \(\phi_{\mathcal{S}}\) is \(R(I_3)\), and so this base step is easy. Assume our fact for \(i\), and consider a sequence \(M_1, M_2, \ldots, M_i, M_{i+1}\) of elements of \(\mathcal{S}\). Write \(M^*\) for \(M_1 M_2 \cdots M_i\). By induction hypothesis, \(\vdash \phi_{\mathcal{S}} \iif R(M^*)\). Since \(M_{i+1}\in\mathcal{S}\), Lemma 14 implies that

\[ \vdash \psi_{M_{i+1}} \andd R(M^*)\to R(M^*\times M_{i+1}). \]

This easily gives \(\vdash \phi_{\mathcal{S}} \rightarrow R(M_1 M_2 \cdots M_i M_{i+1})\).

Lemma 15 implies the Church-Turing Theorem, Theorem 18, in view of the undecidability of matrix mortality.

Exercise 113

Prove Lemma 14, using Lemma 13. This missing piece must use something about first-order logic, since otherwise all of our work in this section would seem to use only propositional logic. The first-order logic treatment of variables and quantification must be used somewhere. Where did that come in?