8Arithmetization
In this chapter, we’ll show that all computable functions and relations on the natural numbers can be defined in the language \(\mathfrak {L}_A\) of arithmetic. As foreshadowed at the end of Chapter 5, it will follow that there can be no true, axiomatizable, and complete theory of arithmetic. Further limitative consequences will be explored in the next two chapters.
8.2 Representability
8.3 Conditions for representability I
8.4 Conditions for representability II
8.5 Wrapping up
8.1Expressing functions and relations
In Section 4.1, I introduced the language \(\mathfrak {L}_{A}\), with non-logical symbols for the number 0 (‘0’), the successor function (‘\(s\)’), addition (‘\(+\)’), and multiplication (‘\(\times \)’). Other arithmetical concepts can be defined in terms of these primitives. Let’s think about what this involves.
Back in Section 4.1, I suggested that we can define ‘\(<\)’ by stipulating that for any terms \(t_{1}\) and \(t_{2}\), ‘\(t_{1} < t_{2}\)’ is short for ‘\(\exists z (t_1 + s(z) = t_2)\)’, where \(z\) is a variable not occurring in \(t_1\) or \(t_2\). This works because every \(\mathfrak {L}_A\)-term denotes a natural number (in the standard model \(\mathfrak {N}\)), and a number \(n\) is less than a number \(m\) iff there is a non-zero number \(k\) such that \(n + k = m\).
In what follows, we’ll focus on a special kind of \(\mathfrak {L}_A\)-terms, called \(\mathfrak {L}_A\)-numerals. An \(\mathfrak {L}_A\)-numeral is a term constructed out of ‘0’, ‘\(s\)’, and the parentheses, without any occurrences of ‘\(+\)’ or ‘\(\times \)’. Every natural number is denoted by a unique \(\mathfrak {L}_{A}\)-numeral (in \(\mathfrak {N}\)): 0 is denoted by ‘0’, 1 by ‘\(s(0)\)’, 2 by ‘\(s(s(0))\)’, and so on. Since every \(\mathfrak {L}_A\)-term denotes a natural number (in \(\mathfrak {N}\)), we lose no generality by focusing on \(\mathfrak {L}_A\)-numerals.
To avoid clutter, we will use ‘\(\overline {n}\)’ as a shorthand for the \(\mathfrak {L}_{A}\)-numeral of the number \(n\). So \(\overline {0}\) is ‘0’ and \(\overline {5}\) is ‘\(s(s(s(s(s(0)))))\)’. More generally, whenever \(t\) is a metalinguistic expression for a number, ‘\(\overline {t}\)’ is the \(\mathfrak {L}_{A}\)-numeral for that number. For example, \(\overline {\sqrt {4}}\) is ‘\(s(s(0))\)’ because ‘\(s(s(0))\)’ is the \(\mathfrak {L}_{A}\)-numeral for the square root of 4 (i.e., for 2).
Now return to the less-than relation. For any numbers \(n\) and \(m\), \(n < m\) iff \(\exists z(\overline {n} + s(z) = \overline {m})\) is true in \(\mathfrak {N}\). In that sense, \(\exists z(\overline {n} + s(z) = \overline {m})\) expresses in \(\mathfrak {L}_{A}\) that \(n\) is less than \(m\). If we replace \(\overline {n}\) and \(\overline {m}\) by variables \(x\) and \(y\), we get the formula \(\exists z(x + s(z) = y)\). This can be seen as a template for expressing less-than statements. The free variables \(x\) and \(y\) are placeholders. To form a less-than statement about particular numbers, one replaces the placeholders by \(\mathfrak {L}_{A}\)-terms. We’ll say that \(\exists z(x + s(z) = y)\) expresses the less-than relation in \(\mathfrak {L}_{A}\). More generally:
An \(\mathfrak {L}_{A}\)-formula \(A(x_{1},\ldots ,x_{k})\) expresses an \(k\)-place relation \(R\) on \(\mathbb {N}\) iff, for all numbers \(n_{1},\ldots ,n_{k}\), \(\mathfrak {N} \Vdash A(\overline {n_{1}},\ldots ,\overline {n_{k}})\) iff \(R\) holds of \(n_{1},\ldots ,n_{k}\).
We’ve talked about expressing relations. We can express functions. For example, we might say that the \(\mathfrak {L}_A\)-expression \(x \times x\) expresses the squaring function that maps any number \(n\) to \(n^2\). Often, however, a function won’t be expressible in this way by an \(\mathfrak {L}_{A}\)-term. Instead, we have to resort to what I called a “syncategorematic” definition in Section 4.2. For example, there is no \(\mathfrak {L}_{A}\)-term ‘\(t(x)\)’ that expresses the factorial function in the sense that for all numbers \(n\), ‘\(t(\overline {n})\)’ denotes (in \(\mathfrak {N}\)) the factorial of \(n\) (i.e., the number \(1 \times 2 \times \ldots \times n\)). There is, however, an \(\mathfrak {L}_{A}\)-formula \(F(x,y)\) such that \(F(\overline {n},\overline {m})\) is true (in \(\mathfrak {N}\)) iff \(m\) is the factorial of \(n\). With the help of this formula, any statement about factorials can be expressed in \(\mathfrak {L}_{A}\). The (false) statement that every number is less than its factorial, for example, can be expressed as \[ \forall x \forall y(F(x,y) \to x < y). \]
An \(\mathfrak {L}_{A}\)-formula \(A(x_{1},\ldots ,x_{k},y)\) expresses a (total) \(k\)-ary function \(f\) on \(\mathbb {N}\) iff, for all numbers \(n_{1},\ldots ,n_{k},m\), \(\mathfrak {N} \Vdash A(\overline {n_{1}},\ldots ,\overline {n_{k}},\overline {m})\) iff \(f(n_{1},\ldots ,n_{k}) = m\).
Definition 8.2 could be extended to partial functions, but we’ll only be interested in total functions from now on.
We say that a relation or function is expressible in \(\mathfrak {L}_{A}\) if it is expressed by some \(\mathfrak {L}_{A}\)-formula. (Many textbooks use the term ‘definable’ instead of ‘expressible’: the less-than relation is then said to be defined by the \(\mathfrak {L}_A\)-formula \(\exists z(x + s(z) = y)\).)
We’ll show that all recursive functions and relations – and therefore all computable functions and relations – are expressible in \(\mathfrak {L}_{A}\). This is not obvious. The factorial function, for example, is computable, but it is hard to find an \(\mathfrak {L}_{A}\)-formula \(F(x,y)\) that expresses it. (Try it!)
For a different type of example, consider the halting-with-bound relation that holds between the code number of a Turing machine \(M\), a number \(n\), and a number \(k\) iff \(M\) halts on input \(n\) within \(k\) steps. This relation is computable: we can simply run \(M\) on \(n\) for \(k\) steps, and return ‘yes’ if \(M\) has halted by then, and ‘no’ otherwise. Since all computable relations are expressible in \(\mathfrak {L}_{A}\), there must be an \(\mathfrak {L}_A\)-expression \(H(x,y,z)\) so that \(H(\overline {m},\overline {n},\overline {k})\) is true (in \(\mathfrak {N}\)) iff the Turing machine coded by \(m\) halts on input \(n\) within \(k\) steps. It’s not at all obvious what such a formula would look like.
As I mentioned in Section 5.5, the expressibility of halting-with-bound leads to a version of Gödel’s incompleteness theorem. If \(H(x,y,z)\) expresses halting-with-bound then \(\exists z H(x,y,z)\) expresses the halting relation: \(\exists z H(\overline {m},\overline {n},z)\) is true (in \(\mathfrak {N}\)) iff the Turing machine coded by \(m\) halts on input \(n\). We know from Theorem 6.1 that there is no algorithm that decides the halting relation. It follows that there can be no complete, axiomatizable, and true theory of arithmetic: otherwise we could decide the halting relation by checking, for any numbers \(m\) and \(n\), whether \(\exists z H(\overline {m},\overline {n},z)\) or its negation is entailed by the axioms.
This version of the incompleteness theorem is sometimes called “semantic”, as it concerns theories that are true. Gödel himself gave prominence to a “syntactic” version of incompleteness that (in its contemporary form) only requires the relevant theories to be consistent. The syntactic theorem relies not on expressibility in \(\mathfrak {L}_{A}\) but on a slightly stronger concept – representability – that I’m going to introduce next.
Explain why the Busy Beaver function \(\Sigma \) is expressible in \(\mathfrak {L}_{A}\). (Hint: consider the relation that holds between four numbers \(m\), \(n\), \(t\), \(k\) iff \(m\) codes a Turing machine with \(n\) states that halts, on blank input, after \(t\) steps leaving \(k\) strokes on the tape.)
8.2Representability
‘\(+\)’, ‘\(\times \)’, ‘\(s\)’ and ‘0’ are non-logical symbols. They have an intended interpretation, but this interpretation isn’t built into the language. An axiomatic \(\mathfrak {L}_{A}\)-theory doesn’t automatically “know” what the non-logical symbols mean. ‘\(0\)’ and ‘\(s(0)\)’, for example, denote different numbers in the intended interpretation, but an axiomatic theory may not be able to prove ‘\(0 \ne s(0)\)’.
The standard axiomatic theory of arithmetic, Peano Arithmetic (PA), can prove \(0 \ne s(0)\). Indeed, whenever \(n \ne m\), PA contains \(\overline {n} \ne \overline {m}\). Trivially, if \(n=m\) then PA contains \(\overline {n} = \overline {m}\), for then \(\overline {n}\) and \(\overline {m}\) are the same term. So PA knows all particular facts about equality between numbers: that \(\overline {17} = \overline {17}\), that \(\overline {17} \ne \overline {29}\), and so on.
PA also knows all particular facts about the less-than relation: whenever \(n < m\), PA contains \(\overline {n} < \overline {m}\), and whenever \(n \not < m\), PA contains \(\neg (\overline {n} < \overline {m})\). Of course, ‘\(<\)’ isn’t really part of the language. What I mean is that whenever \(n < m\), PA contains \(\exists z(\overline {n} + s(z) = \overline {m})\), and whenever \(n \not < m\), PA contains \(\neg \exists z(\overline {n} + s(z) = \overline {m})\). In that sense, \(\exists z(x + s(z) = y)\) represents the less-than relation in PA.
An \(\mathfrak {L}_{A}\)-formula \(A(x_{1},\ldots ,x_{k})\) represents a \(k\)-ary relation \(R\) on \(\mathbb {N}\) in a theory \(T\) iff, for all numbers \(n_{1},\ldots ,n_{k}\),
- (i)
- if \(R\) holds of \(n_{1},\ldots ,n_{k}\), then \(\vdash _{T} A(\overline {n_{1}},\ldots ,\overline {n_{k}})\), and
- (ii)
- if \(R\) does not hold of \(n_{1},\ldots ,n_{k}\), then \(\vdash _{T} \neg A(\overline {n_{1}},\ldots ,\overline {n_{k}})\).
We can also talk about representing functions:
An \(\mathfrak {L}_{A}\)-formula \(A(x_{1},\ldots ,x_{k},y)\) represents a (total) \(k\)-ary function \(f\) on \(\mathbb {N}\) in \(T\) iff, for all numbers \(n_{1},\ldots ,n_{k}\),
- (i)
- \(\vdash _{T} A(\overline {n_{1}},\ldots ,\overline {n_{k}},\overline {f(n_{1},\ldots ,n_{k})})\), and
- (ii)
- \(\vdash _{T} \forall y(A(\overline {n_{1}},\ldots ,\overline {n_{k}},y) \to y = \overline {f(n_{1},\ldots ,n_{k})})\).
Here, \(\overline {f(n_1,\ldots ,n_k)}\) is the \(\mathfrak {L}_A\)-term with \(f(n_1,\ldots ,n_k)\) occurrences of ‘\(s\)’. Condition (ii) effectively requires \(T\) to know that \(A(x_{1},\ldots ,x_{k},y)\) expresses a functional relationship (as discussed in Section 4.2).
An example may help. What is needed for a formula \(F(x,y)\) to represent the factorial function in a theory \(T\)? Condition (i) requires that whenever \(m\) is the factorial of \(n\) then \(T\) proves \(F(\overline {n},\overline {m})\). This leaves open that \(T\) also proves \(F(\overline {n},\overline {k})\) for some \(k \not = m\). Indeed, the formula \(x\!=\!x \land y\!=\!y\) passes condition (i) in any theory \(T\), but there’s no good sense in which this formula represents the factorial function. By condition (ii), \(T\) must know that there is no \(y\) other than \(m\) for which \(F(\overline {n},y)\) holds.
If a function or relation is represented in a theory \(T\) by some formula, we say that the function or relation is representable in \(T\).
If an \(\mathfrak {L}_{A}\)-formula represents a function in a theory \(T \subseteq \mathrm {Th}(\mathfrak {N})\), then the formula also expresses that function.
Proof. Assume \(A(x,y)\) represents a function \(f\) in a theory \(T\), where \(T \subseteq \mathrm {Th}(\mathfrak {N})\). I’ll assume for readability that \(f\) is one-place. We have to show that for all numbers \(n,m\), \(A(\overline {n},\overline {m})\) is true in \(\mathfrak {N}\) iff \(f(n) = m\). For the ‘if’ direction, assume that \(f(n) = m\). By condition (i) in definition 8.4, \(\vdash _{T} A(\overline {n},\overline {m})\). Since \(T \subseteq \mathrm {Th}(\mathfrak {N})\), \(A(\overline {n},\overline {m})\) is true in \(\mathfrak {N}\). For the ‘only if’ direction, assume that \(f(n) \not = m\). By condition (ii) in definition 8.4, \(\vdash _{T} \forall y(A(\overline {n},y) \to y = \overline {f(n)})\). So \(\forall y(A(\overline {n},y) \to y = \overline {f(n)})\) is true in \(\mathfrak {N}\). Since \(\overline {f(n)} \not = \overline {m}\) is true in \(\mathfrak {N}\), it follows that \(\neg A(\overline {n},\overline {m})\) is true in \(\mathfrak {N}\), and so \(A(\overline {n},\overline {m})\) is false in \(\mathfrak {N}\). □
In the following sections, we’ll show that all computable functions are representable in any arithmetical theory that knows some basic facts about arithmetic. It will follow by Proposition 8.1 that all computable functions are expressible in \(\mathfrak {L}_{A}\).
We can focus on functions because a relation is copmutable iff its characteristic function is computable. As the next proposition shows, the representability of all computable functions in a theory entails the representability of all computable relations, if the theory can prove \(0 \not = 1\).
A relation \(R\) is representable in a theory \(T\) iff its characteristic function \(\chi _{R}\) is representable in \(T\), provided that \(\vdash _{T} \overline {0} \not = \overline {1}\).
Proof. I’ll assume for readability that \(R\) is a one-place relation.
For the left-to-right direction, assume that \(R\) is represented in \(T\) by some formula \(A(x)\). Let \(C(x,y)\) be the formula \((A(x) \land y\!=\overline {1}) \lor (\neg A(x) \land y\!=\!0)\). I claim that \(C(x,y)\) represents the characteristic function \(\chi _{R}\) of \(R\). Assume first that \(\chi _{R}(n) = 1\). Then \(R\) holds of \(n\), and \(T\) proves \(A(\overline {n})\). Since \(A(\overline {n})\) entails both \(C(\overline {n},\overline {1})\) and \(\forall y(C(\overline {n},y) \to y = \overline {1})\), \(T\) proves both of these as well. Similarly, if \(\chi _{R}(n) = 0\), then \(T\) proves \(\neg A(\overline {n})\), which entails \(C(\overline {n},0)\) and \(\forall y(C(\overline {n},y) \to y = \overline {0})\). So whenever \(\chi _{R}(n) = m\) then \(T\) proves \(C(\overline {n},\overline {m})\) and \(\forall y(C(\overline {n},y) \to y = \overline {m})\). So \(C(x,y)\) satisfies the two conditions in definition 8.4.
For the other direction, assume \(A(x,y)\) represents \(\chi _{R}\) in \(T\). This means that whenever \(R\) holds of \(n\), then \(\vdash _{T} A(\overline {n},\overline {1})\), by condition (i) in definition 8.4. Moreover, when \(R\) does not hold of \(n\), then \(\vdash _{T} A(\overline {n},\overline {0})\) by condition (i) and \(\vdash _{T} \forall yA(\overline {n},y) \to y=\overline {0}\) by condition (ii). Assuming that \(\vdash _{T} \overline {0} \not = \overline {1}\), it follows that \(A(x,1)\) represents \(R\) in \(T\). □
8.3Conditions for representability I
We want to show that every computable total function is representable in any theory that knows some basic facts about arithmetic. Remember that ‘computable’ has a precise meaning: a total function is computable iff it is recursive. Since every recursive function is constructed from the base functions zero, successor, and projection by composition, primitive recursion, and regular minimization, we can show that all computable functions are representable in a theory \(T\) by showing, first, that the base functions are representable in \(T\), and then that representability in \(T\) is preserved under composition, primitive recursion, and regular minimization.
Let’s start with the zero function \(z\) that maps every number \(n\) to \(0\). It’s not hard to find a formula \(A(x,y)\) so that \(A(\overline {n},\overline {m})\) is true (in \(\mathfrak {N}\)) iff \(m = 0\). The formula \(x\!=\!x \land y\!=\!0\) does the job. So \(x\!=\!x \land y\!=\!0\) expresses \(z\) in \(\mathfrak {L}_{A}\). We need to confirm that it also represents \(z\) in any suitable theory \(T\).
Proof. I claim that \(z\) is represented in every theory \(T\) by the formula \(x\!=\!x \land y\!=\!0\). By definition 8.4, this means that, for all numbers \(n\), \(T\) can prove
- (i)
- \(\overline {n}\!=\overline {n} \land 0\!=\!0\), and
- (ii)
- \(\forall y((\overline {n}\!=\overline {n} \land y\!=\!0) \to y \!=\! 0)\).
Both of these are logical truths. □
Proof. I claim that \(s(x)=y\) represents the successor function in every theory \(T\): for all numbers \(n\), \(T\) can prove
- (i)
- \(s(\overline {n}) = \overline {s(n)}\), and
- (ii)
- \(\forall y(s(\overline {n})=y \to y = \overline {s(n)})\).
Since \(\overline {s(n)}\) and \(s(\overline {n})\) are the same term, both of these are logical truths. □
Proof. Exercise.
Prove Lemma 8.3.
Now for the closure operations. We start with composition.
If a \(k\)-place function \(f\) is representable in a theory \(T\) and \(k\) functions \(g_{1},\ldots ,g_{k}\) are representable in \(T\), then their composition \(h = Cn[f,g_{1},\ldots ,g_{k}]\) is representable in \(T\).
Proof. For readability, I assume that \(k=2\) and that \(g_{1}\) and \(g_{2}\) are one-place functions.
Assume that \(f\) is represented in a theory \(T\) by a formula \(F(x_{1},x_{2},y)\), and that \(g_{1}\), \(g_{2}\) are represented in \(T\) by \(G_{1}(x,y_{1})\) and \(G_{2}(x,y_{2})\), respectively. I claim that \(h = Cn[f,g_{1},g_{2}]\) is represented in \(T\) by the formula \[ \exists v_{1}\exists v_{2}(G_{1}(x,v_{1}) \land G_{2}(x,v_{2}) \land F(v_{1},v_{2},y)). \]
Condition (i) for representations requires that whenever \(h(n) = m\) then \[ \vdash _{T} \exists v_{1}\exists v_{2}(G_{1}(\overline {n},v_{1}) \land G_{2}(\overline {n},v_{2}) \land F(v_{1},v_{2},\overline {m})). \] So assume \(h(n) = m\). Then there are \(k_{1},k_{2}\) such that \(g_{1}(n) = k_{1}\), \(g_{2}(n) = k_{2}\), and \(f(k_{1},k_{2}) = m\). Since \(g_{1}\) and \(g_{2}\) are represented by \(G_{1}(x,y_{1})\) and \(G_{2}(x,y_{2})\), respectively, and \(f\) is represented by \(F(x_{1},x_{2},y)\), we have \begin {flalign*} \quad & \vdash _{T} G_{1}(\overline {n},\overline {k_{1}}) &\\[0.5em] \quad & \vdash _{T} G_{2}(\overline {n},\overline {k_{2}}) &\\[0.5em] \quad & \vdash _{T} F(\overline {k_{1}},\overline {k_{2}},\overline {m}). & \end {flalign*}
The desired claim follows by the fact that \(T\) is closed under first-order consequence.
For condition (ii), we have to show that \[ \vdash _{T} \forall y(\exists v_{1}\exists v_{2}(G_{1}(\overline {n},v_{1}) \land G_{2}(\overline {n},v_{2}) \land F(v_{1},v_{2},y)) \,\to \, y\!=\overline {f(g_{1}(a),g_{2}(a))}). \] This, too, follows from the representability conditions for \(F\), \(G_{1}\), and \(G_{2}\), which yield \begin {flalign*} \quad & \vdash _{T} \forall y(G_{1}(\overline {n},y) \,\to \, y\!=\overline {k_{1}}) &\\[0.5em] \quad & \vdash _{T} \forall y(G_{2}(\overline {n},y) \,\to \, y\!=\overline {k_{2}}) &\\[0.5em] \quad & \vdash _{T} \forall y(F(\overline {c_{1}},\overline {c_{2}},y) \,\to \, y\!=\overline {f(c_{1},c_{2})}). & \end {flalign*}
□
I leave the case of primitive recursion for last: it is by far the hardest. Let’s turn to regular minimization. Suppose \(h = \mathrm {Mn}[f]\), where \(f\) is a regular function. Recall that \(f(x, y)\) is regular if it is total and for all \(x\) there is some \(y\) such that \(f(x, y) = 0\). The function \(h\) takes a number \(x\) and returns the least \(y\) for which \(f(x,y)=0\). Assuming that \(f\) is represented in \(T\) by some formula \(F(x,y,z)\), we have: \(h(x) = y\) iff \(F(x,y,0)\) and there is no \(z < y\) such that \(F(x,z,0)\). We can directly translate this into \(\mathfrak {L}_{A}\): \[ F(x,y,0) \land \forall z(z < y \;\to \; \neg F(x,z,0)). \] This formula expresses \(h\) in \(\mathfrak {L}_A\). Some assumptions are needed for it to represent \(h\) in a theory \(T\). Informally speaking, the theory must have some idea of what \(<\) means. The following conditions are sufficient.
R1 \(\text {For all }n\text {, }\vdash _{T} \forall x (\overline {n} < x \;\lor \; x = \overline {n} \;\lor \; x < \overline {n})\text {.}\) R2 \(\vdash _{T} \neg \exists x (x < 0)\text {.}\) R3 \(\text {For all }n > 0\text {, }\vdash _{T} \forall x (x < \overline {n} \;\to \; (x = 0 \;\lor \; \ldots \;\lor \; x = \overline {n-1}))\text {.}\) R4\(^{-}\) \(\text {For all }n > 0, \vdash _{T} \overline {n} \ne 0\)
Officially, ‘<’ isn’t part of the language. I assume here, and in what follows, that ‘\(t_{1} < t_{2}\)’ is short for ‘\(\exists z(s(z) + t_{1} = t_{2})\)’, where \(z\) is a variable that doesn’t occur in \(t_{1}\) or \(t_{2}\).
If a regular function \(f\) is representable in a theory \(T\), and \(T\) satisfies the conditions R1, R2, R3, and R4\(^{-}\), then the minimization \(\mathrm {Mn}[f]\) of \(f\) is representable in \(T\).
Proof. Assume that \(f\) is a 2-place function represented in \(T\) by \(F(x,y,z)\), where \(T\) satisfies R1, R2, R3, and R4\(^{-}\). I claim that \(h = \mathrm {Mn}[f]\) is represented in \(T\) by \(F(x,y,0) \land \forall z(z < y \;\to \; \neg F(x,z,0))\). We have to confirm that whenever \(h(n) = m\) then \(T\) can prove
- (i)
- \(F(\overline {n},\overline {m},0) \land \forall z(z < \overline {m} \,\to \, \neg F(\overline {n},z,0))\).
- (ii)
- \(\forall y(F(\overline {n},y,0) \land \forall z(z < y \,\to \, \neg F(\overline {n},z,0)) \,\to \, y = \overline {m})\).
From the fact that \(h = \mathrm {Mn}[f]\) and \(h(n) = m\), we know that \(f(n,m) = 0\) and \(f(n,k) \neq 0\) for all \(k < m\). Since \(f\) is represented in \(T\) by \(F\), \(T\) can prove \begin {equation} \tag {1} F(\overline {n},\overline {m},0) \end {equation} as well as (for \(k<m\)) \begin {equation} \tag {2} \forall y(F(\overline {n},\overline {k},y) \,\to \, y = \overline {f(n,k)}). \end {equation} From (2) and R4\(^{-}\), it follows that \(T\) can prove \(\neg F(\overline {n},\overline {k},0)\) for all \(k < m\). By R3, \(T\) can prove \(\forall z(z < \overline {m} \,\to \, (z = 0 \lor \ldots \lor z = \overline {m-1}))\) whenever \(m > 0\). So if \(m>0\) then \(T\) can prove \begin {equation} \tag {3} \forall z(z < \overline {m} \,\to \, \neg F(\overline {n},z,0)). \end {equation} For \(m = 0\), (3) follows from R2. (i) is the conjunction of (1) and (3).
For (ii), we show (by reasoning “inside \(T\)”) that \(T\) can derive \(y = \overline {m}\) from \begin {equation} \tag {4} F(\overline {n},y,0) \land \forall z(z < y \,\to \, \neg F(\overline {n},z,0)). \end {equation} (1) and (4) imply \(\neg (\overline {m} < y)\). From (3) and (4), we have \(\neg (y < \overline {m})\). By R1, it follows that \(y = \overline {m}\). □
Now for the hard part: primitive recursion.
8.4Conditions for representability II
Return to the factorial function \(\mathrm {fac}\) that maps each number \(n\) to \(n! = 1 \times 2 \times \ldots \times n\). The primitive recursive definition goes as follows: \begin {align*} \mathrm {fac}(0) & = 1 \\[0.5em] \mathrm {fac}(s(y)) & = s(y) \times \mathrm {fac}(y). \end {align*}
We need to find a formula \(F(x,y)\) that expresses this function in \(\mathfrak {L}_{A}\).
The trick is to see the recursive definition as defining a sequence: \(\langle \mathrm {fac}(0), \mathrm {fac}(1), \mathrm {fac}(2), \ldots \rangle \). Our formula \(F(x,y)\) will say “\(y\) is the last element of the sequence \(\langle \mathrm {fac}(0), \ldots , \mathrm {fac}(x) \rangle \)”.
Of course, \(\mathfrak {L}_{A}\) doesn’t have terms for sequences. But we know that sequences of numbers can be coded as single numbers. Suppose we can find a formula \({\scriptstyle \class {smallcaps}{\text {ENTRY}}}(x,i,y)\) that expresses “\(y\) is the \(i\)-th entry in the sequence coded by \(x\)”. Using \({\scriptstyle \class {smallcaps}{\text {ENTRY}}}(x,i,y)\), we can then construct a formula \({\scriptstyle \class {smallcaps}{\text {SEQ}}}(z,x)\) saying that
- (i)
- \(z\) codes a sequence whose first entry is 1, and
- (ii)
- for all \(i<x\), the \(s(i)\)-th entry in the sequence coded by \(z\) is the product of the \(i\)th entry and \(s(i)\).
So \({\scriptstyle \class {smallcaps}{\text {SEQ}}}(z,x)\) will say that \(z\) codes the sequence \(\langle \mathrm {fac}(0), \mathrm {fac}(1), \ldots , \mathrm {fac}(x) \rangle \). From this, we can express \(F(x,y)\) as \(\exists z({\scriptstyle \class {smallcaps}{\text {SEQ}}}(z,x) \land {\scriptstyle \class {smallcaps}{\text {ENTRY}}}(z,s(x),y))\). This says that there is a number \(z\) that codes \(\langle \mathrm {fac}(0), \ldots , \mathrm {fac}(x) \rangle \) that \(y\) is the \(s(x)\)-th entry in that sequence. (We need an \(s(x)\) here because \(F(x,0)\) is the first, not the zero-th, entry in the sequence, and so \(\mathrm {fac}(x)\) is the \(s(x)\)-th entry.)
The main task, then, is to find the formula \({\scriptstyle \class {smallcaps}{\text {ENTRY}}}(x,i,y)\) that holds of numbers \(x,i,y\) iff \(y\) is the \(i\)-th entry in the sequence coded by \(x\).
You may remember that in Section 7.2 I showed how to define a primitive recursive function \(\mathrm {entry}(x,y)\) that returns the \(y\)-th number in the sequence coded by \(x\), using the prime exponents method to code sequences of numbers. Unfortunately, my definition of the \(\mathrm {entry}\) function involved primitive recursion, so we can’t assume that this function is expressible in \(\mathfrak {L}_{A}\). In fact, we won’t code sequences of numbers in terms of prime exponents, as we don’t even have an \(\mathfrak {L}_{A}\)-formula for exponentiation yet. We’ll use a different coding method.
To explain that method, assume first that we want to code a sequence \(\langle n_{1}, n_{2}, \ldots , n_{k} \rangle \) of numbers all of which are below 9. We could simply concatenate their decimal representation: \(\langle 1,7,0,7 \rangle \) would be coded as \(1707\). To simplify accessing individual elements of the sequence, we might store the indices (the position numbers) of the elements in the code, so that \(\langle 1,7,0,7 \rangle \) gets coded as \(11273047\). The third element can now be identified as the digit to the right of the ’3’ (in decimal representation). As it stands, this doesn’t quite work because the indices can also be among the coded elements, as is the case for the number 1 in the example: there are two digits to the right of a ’1’. We can disambiguate the indices by prefixing them with yet another digit, 9, that doesn’t occur among the coded numbers. The code of \(\langle 1,7,0,7 \rangle \) becomes \(911927930947\). The \(i\)-th element can now be retrieved as the unique digit to the right of ’\(9i\)’ (in decimal representation).
We’ll adapt this scheme to code arbitrary sequences of numbers. We obviously can’t assume that all of the numbers are below 9. We therefore code sequences not to base 10, but to some base \(p\) that is at least 2 greater than all numbers in the sequence and all index numbers (\(p\!-\!1\) is used to mark the index numbers). For convenience, we’ll always use a prime number as the base \(p\). The sequence \(\langle 1, 12, 0 \rangle \), for example, would be coded in base 17 as \[ 16 \pconcatseventeen 1 \pconcatseventeen 1 \pconcatseventeen 16 \pconcatseventeen 2 \pconcatseventeen 12 \pconcatseventeen 16 \pconcatseventeen 3 \pconcatseventeen 0, \] where ‘\(\pconcatseventeen \)’ is the operation of concatenation in base 17. (I’ll define this formally below.) If \(q\) is the code number of a sequence in base \(p\), the \(i\)-th element of the sequence can be retrieved as
\(\mathrm {alpha}(p,q,i)\) = the unique number \(x\) for which \((p\!-\!1) \pconcat i \pconcat x\) is part of the base-\(p\) numeral of \(q\).
We’ll see that this can be expressed in \(\mathfrak {L}_{A}\).
The \(\mathrm {alpha}\) function retrieves elements from the code \(q\) of a sequence, but it also needs the base \(p\) as a key to the code. We can get rid of the extra argument by coding \(\langle p,q \rangle \) into a single number. We have to use a different coding method here. We’ll use the pairing function that we met in Section 3.1 when we discussed Cantor’s zig-zag method: \[ \mathrm {j}(x,y) = \frac {\mbox {\small 1}}{\mbox {\small 2}} (x+y)(x+y+1)+y \]
The \(\mathrm {j}\) function is easily expressed in \(\mathfrak {L}_{A}\). We can also express two functions \(\mathrm {lft}\) and \(\mathrm {rgt}\) that extract the elements of a pair encoded by \(\mathrm {j}\), so that \(\mathrm {lft}(\mathrm {j}(x,y)) = x\) and \(\mathrm {rgt}(\mathrm {j}(x,y)) = y\). If we have coded a sequence of numbers \(\langle n_{1},\ldots ,n_{k} \rangle \) by \(p\) and \(q\) as described above, and packaged these into a single number \(c = \mathrm {j}(p,q)\), we can now retrieve any element \(n_{i}\) of the doubly coded sequence as \[ \text {beta}(c,i) = \text {alpha}(\mathrm {lft}(c),\mathrm {rgt}(c),i). \] We’ll show that this function \(\mathrm {beta}\) is expressible in \(\mathfrak {L}_{A}\). The formula \({\scriptstyle \class {smallcaps}{\text {BETA}}}(x,y,z)\) that expresses it is the formula \({\scriptstyle \class {smallcaps}{\text {ENTRY}}}(x,y,z)\) that we were looking for.
I’m not actually going to write down \({\scriptstyle \class {smallcaps}{\text {BETA}}}(x,y,z)\) as an \(\mathfrak {L}_A\)-formula. Instead, I’ll show that the function \(\mathrm {beta}\) can be defined by composition and (regular) minimization from certain functions that are easily expressible in \(\mathfrak {L}_{A}\). Since expressibility is preserved under composition and (regular) minimization, it follows that \(\mathrm {beta}\) is expressible.
The base functions I’ll need to define \(\mathrm {beta}\) are projection, addition, multiplication, and the characteristic function \(\chi _=\) of identity. This is the two-place function that returns 1 if its two arguments are equal and 0 otherwise. It is expressed in \(\mathfrak {L}_A\) by \(({x\!=\!y} \land {z\!=\!1}) \lor ({x\neq \!y} \land {z\!=\!0})\). Projection, addition, and multiplication are also easily expressible. We’ve dealt with projection in Lemma 8.3. Addition is expressed by \(x+y = z\); multiplication by \(x \times y = z\). To ensure that these formulas also represent the relevant functions in a theory \(T\), we need the following assumptions:
R4 \(\text {For all }n, m\text {, if }n \neq m\text { then }\vdash _{T} \overline {n} \neq \overline {m}\text {.}\) R5 \(\text {For all }n, m\text {, }\vdash _{T} \overline {n} + \overline {m} = \overline {n+m}\text {.}\) R6 \(\text {For all }n, m\text {, }\vdash _{T} \overline {n} \times \overline {m} = \overline {n\times m}\text {.}\)
Note that R4 subsumes R4\(^{-}\).
Projection, addition, multiplication, and \(\chi _=\) are representable in every theory that satisfies R4–R6.
Proof. Projection is representable in every theory by Lemma 8.3.
The addition function is represented by \(x+y=z\) in every theory \(T\) that satisfies R5: condition (i) in the definition of representation is given by R5; condition (ii) then holds by first-order logic.
The multiplication function is represented by \(x\times y=z\) in every theory \(T\) that satisfies R6: condition (i) is given by R6; (ii) holds by first-order logic.
\(\chi _=\) is represented by \((x\!=\!y \land z\!=\!1) \lor (x\neq \!y \land z\!=\!0)\) in every theory \(T\) that satisfies R4. For condition (i), we need to show that if \(\chi _= (n,m) = k\) then \(\vdash _T {( \overline {n}\!=\overline {m} \land \overline {1}\!=\overline {k})} \lor {(\overline {n}\neq \overline {m} \land \overline {0}\!=\overline {k})}\). There are two ways in which \(\chi _=(n,m) = k\) can hold: either \(n=m\) and \(k=1\) or \(n \neq m\) and \(k=0\). In the first case, \(\overline {n}=\overline {m}\) and \(\overline {1}=\overline {k}\) are logical truths. In the second case, \(\overline {0}=\overline {k}\) is a logical truth and \(\overline {n}\neq \overline {m}\) holds by R4. Condition (ii) holds by first-order logic. □
Now we need to show that \(\mathrm {beta}\) can be defined from projection, addition, multiplication, and \(\chi _=\) by composition and minimization. To this end, let’s first introduce a name for the class of functions that can be so constructed. I’ll call a function tame if it can be defined from projection, addition, multiplication, and \(\chi _=\) by composition and regular minimization; I’ll call a relation tame if its characteristic function is tame.
The following lemmas show that the class of tame relations is closed under truth-functional combinations, bounded quantification, and regular minimization. We’ve met the first two of these operations in Section 7.2. For the third, recall that the minimization \(\mu y\, R(x_{1},\ldots ,x_{n},y)\) of an \(n\!+\!1\)-ary relation \(R\) is the \(n\)-ary function that maps \(x_{1},\ldots ,x_{n}\) to the least \(y\) such that \(R(x_{1},\ldots ,x_{n},y)\). Regular minimization for relations is minimization applied to a relation that is regular in the sense that for all \(x_{1},\ldots ,x_{n}\) there is some \(y\) such that \(R(x_{1},\ldots ,x_{n},y)\).
Proof. Let \(R\) and \(S\) be tame relations (of arity 1, for readability), and \(\chi _R\) and \(\chi _S\) their characteristic functions. Then \begin {align*} \chi _{R \land S}(x) &= \chi _{R}(x) \times \chi _{S}(x)\\[0.5em] \chi _{\neg R}(x) &= \chi _=(\chi _{R}(x),0). \end {align*}
All truth-functional combinations can be constructed from conjunction and negation. □
Proof. Let \(R(x_{1},\ldots ,x_{n},y)\) be a regular tame relation. Then \(\mu y\, R(x_{1},\ldots ,x_{n},y)\) is \(\mathrm {Mn}[\chi _{\neg R}]\). Since \(\chi _{\neg R}\) is tame by Lemma 8.7, so is \(\mathrm {Mn}[\chi _{\neg R}]\). □
The tame relations are closed under bounded quantification: if \(R(x_{1},\ldots ,x_{n},z)\) is a tame \(n\!+\!1\)-ary relation, then so are the \(n\!+\!1\)-ary relations \(\forall z \leq y\, R(x_{1},\ldots ,x_{n},z)\) and \(\exists z \leq y\, R(x_{1},\ldots ,x_{n},z)\).
Proof. Let \(R(x_{1},\ldots ,x_{n},z)\) be a tame relation. For readability, I assume \(n=1\). Let \(d(x,y) = \mu z [\neg R(x,z) \lor y=z]\). By Lemma 8.7, \(\mu z\) is here applied to a tame relation, and the final disjunct ensures that the relation is regular. So \(d\) is tame by Lemma 8.8. If \(d(x,y) < y\) then \(\neg R(x,d(x,y))\); if \(d(x,y) = y\) then \(\forall z \leq y\, R(x,z)\). So \(\forall z \leq y\, R(x,z)\) holds iff \(d(x,y) = y\). (I.e., \(\chi _{\forall z \leq y\, R(x,z)}(x,y) = \chi _=(d(x,y),y)\).)
Since \(\exists z \leq y\, R(x,z)\) is equivalent to \(\neg \forall z \leq y\, \neg R(x,z)\), it is tame by Lemma 8.7. □
Now I’ll show that the \(\mathrm {beta}\) function is tame. It immediately follows that it is representable in any theory that satisfies R1–R6:
There is a function \(\mathrm {beta}\) such that for any finite sequence \(\langle n_{1}, \ldots , n_{k} \rangle \) of natural numbers, there is a number \(c\) such that \(\mathrm {beta}(c,i) = n_{i}\) for all \(1 \leq i \leq k\). Moreover, \(\mathrm {beta}\) is representable in any theory that satisfies R1–R6.
Proof. We use the coding method described above: given a sequence \(\langle n_{1},\ldots ,n_{k} \rangle \), let \(p\) be the smallest prime that’s at least 2 greater than all of \(n_{1},\ldots ,n_{k}\) and \(k\); let \(q\) be the base-\(p\) numeral built as \((p\!-\!1) \pconcat 1 \pconcat n_{1} \pconcat \ldots \pconcat (p\!-\!1) \pconcat k \pconcat n_{k}\); let \(c = \mathrm {j}(p,q)\). I’ll show that we can construct a function \(\mathrm {beta}(c,i)\) that retrieves the \(i\)-th element from the sequence coded by \(c\):
\begin {align*} x < y &\Leftrightarrow \exists z\le \!x (s(z) = y).\\[0.5em] \mathrm {Divides}(x,y) &\Leftrightarrow \exists z\le \!y\,(y=x\times z).\\[0.5em] \mathrm {Prime}(x) &\Leftrightarrow x \ne 0 \land x \ne 1 \land \forall y\leq \!x\,(\mathrm {Divides}(y,x) \,\to \, y\!=\!1 \,\lor \, y\!=\!x).\\[0.5em] \mathrm {Pow}(x,p) &\Leftrightarrow x\not =\!0 \,\land \, \mathrm {Prime}(p) \land \, \forall y\le \!x\, (\mathrm {Divides}(y,x) \,\to \, y\!=\!1 \,\lor \, \mathrm {Divides}(p,y))\\[0.5em] &\quad \text {\;\;(in words: $x$ is a power of the prime $p$)}.\\[0.5em] \eta (p,x) &= \mu y \,((\mathrm {Pow}(y,p) \,\land \, \, x\!<\!y \,\land \, 1\!<\!y) \, \lor \, (\neg \mathrm {Prime}(p) \,\land \, y\!=\!0))\\[0.5em] &\quad \text {\;\;(the smallest power of prime $p$ greater than $x$)}.\\[0.5em] x \pconcat y &= x \times \eta (p,y) +y \\[0.5em] &\quad \text {\;\; (the base-$p$ numeral of $y$ appended to that of $x$)}.\\[0.5em] \mathrm {Part}(x, y, p) &\Leftrightarrow \exists v\le \!y \, \exists w\le \!y \, (v \pconcat x \pconcat w = y \,\lor \, v \pconcat x = y \, \lor \, x \pconcat v = y \, \lor \, x \!=\! y)\\[0.5em] &\quad \text {\;\;(the base-$p$ numeral of $x$ is part of the base-$p$ numeral of $y$)}.\\[0.5em] x \dotminus y &= \mu z\, ((y\!<\!x \,\to \, y\!+\!z\!=\!x) \,\land \, (\neg (y\!<\!x) \,\to \, z\!=\!0))\\[0.5em] &\quad \text {\;\;(truncated subtraction, as in Section~\ref {sec:pr-functions})}.\\[0.5em] \mathrm {alpha}(p,q,i) &= \mu x\, (\mathrm {Part}((p \dotminus 1) \pconcat i \pconcat x, q, p) \lor x\!=\!q)\\[0.5em] &\quad \text {\;\;(the $x$ for which $(p-1) \pconcat i \pconcat x$ is part of the base-$p$ numeral of $q$)}.\\[0.5em] \mathrm {J}(x,y,q) &\Leftrightarrow 2 \times q = (x+y) \times (x+y+1) + 2\times y.\\[0.5em] \mathrm {rgt}(q) &= \mu y\, \exists x\le \!q(\mathrm {J}(x,y,q)).\\[0.5em] \mathrm {lft}(q) &= \mu x\, \exists y\le \!q(\mathrm {J}(x,y,q)).\\[0.5em] \mathrm {beta}(c,i) &= \text {alpha}(\mathrm {lft}(c),\mathrm {rgt}(c),i). \end {align*}
To be clear: the expressions on the right-hand side aren’t \(\mathfrak {L}_{A}\)-formulas; they are metalinguistic descriptions of certain functions and relations. The chain of definitions shows how \(\mathrm {beta}\) can be constructed from addition, multiplication, projection, and \(\chi _=\) by composition, truth-functional combination, bounded quantification, and regular minimization, By Lemmas 8.7, 8.9, and 8.8, it follows that \(\mathrm {beta}\) is tame. By Lemma 8.10, \(\mathrm {beta}\) is representable in any theory \(T\) that satisfies R1–R6. □
With Lemma 8.11, we can show that representability is closed under primitive recursion.
If \(f\) and \(g\) are representable in a theory \(T\) that satisfies R1–R6, and \(h = \mathrm {Pr}[f,g]\), then \(h\) is also representable in \(T\).
Proof. Assume \(h = Pr[f,g]\). For readability, I assume that \(f\) is one-place. Let \(F(x,y)\), \(G(x,y,z,w)\), and \({\scriptstyle \class {smallcaps}{\text {BETA}}}(x,y,z)\) be \(\mathfrak {L}_A\)-formulas that represent \(f\), \(g\), and \(\mathrm {beta}\) in \(T\), respectively. Let \({\scriptstyle \class {smallcaps}{\text {SEQ}}}(c,x,k)\) be the formula \begin {multline*} \exists u ({\scriptstyle \class {smallcaps}{\text {BETA}}}(c,\overline {1},u) \land F(x,u)) \land \\[0.5em] \forall i(i < k \to \exists t \exists u( {\scriptstyle \class {smallcaps}{\text {BETA}}}(c,s(i),t) \land {\scriptstyle \class {smallcaps}{\text {BETA}}}(c,s(s(i)),u) \land G(x,i,t,u))). \end {multline*} This represents (in \(T\)) the relation that holds of \(c,x,k\) iff \(c\) codes \(\langle h(x,0), \ldots , h(x,k) \rangle \). Let \(H(x,k,y)\) be \[ \exists c({\scriptstyle \class {smallcaps}{\text {SEQ}}}(c,x,k) \land {\scriptstyle \class {smallcaps}{\text {BETA}}}(c,s(k),y)). \] This represents the relation that holds of \(x,k,y\) iff \(y\) is the last element of \(\langle h(x,0), \ldots , h(x,k) \rangle \). It therefore represents \(h\) in \(T\). □
Show that all tame functions are recursive. If you are ambitious, you may also want to show the converse: that all recursive functions are tame. (Hint: if \(h = \mathrm {Pr}[f,g]\) then \(h\) can be constructed from \(f\), \(g\), and \(\mathrm {beta}\), roughly as in the proof of Lemma 8.12.)
8.5Wrapping up
The lemmas from the previous two sections combine to give us our main result:
Proof. Let \(T\) be any theory that satisfies R1–R6. By Lemmas 8.1, 8.2, and 8.3, the zero function, successor function, and projection functions are representable in \(T\). By Lemmas 8.4, 8.5, and 8.12, any function constructed by composition, regular minimization, or primitive recursion from functions that are representable in \(T\) is itself representable in \(T\). Since all computable (=recursive) functions can be constructed from zero, successor, and projection by these operations, it follows that all computable functions are representable in \(T\). □
The conditions R1–R6 can be seen as defining a minimal arithmetical theory in which all computable functions and relations are representable. This theory is not especially elegant. More elegant is the theory Q (or “Robinson Arithmetic”) that we met in Section 4.1. As a reminder, here are the axioms of Q:
Q1 \(\forall x\forall y\, (s(x)\!=\!s(y) \,\to \, x\!=\!y)\) Q2 \(\forall x \, 0\not = \!s(x)\) Q3 \(\forall x \,(x\not = 0 \,\to \, \exists y\, x\!=\!s(y))\) Q4 \(\forall x (x + 0 = x)\) Q5 \(\forall x \forall y (x + s(y) = s(x + y))\) Q6 \(\forall x (x \times 0 = 0)\) Q7 \(\forall x \forall y (x \times s(y) = (x \times y) + x)\)
The following proof shows that Q, and therefore every extension of Q, satisfies R1–R6. An extension of Q is a theory that is at least as strong as Q, in the sense that it contains all sentences in Q.
Proof. By Theorems 8.1 and 8.2, it suffices to show that Q (and therefore any extension of Q) satisfies R1–R6.
R1. We show by induction on \(n\) that \(\vdash _Q \forall x (\overline {n} < x \;\lor \; x\!=\overline {n} \;\lor \; x < \overline {n})\). Base: \(n=0\). (I now reason “inside Q”.) By Q3, for all \(x\) either \(x=0\) or \(\exists y\, x=s(y)\). In the second case, \(\exists y (s(y) + 0\!=\!x)\) by Q4, and so \(0<x\). So \(\forall x(x\!=\!0 \;\lor \; 0 < x)\). Induction step: Let \(x\) be any number. We show that \(s(\overline {n}) < x \;\lor \; x\!=\!s(\overline {n}) \;\lor \; x < s(\overline {n})\). By Q3, either \(x=0\) or \(\exists y\, x=s(y)\). If \(x=0\) then \(x < s(\overline {n})\) because \(s(\overline {n}) + 0=s(\overline {n})\) by Q4 and hence \(\exists z(s(z) + 0=s(n))\). Assume \(\exists y\, x=s(y)\). By induction hypothesis, \(\overline {n} < y \;\lor \; y\!=\overline {n} \;\lor \; y < \overline {n}\). If \(\overline {n} < y\) then \(\exists z(s(z) + \overline {n}\!=\!y)\) and \(s(z) + s(\overline {n})\!=\!s(y)\) by Q5; so \(s(\overline {n}) < x\). If \(y\!=\overline {n}\) then \(x = s(\overline {n})\). If \(y < \overline {n}\) then \(\exists z(s(z) + y = \overline {n})\) and \(s(z) + s(y) = s(\overline {n})\) by Q5; so \(x < s(\overline {n})\).
R2. We show that \(Q\) contains \(\neg \exists x (x < 0)\). Fix any \(x,z\). By Q3, either \(x = 0\) or \(\exists y\, x = s(y)\). If \(x=0\), \(s(z) + x = s(z) + 0 = s(z)\) by Q4, hence \(s(z) + x \neq 0\) by Q2. If, alternatively, \(\exists y\, x = s(y)\), then \(s(z) + x = s(z) + s(y) = s(s(z) + y)\) by Q5, hence \(s(z) + x \neq 0\) by Q2. So Q2–Q5 entail \(\forall x \neg \exists z(s(z) + x = 0)\), which is equivalent to \(\neg \exists x (x < 0)\).
R3. We show by induction on \(n\) that whenever \(n > 0\) then \(\vdash _Q \forall x (x < \overline {n} \;\to \; ({x\!=\!0} \;\lor \; \ldots \;\lor \; {x\!=\overline {n-1}}))\). Base: \(n=1\). We show that \(\vdash _Q \forall x (x < \overline {1} \;\to \; x = 0)\). Assume \(x < \overline {1}\); i.e. \(\exists z (s(z) + x = s(0))\). Suppose for reductio that \(x\not = 0\). By Q3, \(\exists y\, x\!=\!s(y)\); so \(s(z)+s(y) = s(0)\); so \(s(s(z)+y) = s(0)\) by Q5, and \(s(z)+y = 0\) by Q1; if \(y=0\) then \(s(z)+0=s(z)=0\) contradicting Q2; if \(y=s(w)\) then \(s(z)+s(w)=s(s(z)+w)=0\), again contradicting Q2. Induction step: Assume \(x < s(\overline {n})\), i.e. \(\exists z(s(z) + x = s(\overline {n}))\). By Q3, either \(x=0\) or \(\exists y\, x=s(y)\). In the second case, \(s(z) + s(y) = s(\overline {n})\), so \(s(s(z) + y) = s(\overline {n})\) by Q5, and \(s(z) + y = \overline {n}\) by Q1; so \(y < \overline {n}\). By induction hypothesis, \(y = 0 \;\lor \; \ldots \;\lor \; y = \overline {n-1}\), so \(x= s(y)\) is one of \(1, \ldots , \overline {n}\). Combining both cases, we have \(x=0 \;\lor \; \ldots \;\lor \; x = \overline {n}\).
R4. We show that if \(n \ne m\), then \(\vdash _Q \overline {n} \ne \overline {m}\). Assume \(n < m\). We show by induction on \(n\) that \(\vdash _Q \overline {n} \ne \overline {m}\). Base: \(n=0\). Then \(\overline {m} = \overline {s(m-1)})\) and hence \(0 \ne \overline {m}\) by Q2. Induction step: \(n=s(k)\). Then \(m = s(d)\) for some \(d\) with \(k < d\). By induction hypothesis, \(\vdash _Q \overline {k} \ne \overline {d}\). So \(\vdash _Q s(\overline {k}) \ne s(\overline {d})\) by Q1. The case for \(m < n\) is analogous.
R5. We show by induction on \(m\) that for all \(n,m\), \(\vdash _Q \overline {n} + \overline {m} = \overline {n+m}\). Base: \(m=0\). Then \(\overline {n} + \overline {m} = \overline {n+m}\) by Q4. Induction step: \(m=s(k)\). By induction hypothesis, \(\overline {n} + \overline {k} = \overline {n+k}\). By Q5, \(\overline {n} + s(\overline {k}) = s(\overline {n} + \overline {k}) = s(\overline {n+k}) = \overline {n + s(k)} = \overline {n+m}\).
R6. We show by induction on \(m\) that for all \(n,m\), \(\vdash _Q \overline {n} \times \overline {m} = \overline {n\times m}\). Base: \(m=0\). Then \(\overline {n} \times \overline {m} = \overline {n\times m}\) by Q6. Induction step: \(m=s(k)\). Then \(\overline {n} \times s(\overline {k}) = \overline {n} \times \overline {k} + \overline {n}\) by Q7, \(= \overline {n\times k} + \overline {n}\) by induction hypothesis, \(= \overline {n\times k + n}\) by R5, \(= \overline {n \times m}\). □
By Proposition 4.1, Peano Arithmetic (PA) is an extension of Q. So all computable functions and relations are representable in PA.
We can also prove a result that goes in the other direction:
Every relation that is representable in an axiomatizable and consistent \(\mathfrak {L}_{A}\)-theory is computable.
Proof. Assume \(A(x_{1},\ldots ,x_{k})\) represents \(R\) in an axiomatizable and consistent theory \(T\). That is, if \(R\) holds of some numbers \(n_{1},\ldots ,n_{k}\), then \(T\) can prove \(A(\overline {n_{1}},\ldots ,\overline {n_{k}})\), and if \(R\) does not hold of \(n_{1},\ldots ,n_{k}\), then \(T\) can prove \(\neg A(\overline {n_{1}},\ldots ,\overline {n_{k}})\). Since \(T\) is consistent, it never proves both \(A(\overline {n_{1}},\ldots ,\overline {n_{k}})\) and \(\neg A(\overline {n_{1}},\ldots ,\overline {n_{k}})\). By Proposition 5.4, every axiomatizable first-order theory is computably enumerable: we can express an algorithm that lists all sentences provable in \(T\). This gives us an algorithm for deciding \(R\): to check whether \(R\) holds of some numbers \(a_{1},\ldots ,n_{k}\), we wait until either \(A(\overline {n_{1}},\ldots ,\overline {n_{k}})\) or \(\neg A(\overline {n_{1}},\ldots ,\overline {n_{k}})\) appears on the list of sentences provable in \(T\). So \(R\) is computable. □
Finally, let’s return to expressibility. As I announced in Section 8.2, our result about representability shows that all computable functions and relations can be expressed in \(\mathfrak {L}_{A}\):
Proof. By Theorem 8.3, all computable functions and relations are representable in Q. All axioms of Q are true in the standard model of arithmetic \(\mathfrak {N}\). So Q \(\subseteq \mathrm {Th}(\mathfrak {N})\). By Proposition 8.1, every formula that represents a function or relation in Q therefore also expresses that function or relation in \(\mathfrak {L}_A\) □
Explain why all computably enumerable relations are expressible in \(\mathfrak {L}_{A}\). (Hint: use Proposition 5.3.)
Say that a relation \(R\) is weakly represented by an \(\mathfrak {L}_{A}\)-formula \(A(x_{1},\ldots ,x_{n})\) in a theory \(T\) iff for all numbers \(n_{1},\ldots ,n_{k}\), \[ R(n_{1},\ldots ,n_{k}) \text { iff } \vdash _{T} A(\overline {n_{1}},\ldots ,\overline {n_{k}}). \] Explain the following facts:
- (a)
- A relation can be weakly representable in a theory without being representable in that theory.
- (b)
- If \(R\) is weakly representable in an axiomatizable and consistent theory then \(R\) is computably enumerable. (Compare Theorem 8.4.)
- (c)
- All computable relations are weakly representable in any \(\mathfrak {L}_{A}\)-theory that is consistent with Q. (Hint: We know that every computable relation \(R\) is represented in Q by some formula \(A\). Let \(\hat {Q}\) be the conjunction of the seven axioms of Q, and consider the formula \(\hat {Q} \to A\).)