42.01.08 · mathematical-logic / first-order-logic-completeness

Representability of Recursive Functions in Arithmetic

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.3-3.5 (representability, the proof predicate, the road to incompleteness); Boolos, Burgess and Jeffrey 2007 *Computability and Logic* 5e (Cambridge) Ch. 16 (the arithmetisation of recursive functions and Q-representability); Hájek and Pudlák 1993 *Metamathematics of First-Order Arithmetic* (Springer) Ch. I (Q, PA, the $\Sigma_n$/$\Pi_n$ arithmetical hierarchy over $\Delta_0$, $\Sigma_1$-completeness, the MRDP route to $\Sigma_1$-definability); Smorynski 1977 'The incompleteness theorems' in the *Handbook of Mathematical Logic* (North-Holland)

Intuition Beginner

A computer can add, multiply, and compare whole numbers. A logical theory of arithmetic is a fixed list of basic rules about those same operations, together with everything you can prove from them. These look like two unrelated worlds: one is a machine grinding through steps, the other is a stack of statements and proofs. This unit shows they are secretly the same world. Whenever a machine settles on a definite answer for definite inputs, a very weak arithmetic can prove the matching numerical fact.

Picture a tiny rulebook for whole numbers. It knows that adding zero changes nothing, that adding one more is the successor, that multiplying builds up from repeated adding, and a few more facts of that kind. It is almost laughably weak: it cannot even prove that addition is commutative in general. Yet for any specific sum or product, with specific numbers written out, it can step through the rules and reach the right total. Ask it about $2 + 3$ and it will prove the answer is $5$ . Ask about $7 \times 6$ and it will prove $42$ .

The deep point is that "compute a function" can be turned into "prove a statement of arithmetic." A function is represented by a formula when the rulebook proves the formula true on exactly the right inputs and outputs, and false on all the wrong ones. The surprising theorem is that every function a machine can compute can be represented this way, in that same weak rulebook. Computation can be mirrored inside arithmetic.

Why does this matter? Once arithmetic can mirror any computation, it can mirror the computation that checks proofs of arithmetic itself. A theory that can talk about its own proofs is a theory that can be made to talk about itself — and that is the doorway to the incompleteness results that come next.

Visual Beginner

The picture is a bridge with two banks. On the left bank, a machine computes; on the right bank, a weak arithmetic proves. Representability is the bridge: every computation on the left has a matching proof on the right.

   LEFT BANK                 BRIDGE                 RIGHT BANK
   (a machine computes)      (representability)     (weak arithmetic Q proves)

   input  2, 3                                       numerals  S S 0 ,  S S S 0
        |                                                 |
        v                                                 v
   add  ->  5             ===================>        Q proves:  "S S 0 + S S S 0 = S S S S S 0"
        |                                                 |
   output 5                                          a finished proof, line by line

   the SAME fact, said two ways:
        machine:   add(2,3) = 5
        arithmetic: Q |- ( 2 + 3 = 5 )   (with numbers written as S S ... 0)

A numeral is how arithmetic writes a number: start from $0$ and apply "successor" ( $S$ , meaning add one) that many times. So $2$ is written $S S 0$ and $3$ is written $S S S 0$ . The machine's "add $2$ and $3$ to get $5$ " becomes the arithmetic's "prove that $S S 0 + S S S 0$ equals $S S S S S 0$ ."

machine does	arithmetic proves	matches?
$add (2, 3) = 5$	$S S 0 + S S S 0 = S S S S S 0$	yes
$mult (2, 3) = 6$	$S S 0 \times S S S 0 = S S S S S S 0$	yes
$add (2, 3) = 9$	$S S 0 + S S S 0 = S S S S S 0$ (so the wrong answer is disproved)	the wrong answer is refuted

The bridge runs both ways for facts: the right answer gets proved, every wrong answer gets refuted.

Worked example Beginner

We watch the weak rulebook prove one specific sum, $2 + 2 = 4$ , using only its rules about adding. Write numbers as numerals: $2$ is $S S 0$ and $4$ is $S S S S 0$ . The rulebook has two facts about addition we will use. First, adding zero changes nothing: $x + 0 = x$ . Second, adding a successor pushes the successor outside: $x + S y = S (x + y)$ .

Step 1. Start from $S S 0 + S S 0$ . The second number is $S S 0$ , which is $S (S 0)$ — a successor. Apply " $x + S y = S (x + y)$ " with $x = S S 0$ and $y = S 0$ . This rewrites $S S 0 + S S 0$ as $S (S S 0 + S 0)$ .

Step 2. Look inside at $S S 0 + S 0$ . Again the second number $S 0$ is a successor, $S (0)$ . Apply the same rule with $y = 0$ . This rewrites $S S 0 + S 0$ as $S (S S 0 + 0)$ . So far the whole expression is $S (S (S S 0 + 0))$ .

Step 3. Now the inside is $S S 0 + 0$ . The second number is $0$ , so apply " $x + 0 = x$ ." This gives $S S 0$ . The whole expression is now $S (S (S S 0))$ .

Step 4. Count the successors: $S (S (S S 0))$ is $S S S S 0$ , which is the numeral for $4$ . The rulebook has proved $S S 0 + S S 0 = S S S S 0$ , that is, $2 + 2 = 4$ .

What this tells us: the rulebook never needed any general theory of addition. It only peeled the second numeral down one successor at a time until it hit zero, then read off the answer. Every specific sum works this way, and the same style of step-by-step peeling handles every specific product too. That is exactly why a machine's definite answer always has a matching proof: the proof simply retraces the computation.

Check your understanding Beginner

Formal definition Intermediate+

Fix the language of arithmetic $L_{A} = {0, S, +, \cdot, <}$ and its standard structure $N = (N; 0, S, +, \cdot, <)$ 42.01.04 pending. For each $n \in N$ the numeral $\underline{n}$ is the closed term $S^{n} 0$ , defined by $\underline{0} = 0$ and $\underline{n + 1} = S \underline{n}$ ; it is the canonical $L_{A}$ -name of $n$ , with $\underline{n}^{N} = n$ .

Robinson arithmetic $Q$ is the $L_{A}$ -theory axiomatised by the universal closures of ^{[Enderton §3.3]}:

Q1: S x \neq = 0, Q2: S x = S y \to x = y, Q3: x \neq = 0 \to \exists y (x = S y), Q4: x + 0 = x, Q5: x + S y = S (x + y), Q6: x \cdot 0 = 0, Q7: x \cdot S y = (x \cdot y) + x, Q8: x < y \leftrightarrow \exists z (S z + x = y) .

