---
title: Arithmetization of Syntax
module: Arithmetization and the Incompleteness Theorems
moduleNumber: 7
lessonNumber: 1
order: 701
summary: >
  Gödel numbering assigns a natural number to every symbol, expression,
  formula, and deduction, turning statements about syntax into statements
  about numbers. The syntactic operations — substitution, "is a wff", "is an
  axiom", "d codes a deduction of a" — come out primitive recursive and hence
  representable in the subtheory, which lets a formula of arithmetic talk about
  formulas, including itself.
topics: [Arithmetization and the Incompleteness Theorems]
sources:
  - book: Enderton
    ref: "Ch. 3 — Undecidability; §3.4 Arithmetization of Syntax"
draft: false
---

In the finitely axiomatized subtheory $\Cn A_E$, every recursive relation is
[representable](/logic/arithmetic-and-definability/a-subtheory-and-representability):
a relation $R$ is representable when some formula $\rho$ proves the right
instance for every tuple, $\vec{n} \in R$ giving $A_E \vdash \rho(\vec{S^{n}0})$
and $\vec{n} \notin R$ giving $A_E \vdash \neg\,\rho(\vec{S^{n}0})$.
Representability now applies to syntax itself, through two constructions.[^ov]

- **Coding.** Assertions about wffs can be converted into assertions about
  natural numbers, by assigning a number to every expression.
- **Internalizing.** Many of those (English) assertions about numbers translate
  into the formal language, and $\Cn A_E$ is strong enough to prove the
  translations.

A formula that expresses a fact about numbers can then express a fact about a
formula, including itself.

## Gödel numbers

The symbols of the language of $\fN$ are the parameters and the logical
symbols, each assigned an integer by a fixed function $h$. Parameters get even
numbers, logical symbols odd ones.

| Parameter | $h$ | Logical symbol | $h$ |
| --- | --- | --- | --- |
| $\forall$ | $0$ | $($ | $1$ |
| $0$ | $2$ | $)$ | $3$ |
| $S$ | $4$ | $\neg$ | $5$ |
| $<$ | $6$ | $\to$ | $7$ |
| $+$ | $8$ | $=$ | $9$ |
| $\cdot$ | $10$ | $v_1$ | $11$ |
| $E$ | $12$ | $v_2, v_3, \dots$ | $13, 15, \dots$ |

Thus $h(\forall) = 0$, $h(0) = 2$, and $h(v_i) = 9 + 2i$. Nothing depends on the
particular table; all that is required is that the language be **recursively
numbered** — that $h$ be a one-to-one map from parameters into the even numbers
for which the relations "$k$ is the value of $h$ at some $m$-place predicate
symbol" and "$k$ is the value of $h$ at some $m$-place function symbol" are both
representable in $\Cn A_E$. For the language of $\fN$ these two
sets are finite (the predicate set is just $\{\langle 6, 2\rangle\}$ for $<$),
so the condition holds trivially.[^recnum]

> **Definition (Gödel number of an expression).** For an expression
> $\varepsilon = s_0 \cdots s_n$, its Gödel number is the sequence number of the
> codes of its symbols,
> $$
> \#\varepsilon \;=\; \langle\, h(s_0),\, \dots,\, h(s_n) \,\rangle
> \;=\; \prod_{i=0}^{n} p_i^{\,h(s_i)+1},
> $$
> where $p_0 = 2, p_1 = 3, p_2 = 5, \dots$ enumerate the primes.

The sequence encoding $\langle a_0, \dots, a_n\rangle = \prod_i p_i^{a_i+1}$ is
the one from the subtheory: its length function $\lh$, its decoding
$(s)_i$ (the exponent of $p_i$, minus one), and its concatenation $\ast$ are all
recursive. The "$+1$" in the exponent keeps a trailing zero from vanishing, so
distinct sequences receive distinct numbers.

For example, the numeral $SS0$ (which names $2$) is the string $S\,S\,0$, so

$$
\#(SS0) \;=\; \langle\, h(S),\, h(S),\, h(0) \,\rangle
\;=\; 2^{4+1}\cdot 3^{4+1}\cdot 5^{2+1}
\;=\; 2^{5}\cdot 3^{5}\cdot 5^{3}
\;=\; 972000.
$$

$$
% caption: The term $SS0$ coded symbol by symbol: each symbol's $h$-value goes
% into the exponent of the next prime, and the product is the term's Gödel number.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw, minimum width=11mm, minimum height=8mm] (s0) at (0,2)   {$S$};
  \node[draw, minimum width=11mm, minimum height=8mm] (s1) at (2.4,2) {$S$};
  \node[draw, minimum width=11mm, minimum height=8mm] (s2) at (4.8,2) {$0$};
  \node[font=\footnotesize, text=black] at (-2.1,2) {symbol};
  \node (h0) at (0,0.8)   {$h = 4$};
  \node (h1) at (2.4,0.8) {$h = 4$};
  \node (h2) at (4.8,0.8) {$h = 2$};
  \node[font=\footnotesize, text=black] at (-2.1,0.8) {code};
  \node[draw=acc, minimum width=11mm, minimum height=8mm] (p0) at (0,-0.6)   {$2^{5}$};
  \node[draw=acc, minimum width=11mm, minimum height=8mm] (p1) at (2.4,-0.6) {$3^{5}$};
  \node[draw=acc, minimum width=11mm, minimum height=8mm] (p2) at (4.8,-0.6) {$5^{3}$};
  \node[font=\footnotesize, text=black] at (-2.1,-0.6) {prime power};
  \foreach \a/\b in {s0/h0, s1/h1, s2/h2} \draw[->, black] (\a) -- (\b);
  \foreach \a/\b in {h0/p0, h1/p1, h2/p2} \draw[->, acc] (\a) -- (\b);
  \node[draw=acc, thick, minimum width=22mm, minimum height=9mm] (prod) at (8.0,-0.6) {$972000$};
  \draw[->, acc, thick] (p2) -- (prod) node[midway, above, font=\footnotesize] {product};
\end{tikzpicture}
$$

> **Worked example (Decoding a Gödel number).** Recover the expression coded
> by $972000$. Factor it,
> $$
> 972000 \;=\; 2^{5}\cdot 3^{5}\cdot 5^{3},
> $$
> a sequence number of length $\lh = 3$ whose entries are the exponents minus
> one,
> $$
> (972000)_0 = 5 - 1 = 4, \qquad (972000)_1 = 5 - 1 = 4, \qquad (972000)_2 = 3 - 1 = 2.
> $$
> Reading the codes back through $h$ — $4 \mapsto S$, $4 \mapsto S$, $2 \mapsto 0$
> — returns the string $SS0$. Encoding and decoding invert each other, so $\#$ is
> one-to-one.

A formula codes the same way once written with primitive symbols. Atomic
formulas are in prefix (Polish) form, so $v_3 = 0$ is the string $=\!v_3\,0$,
and $\exists x\,\alpha$ abbreviates $(\neg\,\forall x\,(\neg\,\alpha))$.

> **Worked example (Gödel number of a formula).** Code the sentence $\exists
> v_3\,\, v_3 = 0$. Unabbreviated, it is the eleven-symbol string
> $$
> (\,\neg\;\forall\; v_3\;(\,\neg\;{=}\; v_3\; 0\,)\,),
> $$
> with $h$-codes
> $$
> \langle 1,\, 5,\, 0,\, 15,\, 1,\, 5,\, 9,\, 15,\, 2,\, 3,\, 3\rangle
> $$
> read off the symbol table ($h(v_3) = 9 + 2\cdot 3 = 15$). The Gödel number is
> the product over the first eleven primes,
> $$
> \#(\exists v_3\,\, v_3 = 0) \;=\; 2^{2}\cdot 3^{6}\cdot 5^{1}\cdot 7^{16}\cdot 11^{2}\cdot 13^{6}\cdot 17^{10}\cdot 19^{16}\cdot 23^{3}\cdot 29^{4}\cdot 31^{4},
> $$
> a number of order $1.3 \times 10^{75}$. The coding is faithful but wildly
> inflationary: a short formula already receives an enormous Gödel number.

To a set $\Gamma$ of expressions we assign the set $\#\Gamma = \{\#\varepsilon :
\varepsilon \in \Gamma\}$ of their Gödel numbers. A sequence of expressions
(for instance a deduction $\langle \alpha_0, \dots, \alpha_n\rangle$) is coded
one level up, by taking the sequence number of the individual Gödel numbers,
$G(\langle \alpha_0, \dots, \alpha_n\rangle) = \langle \#\alpha_0, \dots,
\#\alpha_n\rangle$. The two-level encoding maps an entire proof to a single
integer.

