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

William Tait williamtait at mac.com
Fri Aug 12 11:34:18 EDT 2005

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
>
>
>
>

`