Arithmetization of Syntax

In the finitely axiomatized subtheory $\text{Cn }{A}_E$, every recursive relation is representable: a relation $R$ is representable when some formula $\rho$ proves the right instance for every tuple, $\vec{n}\in R$ giving $A_E⊢\rho (\overrightarrow{S^{n}0})$ and $\vec{n}\notin R$ giving $A_E⊢\neg \rho (\overrightarrow{S^{n}0})$. Representability now applies to syntax itself, through two constructions.¹

• 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 $\text{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 $\mathfrak{N}$ are the parameters and the logical symbols, each assigned an integer by a fixed function $h$. Parameters get even numbers, logical symbols odd ones.

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 $\text{Cn }{A}_E$. For the language of $\mathfrak{N}$ these two sets are finite (the predicate set is just $\{⟨6,2⟩\}$ for $<$), so the condition holds trivially.²

The sequence encoding $⟨a_0,\dots ,a_n⟩={\prod }_i{p}_i^{a_i+1}$ is the one from the subtheory: its length function $\mathrm{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 $SS0$, so

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 ))$.

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

Representable syntactic relations

Under the coding, the operations of syntax become relations and functions on the natural numbers, and those are representable in $\text{Cn }{A}_E$. Throughout, representable with no theory named means representable in $\text{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.³

• 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 \mathrm{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 }_t^x)$ 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 $⟨\#\alpha ,\#x⟩\in \mathrm{Fr}$ iff $x$ occurs free in $\alpha$ is representable, because $x$ occurs free in $\alpha$ exactly when $\mathrm{Sb}(\#\alpha ,\#x,\#0)\ne \#\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\phi \to {\phi }_t^x$, quantifier distribution, the identity axioms, and generalizations of tautologies — the set of Gödel numbers of its instances is representable.

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

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 $\mathrm{lh}d$. So for representable $A$ the whole predicate $d$ codes a deduction from $A$ ending in the sentence $a$ is representable.

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 (\overrightarrow{S^{a}0})$ or its negation and reading off which one it proved.

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.

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 $\text{Cn }A$ is given by

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 $\#\text{Cn }A$ is the domain of a recursive relation, a recursively enumerable set, not in general a recursive one.⁴ The two converge only under an extra hypothesis.

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.

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

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.

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 $\mathfrak{N}$, 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, about itself.