Peano arithmetic $P A$ extends $Q$ (with Q3 then derivable) by the first-order induction schema: for every $L_{A}$ -formula $φ (x, \overset{z}{ˉ})$ , $$ \forall \bar z,\Big[\big(\varphi(0,\bar z) \wedge \forall x,(\varphi(x,\bar z) \to \varphi(Sx,\bar z))\big) \to \forall x,\varphi(x,\bar z)\Big]. $$ Both are sound for $N$ : $N ⊨ Q$ and $N ⊨ P A$ , so every theorem of either is true in the standard model.

A relation $R \subseteq N^{k}$ is represented in a theory $T$ by a formula $ρ (x_{1}, \dots, x_{k})$ when for all $\overset{a}{ˉ} \in N^{k}$ , $$ \bar a \in R \implies T \vdash \rho(\underline{a_1}, \dots, \underline{a_k}), \qquad \bar a \notin R \implies T \vdash \neg\rho(\underline{a_1}, \dots, \underline{a_k}). $$ A function $f : N^{k} \to N$ is represented in $T$ by $φ (\overset{x}{ˉ}, y)$ when for all $\overset{a}{ˉ}$ , $$ T \vdash \forall y,\big(\varphi(\underline{a_1}, \dots, \underline{a_k}, y) \leftrightarrow y = \underline{f(\bar a)}\big). $$ Equivalently $T$ proves the correct instance $φ (\underline{\overset{a}{ˉ}}, \underline{f (\overset{a}{ˉ})})$ and proves uniqueness $\forall y (φ (\underline{\overset{a}{ˉ}}, y) \to y = \underline{f (\overset{a}{ˉ})})$ . The notion of recursive function (closure of the zero, successor, and projection functions under composition, primitive recursion, and minimisation) and recursive relation is imported from the theory of computation 42.04.01; the present unit takes that definition as given and builds the formula that captures each closure step inside $Q$ .

A formula is $Δ_{0}$ (bounded) when every quantifier in it is bounded, of the form $\forall x < t$ or $\exists x < t$ for a term $t$ not containing $x$ ; it is $Σ_{1}$ when of the form $\exists \overset{y}{ˉ} θ$ with $θ \in Δ_{0}$ , and $Π_{1}$ when $\forall \overset{y}{ˉ} θ$ with $θ \in Δ_{0}$ . Bounded quantification is decided by finite search, so the truth value of a closed $Δ_{0}$ sentence in $N$ is mechanically computable.

Counterexamples to common slips Intermediate+

"Representable means true in $N$ ." Representability is a provability condition, strictly stronger than truth on numerals. A formula can be true of $R$ in the standard model yet fail to be proved or refuted by $Q$ on some numerals. The theorem is that recursive relations admit a formula $Q$ actually decides at every numeral, not merely one $N$ verifies.
" $Q$ proves induction for specific numbers, so it is almost $P A$ ." $Q$ has no induction schema at all. It proves each numerical instance of a recursive computation by finite term-rewriting, but it cannot prove $\forall x (x + 0 = 0 + x)$ or $\forall x (x < S x)$ . Representability deliberately needs only this induction-free strength.
"Function representability is just the graph being represented as a relation." Representing the graph ${(\overset{a}{ˉ}, b) : f (\overset{a}{ˉ}) = b}$ as a relation gives the two implications on numerals; function representability additionally demands $T$ prove uniqueness, $\forall y (φ (\underline{\overset{a}{ˉ}}, y) \to y = \underline{f (\overset{a}{ˉ})})$ , an internal functionality that relation-representability does not supply.
" $Σ_{1}$ -completeness means $Q$ proves every true sentence." It proves every true $Σ_{1}$ sentence. True $Π_{1}$ sentences — for instance true but unprovable consistency statements — are exactly where completeness fails; the asymmetry between $Σ_{1}$ (existential, witness-checkable) and $Π_{1}$ (universal) is the whole content.

Key theorem with proof Intermediate+

The signature theorem is that the weak, induction-free theory $Q$ already represents every recursive function. Its engine is the arithmetisation of finite sequences: primitive recursion threads a function value through a growing list of earlier values, and to define it inside arithmetic one must quantify over such lists using only numbers. Gödel's $β$ -function does exactly this.

Lemma ( $β$ -function). Define $β (c, d, i) = rem (c, 1 + (i + 1) d)$ , the remainder of $c$ on division by $1 + (i + 1) d$ . For every finite sequence $a_{0}, \dots, a_{n}$ of natural numbers there exist $c, d \in N$ with $β (c, d, i) = a_{i}$ for all $i \leq n$ . Moreover $β$ is representable in $Q$ by a $Δ_{0}$ formula ^{[Enderton §3.3]}.

Proof. Put $d = m!$ where $m = max (n, a_{0}, \dots, a_{n})$ , and let $u_{i} = 1 + (i + 1) d$ for $i \leq n$ . The $u_{i}$ are pairwise coprime: if a prime $p$ divided both $u_{i}$ and $u_{j}$ with $i < j \leq n$ , it would divide their difference $(j - i) d$ ; since $p ∣ u_{i} = 1 + (i + 1) d$ forces $p ∤ d$ , $p$ divides $j - i \leq n \leq m$ , so $p \leq m$ and $p ∣ d = m!$ , contradicting $p ∤ d$ . Each $a_{i} < 1 + (i + 1) d = u_{i}$ because $a_{i} \leq m \leq d \leq (i + 1) d < u_{i}$ . By the Chinese remainder theorem there is $c < \prod_{i} u_{i}$ with $c \equiv a_{i} (mod u_{i})$ for all $i \leq n$ ; as $a_{i} < u_{i}$ , the least nonnegative residue is $a_{i}$ itself, so $β (c, d, i) = a_{i}$ . For representability, $w = rem (c, v)$ is the unique $w$ with $w < v$ and $\exists q \leq c (c = q \cdot v + w)$ , a $Δ_{0}$ condition; $β (c, d, i) = w$ unfolds to the $Δ_{0}$ formula $\exists q \leq c (c = q \cdot (1 + (i + 1) \cdot d) + w \land w < 1 + (i + 1) \cdot d)$ . $□$

Theorem (representability). Every recursive function $f : N^{k} \to N$ is representable in $Q$ , and every recursive relation is representable in $Q$ .

Proof. Induct on the construction of $f$ as a recursive function 42.04.01. The zero function $z (x) = 0$ is represented by $y = 0$ ; the successor $S$ by $y = S x$ ; the projection $π_{j}^{k} (\overset{x}{ˉ}) = x_{j}$ by $y = x_{j}$ . For each, $Q$ proves the value at any numeral and proves uniqueness because the value formula already has the shape $y = (numeral)$ , which is its own functionality statement.

