I'm having trouble understanding some parts of the paper "[Provably computable functions and the fast growing hierarchy](https://epub.ub.uni-muenchen.de/3843/1/3843.pdf)" 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.



Elementary functions in a formalized PA
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.


Sylvain has already linked to a more explicit definition of the elementary functions. They're being short, but not vague: it's the class of functions closed under the operations listed. That makes it smaller than the primitive recursive functions, since it only allows very specific types of iteration.


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)$.


