A Subtheory of Number Theory and Representability

The full theory of arithmetic is neither decidable nor axiomatizable, so no manageable axiom set captures it. A finite fragment still captures enough: it proves concrete numerical facts, and through them facts about decision procedures. That fragment, the subtheory $A_E$, is measured by a new notion — representability — which replaces the formula is true of the right numbers with the axioms prove the right instances. Representability connects computation to provability, and the incompleteness theorems depend on that connection.

Working in the full language helps even though it is redundant. In $(\mathbb{N};\cdot ,E)$ one can already define $0$, $S$, $<$, and $+$, and in $(\mathbb{N};+,\cdot )$ one can define $E$ along with the rest. Keeping every symbol, exponentiation especially, shortens the proofs.¹

The axioms $A_E$

Let $A_E$ be the following eleven sentences, writing $x\le y$ for $x<y\vee x=y$. The first five govern successor and order; the last six are the recursion equations for the three operations.

Since $\mathfrak{N}$ satisfies every axiom, $\text{Cn }{A}_E\subseteq \text{Th }\mathfrak{N}$. The inclusion is strict: $A_E$ does not prove S3, the sentence $\forall y(y\ne 0\to \exists xy=Sx)$ asserting every nonzero number is a successor.² $A_E$ is deliberately weak. Everything it proves is elementary enough to be checked by hand, and that suffices.

Facts provable in the subtheory

$A_E$ decides the finite facts. Two lemmas make this precise.

Part (b) says $A_E$ proves that the numbers below $k+1$ are exactly $0,1,\dots ,k$. The proof is induction on $k$ in the metalanguage, using L1 to peel off the top value at each step. A consequence: in any model of $A_E$, the standard points named by numerals are ordered in the natural way, and any nonstandard points lie above all of them.²

Uniqueness holds because $A_E$ proves $S^{m}0\ne S^{n}0$ whenever $m\ne n$ (from S1 and S2). Existence is induction on $t$: numerals for $0$ and $S$ are immediate, and A1–A2, M1–M2, E1–E2 let $A_E$ compute a sum, product, or power of two numerals down to a single numeral. The proof is a set of instructions: given a closed term, effectively find the numeral it equals. $A_E$ can carry out $2+2=4$ and every other ground computation.²

The evaluation of closed terms lifts to whole quantifier-free sentences, and even past them.

If $\exists v_1\exists v_2\theta$ is true, then $\theta (S^{m}0,S^{n}0)$ is a true quantifier-free sentence for some $m,n$, hence provable by the quantifier-free completeness of the subtheory, and it implies the existential. The symmetry stops here: there are true universal sentences $\forall x_1\dots \forall x_k\theta$ that $A_E$ does not prove. Weak as it is, $A_E$ handles bounded and existential facts and no more.²

Representability

Definability asks whether a formula is true of exactly the right tuples in $\mathfrak{N}$. Representability asks whether a theory can prove the right instances.

For $T=\text{Cn }{A}_E$ the two conditions read $A_E⊢\rho (\dots )$ and $A_E⊢\neg \rho (\dots )$: the axioms settle each numeral instance the correct way. For $T=\text{Th }\mathfrak{N}$, representing is the same as defining, since membership in $\text{Th }\mathfrak{N}$ is truth. The equality relation is represented in $\text{Cn }{A}_E$ by $v_1=v_2$, since $A_E$ proves $S^{m}0=S^{n}0$ when $m=n$ and refutes it when $m\ne n$.

For a theory contained in $\text{Th }\mathfrak{N}$, representability splits into a semantic half and a syntactic half. Call $\phi$ numeralwise determined by $A_E$ if for every tuple, $A_E$ proves $\phi (\dots )$ or proves $\neg \phi (\dots )$ (it decides each numeral instance one way or the other).

Since $\mathfrak{N}$ is a model of $A_E$, provability implies truth, so condition (2) is forced and the whole burden is condition (1): making $A_E$ strong enough to adjudicate each instance.³ The following table places the two notions side by side.

Recursiveness and Church's thesis

Representability connects to computation through decidability.

The decision procedure enumerates the theorems of $T$ (effectively enumerable, since $T$ is axiomatizable). Given $\vec{a}$, wait until either $\rho (S^{\vec{a}}0)$ or $\neg \rho (S^{\vec{a}}0)$ appears; representability guarantees one does, and consistency guarantees it is the correct verdict.⁴