Composition. If $h, g_{1}, \dots, g_{m}$ are represented by $η, γ_{1}, \dots, γ_{m}$ and $f (\overset{x}{ˉ}) = h (g_{1} (\overset{x}{ˉ}), \dots, g_{m} (\overset{x}{ˉ}))$ , set $$ \varphi(\bar x, y) := \exists w_1 \cdots \exists w_m,\big(\gamma_1(\bar x, w_1) \wedge \cdots \wedge \gamma_m(\bar x, w_m) \wedge \eta(w_1, \dots, w_m, y)\big). $$ Given $\overset{a}{ˉ}$ , let $b_{j} = g_{j} (\overset{a}{ˉ})$ and $b = h (\overset{ˉ}{b}) = f (\overset{a}{ˉ})$ . Each $γ_{j}$ forces $w_{j} = \underline{b_{j}}$ provably, and then $η$ forces $y = \underline{b}$ ; $Q$ proves $φ (\underline{\overset{a}{ˉ}}, \underline{b})$ and the uniqueness, so $f$ is represented.

Primitive recursion. Suppose $f (\overset{x}{ˉ}, 0) = g (\overset{x}{ˉ})$ and $f (\overset{x}{ˉ}, S t) = h (\overset{x}{ˉ}, t, f (\overset{x}{ˉ}, t))$ with $g, h$ represented by $γ, η$ . The value $f (\overset{x}{ˉ}, t)$ is determined by the sequence $a_{0} = g (\overset{x}{ˉ}), a_{1}, \dots, a_{t} = f (\overset{x}{ˉ}, t)$ with $a_{i + 1} = h (\overset{x}{ˉ}, i, a_{i})$ . Encode that sequence by a single pair $(c, d)$ through the $β$ -lemma and set $$ \varphi(\bar x, t, y) := \exists c,\exists d,\Big[\beta(c,d,0) = \text{the value of } g \wedge \forall i < t,\big(\beta(c,d,Si) = h(\bar x, i, \beta(c,d,i))\big) \wedge \beta(c,d,t) = y\Big], $$ where each occurrence of $g$ and $h$ is replaced by its representing formula and $β (c, d, i) = u$ by its $Δ_{0}$ formula. For numerals $\overset{a}{ˉ}, n$ put $b = f (\overset{a}{ˉ}, n)$ and choose $(c, d)$ coding $a_{0}, \dots, a_{n}$ by the $β$ -lemma; $Q$ proves each conjunct on the witnessing $(\underline{c}, \underline{d})$ and proves $y = \underline{b}$ , and uniqueness follows because $Q$ proves the bounded conjunction pins $β (c, d, t)$ to $\underline{b}$ regardless of the coding pair. So $f$ is represented.

Minimisation. If $f (\overset{x}{ˉ}) = μ y [g (\overset{x}{ˉ}, y) = 0]$ with $g$ represented by $γ$ and total where used, set $$ \varphi(\bar x, y) := \gamma(\bar x, y, 0) \wedge \forall z < y,\neg,\gamma(\bar x, z, 0). $$ For $\overset{a}{ˉ}$ with $f (\overset{a}{ˉ}) = b$ , $Q$ proves $γ (\underline{\overset{a}{ˉ}}, \underline{b}, 0)$ and, for each $j < b$ , $\neg γ (\underline{\overset{a}{ˉ}}, \underline{j}, 0)$ ; using Q8 and the provable fact $Q ⊢ \forall z (z < \underline{b} \leftrightarrow z = \underline{0} \lor \dots \lor z = \underline{b - 1})$ , $Q$ collapses the bounded $\forall z < \underline{b}$ to that finite conjunction and proves it, giving $φ (\underline{\overset{a}{ˉ}}, \underline{b})$ and the uniqueness from the leastness. A recursive relation is represented by representing its characteristic function and reading membership off the value $\underline{1}$ versus $\underline{0}$ . $□$

Bridge. This theorem is the foundational reason a theory of numbers can host a theory of computation: $Q$ proves, numeral by numeral, exactly what a machine computes, so the recursive functions of 42.04.01 live inside arithmetic as provably-functional formulas. It builds toward the arithmetisation of syntax and the proof predicate $Prf_{T} (p, x)$ , a primitive recursive relation that is therefore representable here, and it appears again in the first incompleteness theorem 42.01.09 pending, where the diagonal lemma feeds a representing formula back into itself. The $β$ -function is the central insight: by trading quantification over finite sequences for quantification over two numbers it makes primitive recursion arithmetically definable, which is exactly the step that lets unbounded computation be mirrored by a bounded coding. Putting these together, the weakness of $Q$ — no induction at all — becomes a feature: incompleteness will follow already for any consistent theory extending this minimal base, so the phenomenon cannot be blamed on the strength of $P A$ .

Exercises Intermediate+

Exercise 6 (medium, symbolic).

Show that $Q$ is not complete by exhibiting a sentence $σ$ with $Q ⊬ σ$ and $Q ⊬ \neg σ$ , using a nonstandard model. Take $σ := \forall x (x + \underline{1} \neq = \underline{0})$ style reasoning, or better, $σ := \forall x (\underline{0} + x = x)$ .

Hint

$Q$ proves $x + 0 = x$ but not $0 + x = x$ in general. Build a model of $Q$ with an extra element where $0 + a \neq = a$ .

Answer

Let $σ := \forall x (\underline{0} + x = x)$ . It is true in $N$ , so $Q ⊬ \neg σ$ (by soundness, since $N ⊨ Q$ ). To see $Q ⊬ σ$ , take the model $N \cup {a, b, \dots}$ with a nonstandard block on which $+$ is defined so that Q4-Q7 hold but $0 + a = b \neq = a$ ; the standard construction $N \cup (Z \times Q)$ with the usual $Q$ -operations satisfies all of Q1-Q8 yet falsifies $\underline{0} + x = x$ at a nonstandard $x$ . So $σ$ is true but unprovable in $Q$ , witnessing incompleteness of $Q$ . Rubric: full credit for a true-in- $N$ sentence and a $Q$ -model refuting it, hence independence.

Exercise 7 (hard, symbolic).

Prove the $Σ_{1}$ -completeness of $Q$ for the existential prefix: if $θ (\overset{x}{ˉ})$ is $Δ_{0}$ and $N ⊨ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ})$ , then $Q ⊢ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ})$ . You may use without proof that $Q$ decides every closed $Δ_{0}$ sentence in accordance with $N$ .

