Definability of Recursive Functions

The recursive functions are one model of computation. They are equivalent to all other known models of computation (e.g., the lambda calculus, Turing machines, register machines, etc.). The Church-Turing thesis hypothesizes that each of these models (and hence the general recursive functions) capture the intuitive notion of effective computability.

Recursive Functions

First, let's review the definition of recursive functions. The class of (general) recursive functions is defined as follows (see this blog post for one justification of this definition):

Definition (General Recursive Functions). The class of (general) recursive functions \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) consists of the following functions:

Primitive Functions

• The constant functions \(C^k_n : \mathbb{N}^k \rightarrow \mathbb{N}\) defined as

\[C^k_n(x_1,\dots,x_k) = n\]

for every arity (number of arguments) \(k \in \mathbb{N}\) and constant \(n \in \mathbb{N}\). A constant function of arity \(0\) is just a natural number constant, i.e., \(C^0_n = n\). Constant functions have the computational interpretation of a computation that immediately yields a fixed value.

• The successor function \(S : \mathbb{N} \rightarrow \mathbb{N}\) defined as

\[S(x) = x + 1,\]

where it is assumed that the notion of the successor \(x+1\) of the natural number \(x\) is defined somehow. The successor function has the computational interpretation of a computation that outputs the "next" natural number (i.e., yields the successor of a natural number, increments the natural number, etc.).

• All projection functions \(P^k_i\) defined as

\[P^k_i(x_1,\dots,x_i,\dots,x_k) = x_i\]

for all arities \(k \ge 1\) and all indices \(1 \le i \le k\). Projection functions have the computational interpretation of a computation that simply yields one of its inputs.

Composition

• For every general recursive function \(f : \mathbb{N}^m \rightarrow \mathbb{N}\) and list \((g_1,\dots,g_m)\) of \(m\) functions \(g_i : \mathbb{N}^k \rightarrow \mathbb{N}\), the function \(f \circ (g_1,\dots,g_m) : \mathbb{N}^k \rightarrow \mathbb{N}\) defined as follows is general recursive:

\[(f \circ (g_1,\dots,g_m))(x_1,\dots,x_k) = f(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k)).\]

The value \((f \circ (g_1,\dots,g_m))(x_1,\dots,x_k)\) is defined only if \(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k)\) are each defined and \(f(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k))\) is defined. The composition of recursive functions has the computational interpretation of a sequence of computations: each of the computations \(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k)\) is performed, perhaps in the same order, and then the computation \(f(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k))\) is performed.

Primitive Recursion

• For all general recursive functions \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) and \(g : \mathbb{N}^{k+2} \rightarrow \mathbb{N}\), the general recursive function \(\rho(f,g) : \mathbb{N}^{k+1} \rightarrow \mathbb{N}\) is defined as follows:
  • \(\rho(f,g)(0,x_1,\dots,x_k) = f(x_1,\dots,x_k)\),
  • \(\rho(f,g)(S(y),x_1,\dots,x_k) = g(\rho(f,g)(y,x_1,\dots,x_k),y,x_1,\dots,x_k).\)

The value \(\rho(f,g)(y,x_1,\dots,x_k)\) is defined only if \(f(x_1,\dots,x_k)\) is defined and \(\rho(f,g)(y',x_1,\dots,x_k)\) and \(g(\rho(f,g)(y',x_1,\dots,x_k),y',x_1,\dots,x_k)\) are defined for all \(y' \lt y\). The operator \(\rho\) really represents a collection of operators, one for each arity (e.g., \(\rho_k : \mathbb{N}^k \times \mathbb{N}^{k+2} \rightarrow (\mathbb{N}^{k+1} \rightarrow \mathbb{N})\)), and is called the primitive recursion operator. Intuitively, the primitive recursion operator produces a function with the following computational interpretation: it performs a bounded sequence of computations, starting at \(\rho(f,g)(0,x_1,\dots,x_k)\) and terminating at \(\rho(f,g)(y,x_1,\dots,x_k)\), where the result of each prior computation is available to the next computation. It is often convenient to think inductively, however, i.e., to assume that the value \(\rho(f,g)(y,x_1,\dots,x_k)\) is defined and to compute \(\rho(f,g)(S(y),x_1,\dots,x_k)\) in terms of this value.

Minimization

• For all general recursive functions \(f : \mathbb{N}^{k+1} \rightarrow \mathbb{N}\), the function \(\mu(f) : \mathbb{N}^k \rightarrow \mathbb{N}\) defined as follows is general recursive:

