---
title: A Subtheory of Number Theory and Representability
module: Number Theory and Definability
moduleNumber: 6
lessonNumber: 4
order: 604
summary: >
  A finite set of eleven axioms, the recursion equations for successor, order,
  addition, multiplication, and exponentiation, already proves every true
  quantifier-free and existential sentence. Representability asks a theory to
  prove the right instances of a formula rather than merely make them true, and a
  relation is defined to be recursive exactly when some consistent finite theory
  represents it. Church's thesis identifies that with decidability, and closure
  under composition, minimization, and primitive recursion builds the catalog the
  incompleteness proofs need.
topics: [Number Theory and Definability]
sources:
  - book: Enderton
    ref: "Ch. 3 — Undecidability; §3.3 A Subtheory of Number Theory"
draft: false
---

The [full theory of arithmetic](/logic/arithmetic-and-definability/definability-in-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](/logic/incompleteness/incompleteness-and-undecidability)
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.[^econ]

## 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.

| Group | Axiom | Statement |
| --- | --- | --- |
| successor | S1 | $\forall x\ Sx \neq 0$ |
| | S2 | $\forall x\, \forall y\, (Sx = Sy \rightarrow x = y)$ |
| order | L1 | $\forall x\, \forall y\, (x < Sy \leftrightarrow x \le y)$ |
| | L2 | $\forall x\ x \not< 0$ |
| | L3 | $\forall x\, \forall y\, (x < y \vee x = y \vee y < x)$ |
| addition | A1 | $\forall x\ x + 0 = x$ |
| | A2 | $\forall x\, \forall y\ x + Sy = S(x + y)$ |
| multiplication | M1 | $\forall x\ x \cdot 0 = 0$ |
| | M2 | $\forall x\, \forall y\ x \cdot Sy = x \cdot y + x$ |
| exponentiation | E1 | $\forall x\ x E 0 = S0$ |
| | E2 | $\forall x\, \forall y\ x E Sy = (x E y) \cdot x$ |

$$
% caption: The eleven axioms of A_E group into five roles: two fixing successor,
% three fixing order, and one pair of recursion equations for each of addition,
% multiplication, and exponentiation.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  g/.style={draw, minimum width=34mm, minimum height=10mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[g] (s)  at (5.6,2.6)   {successor\\S1, S2};
  \node[g] (o)  at (5.6,1.3)   {order\\L1, L2, L3};
  \node[g] (a)  at (5.6,0)     {addition\\A1, A2};
  \node[g] (m)  at (5.6,-1.3)  {multiplication\\M1, M2};
  \node[g] (e)  at (5.6,-2.6)  {exponentiation\\E1, E2};
  \node[g, draw=acc, text=acc, thick] (ae) at (0,0) {f\/inite theory\\eleven axioms};
  \draw[->, acc] (ae.east) -- (s.west);
  \draw[->, acc] (ae.east) -- (o.west);
  \draw[->, acc] (ae.east) -- (a.west);
  \draw[->, acc] (ae.east) -- (m.west);
  \draw[->, acc] (ae.east) -- (e.west);
\end{tikzpicture}
$$

Since $\fN$ satisfies every axiom, $\Cn A_E \subseteq
\Th\fN$. The inclusion is strict: $A_E$ does not prove S3,
the sentence $\forall y\, (y \neq 0 \rightarrow \exists x\ y = Sx)$ asserting every
nonzero number is a successor.[^ae] $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.

> **Lemma (Knowledge of small numbers).**
> - (a) $A_E \vdash \forall x\ x \not< 0$.
> - (b) For each natural number $k$,
>   $$
>   A_E \vdash \forall x\, \bigl( x < S^{k+1} 0 \leftrightarrow x = S^0 0 \vee
>   \dots \vee x = S^k 0 \bigr).
>   $$

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.[^ae]

> **Lemma (Evaluation of closed terms).** For every variable-free term $t$
> there is a unique natural number $n$ with $A_E \vdash t = S^n 0$.

Uniqueness holds because $A_E$ proves $S^m 0 \neq S^n 0$ whenever $m \neq 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.[^ae]

> **Worked example (Evaluating $2 + 2$ in $A_E$).** Reduce $S^2 0 + S^2 0$ to a
> numeral using only A1 and A2. Peel the second summand with A2
> ($x + Sy = S(x+y)$), twice:
> $$
> S^2 0 + S^2 0 = S^2 0 + S(S0) = S\bigl(S^2 0 + S0\bigr) = S\bigl(S(S^2 0 + 0)\bigr).
> $$
> Then A1 ($x + 0 = x$) closes the inner sum, $S^2 0 + 0 = S^2 0$, so
> $$
> S^2 0 + S^2 0 = S\bigl(S(S^2 0)\bigr) = S^4 0.
> $$
> Hence $A_E \vdash S^2 0 + S^2 0 = S^4 0$, the formal content of "$2 + 2 = 4$."
> The value is unique: by S1 and S2, $A_E$ proves $S^m 0 \neq S^n 0$ whenever
> $m \neq n$, so no other numeral is provably equal to this sum.

$$
% caption: Each numeral is the successor symbol prefixed to zero a fixed number of
% times; the subtheory proves the value of any closed term equals exactly one
% numeral.
\begin{tikzpicture}[>=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \foreach \x/\term/\val in {0/{0}/0, 2.2/{S0}/1, 4.4/{SS0}/2, 6.6/{SSS0}/3} {
    \node[draw, acc, minimum width=14mm, minimum height=8mm] (t\val) at (\x,0.9) {\term};
    \node (v\val) at (\x,-0.4) {\val};
    \draw[->, acc] (\x,0.5) -- (\x,-0.15);
  }
  \node[anchor=west, font=\scriptsize] at (7.8,0.9) {numeral};
  \node[anchor=west, font=\scriptsize] at (7.8,-0.4) {number};
\end{tikzpicture}
$$

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

> **Theorem (The subtheory decides quantifier-free sentences).** Every quantifier-free sentence true in $\fN$ is a
> theorem of $A_E$; every false one is refuted by $A_E$.

> **Corollary (The subtheory proves true existential sentences).** Every existential sentence ($\exists x_1 \dots \exists x_k
> \,\theta$ with $\theta$ quantifier-free) true in $\fN$ is a theorem of
> $A_E$.

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.[^ae]

## Representability

Definability asks whether a formula is true of exactly the right tuples in
$\fN$. Representability asks whether a theory can **prove** the right
instances.

> **Definition (Represents).** A formula $\rho$ (with only $v_1, \dots, v_m$ free)
> _represents_ an $m$-ary relation $R$ in a theory $T$ iff for all $a_1, \dots,
> a_m$,
> $$
> \langle a_1, \dots, a_m\rangle \in R \implies \rho(S^{a_1}0, \dots, S^{a_m}0)
> \in T,
> $$
> $$
> \langle a_1, \dots, a_m\rangle \notin R \implies \bigl(\neg\, \rho(S^{a_1}0,
> \dots, S^{a_m}0)\bigr) \in T.
> $$
> $R$ is _representable in $T$_ iff some formula represents it.

For $T = \Cn A_E$ the two conditions read $A_E \vdash \rho(\dots)$ and
$A_E \vdash \neg\,\rho(\dots)$: the axioms settle each numeral instance the correct
way. For $T = \Th\fN$, representing is the same as defining,
since membership in $\Th\fN$ is truth. The equality relation
is represented in $\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 \neq n$.

> **Worked example (Representing $<$ in $\Cn A_E$).** The formula $v_1 < v_2$
> represents $\{\langle m, n\rangle : m < n\}$, and both clauses must be checked
> on numerals. For the positive instance $1 < 3$, the small-numbers lemma gives
> $$
> A_E \vdash \forall x\, \bigl( x < S^3 0 \leftrightarrow x = 0 \vee x = S0 \vee
> x = S^2 0 \bigr),
> $$
> and $S0$ is among the listed values, so $A_E \vdash S0 < S^3 0$. For the
> negative instance $3 < 1$, the same lemma gives $A_E \vdash \forall x\,(x < S0
> \leftrightarrow x = 0)$; since $A_E \vdash S^3 0 \neq 0$ by S1, substituting
> $x = S^3 0$ yields $A_E \vdash \neg\, S^3 0 < S0$. Every numeral instance is
> settled the correct way, so $v_1 < v_2$ is numeralwise determined and
> represents $<$.

$$
% caption: To represent a relation, the axioms must decide every numeral instance
% the right way: prove the formula when the tuple is in the relation, prove its
% negation when the tuple is out.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  b/.style={draw, minimum width=30mm, minimum height=10mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{grn}{HTML}{2E7D46}
  \definecolor{red}{HTML}{B23A48}
  \node[b] (tup) at (0,0) {tuple of numbers};
  \node[b, draw=grn, text=grn] (in)  at (5.4,1.2)  {in the relation};
  \node[b, draw=red, text=red] (out)  at (5.4,-1.2) {out of the relation};
  \node[b] (pr) at (10.6,1.2)  {axioms prove rho};
  \node[b] (nr) at (10.6,-1.2) {axioms prove not rho};
  \draw[->, grn, thick] (tup) -- (in);
  \draw[->, red, thick] (tup) -- (out);
  \draw[->, grn, thick] (in) -- (pr);
  \draw[->, red, thick] (out) -- (nr);
\end{tikzpicture}
$$

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

> **Theorem (Representability criterion).** A formula $\rho$ represents $R$
> in $\Cn A_E$ iff (1) $\rho$ is numeralwise determined by $A_E$, and
> (2) $\rho$ defines $R$ in $\fN$.

Since $\fN$ 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.[^rep] The following table places the two notions side by
side.

| | Definability | Representability in $\Cn A_E$ |
| --- | --- | --- |
| Question about | truth in $\fN$ | deducibility from $A_E$ |
| Positive clause | $\langle \vec a\rangle \in R \Rightarrow\ \models_{\fN} \rho(\vec{S})$ | $\langle \vec a\rangle \in R \Rightarrow A_E \vdash \rho(\vec{S})$ |
| Negative clause | $\langle \vec a\rangle \notin R \Rightarrow\ \models_{\fN} \neg\rho(\vec{S})$ | $\langle \vec a\rangle \notin R \Rightarrow A_E \vdash \neg\rho(\vec{S})$ |
| Strength | weakest | implies definability |

## Recursiveness and Church's thesis

Representability connects to computation through decidability.

> **Theorem (Representable relations are decidable).** Any relation representable in a consistent axiomatizable
> theory $T$ is decidable.

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.[^church]

> **Corollary (Representability in finitely axiomatizable theories).** Any relation representable in a consistent finitely
> axiomatizable theory is decidable.

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

> **Definition (Recursive).** A relation $R$ on $\mathbb{N}$ is _recursive_ iff it
> is representable in some consistent finitely axiomatizable theory (in a language
> with $0$ and $S$).

> **Church's thesis.** A relation is decidable iff it is recursive; recursiveness
> is the correct formal counterpart of the informal notion of decidability.

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.[^church]

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.

> **Theorem (Computability, decidability, and enumerability coincide).** For a function $f : \mathbb{N}^k \to \mathbb{N}$, the
> following are equivalent: (a) $f$ is computable; (b) $f$, as a relation, is
> decidable; (c) $f$, as a relation, is effectively enumerable.

$$
% caption: For a function viewed as its graph, being computable, being a decidable
% relation, and being an effectively enumerable relation all coincide.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  n/.style={draw, minimum width=30mm, minimum height=10mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[n, draw=acc, text=acc] (c) at (90:2.1)  {computable};
  \node[n] (d) at (210:2.4) {decidable graph};
  \node[n] (e) at (330:2.4) {enumerable graph};
  \draw[->, acc, thick] (c) -- (d);
  \draw[->, acc, thick] (d) -- (e);
  \draw[->, acc, thick] (e) -- (c);
\end{tikzpicture}
$$

Any relation representable in $\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 $\Cn A_E$, so
recursiveness and representability in $A_E$ coincide.[^church] 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.

> **Theorem (Numeralwise determination).**
> - (a) Every atomic formula is numeralwise determined by $A_E$.
> - (b) If $\varphi$ and $\psi$ are, so are $\neg\varphi$ and $\varphi \rightarrow
>   \psi$.
> - (c) If $\varphi$ is, so are the **bounded** quantifications
>   $\forall x\,(x < y \rightarrow \varphi)$ and $\exists x\,(x < y \wedge
>   \varphi)$.

Part (c) carries most of the load and is the reason $A_E$ suffices. To decide $\exists x\,(x <
S^a 0 \wedge \varphi)$, the small-numbers lemma lets $A_E$ replace the bound by the explicit
disjunction $x = 0 \vee \dots \vee x = S^{a-1}0$, turning the bounded quantifier
into a finite Boolean combination of instances it already decides.[^rep]
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 $\Cn A_E$ by the bounded formula

$$
S 0 < v_1 \ \wedge\ \forall x\, \bigl(x < v_1 \rightarrow \forall y\,(y < v_1
\rightarrow x \cdot y \neq v_1)\bigr),
$$

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

### Representable functions and their closure

A formula $\varphi$ **functionally represents** $f : \mathbb{N}^m \to \mathbb{N}$
in $\Cn A_E$ iff for all $\vec a$,

$$
A_E \vdash \forall v_{m+1}\, \bigl(\varphi(S^{\vec a} 0, v_{m+1}) \leftrightarrow
v_{m+1} = S^{f(\vec a)} 0\bigr),
$$

the "$\leftarrow$" half giving the correct value and the "$\rightarrow$" 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.[^funcs]

| Operator | Definition | Result |
| --- | --- | --- |
| Base functions | $S$, constants, projections $I^m_i$, and $+, \cdot, E$ by equations | representable |
| Composition | $f(\vec a) = g(h_1(\vec a), \dots, h_n(\vec a))$ | representable (33L) |
| Minimization | $f(\vec a) = \mu b\,[\,g(\vec a, b) = 0\,]$, least zero | representable (33M) |
| Primitive recursion | $f(a{+}1, \vec b)$ from $f(a, \vec b)$ | representable (33P) |

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":

$$
\psi(v_1, v_2, 0) \ \wedge\ \forall y\,(y < v_2 \rightarrow \neg\,\psi(v_1, y, 0)),
$$

a bounded formula whenever $\psi$ represents $g$.[^funcs] 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$),

$$
\langle a_0, \dots, a_m\rangle = \prod_{i \le m} p_i^{\,a_i + 1},
$$

with the empty sequence coded by $1$. A decoding function $(a)_b$ recovers the
$b$-th entry, a length function $\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.[^funcs]
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) = \tfrac{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)$](/logic/computability-and-representability/representing-exponentiation).
And the equivalence of recursiveness with representability in $A_E$, together with
the [arithmetization of syntax](/logic/incompleteness/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](/logic/incompleteness/incompleteness-and-undecidability)
uses.

[^econ]: Enderton, §3.3 — the full language of number theory, the definability of the omitted symbols within $(\mathbb{N}; \cdot, E)$ and $(\mathbb{N}; +, \cdot)$, and the convenience of keeping exponentiation.
[^ae]: Enderton, §3.3 — the axiom set $A_E$, its strict inclusion in $\Th\fN$ (with $A_E \nvdash \text{S3}$), Lemmas 33A–33B, Theorem 33C, and Corollary 33D.
[^rep]: Enderton, §3.3 — the definition of representing a relation, numeralwise determination, Theorem 33E, and Theorem 33I on closure under connectives and bounded quantifiers.
[^church]: Enderton, §3.3 — Theorem 33F and Corollary 33G (representable in a consistent finite theory implies decidable), the definition of recursive, Church's thesis, and Theorem 33H equating computability with decidability and effective enumerability of the graph.
[^funcs]: Enderton, §3.3 — functional representation (Theorems 33J–33K), closure under composition (33L), minimization (33M), and primitive recursion (33P), and the prime-power coding of finite sequences with its decoding, length, and concatenation functions.