Hint

A true existential has a numeral witness; substitute it and use $Δ_{0}$ -completeness on the resulting closed bounded sentence.

Answer

Suppose $N ⊨ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ})$ . Choose $\overset{a}{ˉ} \in N^{k}$ with $N ⊨ θ (\overset{a}{ˉ})$ . Then $θ (\underline{a_{1}}, \dots, \underline{a_{k}})$ is a closed $Δ_{0}$ sentence true in $N$ , so by the cited $Δ_{0}$ -completeness $Q ⊢ θ (\underline{\overset{a}{ˉ}})$ . By the existential-introduction rule of the predicate calculus, $Q ⊢ \exists \overset{x}{ˉ} θ (\overset{x}{ˉ})$ . The key is that the witness is a concrete tuple of numerals, turning the existential into a decidable closed bounded sentence that $Q$ settles. Rubric: full credit for extracting numeral witnesses, applying $Δ_{0}$ -completeness to the closed instance, and existential introduction.

Exercise 8 (hard, symbolic).

Assuming every recursive function is representable in $Q$ and that the proof-checking relation $Prf_{Q} (p, x)$ (" $p$ codes a $Q$ -proof of the formula with Gödel number $x$ ") is primitive recursive, deduce that $Prf_{Q}$ is representable in $Q$ and that the set of $Q$ -provable sentences is $Σ_{1}$ -definable in $N$ .

Hint

Primitive recursive relations are recursive, hence representable; then existentially quantify the proof code.

Answer

$Prf_{Q}$ is primitive recursive, hence recursive, hence by the representability theorem there is a formula $prf (p, x)$ representing it in $Q$ ; in particular $prf$ may be taken $Δ_{0}$ because proof-checking is a bounded decidable relation on the codes. The provability set is ${x : \exists p Prf_{Q} (p, x)}$ , defined in $N$ by $Pr_{Q} (x) := \exists p prf (p, x)$ , a $Σ_{1}$ formula. Thus "is a $Q$ -theorem" is $Σ_{1}$ , the precise sense in which arithmetic can express its own provability. Rubric: full credit for the recursive-implies-representable step, the $Δ_{0}$ proof predicate, and the $Σ_{1}$ provability formula.

Advanced results Master

The representability theorem supports four developments: the optimality of $Q$ as a base, the exact strength of $Σ_{1}$ -completeness, the equivalence of $Σ_{1}$ -definability with recursive enumerability that runs through the MRDP theorem, and the arithmetisation of provability that opens onto incompleteness.

Theorem 1 (representable $=$ recursive in $Q$ ; optimality of the base). A function is representable in $Q$ iff it is recursive, and likewise for relations ^{[Boolos-Burgess-Jeffrey Ch. 16]}. The forward direction is the Key theorem; the reverse holds because a representing formula gives an effective procedure — search for a $Q$ -proof of $φ (\underline{\overset{a}{ˉ}}, \underline{m})$ over $m$ , which by representability halts at $m = f (\overset{a}{ˉ})$ — so representability in any recursively axiomatised consistent theory implies recursiveness. The base cannot be weakened past $Q$ in the relevant sense: the eight axioms are exactly what the induction over composition, primitive recursion (via $β$ ), and minimisation (via Q8) consume, and any consistent theory in which all recursive functions are representable interprets $Q$ . Representability is thus an absolute, theory-independent boundary coinciding with computability, and it holds already without induction.

Theorem 2 ( $Σ_{1}$ -completeness and its sharp boundary). Every true $Σ_{1}$ sentence is a theorem of $Q$ , and the bound is exact: $Q$ correctly decides every closed $Δ_{0}$ sentence, true existentials are provable by numeral witnesses, but true $Π_{1}$ sentences need not be provable ^{[Hájek-Pudlák Ch. I]}. The proof reduces a $Σ_{1}$ sentence to a closed $Δ_{0}$ instance at a numeral witness and runs the bounded-evaluation lemma, which proves by metatheoretic induction on bounded formulas that $Q$ agrees with $N$ on every closed $Δ_{0}$ sentence. The $Σ_{1} / Π_{1}$ asymmetry is the engine of incompleteness: a consistency statement $Con_{T}$ is $Π_{1}$ , true (when $T$ is consistent) but unprovable, and the first incompleteness sentence is $Π_{1}$ for the same reason — its negation would be a false $Σ_{1}$ sentence, which $Σ_{1}$ -completeness would force $T$ to disprove.

Theorem 3 (the $Σ_{1}$ /recursively-enumerable identification and MRDP). A relation is $Σ_{1}$ -definable in $N$ iff it is recursively enumerable iff its characteristic-of-membership function is the domain of a partial recursive function ^{[Hájek-Pudlák Ch. I]}. The forward implication uses representability to convert a recursive enumeration into an existential over proof-or-computation codes; the converse is Kleene's normal form, $\exists \overset{y}{ˉ}$ over a $Δ_{0}$ Kleene- $T$ predicate. The Matiyasevich-Robinson-Davis-Putnam theorem sharpens this dramatically: every $Σ_{1}$ (equivalently c.e.) relation is Diophantine, defined by $\exists \overset{y}{ˉ} (p (\overset{x}{ˉ}, \overset{y}{ˉ}) = q (\overset{x}{ˉ}, \overset{y}{ˉ}))$ for polynomials with natural-number coefficients, so the existential quantifier prefix can be collapsed onto a single polynomial equation (co-produced as 42.04.07). Representability in $Q$ is the textbook-level half of this tower; MRDP is its number-theoretic apex, and together they make "computably enumerable" and "arithmetically existential" one notion.

Theorem 4 (arithmetisation of syntax and the proof predicate). Fix a Gödel numbering $┌ \cdot ┐$ assigning numbers to terms, formulas, and finite sequences of formulas. The relations " $x$ codes a formula," " $y$ codes a proof in $T$ of the formula coded by $x$ ," and the substitution function $sub (┌ φ ┐, n) = ┌ φ (\underline{n}) ┐$ are all primitive recursive for any recursively axiomatised $T$ ^{[Enderton §3.5]}. By the representability theorem each is representable in $Q$ : there is a $Δ_{0}$ formula $Prf_{T} (p, x)$ and the $Σ_{1}$ provability predicate $Pr_{T} (x) = \exists p Prf_{T} (p, x)$ , and a representing formula for $sub$ . This is the arithmetisation groundwork: the theory's own syntax becomes a recursive structure on numbers, and $Q$ proves the matching numerical facts about it. The diagonal lemma — for every $ψ (x)$ a sentence $G$ with $T ⊢ G \leftrightarrow ψ (┌ G ┐)$ — is then a one-line consequence of the representability of $sub$ , and feeding $ψ = \neg Pr_{T}$ yields the Gödel sentence (developed in the co-produced 42.01.09 pending).

