# Elementary functions in a formalized PA

I'm having trouble understanding some parts of the paper "Provably computable functions and the fast growing hierarchy" by Buchholz and Wainer (1987).

On page 183 they say that their system has axioms corresponding to the "defining equations of each elementary function $f$". They give as an example the axioms of "$+$".

Earlier, on page 182, they define the "elementary functions" as "those which can be explicitly defined from the zero, successor, subtraction, projection and addition funtions using bounded sums and products."

My questions:

1) Why isn't it enough to have only "$+$" and "$\cdot$" in the system? Can't all other functions be expressed in terms of addition and multiplication (using additional variables and quantifiers)? Why do they need their system to have a symbol for the graph of each possible function?

2) The above-mentioned definition of "elementary function" is kind of vague. Are they referring to primitive-recursive functions? mu-recursive functions?

3) I know the defining axioms of the graphs of addition and multiplication. But what are, in general, the defining axioms of the graph of an arbitrary elementary function $f$?

Then, on page 192 they define "positive $\Sigma_1$ formulas" as (roughly) formulas that do not use $\forall$ quantifiers. And on page 193-194 (Theorem 5) the main result is based on such formulas. But I don't understand. In order to express other functions in terms of $+$ and $\cdot$ you do need $\forall$ sometimes. Well, obviously this has to do with my previous questions.

I think your first and last questions more or less answer each other: the elementary functions can be defined using quantifiers, so adding them as symbols makes the quantifier-free formulas more expressive (and, by extension, $\Sigma_1$ and so on). This makes their final result stronger: it includes formulas which use these additional symbols; if we tried to express those functions just using addition and multiplication, we'd need other quantifiers which would put the formula outside the scope of the theorem.
The defining axioms of an elementary function f have to be given inductively by the definition of f. For example, if $f(m,\vec x)=\sum_{i=0}^m g(i,\vec x)$ (where $g$ is some simpler function whose axioms have already been given) then $f$ can be defined by $f(0,\vec x)=g(\vec x)$ and $f(m+1,\vec x)=f(m,\vec x)+g(m+1,\vec x)$.
• Thanks! On page 184 they write that every computable function $f(n_1, \ldots, n_k)$ can be written as $f(n_1, \ldots, n_k) = V(\text{least$m$such that }T(n_1, \ldots, n_k,m) = 0)$, where $V$ and $T$ are elementary. Presumably, "computable" here is the same as mu-recursive. How do you show this? – Gabriel Nivasch Jan 22 '17 at 15:09