[FOM] Parson's Thesis? [A primitive recursive analogue ...]

[William Tait]

The following is a modified version of a section of a review of the  
Goedel correspondence that I am writing. It argues for a special  
role, not just for the primitive recursive functions, but for  
primitive recursive arithmetic, PRA.

It makes for a long-winded posting, but in the interest of saving me  
some labor, I have not attempted to alter it much. I should also note  
that it repeats in a large measure what I have published on the  
concept of finitism.

PRA, to which Goedel refers in Goedel:*38a as 'finitary number  
theory', is characterized by two moments. One is that the basic  
principle of definition of functions, aside from explicit definition,  
is definition by iteration or primitive recursion. This principle  
follows from the idea of an arbitrary number. It is simply the  
principle that we can uniquely transfer the finite iteration given by  
the arbitrary number n from the successor function starting at 0 to  
any operation Phi on a domain D of objects starting at a, yielding  
Phi^n(a), where a is any object in D.

(Mathematical induction is just primitive recursion applied to a  
domain of proofs. The reduction of the general form of primitive  
recursion, including mathematical induction, to pure iteration is  
discussed in in my book *The Provenance of Pure Reason*,  pp. 57-58,  
and in a forthcoming paper on the DIalectica interpretation.)

The usual axioms of 0 and successor (which are derivable when we take  
\not-phi to abbreviate phi implies  0=1) simply express the fact that  
the arbitrary iteration given by n is `free' (i.e., contains no  
loops), so that it can operate as an iterator of an arbitrary  
operation. It seems reasonable to hold, with Weyl [See \cite{weyl: 
21}, the end of Part II section 1 (``The Basic Ideas'') and the first  
paragraph of section 2a (``Functio Discreta''), and also \cite[p. 33] 
{weyl:49}.}  that definition by iteration simply expresses what we  
mean by number, and itself needs no further foundation. Thus, in the  
case of primitive recursion definition, there is no question of  
proving that the recursion equations define a function, in the sense  
that a unique value can be computed for each argument. These  
equations merely express the fact that we can uniquely construct  
\Phi^n(a) for arbitrary n; and this is contained in the very idea of  
an arbitrary number.

[Not withstanding, there is a predicativity in this conception of  
number, noted by Bernays in letter 76 (16 March 1972) to Goedel and  
by Edward Nelson, arising from the two faces of number: on the one  
hand,  object of the domain N, and on the other, (type-free) iterator  
of operations on any domain, including the domain N.]

The other moment of PRA is that we apply iteration or primitive  
recursion only to operations on domains D of finite objects---call  
them *finitary domains*. (Since proofs of closed numerical equations  
are computations and these are finite objects, proof by mathematical  
induction in PRA is justified on these grounds.) These two moments  
determine PRA, and this explains its special `minimal' role and why  
it deserves the title ``finitary'' (independently of any historical  
uses of this term): it contains the principle that define our concept  
of number, but applies it only to operations on finitary domains.

PRA has interesting subsystems such as the system based on the Kalmar  
elementary functions, but they all involve restrictions on iteration  
to some special class of operations on finitary domains and so, at  
least from our point of view, are arbitrary.

Extensions of PRA are of two kinds: in one, we admit iteration  
applied to operations on domains which contain infinite objects--- 
call them *infinitary domains*. For example, we may apply iteration  
to operations on the domain of functions of  finite types (over the  
domain  N of numbers), obtaining Goeodel's theory T of impredicative  
primitive recursive functions of finite type, or on the domains of  
objects of type phi (in the sense of the Curry-Howard theory of  
propositions-as-types), where phi is a sentence of Heyting arithmetic  
HA, obtaining the proofs of HA. These extensions still follow from  
our basic conception of number as arbitrary free finite iteration,  
but they give up all pretense to finiteness.

The other kind of extension of PRA retains the restriction to  
finitary domains, but admits principles of definition of functions on  
them that cannot be obtained solely by iteration of operations on  
them. The main examples in the literature are functions (such as the  
Ackermann  function) defined by manifold nested recursions. But on  
what grounds do we admit such definitions? In the case of manifold  
nested recursion, we can obtain the function in question by applying  
iteration to operations on either one of Goedel's finite types or on  
the Curry-Howard type phi for suitable arithmetic sentence phi. It is  
also possible to reduce k+1-fold nested recursion (k >=) to ordinary  
(i.e. un-nested) recursion on an ordering of N of order type omega^ 
{(\omega^k)}.  But then, as with the case of the original definition  
by nested recursion, we may ask on what grounds should we accept such  
definitions by transfinite recursion: to obtain them by iteration, we  
again need to iterate operations on infinitary domains.

