Existential bounded representation of a primitive recursive function (source code)

= Existential bounded representation of a primitive recursive function

The graph of every primitive recursive $f:\mathbb N^k\to\mathbb N$ has a formula
$$
y=f(\mathbf x)\quad\Longleftrightarrow\quad
\exists\mathbf z\,\delta(y,\mathbf x,\mathbf z)
$$
in the language of ordered rings, where every quantifier inside $\delta$ is bounded. Composition uses existentially quantified intermediate values, while primitive recursion uses a boundedly checked code for the finite sequence of intermediate values.