$$
% caption: A deduction is a sequence of formulas; each line is coded by its own
% Gödel number, and those numbers are packed into one sequence number for the proof.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \foreach \i/\y in {0/2.1, 1/0.9, 2/-0.3}{
    \node[draw, minimum width=28mm, minimum height=8mm, anchor=west] (f\i) at (0,\y) {line \i: a formula};
    \node[minimum width=12mm] (g\i) at (4.9,\y) {$n_{\i}$};
    \draw[->, black] (f\i.east) -- (g\i.west);
  }
  \node[font=\footnotesize, text=black, anchor=west] at (3.9,3.0) {encode};
  \node[draw=acc, thick, minimum width=44mm, minimum height=9mm] (code) at (8.4,0.9)
    {$2^{n_0+1}\; 3^{n_1+1}\; 5^{n_2+1}$};
  \node[font=\footnotesize, text=acc, anchor=south] at (8.4,1.45) {code of the proof};
  \foreach \i in {0,1,2} \draw[->, acc] (g\i.east) -- (code.west);
\end{tikzpicture}
$$

## Representable syntactic relations

Under the coding, the operations of syntax become relations and
functions on the natural numbers, and those are representable in
$\Cn A_E$. Throughout, "representable" with no theory named means
representable in $\Cn A_E$. The catalog below is proved item by item;
each proof rewrites an inductive definition of a syntactic class as a recursion
on Gödel numbers, then checks that the recursion falls inside the representable
functions using bounded quantification and the recursion results of the
subtheory.[^catalog]

- **Variables.** The set of Gödel numbers of variables is $\{a : (\exists b < a)\,
  a = 11 + 2b\}$, immediately representable.
- **Terms.** The set of Gödel numbers of terms is representable. A term is either
  a variable or a function symbol applied to shorter terms, and each constituent
  has a smaller Gödel number, so the characteristic function is defined by
  recursion. The only subtlety is bounding the quantifier over the constituent
  sequence, which one does with $i < a^{\,a\,\cdot\,\lh\,a}$.
- **Atomic formulas, wffs.** Both sets of Gödel numbers are representable, by the
  same pattern: transcribe the inductive definition into a recursion on Gödel
  numbers and bound each internal quantifier.