To the response that we just see intuitively that this or that is a  
valid means of defining functions---that we can see that a value can  
always be computed from the definition, it seems justified to demand  
that the intuition be transformed into a proof. For the basis of the  
intuition must be the principles that define our conception of  
number, 0 and successor and iteration. To see intuitively the  
validity of a particular definition of a numerical function therefore  
must mean to see intuitively that it follows from these principles.  
But what can ``follows from'' mean other than that ``it can be proved  
from''?  When such a proof has been given to show that a certain  
system of equations defines a function, where that function is mot  
pr, we will see that it involves applying iteration to operations on  
infinitary domains. This demand for proof applies not only to  
definition by manifold nested recursions, but to any candidate for an  
intuitionist or finitist function defined by a system of equations.  
If it is not defined by iteration and explicit definition, then we  
should demand a proof that the equations are satisfied. Otherwise,  
the question of what, beyond the primitive recursive functions, is to  
be admitted as a finitist or intuitionistic function will be entirely  
subjective, depending upon one's personal intuitions. (I think that  
this is precisely the position that Goedel attributed to Hilbert.)

Perhaps a good way to summarize is that what can be proved ought to  
be proved. The principle of iteration cannot be proved: It is the  
starting point for proofs in arithmetic.

As a matter of fact, in letter \#69 (7 January 1970) Bernays himself  
manifests the conception of finitism that Goedel attributed to  
Hilbert, when he suggests that 2-fold nested recursion, i.e., nested  
recursion on \omega^2 is finitary in the same sense that ordinary  
recursion on omega is ``i.e., if one views them as a description of  
computation procedures for which it can be seen that the function  
determined by the specific procedure satisfies the recursion  
equations \ldots .''  But the nature of his ``it can be seen''  
becomes clear when he then goes on to make the insight more concrete  
by regarding the computation of the function f(m,y) defined by nested  
recursion on \omega^2 (where the argument (m, y) represents the  
ordinal omega.m + y) as the step-by-step computation of the  
functions  f_m, where f_m(y) = f(m,y) and f_{m+1} is defined by  
primitive recursion from f_m. But the insight that f(x,y) can be  
computed for arbitrary x and y, is really the insight that f_{x+1} 
(y)  can be computed if f_x(z) can be computed for *arbitrary* z.  
Thus the insight involves a construction of a function h by  
iteration: namely, h0 is  a given function and h(x+1) = G(x, hx),  
where G is a function of the *infinitary* type N to [(N to N) to (N  
to N)]. (f(x,y) is  (hx)y.) In this case, what is `seen''  is, in  
outline, a *proof*. But by suppressing the details of the proof, one  
avoids noticing exactly what is involved in it. Another case of this  
is in Goedel's Dialectica paper, in connection with his contention  
that we see immediately that his primitive recursive functions of  
finite type are computable (in his sense).

Regards,

Bill Tait

On Aug 9, 2005, at 2:39 PM, H. Enderton wrote:




> Rex Butler wrote:
>
>
>
>
>> 1.  What can be said about the canonical nature of the primitive
>> recursive functions? ...  Are there other seemingly canonical
>> classes of provably recursive functions?
>>
>>
>>
>>
>
> A good question.  Is there any inherent significance to the class
> of primitive recursive functions, or is it merely a convenient
> class of total recursive functions with the property of having
> recognizably total descriptions?  (The class of all total recursive
> functions lacks this property, so *something* is needed.)
>
> One piece of evidence for inherent signifance is the theorem
> by Parsons you cite (being the provably total functions in
> I-Sigma_1).  Another is the fact that the primitive recursive
> functions are exactly the ones having programs without "go to"
> commands.  (For a precise version, see Chapter 13 in the textbook
> by Davis and Weyuker.  For some reason, this chapter was dropped
> in the second edition.)  Of course, this characterization has
> more a computer science flavor than a foundational one.
>
> But a competing class consists of the (Kalmar) elementary functions.
> A smaller class, it also has claims to inherent significance.
> A 1963 paper by Robert Ritchie shows that these are exactly the
> functions for which the running time is predictable (this concept
> requires an iterative definition).  See the review JSL XXVIII 252.
> Again, this might get a computer science classification.
>
> Perhaps others can point out evidence in favor of assigning
> "canonical nature" to one or the other of these classes -- or
> to other candidates.
>
> --Herb Enderton
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
>
>