\[\mu(f)(x_1,\dots,x_k) = \begin{cases}y & \text{if } f(y, x_1, \dots, x_k) = 0 \\& \text{and } f(y', x_1, \dots, x_k) \gt 0 \text{ for all } y' \lt y \\ \text{undefined} & \text{otherwise}.\end{cases}\]

The function \(\mu(f)\) is thus a partial function that is undefined whenever there is no such \(y\). The function \(f\) is not required to be total (the conditions \(f(y, x_1, \dots, x_k) = 0\) and \(f(y', x_1, \dots, x_k) \gt 0\) are implicitly unsatisfied when the function \(f\) is undefined for the respective inputs). The operator \(\mu\) really represents a collection of operators, one for each arity (e.g., \(\mu_k : \mathbb{N}^{k+1} \rightarrow (\mathbb{N}^k \rightarrow \mathbb{N})\)), and is called the minimization operator.

Intuitively, the minimization operator produces a function with the following computational interpretation: it iteratively searches, starting at \(0\) and proceeding in increasing order, for the first value \(y\) such that \(f(y, x_1, \dots, x_k) = 0\). If an input for which \(f\) is undefined is encountered prior to ending the search, the output is undefined. Likewise, if \(f(y, x_1, \dots, x_k) \ne 0\) for all values \(y\), then the output is undefined.

Iterative Characterization of Primitive Recursion

The primitive recursive functions can be characterized via iteration, which is essential for some of the following proofs.

Theorem (Iteration). For any primitive recursive function \(\rho(f, g)\),

\[\rho(f,g)(n,x_1,\dots,x_k) = y\]

if and only there exists a finite sequence of \(n+1\) natural numbers \(a_0, \dots, a_n\) such that following conditions are met:

• \(a_0 = f(0, x_1, \dots, x_k)\),
• \(a_{i+1} = g(a_i, i, x_1, \dots, x_k)\) for all \(i \lt n\),
• \(a_n = y\).

Proof. By induction. \(\square\)

Examples

Let's review a few examples of recursive functions.

Addition

Addition \(m+n\) of natural numbers \(m\) and \(n\) can be implemented as follows:

\[\textrm{add} = \rho(P^1_1, S \circ P^3_1).\]

According to the definitions, this means that

\begin{align*}\textrm{add}(0, n) &= \rho(P^1_1, S \circ P^3_1)(0,n) \\&= P^1_1(n) \\&= n\end{align*}

and

\begin{align*}\textrm{add}(m+1, n) &=\rho(P^1_1, S \circ P^3_1)(S(m),n) \\&= (S \circ P^3_1)(\rho(P^1_1, S \circ P^3_1)(m,n),m,n) \\&= S(\rho(P^1_1, S \circ P^3_1)(m,n)) \\&= \textrm{add}(m, n) + 1.\end{align*}

Multiplication

Multiplication \(m \cdot n\) of natural numbers \(m\) and \(n\) can be implemented as follows:

\[\textrm{mul} = \rho(C^1_0, \textrm{add} \circ (P^3_1, P^3_3)).\]

According to the definitions, this means that

\begin{align*}\textrm{mul}(0,n) &= \rho(C^1_0, \textrm{add} \circ (P^3_1, P^3_3))(0,n) \\&= C^1_0(n) \\&= 0\end{align*}

and

\begin{align*}\textrm{mul}(m+1,n) &= \rho(C^1_0, \textrm{add} \circ (P^3_1, P^3_3))(S(m),n) \\&= (\textrm{add} \circ (P^3_1, P^3_3))(\rho(C^1_0, \textrm{add} \circ (P^3_1, P^3_3))(m, n),m,n) \\&= (\textrm{add} \circ (P^3_1, P^3_3))(\textrm{mul}(m, n),m,n) \\&= \textrm{add}(P^3_1(\textrm{mul}(m, n),m,n), P^3_3(\textrm{mul}(m, n),m,n)) \\&= \textrm{add}(\textrm{mul}(m, n), n) \\&= m \cdot n + n \\&= (m + 1) \cdot n.\end{align*}

Predecessor

The predecessor operation \(\textrm{pred}(n)\), i.e., the operation

\[\textrm{pred}(n) = \begin{cases} n - 1 & \text{if } n \ge 1 \\ 0 & \text{otherwise}\end{cases}\]

can be defined as follows:

\[\textrm{pred} = \rho(C^0_0, P^2_2).\]

According to the definitions, this means that

\begin{align*}\textrm{pred}(0) &= \rho(C^0_0, P^2_2)(0) \\&= C^0_0 \\&= 0\end{align*}

and

\begin{align*}\textrm{pred}(n+1) &= \rho(C^0_0, P^2_2)(S(n)) \\&= P^2_2(\rho(C^0_0, P^2_2)(n), n) \\&= n.\end{align*}

Subtraction

Truncated subtraction \(m \dot{-} n\), i.e., the operation

\[m \dot{-} n = \begin{cases}m - n & \text{if } m \ge n \\ 0 & \text{if } m \lt n\end{cases}\]

can be defined as follows: first, we define reversed truncated subtraction \(\textrm{rsub}(m,n) = n - m\) as follows:

\[\textrm{rsub}(m,n) = \rho(P^1_1, \textrm{pred} \circ P^3_1).\]

This is necessary since recursion occurs in the first argument. According to the definitions, this means that

\begin{align*}\textrm{rsub}(0,n) &= \rho(P^1_1, \textrm{pred} \circ P^3_1)(0,n) \\&= P^1_1(n) \\&= n \\&= n - 0\end{align*}

and

\begin{align*}\textrm{rsub}(m+1,n) &= \rho(P^1_1, \textrm{pred} \circ P^3_1)(S(m), n) \\&= (\textrm{pred} \circ P^3_1)(\rho(P^1_1, \textrm{pred} \circ P^3_1)(m,n),m,n) \\&= (\textrm{pred} \circ P^3_1)(\textrm{rsub}(m,n),m,n) \\&= \textrm{pred}(P^3_1(\textrm{rsub}(m,n),m,n)) \\&= \textrm{pred}(\textrm{rsub}(m,n)) \\&= (n-m)-1 \\&= n-(m+1).\end{align*}

Then, we can define truncated subtraction by swapping the arguments:

\[\textrm{sub} = \textrm{rsub} \circ (P^2_2, P^2_1).\]

Zero Test

Often it is useful to test whether a number is \(0\) or not. In general, predicates can be represented by recursive functions that output \(0\) for false and a non-zero value for true. The predicate testing for zero can be defined as

\[\textrm{is-zero} = \rho(C^0_1, C^2_0).\]

According to the definitions, it follows that

\begin{align*}\textrm{is-zero}(0) &= \rho(C^0_1, C^2_0)(0) \\&= C^0_1 = 1\end{align*}

and

\begin{align*}\textrm{is-zero}(n+1) &= \rho(C^0_1, C^2_0)(S(n)) \\&= C^2_0(\rho(C^0_1, C^2_0)(n),n) \\&= C^2_0(\rho(C^0_1, C^2_0)(n), n) \\&= 0.\end{align*}

Logical Operations

A ternary operator (if-then-else) can be defined as follows:

\[\textrm{if} = \rho(P^2_2, P^4_3).\]

According to the definitions,

\begin{align*}\textrm{if}(0, t, f) &= \rho(P^2_2, P^4_3)(0,t,f) \\&= P^2_2(t,f) \\&= f\end{align*}

and

\begin{align*}\textrm{if}(n+1, t, f) &= \rho(P^2_2, P^4_3)(S(n),t,f) \\&= P^4_3(\rho(P^2_2, P^4_3)(n,t,f),n,t,f) \\&= t.\end{align*}

Thus, \(\textrm{if}\) selects the value \(t\) (second argument) when the "condition" (first argument) is "true" (not \(0\)) and it selects the value \(f\) (third argument) when the "condition" is "false" (\(0\)).

Logical negation can be implemented as

\[\textrm{not} = \textrm{if} \circ (P^1_1, C^1_0, C^1_1).\]

According to the definitions,

\begin{align*}\textrm{not}(0) &= (\textrm{if} \circ (P^1_1, C^1_0, C^1_1))(0) \\&= \textrm{if}(P^1_1(0), C^1_0(0), C^1_1(0)) \\&= \textrm{if}(0, 0, 1) \\&= 1\end{align*}

and

\begin{align*}\textrm{not}(n+1) &= (\textrm{if} \circ (P^1_1, C^1_0, C^1_1))(S(n)) \\&= \textrm{if}(P^1_1(S(n)), C^1_0(S(n)), C^1_1(S(n))) \\&= \textrm{if}(S(n), 0, 1) \\&= 0.\end{align*}

Order

Ordering, such as \(m \le n\), can be defined as follows:

\[\textrm{le} = \textrm{is-zero} \circ \textrm{sub}.\]

Likewise, \(m \ge n\) can be defined by swapping arguments:

\[\textrm{ge} = \textrm{le} \circ (P^2_2, P^2_1).\]

Strictly inequality \(m \lt n\) can be defined as follows:

\[\textrm{lt} = \textrm{not} \circ \textrm{ge},\]

\[\textrm{gt} = \textrm{not} \circ \textrm{le}.\]

Square Root

The integer square root of a natural number \(n\) (i.e., the least value \(r\) such that \((r+1)^2 \gt n\)) can be computed using the minimization operator as follows (it is also possible to use primitive recursion, but less convenient):

\[\textrm{sqrt} = \mu(\textrm{le} \circ (\textrm{mul} \circ (S \circ P^2_1, S \circ P^2_1), P^2_2)).\]

According to the definitions, this means that

\begin{align*}\textrm{sqrt}(n) &= \mu(\textrm{le} \circ (\textrm{mul} \circ (S \circ P^2_1, S \circ P^2_1), P^2_2))(n)\end{align*}

which is, by definition, the least value \(r\) such that

\[(\textrm{le} \circ (\textrm{mul} \circ (S \circ P^2_1, S \circ P^2_1), P^2_2))(r, n) = 0\]

and hence the least value \(r\) such that

\[\textrm{le}(\textrm{mul}(S(r), S(r)), n)\]

is "false" (\(0\)), which means it is the least value such that \((r+1)^2 \gt n\), as required.

Structural Induction

Our goal is to prove that the class of recursive functions satisfies certain properties. The class of recursive functions is an inductively-defined set.

The natural numbers are the prototypical example of an inductively-defined set. The natural numbers can be characterized as the smallest set containing \(0\) (where \(0\) is some designated element that we choose to represent zero, e.g., \(\emptyset\)) that is closed under the successor operation \(S\) (where we designate an appropriate function to represent this successor operation, e.g., \(S(n) = n \cup \{n\}\)). This permits inductive proofs; consider the subset \(A \subseteq \mathbb{N}\) defined in terms of some property \(P\):

\[A = \{n \in \mathbb{N} : P(n)\}.\]

If \(0 \in A\) and \(S(n) \in A\) whenever \(n \in A\), then, since \(\mathbb{N}\) is the smallest such set, \(\mathbb{N} \subseteq A\) and hence \(A = \mathbb{N}\), which implies that \(P(n)\) is satisfied for all \(n \in \mathbb{N}\). This is the familiar technique of proof by induction:

1. Prove \(P(0)\).
2. Prove \(P(n+1)\) assuming \(P(n)\).
3. Conclude \(P(n)\) for all \(n \in \mathbb{N}\).

This same technique applies to other inductively-defined sets (i.e., sets defined as the smallest sets containing certain elements and closed under certain operations).

In particular, the set of recursive functions represents an inductively-defined set: it contains the constant and projection functions and is closed under the composition, primitive recursion, and minimization operators (of all arities). This likewise yields an inductive proof technique; to prove that all recursive functions satisfy some property, do the following:

1. Prove that the property is satisfied by all constant functions \(C^k_n\).
2. Prove that the property is satisfied by all projection functions \(P^k_n\).
3. Prove that the property is satisfied by the successor function \(S\).
4. Prove that the property is satisfied by all compositions \(f \circ (g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k))\) assuming that it is satisfied by \(f\) and by each of \(g_1(x_1,\dots,x_k),\dots,g_m(x_1,\dots,x_k)\).
5. Prove that the property is satisfied by all primitive recursive functions \(\rho(f, g)\) assuming that it is satisfied by each of \(f\) and \(g\).
6. Prove that the property is satisfied by all minimizing functions \(\mu(f)\) assuming that it is satisfied by \(f\).
7. Conclude that the property is satisfied by all recursive functions.

Logic

Next, we will describe the basic apparatus of formal, first-order predicate logic.

Signatures

A signature defines a collection of non-logical symbols.

Definition (Signature). A signature \(\Sigma = (C, F, R, a)\) consists of a set \(C\) of constant symbols, a set \(F\) of function symbols, a set \(R\) of relation symbols, and a function \(a : F \cup R \rightarrow \mathbb{N}\) that assigns an arity to each function and relation symbol (the number of arguments each accepts). By convention, \(a(f) \ge 1\) for all \(f \in F\) and \(a(A) \ge 1\) for all \(A \in R\).

Note: some authors define constants as \(0\)-argument functions, thus permitting \(a(f) = 0\).

Example. One possible signature for arithmetic is \(C = \{0\}, F = \{S, +, \cdot\}, R = \{\lt\}\) (where \(S\) is the successor function symbol) with \(a(S) = a, a(+) = a(\cdot) = 2\) and \(a(\lt) = 2\). Here we assume that some set (it does not matter which) uniquely represents each symbol.

Languages

A signature determines a first-order language.

Every first order language has an associated countably infinite set of variables \(V\), often denoted \(v_0, v_1, \dots\), etc.

Languages are defined inductively. We first specify the terms of a first-order language, which are analogous to noun phrases in natural language. Roughly, they are the expressions about which the language makes assertions.

Definition (Term). A term relative to a signature \(\Sigma = (C, F, R, a)\) is an element of the set \(\mathrm{Term}(\Sigma)\) of terms inductively defined as follows:

• Every variable is a term.
• Every constant symbol is a term.
• \(f(t_1, \dots, t_n)\) is a term for every function symbol \(f \in F\) with arity \(a(f) = n\) and every sequence of terms \(t_1, \dots, t_n\).

A first-order language is the collection of all formulas for a given signature, that is, all well-formed expressions utilizing the elements of the signature. Note: sometimes a signature is conflated with the first-order language it represents, and the signature is called the "language".

Definition (Formula). A formula relative to a signature \(\Sigma = (C, F, R, a)\) is an element of the set \(\mathrm{Form}(\Sigma)\) of formulas inductively defined as follows:

• \(\bot\) is a formula.
• \(\top\) is a formula.
• \(A(t_1, \dots, t_n)\) is a formula for every relation symbol \(A \in R\) with arity \(a(A) = n\) and every sequence of terms \(t_1,\dots,t_n\).
• \(=(t_1, t_2)\) is a formula for all terms \(t_1\) and \(t_2\).
• \(\neg \varphi\) is a formula for every formula \(\varphi\).
• \((\varphi \lor \psi)\) is a formula for all formulas \(\varphi\) and \(\psi\).
• \((\varphi \land \psi)\) is a formula for all formulas \(\varphi\) and \(\psi\).
• \((\varphi \rightarrow \psi)\) is a formula for all formulas \(\varphi\) and \(\psi\).
• \(\forall x \varphi\) is a formula for all variables \(x\) and formulas \(\varphi\).
• \(\exists x \varphi\) is a formula for all variables \(x\) and formulas \(\varphi\).

We formally write \(=(t_1, t_2)\) since \(=\) is a two-place relation symbol (which is regarded as a logical symbol in our approach). We may write \(t_1 = t_2\) informally, but only the expression \(=(t_1, t_2)\) is part of the formal language.

Likewise, we permit informal abbreviations such as \((\varphi \leftrightarrow \psi)\) that abbreviate \(((\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi))\), but only the latter is a formula of the respective language.

We may also informally drop parentheses if the parsing of the expression is understood from context. However, the parentheses are required for formulas of the language. The parentheses ensure that the language is unambiguous - i.e., that there is a unique sequence of rules for producing each formula. For instance, without parentheses, the expression

\[\varphi \rightarrow \psi \rightarrow \chi\]

would be ambiguous; with parentheses, one of two possibilities is explicitly indicated:

\[((\varphi \rightarrow \psi) \rightarrow \chi)\]

or

\[(\varphi \rightarrow (\psi \rightarrow \chi)).\]

Certain formulas are atomic, i.e., they cannot be decomposed into constituent formulas.

Definition (Atomic Formula). An atomic formula of a first-order language with signature \(\Sigma\) is an element of the set \(\mathrm{Atom}(\Sigma)\) of atomic formulas inductively defined as follows:

• \(\bot\) is an atomic formula.
• \(\top\) is an atomic formula.
• \(A(t_1, \dots, t_n)\) is an atomic formula for every relation symbol \(A \in R\) with arity \(a(A) = n\) and every sequence of terms \(t_1,\dots,t_n\).
• \(=(t_1, t_2)\) is an atomic formula for all terms \(t_1\) and \(t_2\).

It is important to distinguish between free variables and bound variables in a first-order language; the former are not in the scope by any quantifier, whereas the latter are in the scope of a quantifier.

Definition (Free Variable). A free variable of a formula \(\varphi \in \mathrm{Form}(\Sigma)\) of a first-order language with signature \(\Sigma\) is an element of the set \(\mathrm{Free}(\varphi)\) of free variables inductively defined as follows:

• If \(\varphi\) is atomic, then all occurrences of variables are free.
• If \(\varphi \equiv \neg \psi\), then the free variables of \(\varphi\) are precisely those of \(\psi\).
• If \(\varphi \equiv (\psi \lor \chi)\), then the free variables of \(\varphi\) are those of \(\psi\) together with those of \(\chi\).
• If \(\varphi \equiv (\psi \land \chi)\), then the free variables of \(\varphi\) are those of \(\psi\) together with those of \(\chi\).
• If \(\varphi \equiv (\psi \rightarrow \chi)\), then the free variables of \(\varphi\) are those of \(\psi\) together with those of \(\chi\).
• If \(\varphi \equiv \forall x \psi\), then the free variables of \(\varphi\) are those of \(\psi\) except for \(x\).
• If \(\varphi \equiv \exists x \psi\), then the free variables of \(\varphi\) are those of \(\psi\) except for \(x\).

A bound variable is a variable that does not occur free in a formula.

A formula is open if it contains free variables and closed otherwise. A sentence is a closed formula.

Induction

Since terms and formulas are inductively defined, there is a corresponding inductive proof principle.

Lemma (Term Induction). For any first-order language with signature \(\Sigma = (C,F,R,a)\), a property \(P\) is satisfied by all terms \(t \in \mathrm{Term}(\Sigma)\) if the following conditions are satisfied:

• The property \(P\) is satisfied for every variable \(v \in V\).
• The property \(P\) is satisfied for every constant \(c \in C\).
• The property \(P\) is satisfied for \(f(t_1, \dots, t_n)\) for an arbitrary \(n\)-place function symbol \(f \in F\) and an arbitrary sequence of terms \(t_1, \dots, t_n\) assuming is satisfied for each of the terms \(t_1, \dots, t_n\).

Lemma (Formula Induction). For any first-order language with signature \(\Sigma = (C, F, R, a)\), a property \(P\) is satisfied by all formulas \(\varphi \in \mathrm{Form}(\Sigma)\) if the following conditions are satisfied:

• The property \(P\) is satisfied for \(\top\).
• The property \(P\) is satisfied for \(\bot\).
• The property \(P\) is satisfied for \(A(t_1, \dots, t_n)\) for an arbitrary \(n\)-place relation symbol \(A \in R\) and an arbitrary sequence of terms \(t_1, \dots, t_n\).
• The property \(P\) is satisfied for \(=(t_1, t_2)\) for arbitrary terms \(t_1, t_2\).
• The property \(P\) is satisfied for \(\neg\varphi\) assuming it is satisfied for an arbitrary \(\varphi\).
• The property \(P\) is satisfied for \((\varphi \lor \psi)\) for arbitrary formulas \(\varphi, \psi\) assuming that it is satisfied for \(\varphi\) and \(\psi\).
• The property \(P\) is satisfied for \((\varphi \land \psi)\) for arbitrary formulas \(\varphi, \psi\) assuming that it is satisfied for \(\varphi\) and \(\psi\).
• The property \(P\) is satisfied for \((\varphi \rightarrow \psi)\) for arbitrary formulas \(\varphi, \psi\) assuming that it is satisfied for \(\varphi\) and \(\psi\).
• The property \(P\) is satisfied for \(\forall x \varphi\) for an arbitrary variable \(x\) and formula \(\varphi\) assuming that it is satisfied by \(\varphi\).
• The property \(P\) is satisfied for \(\exists x \varphi\) for an arbitrary variable \(x\) and formula \(\varphi\) assuming that it is satisfied by \(\varphi\).

Substitution

Definition (Substitution in Terms). The substitution \(s[t/x]\) of a term \(t\) for a variable \(x\) within another term \(s\) for a signature \(\Sigma\) is the result of the application of a function \((s, t, x) \mapsto s[t/x]\) defined via structural recursion as follows:

• \(x[t/x] = t\), and \(y[t/x] = y\) whenever \(y \not \equiv x\) for any variable \(y\).
• \(c[t/x] = c\) for any constant \(c\).
• \(f(t_1, \dots, t_n)[t/x] = f(t_1[t/x], \dots, t_n[t/x])\) for all function symbols \(f\).

We assume the existence of a function \(\mathrm{fresh}\) which accepts a certain number of terms or formulas and generates a "fresh" variable, i.e., one which does not occur in any of the supplied terms or formulas. Such functions can be defined by structural recursion.

Definition (Substitution in Formulas). The substitution \(\varphi[t/x]\) of a term \(t\) for a variable \(x\) within a formula \(\varphi\) for a signature \(\Sigma\) is the result of the application of a function \((\varphi, t, x) \mapsto \varphi[t/x]\) defined via structural recursion as follows:

• \(\top[t/x] = \top\).
• \(\bot[t/x] = \bot\).
• \(A(t_1, \dots, t_n)[t/x] = A(t_1[t/x], \dots, t_n[t/x])\) for any relation symbol \(A\).
• \(=(t_1, t_2)[t/x]\) is \(=(t_1[t/x], t_2[t/x])\).
• \((\neg\varphi)[t/x] = \neg(\varphi[t/x])\) (here, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\varphi \lor \psi)[t/x] = (\varphi[t/x] \lor \psi[t/x])\).
• \((\varphi \land \psi)[t/x] = (\varphi[t/x] \land \psi[t/x])\).
• \((\varphi \rightarrow \psi)[t/x] = (\varphi[t/x] \rightarrow \psi[t/x])\).
• \((\forall x \varphi)[t/x] = \forall x \varphi\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\forall y \varphi)[t/x] = \forall y (\varphi[t/x])\) if \(y \not \equiv x\) and \(y \not \in \mathrm{Free}(t)\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\forall y \varphi)[t/x] = \forall z ((\varphi[z/y])[t/x])\), where \(z = \mathrm{fresh}(\varphi, t, x)\), if \(y \not \equiv x\) and \(y \in \mathrm{Free}(t)\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\exists x \varphi)[t/x] = \exists x \varphi\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\exists y \varphi)[t/x] = \exists y (\varphi[t/x])\) if \(y \not \equiv x\) and \(y \not \in \mathrm{Free}(t)\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).
• \((\exists y \varphi)[t/x] = \exists z ((\varphi[z/y])[t/x])\), where \(z = \mathrm{fresh}(\varphi, t, x)\), if \(y \not \equiv x\) and \(y \in \mathrm{Free}(t)\) (again, parentheses clarify the application of the substitution operation, and do not represent part of the formal expressions).