Synthesis. The representability theorem is the foundational reason computation can be mirrored inside arithmetic, and putting these together it controls all four developments: the $β$ -function makes primitive recursion arithmetically definable, which is exactly what lets every recursive function become a provably-functional formula of $Q$ , and this is the central insight that the whole incompleteness phenomenon rests on a theory with no induction. Theorem 1's identification of representable with recursive is dual to the computability-side fact that representability gives an effective halting search, so the boundary is the same object seen from logic and from computation 42.04.01. The $Σ_{1}$ -completeness of Theorem 2 generalises the numeral-by-numeral provability of the Key theorem from individual function values to all existential truths, and its $Π_{1}$ failure is the bridge to the unprovable consistency statement; Theorem 3 widens $Σ_{1}$ -definability into the recursively enumerable sets and, through MRDP 42.04.07, onto Diophantine equations, so that "halts" (the halting problem of 42.04.02) and "satisfies a polynomial equation" and "is provable" are one notion in three languages. Theorem 4 turns the representing apparatus on the theory's own syntax: the proof predicate is primitive recursive, hence representable, hence arithmetic can speak of its own provability — and the diagonal lemma closes the loop, so that the self-reference defeating the halting checker 42.04.02 reappears as a sentence of arithmetic asserting its own unprovability 42.01.09 pending.

Full proof set Master

Proposition 1 ( $β$ -function lemma). For $β (c, d, i) = rem (c, 1 + (i + 1) d)$ and any $a_{0}, \dots, a_{n}$ there are $c, d$ with $β (c, d, i) = a_{i}$ for $i \leq n$ ; and $β$ is $Δ_{0}$ -representable in $Q$ .

Proof. Let $m = max (n, a_{0}, \dots, a_{n})$ , $d = m!$ , $u_{i} = 1 + (i + 1) d$ . Coprimality: a common prime $p$ of $u_{i}, u_{j}$ ( $i < j \leq n$ ) divides $(u_{j} - u_{i}) = (j - i) d$ ; from $u_{i} \equiv 1 (mod p)$ and $u_{i} = 1 + (i + 1) d$ one gets $p ∤ d$ , so $p ∣ (j - i)$ , hence $p \leq j - i \leq n \leq m$ and $p ∣ m! = d$ , a contradiction. Bound: $a_{i} \leq m \leq m! = d < 1 + (i + 1) d = u_{i}$ . CRT yields $c$ with $c \equiv a_{i} (mod u_{i})$ ; since $0 \leq a_{i} < u_{i}$ , $rem (c, u_{i}) = a_{i}$ . The graph $β (c, d, i) = w$ is $\exists q \leq c (c = q \cdot (1 + (i + 1) \cdot d) + w \land w < 1 + (i + 1) \cdot d)$ , all quantifiers bounded by $c$ , hence $Δ_{0}$ ; $Q$ proves it on numerals because the division identity and the strict inequality are closed $Δ_{0}$ facts, decided by $Q$ in accordance with $N$ . $□$

Proposition 2 (initial functions and composition). Zero, successor, and projections are representable in $Q$ , and the representable functions are closed under composition.

Proof. $z$ by $y = 0$ , $S$ by $y = S x$ , $π_{j}^{k}$ by $y = x_{j}$ ; in each case $Q$ proves the unique value at any numeral tuple directly from the term identities and the reflexivity of equality. For composition with $f (\overset{x}{ˉ}) = h (g_{1} (\overset{x}{ˉ}), \dots, g_{m} (\overset{x}{ˉ}))$ and representing formulas $η, γ_{j}$ , set $φ (\overset{x}{ˉ}, y) = \exists \overset{w}{ˉ} (⋀_{j} γ_{j} (\overset{x}{ˉ}, w_{j}) \land η (\overset{w}{ˉ}, y))$ . At $\overset{a}{ˉ}$ , write $b_{j} = g_{j} (\overset{a}{ˉ})$ , $b = f (\overset{a}{ˉ})$ : $Q ⊢ γ_{j} (\underline{\overset{a}{ˉ}}, \underline{b_{j}})$ and the uniqueness force $w_{j} = \underline{b_{j}}$ , and $Q ⊢ η (\underline{\overset{ˉ}{b}}, \underline{b})$ with its uniqueness force $y = \underline{b}$ . Hence $Q ⊢ φ (\underline{\overset{a}{ˉ}}, \underline{b})$ and $Q ⊢ \forall y (φ (\underline{\overset{a}{ˉ}}, y) \to y = \underline{b})$ . $□$

Proposition 3 (primitive recursion). If $g, h$ are representable then so is $f$ defined by $f (\overset{x}{ˉ}, 0) = g (\overset{x}{ˉ})$ , $f (\overset{x}{ˉ}, S t) = h (\overset{x}{ˉ}, t, f (\overset{x}{ˉ}, t))$ .