The converse cannot be proved from an informal notion of decidability; asserting it is a judgment, not a theorem.

The thesis is supported, not proved. Every relation mathematicians have judged decidable has turned out recursive, and every independent formalization of effective procedure (Turing machines chief among them, in 1936) has defined the same class. The coincidence of so many routes is the evidence for the identification, which is why it is also called the Church–Turing thesis.⁴

Functions get a parallel treatment. A function $f:{\mathbb{N}}^k\to \mathbb{N}$ is computable if some effective procedure produces $f(\vec{a})$ from $\vec{a}$. Viewing $f$ as its graph, a $(k+1)$-ary relation, ties computability to the relational notions.

Any relation representable in $\text{Cn }{A}_E$ is recursive, since $A_E$ is consistent and finite. The converse holds too, proved later: every recursive relation is representable in the single theory $\text{Cn }{A}_E$, so recursiveness and representability in $A_E$ coincide.⁴ Choosing $A_E$ was motivated by exactly this: it is weak enough to check and strong enough to represent every recursive relation.

Building the catalog

To make the coincidence useful, one shows concrete relations and functions are representable. The representability criterion reduces this to finding a defining formula that is numeralwise determined by $A_E$, and numeral determination has good closure properties.

Part (c) carries most of the load and is the reason $A_E$ suffices. To decide $\exists x(x<S^{a}0\wedge \phi )$, the small-numbers lemma lets $A_E$ replace the bound by the explicit disjunction $x=0\vee \cdots \vee x=S^{a-1}0$, turning the bounded quantifier into a finite Boolean combination of instances it already decides.³ Unbounded quantifiers are not covered, and cannot be: it is possible for $A_E$ to prove $\neg \psi (S^{n}0)$ for every $n$ without proving $\forall x\neg \psi (x)$.

The set of primes is represented in $\text{Cn }{A}_E$ by the bounded formula

which defines the primes in $\mathfrak{N}$ and, being built from atomic formulas by connectives and bounded quantifiers, is numeralwise determined.

Representable functions and their closure

A formula $\phi$ functionally represents $f:{\mathbb{N}}^m\to \mathbb{N}$ in $\text{Cn }{A}_E$ iff for all $\vec{a}$,

the $\leftarrow$ half giving the correct value and the $\to$ half adding uniqueness. A function representable as a relation is functionally representable, after adjoining a least-witness clause (Theorem 33K). The representable functions are closed under the operators that generate the recursive functions.⁵

The minimization operator $\mu b[g(\vec{a},b)=0]$ returns the least $b$ with $g(\vec{a},b)=0$, and is represented by formalizing $g(\vec{a},b)=0$ and no smaller value works:

a bounded formula whenever $\psi$ represents $g$.⁵ Primitive recursion is the subtle case, because $f(a+1,\vec{b})$ depends on the earlier value $f(a,\vec{b})$, and expressing that inside arithmetic requires encoding a whole finite sequence of values as a single number.

Coding finite sequences

Enderton's coding uses prime powers. Writing $p_i$ for the $(i+1)$st prime ($p_0=2$, $p_1=3$, $p_2=5,\dots$),

with the empty sequence coded by $1$. A decoding function $(a{)}_b$ recovers the $b$-th entry, a length function $\mathrm{lh}$ recovers $m+1$, and a concatenation operation joins two coded sequences; all are representable, built from divisibility and the prime-listing function by the operators above.⁵ With sequence coding in hand, primitive recursion becomes representable: $f(a,\vec{b})$ is the code of the finite sequence of earlier values, defined as the least sequence number of the right length whose entries obey the recursion.

Two gaps remain, both closed elsewhere. The prime-power code grows fast; a polynomial pairing function $J(a,b)=\frac{1}{2}[(a+b{)}^2+3a+b]$ and Gödel's $\beta$-function do the same job with only addition and multiplication, which is what lets exponentiation be represented in $(\mathbb{N};+,\cdot )$. And the equivalence of recursiveness with representability in $A_E$, together with the arithmetization of syntax, turns the catalog assembled here into representable predicates about formulas and deductions. Those are the ingredients the diagonal argument of the incompleteness theorem uses.