- **Substitution.** There is a representable function $\mathrm{Sb}$ with
  $\mathrm{Sb}(\#\alpha, \#x, \#t) = \#(\alpha^{x}_{t})$ for a term or formula
  $\alpha$, variable $x$, and term $t$. Substitution is defined by six clauses
  (recurse through the connectives and skip a quantifier that binds $x$); each
  clause is a representable relation, and no two clauses can apply at once, so
  the graph is single-valued.
- **Free occurrence.** The relation $\mathrm{Fr}$ with $\langle \#\alpha, \#x
  \rangle \in \mathrm{Fr}$ iff $x$ occurs free in $\alpha$ is representable,
  because $x$ occurs free in $\alpha$ exactly when $\mathrm{Sb}(\#\alpha, \#x,
  \#0) \neq \#\alpha$: substituting $0$ for $x$ changes $\alpha$ iff $x$ was
  actually there to change.
- **Sentences, substitutability, generalizations.** The sets of Gödel numbers of
  sentences (a wff with no free variable), of substitutable-triples
  $\mathrm{Sbl}$ ($t$ is free for $x$ in $\alpha$), and of the relation
  $\mathrm{Gen}$ (one formula is a generalization of another) are all
  representable.
- **Tautologies.** The set of Gödel numbers of tautologies is representable. The
  informal decision procedure is truth tables; recast on Gödel numbers, one
  extracts the list of prime constituents of a formula, encodes a truth
  assignment for them as a number, evaluates the formula under that assignment,
  and quantifies (with a representable bound) over all assignments.
- **Logical axioms.** For each of the axiom schemas — quantifier instantiation
  $\forall x\, \varphi \to \varphi^{x}_{t}$, quantifier distribution, the identity
  axioms, and generalizations of tautologies — the set of Gödel numbers of its
  instances is representable.

> **Worked example (Free occurrence as a substitution test).** The relation
> $\mathrm{Fr}$ reduces to a single value of $\mathrm{Sb}$: substitute the term
> $0$ for $x$ and check whether the expression changes. Take $\alpha$ to be
> $=\!v_1\,0$ (the atomic formula $v_1 = 0$) and $x = v_1$. Replacing $v_1$ by
> $0$ turns the string $=\!v_1\,0$ into $=\!0\,0$ (that is, $0 = 0$), a different
> expression, so
> $$
> \mathrm{Sb}(\#\alpha, \#v_1, \#0) \neq \#\alpha
> $$
> and $\langle\#\alpha, \#v_1\rangle \in \mathrm{Fr}$: $v_1$ occurs free. Now take
> $\alpha' = \forall v_1\, {=}\!v_1\,0$. The quantifier $\forall v_1$ binds the
> very variable being substituted, so no substitution clause fires and
> $\mathrm{Sb}$ returns its input unchanged,
> $$
> \mathrm{Sb}(\#\alpha', \#v_1, \#0) = \#\alpha',
> $$
> which records that $v_1$ is not free in $\alpha'$.

The one remaining ingredient is the notion of a deduction itself.

> **Definition (Coded deduction).** For a set $A$ of formulas whose Gödel-number
> set $\#A$ is representable, a number $d$ codes a deduction from $A$ iff $d$ is a
> sequence number of positive length such that for every $i < \lh\,d$,
> the line $(d)_i$ is a member of $A$, or is a logical axiom, or follows by modus
> ponens from two earlier lines.

```algorithm
caption: $\textsc{IsDeduction}(d, A)$ — the arithmetic test that a number codes a proof from $A$
require $d$ is a sequence number and $\lh\,d > 0$
for each $i < \lh\,d$ do
  if $(d)_i \in \#A$ then continue        // a hypothesis
  if $(d)_i$ codes a logical axiom then continue
  if there exist $j, k < i$ with $(d)_j$ the code of $\big((d)_k \to (d)_i\big)$ then continue  // modus ponens
  return false
return true
```

Every test on a line — membership in $\#A$, being a logical axiom, the
modus-ponens pattern via the concatenation $\ast$ — is a representable relation,
and the quantifiers over $i, j, k$ are all bounded by $\lh\,d$. So for
representable $A$ the whole predicate "$d$ codes a deduction from $A$ ending in
the sentence $a$" is representable.

$$
% caption: Each syntactic predicate becomes an arithmetic relation on Gödel
% numbers, and every one of them is representable in the subtheory.
\begin{tikzpicture}[font=\small, >=stealth,
  b/.style={draw, minimum width=24mm, minimum height=8mm}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[b] (wff)  at (0,2.0)  {Formula($a$)};
  \node[b] (term) at (0,0.8)  {Term($a$)};
  \node[b] (sb)   at (0,-0.4) {Sb($a$; $b$; $c$)};
  \node[b] (ded)  at (0,-1.6) {Ded($d$; $a$)};
  \node[draw=acc, thick, minimum width=40mm, minimum height=13mm, align=center]
    (rep) at (6.6,0.2) {arithmetic relations};
  \foreach \n in {wff, term, sb, ded} \draw[->, acc] (\n.east) -- (rep.west);
\end{tikzpicture}
$$

## The characterization theorem

The catalog culminates in a converse to representability. Every recursive
relation is representable, because a recursive $R$ is (by the subtheory) already
representable by some formula $\rho$ using a finite consistent $A$, and one can
decide $\vec{a} \in R$ by searching for the least coded deduction from $A$ of
$\rho(\vec{S^{a}0})$ or its negation and reading off which one it proved.

> **Theorem (Recursive equals representable).** A relation on the natural numbers is recursive if and only
> if it is representable in the theory $\Cn A_E$.

Since the reverse direction (representable $\Rightarrow$ recursive) is
immediate, the two notions coincide, and from here "recursive" and
"representable" are used interchangeably. The equivalence extends to semantics.

> **Corollary (Recursive relations are arithmetical).** Every recursive relation is definable in $\fN$.

Any syntactic property with a
recursive test is picked out inside the standard model by an arithmetic formula.

## Provability is recursively enumerable

The coded-deduction predicate fixes the complexity of provability. Suppose $A$
is a set of sentences whose Gödel numbers form a recursive set. Then membership
in $\Cn A$ is given by

$$
a \in \#\Cn A
\;\iff\;
\exists d\,\big[\, d \text{ codes a deduction from } A \text{ ending in the sentence } a \,\big].
$$

The bracketed part is recursive. But the search for $d$ is unbounded: there is no
recursive ceiling on how long a proof of $a$ might be. So the most one can
extract is that $\#\Cn A$ is the domain of a recursive relation, a
**recursively enumerable** set, not in general a recursive one.[^re] The two
converge only under an extra hypothesis.

> **Proposition (A complete recursive theory is decidable).** If $\#A$ is
> recursive and $\Cn A$ is a complete theory, then $\#\Cn A$ is recursive.

The argument mirrors the earlier result that a complete axiomatizable theory is
decidable: to test whether the sentence $\sigma$ is a theorem, search for the
least coded deduction of $\sigma$ or of $\neg\,\sigma$; completeness guarantees
one exists, and which one turns up settles membership.

$$
% caption: A recursive set of axioms yields at best a recursively enumerable set
% of theorems; completeness is the extra hypothesis that closes the gap to recursive.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[acc, thick] (0,0) ellipse (3.6 and 2.3);
  \node[font=\footnotesize, text=acc, anchor=south] at (0,2.35) {recursively enumerable};
  \draw[black, thick, fill=acc!8] (0,-0.35) ellipse (2.1 and 1.35);
  \node[font=\footnotesize] at (0,0.55) {recursive};
  \node[align=center, font=\footnotesize, text=black] at (0,-0.2)
    {theorems of a complete\\recursive theory};
  \node[align=center, font=\footnotesize] at (0,-2.0)
    {theorems of a recursive theory};
\end{tikzpicture}
$$

## Church's thesis reconsidered

The recursive-equals-representable theorem also lends weight to Church's thesis, the claim that a function
is recursive precisely when it is effectively computable. Suppose $R$ is decidable
by some effective procedure. That procedure is a finite program whose execution
is a sequence of simple atomic steps. By devices akin to Gödel numbering, code
each machine state as a number; then the characteristic function of $R$ takes the
shape

$$
K_R(\vec{a}) \;=\; U\big[\text{the least } s \text{ such that }
(s)_0 \text{ encodes the input } \vec{a},\ \text{each } (s)_i \text{ follows from } (s)_{i-1}
\text{ by the applicable step, and } (s)_{\mathrm{last}} \text{ halts}\big],
$$

with $U$ a simple function reading the verdict off the final state. The
recursiveness of $R$ reduces to the recursiveness of the step relation and of
$U$, and it is hard to imagine a procedure counted as effective whose single
atomic step is not itself recursive. The syntactic coding is why the informal notion of computation and the formal
notion of recursiveness are believed to coincide, a coincidence developed in
full for [recursive functions](/logic/computability-and-representability/recursive-functions).

$$
% caption: The two directions of coding — a Gödel number encodes an expression,
% and decoding recovers it — let arithmetic and syntax stand in for each other.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw, minimum width=32mm, minimum height=15mm, align=center] (syn) at (0,0)
    {expressions\\formulas, deductions};
  \node[draw=acc, thick, minimum width=32mm, minimum height=15mm, align=center] (num) at (6.5,0)
    {natural numbers};
  \draw[->, acc, thick] (syn.north east) to[bend left=22] node[midway, above, font=\footnotesize] {encode} (num.north west);
  \draw[->, black, thick] (num.south west) to[bend left=22] node[midway, below, font=\footnotesize] {decode} (syn.south east);
\end{tikzpicture}
$$

The encode–decode round trip is exact: distinct expressions get distinct
numbers, and every syntactic operation has an arithmetic shadow. A formula of the
language of $\fN$, speaking on its face only of numbers and their successors and
products, can therefore be read as speaking about formulas — and, evaluated at
[its own Gödel number](/logic/incompleteness/incompleteness-and-undecidability),
about itself.

[^ov]: Enderton, §3.4 — the two stated themes of arithmetization and the promise that the resulting self-reference is exploited in §3.5 for undefinability and undecidability.
[^recnum]: Enderton, §3.4 — Gödel numbers: the symbol table, the function $h$, and the definition of a recursively numbered language requiring the predicate- and function-symbol relations to be representable in $\Cn A_E$.
[^catalog]: Enderton, §3.4 — the catalog (items 1–18) of representable syntactic relations and functions, each reducing an inductive syntactic definition to a bounded recursion on Gödel numbers. The catalog culminates in Theorem 34A (a relation is recursive iff it is representable in $\Cn A_E$) and Corollary 34B (every recursive relation is definable in $\fN$).
[^re]: Enderton, §3.4, items 20–21 — $\#\Cn A$ is the domain of a recursive relation (recursively enumerable) for recursive $A$, and is recursive when the theory is in addition complete.