We may write \(\varphi[t_1/x_1, \dots, t_n/x_n]\) to represent multiple simultaneous substitutions, which may be defined as the iterative substitution

\[(\dots ((\varphi[t_1/x_2])[t_2/x_2])\dots)[t_n/x_n].\]

We will also write \(\varphi(x_1, \dots, x_n)\) to indicate a formula whose free variables are precisely \(x_1, \dots, x_n\) and \(\varphi(t_1, \dots, t_n)\) for the substitution \(\varphi[t_1/x_1, \dots, t_n/x_n]\).

Structures

Definition (Structure). A structure \(\mathcal{A}\) consists of a set \(\lvert \mathcal{A} \rvert\) called a domain, a signature \(\Sigma = (C,F,R,a)\), and an interpretation \(I = (I_C, I_F, I_R)\), which is a tuple of functions which assign values to the constant symbols, function symbols, and relation symbols of the signature as follows:

• For every constant symbol \(c \in C\), there is an associated element \(I_C(c) = c^{\mathcal{A}} \in \lvert \mathcal{A} \rvert\).
• For every function symbol \(f \in F\) of arity \(a(f) = n\), there is an associated function \(I_F(f) = f^{\mathcal{A}} : \lvert \mathcal{A} \rvert^n \rightarrow \lvert \mathcal{A} \rvert\).
• For every relation symbol \(A \in R\) of arity \(a(R) = n\), there is an associated relation \(I_R(A) = A^{\mathcal{A}} \subseteq \lvert \mathcal{A} \rvert^n\).

