1
$\begingroup$

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.

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Gabriel Nivasch
    Commented Jan 22, 2017 at 15:09
  • $\begingroup$ @GabrielNivasch Yes, computable is mu-recursive. The proof is the usual tedious encoding argument for computable functions, plus noticing that the functions you need are elementary: T says that m encodes the value of the function together walith a sequence of data verifying the calculation, then V extracts the value from m (say, the first element of the pair). $\endgroup$
    – Henry Towsner
    Commented Jan 22, 2017 at 15:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .