PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Ackermann function is total computable but not primitive recursive

Statement

Let $A : N^{2} \to N$ be the Ackermann-Peter function defined by $A (0, n) = n + 1,$ $A (m + 1, 0) = A (m, 1),$ $A (m + 1, n + 1) = A (m, A (m + 1, n)) .$ Then $A$ is a total computable function, but $A$ is not primitive recursive.

Facts & Assumptions

Given: The function $A$ defined in the statement.

[L1]

Primitive recursive functions are the total functions obtained from the initial functions by finitely many compositions and primitive recursions, by Primitive recursive functions.

[L2]

A machine computes a partial function when it halts with the required output on every input in the domain and diverges off the domain, by Partial functions computed by a machine under fixed encodings.

[F1]

For each fixed $m$ , the unary function $A_{m} (n) : = A (m, n)$ is strictly increasing in $n$ , and $A_{m + 1}$ is obtained by iterating $A_{m}$ a growing number of times. Consequently, for fixed $c$ and $r$ , some sufficiently high row $A_{d}$ with $d > c$ eventually dominates the shifted row $n \mapsto A_{c} (n + r)$ , and passing to a sufficiently higher row absorbs any fixed finite composition or an $n$ -fold iteration of lower rows.

Proof

technique · direct

1.1

A deterministic machine can evaluate $A (m, n)$ by keeping a finite stack of pending calls. Start with the one stack entry $(m, n)$ . If the top entry is $(0, r)$ , replace it by the value $r + 1$ ; if it is $(p + 1, 0)$ , replace it by $(p, 1)$ ; and if it is $(p + 1, r + 1)$ , replace it by the two pending calls $(p + 1, r)$ and then $(p, □)$ , where the second frame waits for the value returned by the first and then substitutes it into $A (p, \cdot)$ . Every individual rewrite is effective on a coded stack, so by [L2] this gives a machine procedure for evaluating $A$ .

L2F1givenconstruct

1.2

For each primitive recursive $k$ -ary function $f$ , structural induction on its construction from [L1] gives constants $c, r$ such that $f (x_{1}, \dots, x_{k}) \leq A_{c} (\max_{i} x_{i} + r)$ for all inputs. The initial functions satisfy such a bound. For composition, apply the induction bounds to all inner functions, take their maximum, and then apply the bound for the outer function; monotonicity and the absorption property in [F1] replace the resulting finite composition by one higher fixed row. For primitive recursion, the recursion variable bounds the number of successive applications of the step function; [F1] again absorbs those boundedly many lower-row iterations into a higher fixed row.

L1F1giveninduction

2.1

The defining recursion decreases the left argument whenever the right argument is reset, and otherwise decreases the right argument before the left argument is used again. Induction on $m$ and then on $n$ therefore shows that every call chain eventually reaches the base clause $A (0, r) = r + 1$ . Hence the machine from step 1.1 halts on every input $(m, n)$ , so $A$ is total computable.

F1step 1.1

2.2

If $A$ itself were primitive recursive, step 1.2 would give fixed $c, r$ with $A (m, n) \leq A_{c} (\max {m, n} + r)$ for all $m, n$ . Setting $m = n$ and then taking $n > c$ sufficiently large gives $A (n, n) > A_{c} (n + r)$ by [F1], contradicting that bound. Therefore $A$ is not primitive recursive.

F1step 1.2

3.1

Steps 2.1 and 2.2 prove that Ackermann's function is total computable but not primitive recursive.

step 2.1step 2.2∎

Depends on

Used by

The Ackermann function refutes the claim that all total computable functions are primitive recursive Counterexample
FALSE: every total computable function is primitive recursive False statement

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jeremy Avigad and Richard Zach, Recursive Functions (standard reference, not scraped)
Klaus Sutner, Primitive Recursion (standard reference, not scraped)