Example. Using the signature for arithmetic \(C = \{0\}, F = \{S, +, \cdot\}, R = \{\lt\}\) with \(a(S) = 1, a(+) = a(\cdot) = 2\) and \(a(\lt) = 2\), the standard interpretation \(\mathcal{N}\) consists of the domain \(\mathbb{N}\) with \(0^{\mathcal{N}} = 0\), \(S^{\mathcal{N}}(n) = n + 1\), \(+^{\mathcal{N}}(m, n) = m + n\), \(\cdot^{\mathcal{N}}(m, n) = m \cdot n\), and \(\lt^{\mathcal{N}} = \{(m,n) \in \mathbb{N} \times \mathbb{N} : m \lt n\}\), i.e., it interprets the symbols in their usual fashion.

Definition (Variable Assignment). A variable assignment for a structure \(\mathcal{A}\) is function \(s : V \rightarrow \lvert \mathcal{A} \rvert\) that assigns an element of the respective domain to every variable. Given a variable assignment \(s\) and an element \(a \in \lvert \mathcal{A} \rvert\), the variable assignment \(s[a/x]\) for a variable \(x \in V\) is defined as

\[s[a/x](y) = \begin{cases}a & \text{if } y \equiv x \\ s(y) & \text{otherwise.}\end{cases}\]

Definition (Value of a Term). The value \(\mathrm{val}^{\mathcal{A}}_s(t)\) of a term \(t\) within a structure \(\mathcal{A}\) relative to a variable assignment \(s\) is defined by structural recursion as follows:

• \(\mathrm{val}^{\mathcal{A}}_s(c) = c^{\mathcal{A}}\) for all constants \(c\).
• \(\mathrm{val}^{\mathcal{A}}_s(x) = s(x)\) for all variables \(x\).
• \(\mathrm{val}^{\mathcal{A}}_s(f(t_1,\dots,t_n)) = f^{\mathcal{A}}(\mathrm{val}^{\mathcal{A}}_s(t_1), \dots, \mathrm{val}^{\mathcal{A}}_s(t_n))\).

Definition (Satisfaction). The satisfaction predicate \(\mathcal{A},s \models \varphi\) for formulas \(\varphi\) is defined for a structure \(\mathcal{A}\) and variable assignment \(s\) recursively as follows:

• \(\mathcal{A},s \models \top\).
• \(\mathcal{A},s \models A(t_1, \dots, t_n)\) if and only if \((\mathrm{val}^{\mathcal{A}}_s(t_1), \dots, \mathrm{val}^{\mathcal{A}}_s(t_n)) \in A^{\mathcal{A}}\).
• \(\mathcal{A},s \models =(t_1, t_2)\) if and only if \(\mathrm{val}^{\mathcal{A}}_s(t_1) = \mathrm{val}^{\mathcal{A}}_s(t_2)\).
• \(\mathcal{A},s \models \neg \varphi\) if and only if \(\mathcal{A},s \not \models \varphi\).
• \(\mathcal{A},s \models (\varphi \lor \psi)\) if and only if \(\mathcal{A},s \models \varphi\) or \(\mathcal{A},s \models \psi\).
• \(\mathcal{A},s \models (\varphi \land \psi)\) if and only if \(\mathcal{A},s \models \varphi\) and \(\mathcal{A},s \models \psi\).
• \(\mathcal{A},s \models (\varphi \rightarrow \psi)\) if and only if \(\mathcal{A},s \not \models \varphi\) or \(\mathcal{A},s \models \psi\).
• \(\mathcal{A},s \models \forall x \varphi\) if and only if \(\mathcal{A},s[a/x] \models \varphi\) for all \(a \in \lvert \mathcal{A} \rvert\).
• \(\mathcal{A},s \models \exists x \varphi\) if and only if \(\mathcal{A},s[a/x] \models \varphi\) for some \(a \in \lvert \mathcal{A} \rvert\).

If \(\mathcal{A},s \models \varphi\), we say that the structure \(\mathcal{A}\) satisfies the formula \(\varphi\) under the variable assignment \(s\).

Definition (Truth). The truth predicate \(\mathcal{A} \models \varphi\) for sentences \(\varphi\) is defined for a structure \(\mathcal{A}\) as follows: \(\mathcal{A} \models \varphi\) if and only if \(\mathcal{A},s \models \varphi\) for all variable substitutions \(s\). If \(\mathcal{A} \models \varphi\), we say that the sentence \(\varphi\) is true in the structure \(\mathcal{A}\). Given a set of sentences \(\Gamma\), we also write \(\mathcal{A} \models \Gamma\) to indicate that \(\mathcal{A} \models \varphi\) for every \(\varphi \in \Gamma\).

Definition (Validity). A sentence \(\varphi\) relative to a signature \(\Sigma\) is valid, written \(\models \varphi\), if \(\mathcal{A} \models \varphi\) for every structure \(\mathcal{A}\) with signature \(\Sigma\).

Definition (Entailment). A set \(\Gamma\) of sentences entails a sentence \(\varphi\), written \(\Gamma \models \varphi\), if \(\mathcal{A} \models \varphi\) for every structure \(\mathcal{A}\) of the respective signature such that \(\mathcal{A} \models \Gamma\).

Theories

Definition (Sentential Closure). A set of sentences \(\Gamma\) is closed if \(\varphi \in \Gamma\) for every sentence \(\varphi\) such that \(\Gamma \models \varphi\). The closure of \(\Gamma\) is \(\{\varphi : \Gamma \models \varphi\}\). Thus, \(\Gamma\) is closed precisely when \(\Gamma = \{\varphi : \Gamma \models \varphi\}\).

Definition (Axiomatization). A set of sentences \(\Gamma\) is axiomatized by a set of sentences \(\Delta \subseteq \Gamma\) if \(\Gamma\) is the closure of \(\Delta\).

Definition (Theory). A theory is a set of sentences, called axioms.

Note: often, a theory is defined as a closed set of sentences, i.e., the theory represents the closure of everything entailed by its contents. Here, we designate a theory as a collection of axioms.

Models

Definition (Model). A model of a theory \(\Gamma\) is a structure \(\mathcal{M}\) such that \(\mathcal{M} \models \varphi\) for all \(\varphi \in \Gamma\).

Definability

Definition (Standard Signature of Arithmetic). The standard signature of arithmetic \(\Sigma_A\) is defined as follows:

• Constant symbols: \(0\).
• Function symbols: \(S, +, \cdot\).
• Relation symbols: \(\lt\).

This is sometimes compactly written as \(\Sigma_A = \{0,S,+,\cdot,\lt\}\). The standard language of arithmetic \(\mathcal{L}_A\) is then the first-order language corresponding to \(\Sigma_A\).

Definition (Numeral). A numeral is a term \(\bar{n}\) that represents a natural number \(n \in \mathbb{N}\) in the standard language of arithmetic. It is defined by the following recursive function:

• \(\bar{0} = 0\) (here, the \(0\) on the left is a natural number and the \(0\) on the right is the respective constant symbol).
• \(\overline{n+1} = S(\bar{n})\).

Definition (Standard Structure of Arithmetic). The standard structure of arithmetic \(\mathcal{N}\) is the following structure:

• The domain is \(\mathbb{N}\).
• The signature is the standard signature of arithmetic.
• \(0^{\mathcal{N}}\) = 0.
• \(S^{\mathcal{N}}(n) = n + 1\).
• \(+^{\mathcal{N}}(m,n) = m+n\).
• \(\cdot^{\mathcal{N}}(m,n) = m \cdot n\).
• \(\lt^{\mathcal{N}} = \{(m,n) \in \mathbb{N} \times \mathbb{N} : m \lt n\}\).

Definition (Definability). A function \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) is definable in the standard structure of arithmetic \(\mathcal{N}\) if there exists a formula \(\varphi_f(x_1,\dots,x_k,y)\) in the standard language of arithmetic \(\mathcal{L}_A\) such that, for all \(n_1,\dots,n_k,m \in \mathbb{N}\), if \(f(n_1, \dots, n_k) = m\), then

\(\mathcal{N} \models \forall y \left(\varphi(\bar{n_1}, \dots, \bar{n_k}, y) \leftrightarrow y = \bar{m}\right)\).

Lemma. For all natural numbers \(n\), and for every valuation \(s\), \(\mathrm{val}_s^{\mathcal{N}}(\bar{n}) = n\).

Proof. By definition, \(\mathrm{val}_s^{\mathcal{N}}(\bar{0}) = \bar{0}^{\mathcal{N}} = 0\). Suppose that \(\mathrm{val}_s^{\mathcal{N}}(\bar{n}) = n\) for an arbitrary natural number \(n\). Then, by definition,

\begin{align*}\mathrm{val}_s^{\mathcal{N}}(\overline{n+1}) &= \mathrm{val}_s^{\mathcal{N}}(S(\bar{n})) \\&= \mathrm{val}_s^{\mathcal{N}}(\bar{n}) + 1 \\&= n + 1.\end{align*}

\(\square\)

The following lemma provides a useful link between semantic substitution (via a valuation) and syntactic substitution.