Proof. Let $γ, η$ represent $g, h$ . Using Proposition 1, set $$ \varphi(\bar x, t, y) := \exists c,\exists d,\Big[\exists v,(\beta(c,d,0) = v \wedge \gamma(\bar x, v)) \wedge \forall i < t,\exists u \exists u',(\beta(c,d,i) = u \wedge \beta(c,d,Si) = u' \wedge \eta(\bar x, i, u, u')) \wedge \beta(c,d,t) = y\Big]. $$ At numerals $\overset{a}{ˉ}, n$ , set $a_{0} = g (\overset{a}{ˉ})$ , $a_{i + 1} = h (\overset{a}{ˉ}, i, a_{i})$ , $b = a_{n} = f (\overset{a}{ˉ}, n)$ , and pick $(c, d)$ coding $a_{0}, \dots, a_{n}$ . $Q$ proves the base conjunct via $γ$ , each bounded- $i$ conjunct via $η$ and the $β$ -graph (the bounded $\forall i < \underline{n}$ collapsing to the explicit finite conjunction since $Q ⊢ \forall i (i < \underline{n} \leftrightarrow ⋁_{j < n} i = \underline{j})$ ), and the final $β (c, d, \underline{n}) = \underline{b}$ . So $Q ⊢ φ (\underline{\overset{a}{ˉ}}, \underline{n}, \underline{b})$ . Uniqueness: any $y^{'}$ with $φ (\underline{\overset{a}{ˉ}}, \underline{n}, y^{'})$ forces, through the same bounded conjunction and the provable functionality of $γ, η$ and $β$ , that $β (c^{'}, d^{'}, \underline{n}) = \underline{b}$ , hence $y^{'} = \underline{b}$ ; thus $Q ⊢ \forall y (φ (\underline{\overset{a}{ˉ}}, \underline{n}, y) \to y = \underline{b})$ . $□$

Proposition 4 (minimisation). If $g$ is representable and $f (\overset{x}{ˉ}) = μ y [g (\overset{x}{ˉ}, y) = 0]$ is total, then $f$ is representable in $Q$ .

Proof. Let $γ$ represent $g$ and set $φ (\overset{x}{ˉ}, y) := γ (\overset{x}{ˉ}, y, 0) \land \forall z < y \neg γ (\overset{x}{ˉ}, z, 0)$ . At $\overset{a}{ˉ}$ with $f (\overset{a}{ˉ}) = b$ : $g (\overset{a}{ˉ}, b) = 0$ gives $Q ⊢ γ (\underline{\overset{a}{ˉ}}, \underline{b}, 0)$ ; for each $j < b$ , $g (\overset{a}{ˉ}, j) \neq = 0$ gives $Q ⊢ \neg γ (\underline{\overset{a}{ˉ}}, \underline{j}, 0)$ by representability of $g$ as a function (its value at $\underline{j}$ is a numeral $\neq = \underline{0}$ , and $Q$ proves distinct numerals unequal). The bounded $\forall z < \underline{b}$ collapses to $⋀_{j < b} \neg γ (\underline{\overset{a}{ˉ}}, \underline{j}, 0)$ via $Q ⊢ \forall z (z < \underline{b} \leftrightarrow ⋁_{j < b} z = \underline{j})$ (provable from Q8 and the numeral case analysis), which $Q$ proves. Hence $Q ⊢ φ (\underline{\overset{a}{ˉ}}, \underline{b})$ , and uniqueness follows because any $y^{'}$ satisfying $φ$ has $γ (\underline{\overset{a}{ˉ}}, y^{'}, 0)$ and is below none of the witnesses, forcing $y^{'} = \underline{b}$ by the leastness and numeral trichotomy. $□$

Proposition 5 ( $Σ_{1}$ -completeness of $Q$ ). Every true $Σ_{1}$ sentence is provable in $Q$ .

Proof. First, the bounded-evaluation lemma: for every closed $Δ_{0}$ sentence $θ$ , $N ⊨ θ \Rightarrow Q ⊢ θ$ and $N \neq ⊨ θ \Rightarrow Q ⊢ \neg θ$ , by metatheoretic induction on $θ$ . Atomic closed equalities and inequalities between closed terms evaluate to numerals, and $Q$ proves $\underline{m} = \underline{n}$ when $m = n$ and $\underline{m} \neq = \underline{n}$ when $m \neq = n$ (from Q1, Q2), and decides $\underline{m} < \underline{n}$ from Q8; Boolean connectives pass through; a bounded quantifier $\exists z < \underline{k} ψ$ is equivalent over $Q$ to the finite disjunction $⋁_{j < k} ψ (\underline{j})$ (using $Q ⊢ \forall z (z < \underline{k} \leftrightarrow ⋁_{j < k} z = \underline{j})$ ), and $\forall z < \underline{k} ψ$ to the finite conjunction, reducing to the inductive hypothesis on each closed instance. Now a $Σ_{1}$ sentence $\exists \overset{y}{ˉ} θ (\overset{y}{ˉ})$ true in $N$ has a numeral witness $\overset{a}{ˉ}$ with $N ⊨ θ (\underline{\overset{a}{ˉ}})$ ; by the lemma $Q ⊢ θ (\underline{\overset{a}{ˉ}})$ , and existential introduction gives $Q ⊢ \exists \overset{y}{ˉ} θ (\overset{y}{ˉ})$ . $□$

Proposition 6 (the proof predicate is representable; provability is $Σ_{1}$ ). For recursively axiomatised $T$ the relation $Prf_{T} (p, x)$ is primitive recursive, hence representable in $Q$ by a $Δ_{0}$ formula, and $Pr_{T} (x) = \exists p Prf_{T} (p, x)$ is $Σ_{1}$ .

Proof. Gödel numbering renders " $x$ codes an $L_{A}$ -formula" and " $p$ codes a finite sequence of formulas each of which is a logical axiom, an axiom of $T$ , or follows from earlier ones by a rule, the last being the formula coded by $x$ " as primitive recursive predicates: each clause is a bounded check over the components of $p$ , decidable by primitive recursion on the sequence-coding (itself built from the $β$ -function of Proposition 1). Being primitive recursive, $Prf_{T}$ is recursive, so by Propositions 2-4 it is representable in $Q$ ; as the checking is bounded by $p$ the representing formula is $Δ_{0}$ . Then $Pr_{T} (x) = \exists p Prf_{T} (p, x)$ is $Σ_{1}$ by definition. By Proposition 5, every true instance $Pr_{T} (┌ σ ┐)$ — that is, every actual theorem $σ$ — is $Σ_{1}$ -provably so in $Q$ , the formal counterpart of "if $T ⊢ σ$ then $Q ⊢ Pr_{T} (┌ σ ┐)$ ." $□$

Connections Master

Structures and Tarski semantics 42.01.04 pending supply the standard model $N$ and the satisfaction relation against which truth of $Δ_{0}$ and $Σ_{1}$ sentences is measured, and the numeral $\underline{n}$ is the closed term whose value $\underline{n}^{N} = n$ makes "true on numerals" precise. That unit owns the semantics of the arithmetic language; this unit adds the provability layer over it, the gap between $N ⊨ σ$ and $Q ⊢ σ$ that $Σ_{1}$ -completeness measures and that incompleteness exploits.
Models of computation and the recursive functions 42.04.01 define the recursive functions whose representability is the theorem of this unit; the inductive closure conditions — composition, primitive recursion, minimisation — are exactly the cases of the representability induction, and the equivalence "representable in $Q$ iff recursive" identifies that unit's notion of computability with this unit's notion of provable-numeral-functionality. The $β$ -function is the device that imports primitive recursion, defined there, into the formula language here.
The halting problem and the recursion theorem 42.04.02 are the computational shadow of this arithmetisation: the self-application that defeats the halting checker is the same diagonal that, once the proof predicate is representable here, produces the Gödel sentence; and the undecidability of arithmetic — $K \leq_{m} {┌ σ ┐ : Q ⊢ σ}$ — is immediate once provability is $Σ_{1}$ and representability lets $Q$ track computation. Church's theorem on the Entscheidungsproblem routes through exactly the representability established here.
Gödel's incompleteness theorems 42.01.09 pending, co-produced with this unit, are its destination: the diagonal lemma is a one-line consequence of the representability of the substitution function $sub$ proved here, and the first incompleteness sentence $G \leftrightarrow \neg Pr_{T} (┌ G ┐)$ is built from the $Σ_{1}$ provability predicate of Proposition 6. The second incompleteness theorem additionally needs the Hilbert-Bernays-Löb derivability conditions, whose first condition is precisely the $Σ_{1}$ -completeness of Proposition 5 formalised inside $T$ .

Historical & philosophical context Master

The representability of the recursive functions in a weak arithmetic is the technical core of Kurt Gödel's 1931 paper Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, where the $β$ -function (Gödel's " $β$ ") was introduced precisely to express primitive recursion inside arithmetic without a primitive sequence type, using the Chinese remainder theorem to code finite sequences by pairs of numbers ^{[Enderton §3.3]}. Gödel proved that the primitive recursive functions are definable in the arithmetic of Principia; the extension to all recursive functions and the isolation of the minimal theory followed from the convergence of the competing analyses of computability — Gödel and Herbrand's general recursive functions, Church's $λ$ -definability, and Turing's machines — into the single class fixed by the Church-Turing thesis.

Raphael Robinson isolated the finitely axiomatised theory $Q$ in 1950 (in "An essentially undecidable axiom system"), showing that this induction-free fragment already suffices for representability and hence for essential undecidability, so that the incompleteness and undecidability phenomena attach to a theory far weaker than full Peano arithmetic ^{[Boolos-Burgess-Jeffrey Ch. 16]}. Alfred Tarski, Andrzej Mostowski, and Robinson systematised the method of essentially undecidable theories in Undecidable Theories (1953), making $Q$ -representability the standard route to undecidability results across mathematics. The sharpening of $Σ_{1}$ -definability to Diophantine definability — that every recursively enumerable set is the solution set of a polynomial equation — was completed by Yuri Matiyasevich in 1970, building on Julia Robinson, Martin Davis, and Hilary Putnam, resolving Hilbert's tenth problem in the negative ^{[Hájek-Pudlák Ch. I]}.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@article{godel1931,
  author  = {G\"{o}del, Kurt},
  title   = {\"{U}ber formal unentscheidbare S\"{a}tze der {Principia Mathematica} und verwandter Systeme {I}},
  journal = {Monatshefte f\"{u}r Mathematik und Physik},
  volume  = {38},
  year    = {1931},
  pages   = {173--198}
}

@article{robinson1950essentially,
  author  = {Robinson, Raphael M.},
  title   = {An essentially undecidable axiom system},
  journal = {Proceedings of the International Congress of Mathematicians (Cambridge, Mass.)},
  volume  = {1},
  year    = {1950},
  pages   = {729--730}
}

@book{tarskimostowskirobinson1953,
  author    = {Tarski, Alfred and Mostowski, Andrzej and Robinson, Raphael M.},
  title     = {Undecidable Theories},
  publisher = {North-Holland},
  year      = {1953}
}

@book{boolosburgessjeffrey2007,
  author    = {Boolos, George S. and Burgess, John P. and Jeffrey, Richard C.},
  title     = {Computability and Logic},
  edition   = {5},
  publisher = {Cambridge University Press},
  year      = {2007}
}

@book{hajekpudlak1993,
  author    = {H\'{a}jek, Petr and Pudl\'{a}k, Pavel},
  title     = {Metamathematics of First-Order Arithmetic},
  series    = {Perspectives in Mathematical Logic},
  publisher = {Springer},
  year      = {1993}
}

@article{matiyasevich1970,
  author  = {Matiyasevich, Yuri V.},
  title   = {Enumerable sets are {Diophantine}},
  journal = {Soviet Mathematics Doklady},
  volume  = {11},
  year    = {1970},
  pages   = {354--358}
}

@incollection{smorynski1977incompleteness,
  author    = {Smory\'{n}ski, Craig},
  title     = {The incompleteness theorems},
  booktitle = {Handbook of Mathematical Logic},
  editor    = {Barwise, Jon},
  publisher = {North-Holland},
  year      = {1977},
  pages     = {821--865}
}

Prerequisites

42.01.04

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §3.3 read informally — the idea that a finite list of basic facts about adding, multiplying, and comparing whole numbers (the axioms of a weak arithmetic) is already strong enough that, whenever a machine computes a definite answer for definite inputs, the arithmetic can prove the matching numerical statement; numerals as the formal names $0, S0, SS0, \dots$ of the whole numbers and the meaning of 'the arithmetic proves $f(2,3)=5$'; checking by hand that a weak arithmetic proves small sums and products
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.3 (Robinson arithmetic Q and Peano arithmetic PA as theories of $(\mathbb N; 0, S, +, \cdot, <)$; the numeral $\underline n = S^n 0$; a relation $R$ represented in a theory $T$ by a formula $\varphi$ when $T \vdash \varphi(\underline{a})$ for $\bar a \in R$ and $T \vdash \neg\varphi(\underline a)$ otherwise; a function represented when $T$ proves the graph formula functional on numerals; the theorem that every recursive function is representable in Q, by induction over the closure conditions defining the recursive functions; Gödel's $\beta$-function and the arithmetisation of finite sequences via the Chinese remainder theorem; $\Delta_0$ and $\Sigma_1$ formulas and the $\Sigma_1$-completeness of Q)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.3-3.5 (representability, the proof predicate, the road to incompleteness); Boolos, Burgess and Jeffrey 2007 *Computability and Logic* 5e (Cambridge) Ch. 16 (the arithmetisation of recursive functions and Q-representability); Hájek and Pudlák 1993 *Metamathematics of First-Order Arithmetic* (Springer) Ch. I (Q, PA, the $\Sigma_n$/$\Pi_n$ arithmetical hierarchy over $\Delta_0$, $\Sigma_1$-completeness, the MRDP route to $\Sigma_1$-definability); Smorynski 1977 'The incompleteness theorems' in the *Handbook of Mathematical Logic* (North-Holland)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), §3.3-3.5. Develops the theory of the standard model of arithmetic and the bridge from computability to formal provability. The language of arithmetic is $\{0, S, +, \cdot, <\}$ (Enderton uses $0, S, +, \cdot, E, <$ with exponentiation; the core development needs only $0,S,+,\cdot,<$). The numeral $\underline n$ naming the natural number $n$ is $S S \cdots S 0$ with $n$ occurrences of $S$, defined by $\underline 0 = 0$, $\underline{n+1} = S\underline n$. Robinson arithmetic $Q$ is the finitely axiomatised theory with axioms: $\forall x\,(Sx \ne 0)$; $\forall x\forall y\,(Sx = Sy \to x = y)$; $\forall x\,(x \ne 0 \to \exists y\,(x = Sy))$; $\forall x\,(x + 0 = x)$; $\forall x\forall y\,(x + Sy = S(x+y))$; $\forall x\,(x \cdot 0 = 0)$; $\forall x\forall y\,(x \cdot Sy = x\cdot y + x)$; and the order axiom $\forall x\forall y\,(x < y \leftrightarrow \exists z\,(Sz + x = y))$ (or $x \le y \leftrightarrow \exists z\,(z+x=y)$ depending on the presentation). Peano arithmetic $PA$ adds the first-order induction schema: for each formula $\varphi(x)$, $[\varphi(0) \wedge \forall x\,(\varphi(x) \to \varphi(Sx))] \to \forall x\,\varphi(x)$. A relation $R \subseteq \mathbb N^k$ is representable in a theory $T$ iff there is a formula $\rho(x_1,\dots,x_k)$ such that for all $\bar a$: if $\bar a \in R$ then $T \vdash \rho(\underline{a_1},\dots,\underline{a_k})$, and if $\bar a \notin R$ then $T \vdash \neg\rho(\underline{a_1},\dots,\underline{a_k})$. A function $f : \mathbb N^k \to \mathbb N$ is representable in $T$ iff there is a formula $\varphi(x_1,\dots,x_k,y)$ with, for all $\bar a$, $T \vdash \forall y\,(\varphi(\underline{a_1},\dots,\underline{a_k},y) \leftrightarrow y = \underline{f(\bar a)})$ — equivalently $T$ proves $\varphi(\underline{\bar a}, \underline{f(\bar a)})$ and proves the uniqueness $\forall y\,(\varphi(\underline{\bar a}, y) \to y = \underline{f(\bar a)})$. The representability theorem: a function (relation) is representable in $Q$ iff it is recursive (recursive), the forward direction by induction on the definition of the recursive functions — the initial functions zero, successor, projections are directly represented, composition and primitive recursion are handled by combining graph formulas, and the recursion case requires coding the finite sequence of intermediate values, achieved by Gödel's $\beta$-function. Gödel's $\beta$-function $\beta(c, d, i) = \mathrm{rem}(c, 1 + (i+1)d)$ (the remainder of $c$ on division by $1 + (i+1)d$) has the property (the $\beta$-function lemma) that for every finite sequence $a_0, \dots, a_n$ there exist $c, d$ with $\beta(c,d,i) = a_i$ for all $i \le n$, proved using the Chinese remainder theorem on the pairwise-coprime moduli $1 + (i+1)d$ for $d = (\max(n, a_0, \dots, a_n))!$; $\beta$ is itself given by a $\Delta_0$ formula, so quantification over finite sequences is replaced by quantification over the two numbers $c, d$, making primitive recursion arithmetically definable. $\Delta_0$ (bounded) formulas have all quantifiers bounded ($\forall x < t$, $\exists x < t$); $\Sigma_1$ formulas are $\exists \bar y\,\theta$ with $\theta \in \Delta_0$. The $\Sigma_1$-completeness of $Q$: every true $\Sigma_1$ sentence is provable in $Q$ (and a fortiori in $PA$); equivalently $Q$ correctly decides every $\Delta_0$ sentence. The proof predicate $\mathrm{Prf}_T(p, x)$ ('$p$ codes a $T$-proof of the formula coded by $x$') and the provability predicate $\mathrm{Pr}_T(x) = \exists p\,\mathrm{Prf}_T(p,x)$ are arithmetised by Gödel-numbering formulas and proofs; $\mathrm{Prf}_T$ is a primitive recursive relation, hence representable in $Q$, and this representability is what lets arithmetic talk about its own provability — the groundwork for the incompleteness theorems (Enderton §3.5).
Boolos, G., Burgess, J. and Jeffrey, R. — Computability and Logic · 5th edition, Cambridge University Press (2007), Chapters 15-16. Ch. 15 develops the arithmetisation of syntax and the recursive functions; Ch. 16 ('Representability of Recursive Functions') proves that the recursive functions and relations are exactly those representable (called 'arithmetically definable in $Q$' / 'capturable') in Robinson arithmetic $Q$. The treatment fixes $Q$ as the minimal theory adequate for representability, defines the numerals and the representability of relations (a formula that $Q$ proves true on numerals in the relation and proves false off it) and of functions (the graph proved functional), and carries out the induction over the inductive definition of the recursive functions: the base functions, substitution (composition), primitive recursion via the $\beta$-function trick for coding the course-of-values sequence, and minimisation (the least-number operator) handled by the order axiom of $Q$. The book emphasises that $Q$ is $\Sigma_1$-complete and that representability needs only this weak base, so the incompleteness phenomenon does not depend on the strength of $PA$. The chapter is the standard self-contained source for the equivalence 'recursive = representable in $Q$' used to derive Gödel's first and second incompleteness theorems and the undecidability of arithmetic and of first-order logic.
Hájek, P. and Pudlák, P. — Metamathematics of First-Order Arithmetic · Perspectives in Mathematical Logic, Springer (1993), Chapter I and the introductory parts of Chapter V. Chapter I sets up the language of arithmetic, Robinson's $Q$, the fragments $I\Delta_0$, $I\Sigma_n$, and full $PA$, and the arithmetical hierarchy $\Sigma_n / \Pi_n$ stratifying formulas by quantifier alternation over the bounded ($\Delta_0$) formulas. It proves the $\Sigma_1$-completeness of $Q$: every true $\Sigma_1$ sentence is a theorem of $Q$, with the bounded-formula evaluation lemma at its core (Q decides every closed $\Delta_0$ sentence in accordance with truth in $\mathbb N$). The text treats the coding of finite sequences (the $\beta$-function and the related pairing and sequence-coding apparatus), the formalisation of recursive definitions inside $I\Sigma_1$, and the representability/definability of the recursive functions, situating $Q$-representability inside the broader programme of bounded arithmetic and the relationship to the MRDP theorem (every recursively enumerable relation is $\Sigma_1$, indeed Diophantine). It is the reference for the proof-theoretic strength needed for various closure properties and for the exact role $\Sigma_1$-completeness plays in the derivability conditions for the second incompleteness theorem.

Estimated time

beginner: 18m
intermediate: 52m
master: 88m