Primitive recursion and arithmetic encoding

Start with zero, successor, and coordinate projections, then close under composition and primitive recursion. A recursion specifies the value at zero and obtains the next value from the current index, the previous value, and fixed parameters. On any natural input, only finitely many predecessor stages are required. Structural induction on definitions therefore proves every primitive recursive function total. Bounded searches and bounded quantifiers over primitive recursive predicates can also be implemented within this class.

For example, set T(0)=0 and add n+1 to pass from T(n) to T(n+1). This computes triangular sums without an unbounded stopping test. General computability is broader: unbounded minimization may produce partial functions, and there are total computable functions outside primitive recursion. One must not infer that every terminating program has a primitive recursive running-time bound or that its totality is automatically provable in a particular arithmetic theory.

For a finite sequence of natural numbers, use successive primes starting with two and raise prime i to the corresponding entry plus one. Encode the empty sequence as one. The plus one ensures that a zero entry still leaves a prime factor, so trailing zeros are not lost. Valid nonempty codes use precisely an initial consecutive segment of primes, each with positive exponent, and no other prime factors. A number with a gap, such as ten, is malformed under this convention.

Unique prime factorization recovers every exponent and hence every entry. For a positive candidate N, trial division and all required exponent searches can be bounded by N; standard bounded constructions make validity, length, and entry extraction primitive recursive, with declared default outputs for malformed codes or out-of-range indices. Efficient decoding is a separate issue: prime-exponent codes can grow very large. Other encodings may be more economical without changing the underlying computability results.

Assign effective token numbers to symbols, then encode token sequences, parse trees, proof lines, and finite machine configurations. With standard carefully chosen encodings, syntactic parsing, substitution, and checking a bounded computation trace are primitive recursive. This is a constructive claim about finite local tests, not a claim that every arbitrary numbering has the same convenient complexity. Our elementary sequence code illustrates the first layer; a complete proof coding additionally specifies its grammar and inference rules.

For a theory with a merely c.e. axiom set, do not assume that an unsupported line's axiom status is decidable. Include a finite enumeration-stage certificate demonstrating that the line was emitted as an axiom, together with the ordinary inference checks. Bounded simulation verifies that certificate. The resulting certified proof relation can be primitive recursive in a standard encoding, while existence of some certified proof is expressed by an unbounded existential quantifier. The existential search is exactly where a decidability guarantee can fail.