Lemma (Numeral Substitution in Terms). For all terms \(t\) relative to the standard signature of arithmetic and for any valuation \(s\), \(\mathrm{val}^{\mathcal{N}}_s[a/x](t) = \mathrm{val}^{\mathcal{N}}_s(t[\bar{a}/x])\).

Proof. By induction.

• For the constant \(0\), \(\mathrm{val}^{\mathcal{N}}_s[a/x](0) = 0 = \mathrm{val}^{\mathcal{N}}_s(0[\bar{a}/x])\).
• For any variable \(y\), if \(y \not \equiv x\), then \(\mathrm{val}^{\mathcal{N}}_s[a/x](y) = \mathrm{val}^{\mathcal{N}}_s(y) = \mathrm{val}^{\mathcal{N}}_s(y[\bar{a}/x])\). Also \(\mathrm{val}^{\mathcal{N}}_s[a/x](x) = a = \mathrm{val}^{\mathcal{N}}_s(\bar{a}) = \mathrm{val}^{\mathcal{N}}_s(x[\bar{a}/x])\).
• For any function symbol \(f\) and terms \(t_1, \dots, t_n\), assuming \(\mathrm{val}^{\mathcal{N}}_s[a/x](t_i) = \mathrm{val}^{\mathcal{N}}_s(t_i[\bar{a}/x])\) for all the terms \(t_i\), it then follows that

\begin{align*}\mathrm{val}^{\mathcal{N}}_s[a/x](f(t_1, \dots, t_n)) &= f^{\mathcal{N}}(\mathrm{val}^{\mathcal{N}}_s[a/x](t_1), \dots, \mathrm{val}^{\mathcal{N}}_s[a/x](t_n))) \\&= f^{\mathcal{N}}(\mathrm{val}^{\mathcal{N}}_s(t_1[\bar{a}/x]), \dots, \mathrm{val}^{\mathcal{N}}_s(t_n[\bar{a}/x]))) \\&= \mathrm{val}^{\mathcal{N}}_s((f(t_1, \dots, t_n))[\bar{a}/x]).\end{align*}

\(\square\)

Lemma (Numeral Substitution in Formulas). For all formulas \(\varphi\), \(\mathcal{N},s[a/x] \models \varphi\) if and only if \(\mathcal{N},s \models \varphi[\bar{a}/x]\).

Proof. By structural induction. \(\square\)

Next, we will proceed to prove that all of the recursive functions are definable. We will give direct proofs in order to demonstrate the low-level mechanics of applying structures. For more complicated proofs, one could demonstrate various meta-theorems that enable higher-level reasoning about definability.

Theorem (Constants Definable). All constants \(C^0_n\) are definable.

Proof. Let \(s\) be any valuation and \(m \in \mathbb{N}\) be any natural number. The constant \(C^0_m\) is defined by the formula

\[\varphi(y) \equiv y = \bar{m}.\]

Let \(a \in \mathbb{N}\) be any natural number. There are two possibilities: \(a = m\), or \(a \ne m\). Suppose \(a = m\). Then \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = s[a/y](y) = s[m/y](y) = m\) and \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(\bar{m}) = m\), so \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = \mathrm{val}_{s[a/y]}^{\mathcal{N}}(\bar{m})\) and thus \(\mathcal{N},s[a/y] \models y = \bar{m}\). Next, suppose \(a \ne m\) and \(\mathcal{N},s[a/y] \models \varphi(y) \equiv y = \bar{m}\). Then \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = \mathrm{val}_{s[a/y]}^{\mathcal{N}}(\bar{m}) \) so \(a = m\), a contradiction. Therefore, if \(a \ne m\), then \(\mathcal{N},s[a/y] \not \models \varphi(y) \equiv y = \bar{m}\). Thus, in all cases, \(\mathcal{N},s[a/y] \not \models \varphi(y)\) or \(\mathcal{N},s[a/y] \models y = \bar{m}\), and thus \(\mathcal{N},s[a/y] \models \varphi(y) \rightarrow y = \bar{m}\). Since \(\varphi(y) \equiv y = \bar{m}\), it follows that \(\mathcal{N},s[a/y] \models y = \bar{m} \rightarrow \varphi(y)\) and hence \(\mathcal{N},s[a/y] \models \varphi(y) \leftrightarrow y = \bar{m}\). Since \(a\) was arbitrary, it follows that \(\mathcal{N},s \models \forall y\left(\varphi(y) \leftrightarrow y = \bar{m}\right)\), and since \(s\) was arbitrary, it follows that \(\mathcal{N} \models \forall y\left(\varphi(y) \leftrightarrow y = \bar{m}\right)\). \(\square\)

Theorem (Constant Functions Definable). All constant functions \(C^k_n\) are definable.

Proof. The proof is essentially the same as the proof that all constants are definable. The constant function \(C^k_m\) is defined by the formula

\[\varphi(x_1, \dots, x_k, y) \equiv x_1 = x_1 \land \dots \land x_k = x_k \land y = \bar{m}.\]

Each of the conjunctions \(x_i = x_i\) is a tautology and is added only so that the free variables of the expression \(\varphi(x_1, \dots, x_k, y)\) will include each of the variables \(x_i\). \(\square\)

Theorem (Successor Function Definable). The successor function \(S(n) = n+ 1\) is definable.

Proof. Let \(s\) be any valuation and \(n \in \mathbb{N}\) be any natural number. The successor function is defined by the following formula:

\[\varphi(x, y) \equiv S(x) = y.\]

Let \(a \in \mathbb{N}\) be any natural number. There are two possibilities: either \(a = n+1\) or \(a \ne n+1 \). Suppose \(a = n+1\). Then, \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = n + 1 = \mathrm{val}_{s[a/y]}^{\mathcal{N}}(\overline{n+1})\) and hence \(\mathcal{N},s[a/y] \models y = \overline{n+1}\). Next, suppose \(a \ne n+1\) and \(\mathcal{N},s[a/y] \models S(\bar{n}) = y\). Then, \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(S(\bar{n})) = n + 1 = a\), a contradiction. Thus, if \(a \ne n+1\), then \(\mathcal{N},s[a/y] \not \models S(\bar{n}) = y\). In either case, \(\mathcal{N},s[a/y] \not \models S(\bar{n}) = y\) or \(\mathcal{N},s[a/y] \models y = \overline{n+1}\) and thus \(\mathcal{N},s[a/y] \models S(\bar{n}) = y \rightarrow y = \overline{n+1}\).

Again, suppose \(a=n+1\). Then, \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(S(\bar{n})) = n + 1\) and \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = n+1\), and thus \(\mathcal{N},s[a/y] \models S(\bar{n}) = y\). Next, suppose \(a \ne n+1\) and \(\mathcal{N},s[a/y] \models y = \overline{n+1}\). Then, \(a = n+1\), a contradiction. Thus, if \(a \ne n+1\), then \(\mathcal{N},s[a/y] \not \models y = \overline{n+1}\). In either case, \(\mathcal{N},s[a/y] \not \models y = \overline{n+1}\) or \(\mathcal{N},s[a/y] \models y = \overline{n+1}\), and hence \(\mathcal{N},s[a/y] \models y = \overline{n+1} \rightarrow S(\bar{n}) = y\).

It then follows that \(\mathcal{N},s[a/y] \models S(\bar{n}) = y \leftrightarrow y = \overline{n+1}\) and thus, since \(a\) was arbitrary, \(\mathcal{N},s\models \forall y \left(S(\bar{n}) = y \leftrightarrow y = \overline{n+1}\right)\). Since \(s\) was arbitrary, \(\mathcal{N} \models \forall y \left(S(\bar{n}) = y \leftrightarrow y = \overline{n+1}\right)\). \(\square\)

Theorem (Projection Functions Definable). The projection functions \(P^k_i\) are definable.

Proof. Let \(s\) be any valuation, and let \(n_1, \dots, n_k \in \mathbb{N}\) be any natural numbers. The projection function \(P^k_i\) is defined by the following formula:

\[\varphi(x_1, \dots, x_k, y) \equiv x_1 = x_1 \land \dots \land y = x_i \land \dots \land x_k = x_k.\]

Let \(a \in \mathbb{N}\) be any natural number. There are two possibilities: either \(a = n_i\) or \(a \ne n_i\). Suppose \(a = n_i\). Then \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = a = n_i\) and \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(\bar{n_i}) = n_i\), so \(\mathcal{N},s[a/y] \models y = \bar{n_i}\). Suppose \(a \ne n_i\) and \(\mathcal{N},s[a/y] \models \varphi(x_1, \dots, x_k, y)\). Then, \(\mathrm{val}_{s[a/y]}^{\mathcal{N}}(y) = \mathrm{val}_{s[a/y]}^{\mathcal{N}}(\bar{n_i})\) and thus \(a = n_i\), a contradiction, and thus, if \(a \ne n_i\), then \(\mathcal{N},s[a/y] \not \models \varphi(x_1, \dots, x_k, y)\). In either case, \(\mathcal{N},s[a/y] \not \models \varphi(x_1, \dots, x_k, y)\) or \(\mathcal{N},s[a/y] \models y = \bar{n_i}\), so \(\mathcal{N},s[a/y] \models \varphi(x_1, \dots, x_k, y) \rightarrow y = \bar{n_i}\). A similar argument shows that \(\mathcal{N},s[a/y] \models y = \bar{n_i} \rightarrow \varphi(x_1, \dots, x_k, y)\), and thus \(\mathcal{N},s[a/y] \models \varphi(x_1, \dots, x_k, y) \leftrightarrow y = \bar{n_i}\). Since \(s\) and \(a\) were arbitrary, \(\mathcal{N} \models \forall y \left(\varphi(x_1, \dots, x_k, y) \leftrightarrow y = \bar{n_i}\right)\). \(\square\)

Theorem (Composition is Definable). If \(f : \mathbb{N}^{\ell} \rightarrow \mathbb{N}\) is definable by a formula \(\varphi_f(x^f_1, \dots, x^f_{\ell}, y^f)\) and \(g_1, \dots, g_{\ell} : \mathbb{N}^k \rightarrow \mathbb{N}\) are definable by formulas \(\varphi_{g_1}(x^{g_1}_1, \dots, x^{g_1}_k, y^{g_1}), \dots, \varphi_{g_{\ell}}(x^{g_{\ell}}_1, \dots, x^{g_{\ell}}_k, y^{g_{\ell}})\), the composition \(f \circ (g_1, \dots, g_{\ell})\) is definable.

Proof. Let \(s\) be any valuation, and let \(n_1, \dots, n_k \in \mathbb{N}\) be any natural numbers. The composition \(f \circ (g_1, \dots, g_{\ell})\) is defined by the following formula (we suppress parentheses for legibility):

\[\varphi(x_1, \dots, x_k, y) \equiv \exists z_1 \dots \exists z_{\ell} \varphi_{g_1}(x_1, \dots, x_k, z_1) \land \dots \land \varphi_{g_{\ell}}(x_1, \dots, x_k, z_{\ell}) \land \varphi_f(z_1, \dots, z_{\ell}, y).\]

Define \(m = (f \circ (g_1, \dots, g_{\ell}))(n_1, \dots, n_k)\) and \(m_i = g_i(n_1,\dots,n_k)\) for \(1 \le i \le \ell\) so that \(m = f(m_1,\dots,m_{\ell})\).

Let \(a \in \mathbb{N}\) be an arbitrary natural number. There are two possibilities: either \(a = m\) or \(a \ne m\).

If \(a = m\), then \(\mathcal{N},s[a/y] \models y = \bar{m}\), so suppose \(a \ne m\) and \(\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k},y)\). Then, by definition, there exist natural numbers \(a_1, \dots, a_{\ell} \in \mathbb{N}\) such that

\[\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models \varphi_{g_1}(\bar{n_1}, \dots, \bar{n_k}, z_1) \land \dots \land \varphi_{g_{\ell}}(\bar{n_1}, \dots, \bar{n_k}, z_{\ell}) \land \varphi_f(z_1, \dots, z_{\ell}, y).\]

Since \(g_i\) is defined by \(\varphi_{g_i}\), by definition,

\[\mathcal{N}\models \forall z_i \left(\varphi_{g_i}\left(\bar{n_1},\dots, \bar{n_k}, z_i\right) \leftrightarrow z_i = \bar{m_i}\right),\]

and thus

\[\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models \left(\varphi_{g_i}\left(\bar{n_1},\dots, \bar{n_k}, z_i\right) \leftrightarrow z_i = \bar{m_i}\right),\]

which means that either \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \not \models \varphi_{g_i}\left(\bar{n_1},\dots, \bar{n_k}, z_i\right)\) or \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models z_i = \bar{m_i}\). However, \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models \varphi_{g_i}\left(\bar{n_1},\dots, \bar{n_k}, z_i\right)\), so it must be the case that \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models z_i = \bar{m_i}\), which implies that \(a_i = m_i\).

Likewise, since \(f\) is defined by \(\varphi_f\), by definition,

\[\mathcal{N}\models \forall y \left(\varphi_f\left(\bar{m_1},\dots, \bar{m_k}, y\right) \leftrightarrow y = \bar{m}\right),\]

and thus

\[\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models \left(\varphi_f\left(\bar{m_1},\dots, \bar{m_k}, y\right) \leftrightarrow y = \bar{m}\right),\]

which means that either \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \not \models \left(\varphi_f\left(\bar{m_1},\dots, \bar{m_k}, y\right)\right)\) or \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models y = \bar{m}\). However, \(\mathcal{N},s[a_1/z_1,\dots,a_{\ell}/z_{\ell},a/y] \models \varphi_f(z_1, \dots, z_{\ell}, y)\) and \(a_i = m_i\), so, by the numeral substitution lemma, \(\mathcal{N},s[a/y] \models \varphi_f(\bar{m_1}, \dots, \bar{m_{\ell}}, y)\), and thus \(\mathcal{N},s[a/y] \models y = \bar{m}\), which implies that \(a = m\), a contradiction. Therefore, if \(a \ne m\), then \(\mathcal{N},s[a/y] \not \models \varphi(\bar{n_i},\dots,\bar{n_k},y)\).

Thus, whether \(a = m\) or \(a \ne m\), either \(\mathcal{N},s[a/y] \not \models \varphi(\bar{n_i},\dots,\bar{n_k},y)\) or \(\mathcal{N},s[a/y] \models y = \bar{m}\), and thus

\[\mathcal{N},s[a/y] \models \varphi(\bar{n_i},\dots,\bar{n_k},y) \rightarrow y = \bar{m}.\]

Converse

Suppose \(a = m\). Then, since each of the functions \(g_i\) are definable, by definition,

\[\mathcal{N}\models \forall z_i \left(\varphi_{g_i}(\bar{n_1},\dots,\bar{n}_{\ell}, z_i) \leftrightarrow z_i = \bar{m_i}\right),\]

and thus, in particular,

\[\mathcal{N},s[m_1/z_1,\dots,m_{\ell}/z_{\ell},a/y]\models z_i = \bar{m_i} \rightarrow \varphi_{g_i}(\bar{n_1},\dots,\bar{n}_{\ell}, z_i),\]

and since \(\mathcal{N},s[m_1/z_1,\dots,m_{\ell}/z_{\ell},a/y] \models z_i = \bar{m_i}\), it then follows that

\[\mathcal{N},s[m_1/z_1,\dots,m_{\ell}/z_{\ell},a/y] \models \varphi_{g_i}(\bar{n_1},\dots,\bar{n}_{\ell}, z_i).\]

Likewise, since \(f\) is definable, by definition,

\[\mathcal{N} \models \forall y \left(\varphi_f(\bar{m_1},\dots,\bar{m}_{\ell}, y) \leftrightarrow y = \bar{m}\right),\]

and thus, in particular,

\[\mathcal{N},s[a/y]\models y = \bar{m} \rightarrow \varphi_f(\bar{m_1},\dots,\bar{m}_{\ell}, y),\]

and since \(\mathcal{N},s[a/y] \models y = \bar{m}\), it then follows that

\[\mathcal{N},s[a/y] \models \varphi_f(\bar{m_1},\dots,\bar{m}_{\ell}, y).\]

By the numeral substitution lemma,

\[\mathcal{N},s[m_1/z_1,\dots,m_{\ell}/z_{\ell},a/y] \models \varphi_f(z_1,\dots,z_{\ell}, y).\]

Thus, it follows that

\[\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_{\ell}}, y) \equiv \exists z_1 \dots \exists z_{\ell} \varphi_{g_1}(\bar{n_1},\dots,\bar{n}_{\ell}, z_1) \land \dots \land \varphi_{g_{\ell}}(\bar{n_1},\dots,\bar{n}_{\ell}, z_{\ell}) \land \varphi_f(z_1,\dots,z_{\ell}, y).\]

Next, suppose that \(a \ne m\). Then \(\mathcal{N},s[a/y] \not \models y = \bar{m}\).

Thus, whether \(a = m\) or \(a \ne m\), either \(\mathcal{N},s[a/y] \not \models y = \bar{m}\) or \(\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_{\ell}}, y)\), and so

\[\mathcal{N},s[a/y] \models y = \bar{m} \rightarrow \varphi(\bar{n_1},\dots,\bar{n_{\ell}}, y).\]

Since \(s\) and \(a\) were arbitrary,

\[\mathcal{N} \models \forall y \left(\varphi(\bar{n_1},\dots,\bar{n_{\ell}}, y) \leftrightarrow y = \bar{m}\right).\]

\(\square\)

Theorem (Minimization is Definable). If \(f : \mathbb{N}^{k+1} \rightarrow \mathbb{N}\) is definable by a formula \(\varphi_f(z, x_1, \dots, x_k, u)\), then the minimization function \(\mu(f) : \mathbb{N}^k \rightarrow \mathbb{N}\) is definable.

Proof. \(\mu(f)\) is defined by the following formula:

\[\varphi(x_1, \dots, x_k, y) \equiv \varphi_f(y, x_1, \dots, x_k, 0) \land \forall z \left(z \lt y \rightarrow \exists u \left(\varphi_f(z, x_1, \dots, x_k, u) \land u \ne 0 \right)\right).\]

Let \(n_1,\dots, n_k \in \mathbb{N}\) be any natural numbers. Suppose that \(\mu(f)(n_1,\dots,n_k)\) is defined and let \(m = \mu(f)(n_1,\dots,n_k)\).

There are three possibilities: \(a = m\), \(a \lt m\), or \(a \gt m\).

Suppose \(a = m\). Then, \(\mathcal{N},s[a/y] \models y = \bar{m}\).

Next, suppose \(a \lt m\) and \(\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k},y)\). Then, \(\mathcal{N},s[a/y] \models \varphi_f(y,\bar{n_1},\dots,\bar{n_k},0)\), and, by the numeral substitution lemma, \(\mathcal{N},s \models \varphi_f(\bar{a},\bar{n_1},\dots,\bar{n_k},0)\). Since \(f\) is defined by \(\varphi_f\), by definition

\[\mathcal{N}\models \forall z \left(\varphi_f(\bar{a}, \bar{n_1},\dots,\bar{n_k}, z) \leftrightarrow z = \bar{m_f}\right),\]

where \(m_f = f(a, n_1, \dots, n_k)\), and thus in particular

\[\mathcal{N},s[0/z] \models \varphi_f(\bar{a}, \bar{n_1},\dots,\bar{n_k}, z) \leftrightarrow z = \bar{m_f},\]

which, by the numeral substitution lemma, implies that

\[\mathcal{N},s \models \varphi_f(\bar{a}, \bar{n_1},\dots,\bar{n_k}, 0) \leftrightarrow 0 = \bar{m_f}.\]

Since \(\mathcal{N},s \models \varphi_f(\bar{a},\bar{n_1},\dots,\bar{n_k},0)\), it follows that \(\mathcal{N},s \models 0 = \bar{m_f}\), and hence \(m_f = 0\). Thus, \(f(a,n_1,\dots,n_k) = 0 = f(m,n_1,\dots,n_k)\) and \(a \lt m\), which contradicts the fact that \(m\) is the least value such that \(0 = f(m,n_1,\dots,n_k)\). Therefore, if \(a \lt m\), then \(\mathcal{N},s[a/y] \not \models \varphi(\bar{n_1},\dots,\bar{n_k},y)\).

Next, suppose \(a \gt m\) and \(\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k},y)\). Then,

\[\mathcal{N},s[a/y] \models \forall z \left(z \lt y \rightarrow \exists u \left(\varphi_f(z, x_1, \dots, x_k, u) \land u \ne 0 \right)\right),\]

and thus, in particular

\[\mathcal{N},s[a/y, \bar{m}/z] \models z \lt y \rightarrow \exists u \left(\varphi_f(z, x_1, \dots, x_k, u) \land u \ne 0 \right),\]

which, by the numeral substitution lemma, implies that

\[\mathcal{N},s[a/y] \models \bar{m} \lt y \rightarrow \exists u \left(\varphi_f(\bar{m}, x_1, \dots, x_k, u) \land u \ne 0 \right).\]

Since \(a \gt m\), it follows that \(\mathcal{N},s[a/y] \models \bar{m} \lt y\), and thus

\[\mathcal{N},s[a/y] \models \exists u \left(\varphi_f(\bar{m}, x_1, \dots, x_k, u) \land u \ne 0 \right).\]

This means that there exists a \(b \in \mathbb{N}\) such that

\[\mathcal{N},s[a/y,b/u] \models \varphi_f(\bar{m}, x_1, \dots, x_k, u) \land u \ne 0 .\]

Since \(\varphi_f\) defines \(f\) and \(f(m, n_1, \dots, n_k) = 0\) it follows that

\[\mathcal{N} \models \forall u \left( \varphi_f(\bar{m}, \bar{n_1}, \dots, \bar{n_k}, u) \leftrightarrow u = 0\right),\]

and thus

\[\mathcal{N},s[b/u] \models \varphi_f(\bar{m}, \bar{n_1}, \dots, \bar{n_k}, u) \leftrightarrow u = 0.\]

But then \(\mathcal{N},s[a/y,b/u] \models u \ne 0\) and \(\mathcal{N},s[a/y,b/u] \models u = 0\), so \(u=0\) and \(u \ne 0\), a contradiction. Therefore, if \(a \gt m\), then \(\mathcal{N},s[a/y] \not \models \varphi(\bar{n_1},\dots,\bar{n_k}, y)\).

Thus, whether \(a = m\), \(a \lt m\), or \(a \gt m\), either \(\mathcal{N},s[a/y] \not \models \varphi(\bar{n_1},\dots,\bar{n_k}, y)\) or \(\mathcal{N},s[a/y] \models y = \bar{m}\), and thus

\[\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k}, y) \rightarrow y = \bar{m}.\]

Converse

Let \(a \in \mathbb{N}\) be any natural number. There are two possibilities: either \(a = m\), or \(a \ne m\).

If \(a \ne m\), then \(\mathcal{N},s[a/y] \not \models y = \bar{m}\).

Suppose \(a = m\). Since \(f\) is defined by \(\varphi_f\) and \(f(a,n_1,\dots,n_k) = 0\), it follows that

\[\mathcal{N},s[0/u]\models \varphi_f(\bar{a}, \bar{n_1}, \dots, \bar{n_k}, u) \leftrightarrow u = 0,\]

which then implies that

\[\mathcal{N},s[0/u] \models \varphi_f(\bar{a}, \bar{n_1}, \dots, \bar{n_k}, u),\]

which, by the numeral substitution lemma, means that

\[\mathcal{N},s \models \varphi_f(\bar{a}, \bar{n_1}, \dots, \bar{n_k}, 0),\]

and, again, by the numeral substitution lemma,

\[\mathcal{N},s[a/y] \models \varphi_f(y, \bar{n_1}, \dots, \bar{n_k}, 0).\]

Let \(b \in \mathbb{N}\) be any natural number. There are two possibilities: \(b \lt a\), or \(b \ge a\). If \(b \ge a\), then \(\mathcal{N},s[a/y,b/z] \not \models z \lt y\). Suppose \(b \lt a\). Define \(c = f(b, \bar{n_1},\dots,\bar{n_k})\). By definition of \(\mu(f)\), it must be the case that \(c \ne 0\) since \(b \lt a\) and \(\mu(f)(n_1,\dots,n_k) = a\). Thus, \(\mathcal{N},s[a/y,b/z,c/u] \models u \ne 0\). Since \(\varphi_f\) defines \(f\), it follows that

\[\mathcal{N} \models \forall u \left( \varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \leftrightarrow u = \bar{c}\right)\]

and thus

\[\mathcal{N},s[a/y,b/z,c/u] \models \varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \leftrightarrow u = \bar{c},\]

and, since \(\mathcal{N},s[a/y,b/z,c/u] \models u = \bar{c}\), it follows that

\[\mathcal{N},s[a/y,b/z,c/u] \models \varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u).\]

Thus, it follows that

\[\mathcal{N},s[a/y,b/z] \models \exists u \left(\varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \land u \ne 0\right).\]

Since, regardless of whether \(b \lt a\) or \(b \ge a\), it is the case that either \(\mathcal{N},s[a/y,b/z] \not \models z \lt y\) or \(\mathcal{N},s[a/y,b/z] \models \exists u \left(\varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \land u \ne 0\right)\), it follows that

\[\mathcal{N},s[a/y] \models \forall z \left( z \lt y \rightarrow \exists u \left(\varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \land u \ne 0\right)\right),\]

and likewise that

\[\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k}, y) \equiv \varphi_f(y,\bar{n_1},\dots,\bar{n_k}, 0) \land \forall z \left( z \lt y \rightarrow \exists u \left(\varphi_f(\bar{b}, \bar{n_1}, \dots, \bar{n_k}, u) \land u \ne 0\right)\right).\]

Since, regardless of whether \(a=m\) or \(a \ne m\), either \(\mathcal{N},s[a/y] \models y \ne \bar{m}\) or \(\mathcal{N},s[a/y] \models \varphi(\bar{n_1},\dots,\bar{n_k}, y)\), it follows that

\[\mathcal{N},s[a/y] \models y = \bar{m} \rightarrow \varphi(\bar{n_1},\dots,\bar{n_k}, y).\]

Conclusion

It then follows that

\[\mathcal{N} \models \forall y \left( \varphi(\bar{n_1},\dots,\bar{n_k}, y) \leftrightarrow y = \bar{m}\right).\]

\(\square\)

Definability of Primitive Recursive Functions

The primitive recursive functions are much more difficult to define since they are the only class of recursive functions that is actually defined via recursion. We will simply state the iterative characterization of the primitive recursive functions using a formula. However, since this characterization refers to a sequence of natural numbers, we need some way to define sequences. First, we will establish a few preliminary results from number theory.

The Chinese Remainder Theorem

The Chinese Remainder Theorem is essential for encoding sequences of numbers.

Theorem (Chinese Remainder). For any pairwise coprime finite sequence of integers \(n_1, \dots, n_k\) (called moduli or divisors) such that \(n_i \gt 1\) and any finite sequence \(a_1, \dots, a_k\) of integers such that \(0 \le a_i \lt n_i\), there exists a unique integer \(x\) such that \(0 \le x \lt N\) (where \(N = \prod_{i=1}^k n_i\)) and \(x \bmod n_i = a_i\).

Proof. (Uniqueness). Suppose \(x_1\) and \(x_2\) are each solutions to the system of congruences, i.e.,

\[x_1 \bmod n_i = a_i = x_2 \bmod n_i.\]

Then, by properties of modular arithmetic, it follows that

\begin{align*}(x_1 - x_2) \bmod n_i &= ((x_1 \bmod n_i) - (x_2 \bmod n_i)) \bmod n_i \\&= (a_i - a_i) \bmod n_i \\&= 0.\end{align*}

This means that each modulus \(n_i\) divides \(x_1 - x_2\), i.e., that \(x_1 - x_2\) is a multiple of every modulus \(n_i\). By the fundamental theorem of number theory, each of the \(n_i\) is the product of prime numbers \(p^i_j\). Since the moduli \(n_i\) are pairwise coprime, by definition, \(\mathrm{gcd}(n_{i_1}, n_{i_2}) = 1\) and hence the sets \(\{p^{i_1}_{j_1}\}\) and \(\{p^{i_2}_{j_2}\}\) are disjoint. Since \(n_i\lvert (x_1 - x_2)\), \(x_1 - x_2\) must contain all the prime factors of \(n_i\) (with at least as many instances of each). Then the product \(n_1\dots n_k = N\) combines all these prime factors without any duplication, so \(N \lvert (x_1 - x_2)\), i.e. \((x_1 - x_2) \bmod N = 0\). Since \(x_1 \lt N\) and \(x_2 \lt N\), then \((x_1 - x_2) \bmod N = 0\) implies that \(x = y\).

(Existence). The map

\[x \in \mathbb{N} \mapsto (x \bmod n_1, \dots, x \bmod n_k) \in \mathbb{N}^k\]

is injective since we previously established that there is a unique \(x\) satisfying this property. Since \(\mathbb{N} \cong \mathbb{N}^k\), this map is also surjective, and hence, for any tuple \((a_1, \dots, a_k) \in \mathbb{N}^k\), there exists an \(x \in \mathbb{N}\) such that

\[(x \bmod n_1, \dots, x \bmod n_k) = (a_1, \dots, a_k) \in \mathbb{N}^k.\]

\(\square\)

This proof is non-constructive, but that is sufficient for our purposes. It is also possible to indicate a constructive proof.

Although this result was established in the context of the integers (since we made use of subtraction, etc.), it is effectively restricted to the natural numbers since the moduli \(n_i\) are all restricted such that \(n_i \gt 1\) and the sequence \((a_i)\) is restricted such that \(a_i \ge 0\) and also \(x \ge 0\).

The Chinese Remainder Theorem indicates a means for representing sequences as numbers: assuming we have appropriate moduli \((n_i)\), we can represent any sequence \((a_i)\) via the single number \(x\).

Determining Moduli

Next, we will indicate how to determine an appropriate sequence of moduli.

Theorem (Moduli). For every sequence \(a_1, \dots, a_k\) of natural numbers, there exists a natural number \(N\) and a corresponding pairwise coprime sequence \(n_1, \dots, n_k\) defined such that \(n_i = N \cdot i + 1\) and \(a_i \lt n_i\).

Proof. Let \(n\) be any natural number such that \(a_i \lt n\) for all \(a_i\). Define \(N = n!\). Consider any pair \(n_i\) and \(n_j\) of elements of the sequence such that \(i \lt j\). Suppose that there exists a prime number \(p\) such that p divides both \(n_i\) and \(n_j\). Then, by definition, \(p\) divides both \(N \cdot i + 1\) and \(N \cdot j + 1\). This means that \(p\) divides the difference \(N(j - i) = n_j - n_i\). The difference \(N(j-i)\) is a product of factors, each of which is less than \(n\), and since this product is divisible by \(p\), \(p\) likewise divides one of these factors, i.e., \(p \le n\). But then \((N \cdot i) + 1 \bmod p = 1\) and \((N \cdot j) + 1 \bmod p = 1\), so \(p\) divides neither \(n_i\) nor \(n_j\), a contradiction. Therefore, there exists no such prime number \(p\) that divides both \(n_i\) and \(n_j\), i.e., \(n_i\) and \(n_j\) are coprime. Since \(a_i \lt n\) and \(N = n!\), \(a_i \lt N\) and \(a_i \lt N \cdot i + 1\) for all \(1 \le i \le k\) and so \(a_i \lt n_i\). \(\square\)

Thus, we can represent the moduli using a single number \(N\). We can therefore represent any sequence using a pair of numbers.

Beta Function

We will define the \(\beta\)-function, which accepts a pair of numbers \((s,t)\) encoding a sequence and an index \(i\) and outputs the \(i\)-th term of this sequence. However, since we want this function to be defined for all natural numbers (including \(0\)), we will define it for sequences whose index starts at \(0\) rather than \(1\).

Lemma (\(\mathbf{\beta}\)-function). For any sequence of natural numbers \(a_0, \dots, a_k\), there exist natural numbers \(s\) and \(t\) such that

\[a_i = \beta(s,t,i),\]

where

\[\beta(s,t,i) = s \bmod \left(t \cdot (i+1) + 1\right).\]

Proof. The sequence \(a_0, \dots, a_k\) corresponds to a sequence \(a'_1, \dots, a'_{k+1}\) such that \(a_i = a'_{i+1}\). By the moduli theorem, there exists a natural number \(N\) and a corresponding pairwise coprime sequence of natural numbers \(n_1, \dots, n_{k+1}\) such that \(n_i = N \cdot i + 1\) and \(a'_i \lt n_i\). By the Chinese Remainder Theorem, there exists a unique natural number \(x\) such that \(a'_i = x \bmod n_i\). Letting \(s = x\) and \(t = N\) and noting that \(a_i = a'_{i+1}\) yields the desired result. \(\square\)

Next, we will show that the \(\beta\)-function is definable.

Theorem (\(\mathbf{\beta}\)-function is Definable). The \(\beta\) function is definable.

Proof. The \(\beta\)-function is defined by the following formula (where we use infix notation for legibility):

\[\varphi(s, t, i, y) \equiv \exists q \left((y \lt t \cdot (i+1)+1) \land q \cdot (t \cdot (i+1) + 1) + y = s\right).\]

Let \(s\) be any valuation and \(a\) any natural number. Let \(s,t,i\) be any natural numbers, and define \(m = \beta(s,t,i)\). There are two cases: either \(a = m\) or \(a \ne m\).

If \(a=m\) then \(\mathcal{N},s[a/y] \models y = \bar{m}\).

Suppose \(a \ne m\) and \(\mathcal{N},s[a/y] \models \varphi(\bar{s}, \bar{t}, \bar{i}, y)\). Then, by definition, there exists some natural number \(b\) such that \(\mathcal{N},s[a/y,b/q] \models y \lt \bar{t} \cdot (\bar{i}+1)+1\) and \(\mathcal{N},s[a/y,b/q] \models q \cdot (\bar{t} \cdot (\bar{i}+1) + 1) + y = \bar{s}\), which, by definition, means that \(a \lt t \cdot (i+1)+1\) and \(b \cdot (t \cdot (i+1) + 1) + a = s\), i.e., that \(a = s \bmod (t \cdot (i+1) + 1) = \beta(s,t,i) = m\), a contradiction. Thus, if \(a \ne m\), then \(\mathcal{N},s[a/y] \not \models \varphi(\bar{s},\bar{t}, \bar{i}, y)\).

Whether \(a=m\) or \(a \ne m\), either \(\mathcal{N},s[a/y] \not \models \varphi(\bar{s},\bar{t}, \bar{i}, y)\) or \(\mathcal{N} \models y = \bar{m}\), and thus

\[\mathcal{N},s[a/y] \models \varphi(\bar{s}, \bar{t}, \bar{i}, y) \rightarrow y = \bar{m}.\]

Converse

If \(a \ne m\), then \(\mathcal{N},s[a/y] \not \models y = \bar{m}\).

Suppose \(a = m\). Let \(b\) denote the quotient, i.e., the unique natural number such that \(b \cdot (t \cdot (i+1) + 1) + m = s\). Then, since \(a \lt t \cdot (i+1)+1\) it follows that \(\mathcal{N},s[a/y,b/q] \models \bar{a} \lt \bar{t} \cdot (\bar{i}+1)+1\) and since \(\mathrm{val}^{\mathcal{N}}_{s[a/y,b/q]}\left(q \cdot (\bar{t} \cdot (\bar{i}+1) + 1) + y\right) = \mathrm{val}^{\mathcal{N}}_{s[a/y,b/q]}(\bar{s})\), it follows that \(\mathcal{N},s[a/y,b/q] \models q \cdot (\bar{t} \cdot (\bar{i}+1) + 1) + y = \bar{s}\), which further means that \(\mathcal{N},s[a/y] \models \exists q \left((y \lt \bar{t} \cdot (\bar{i}+1)+1) \land q \cdot (\bar{t} \cdot (\bar{i}+1) + 1) + y = \bar{s}\right) \equiv \varphi(\bar{s}, \bar{t}, \bar{i}, y)\).

Thus, whether \(a=m\) or \(a \ne m\), either \(\mathcal{N} \not \models y = \bar{m}\) or \(\mathcal{N},s[a/y] \models \varphi(\bar{s}, \bar{t}, \bar{i}, y)\), so

\[\mathcal{N},s[a/y] \models y = \bar{m} \rightarrow \varphi(\bar{s}, \bar{t}, \bar{i}, y).\] \(\square\)

Conclusion

This means that

\[\mathcal{N},s[a/y] \models \varphi(\bar{s}, \bar{t}, \bar{i}, y) \leftrightarrow y = \bar{m}.\]

Since \(a\) was arbitrary, it follows that

\[\mathcal{N} \models \forall y \left(\varphi(\bar{s}, \bar{t}, \bar{i}, y) \leftrightarrow y = \bar{m}\right).\]

\(\square\)

Iterative Definition of Primitive Recursive Functions

We can now write a formula that defines a primitive recursive function by translating the iterative characterization of a primitive recursive function into a logical formula using the \(\beta\)-function.

Theorem (Primitive Recursive Functions are Definable). For any recursive function \(f : \mathbb{N}^k \rightarrow \mathbb{N}\) and any recursive function \(g : \mathbb{N}^{k+2} \rightarrow \mathbb{N}\), if \(f\) is defined by a formula \(\varphi_f\) and \(g\) is defined by a formula \(\varphi_g\), then the primitive recursive function \(\rho(f,g) : \mathbb{N}^{k+1} \rightarrow \mathbb{N}\) is definable.

Proof. The primitive recursive function \(\rho(f,g)\) is defined by the following formula:

\begin{align*}\varphi(x, x_1, \dots, x_k, y) \equiv \exists s \exists t \left(\exists y_0 \left(\varphi_{\beta}(s, t, 0, y_0) \land \varphi_f(x_1, \dots, x_k, y_0)\right) \land \forall i \lt x \exists y_1 \exists y_2 \left(\varphi_{\beta}(s,t,i, y_1) \land \varphi_{\beta}(s,t,S(i),y_2) \land \varphi_g(y_1, i, x_1, \dots, x_k, y_2)\right) \land \varphi_{\beta}(s,t,x,y)\right).\end{align*}

\(\square\)

All Recursive Functions are Definable

Thus, having proved that the constant functions, projection functions, successor function, composition, minimization, and primitive recursive functions are all definable, we have established the following theorem:

Theorem (Recursive Functions are Definable). All recursive functions are definable.

Conclusion

The definability of recursive functions can be used to establish their representability in particular formal theories of arithmetic, which is a much stronger result.