[FOM] Parson's Thesis?

[Thomas Forster]

On the subject of the naturalness of the hierachy of PR functions, her 
is my two penn'orth

   Quite often when we have a natural recursively defined family we have a
good notion of restricted quantifier.  One thinks immediately of the
cumulative hierarchy - where the good notion of restricted quantifier is
$(\forall x \in y) ... and $(\exists x \in y) ... - and of the natural
numbers - where the good notion of restricted quantifier is $(\forall x <
y) ... and $(\exists x < y) ...

What do i mean by a "good" notion of restricted quantifier?  I mean that 
the restricted quantifiers behave more like propositional connectives than
quantifiers - in that one can prove Prenex-normal-form-like theorems for 
them: one an pull unrestriced quantifiers to the front of formulae past 
restricted quantifiers. (The fact that one seems to need the axiom scheme 
of replacement to do this in set theory has always seemed to me to be an 
argument in favour of adopting replacment that should be ued more wisely)

Now the PR functions are an inductively defined family.  There is a 
notion of restricted quantifier corresponding to this induction.   Does it 
behave well?  Does it give us concise formulations of cute facts?  And 
might its good (or otherwise) behaviour have any baring on the naturalness 
of the hierarchy of PR functions?



On Wed, 10 Aug 2005, Curtis Franks wrote:

> Herb 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?
> > 
> > One piece of evidence for inherent signifance 
>  > [of prim. rec. functions] is the theorem
> > by Parsons you cite (being the provably total functions in
> > I-Sigma_1).  ... 
>  > 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.
> 
> As in the case of prim. rec. functions, the CS route to motivating 
> Kalmar elementary functions is one among many. Professor Enderton points 
> out Ritchie's AMS report where these functions are identified with those 
> computable by Myhill's deterministic linearly bounded automata. Parikh 
> [1971 JSL] proved also that these are the provably total functions of 
> his "Bounded Peano Arithmetic" PB, which today is known as I\Delta_0. 
> Parikh's reconstrual of effectiveness in terms of what can be carried 
> out in bounded arithmetic is of a more logical or philosophical nature 
> than a CS nature. It is worth noting that Parikh directly addresses in 
> that study the current question "... on Church's Thesis. One may still 
> accept recursive = effective but would not accept the classical proof 
> that [all prim. rec. functions are recursive]. Rather the provably 
> recursive functions of PB ... may have more claim to be the class of 
> effective functions" [pg. 506].
> 
> Curtis Franks
> Dept. Logic and Philosophy of Science
> University of California, Irvine
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
> 

-- 

  URL: www.dpmms.cam.ac.uk/~tf   Tel: 01223-337981
  (U Cambridge); 020-7882-3659 (QMW); 3737599 x 86174
  (U Auckland); 021-0580093 (mobile in NZ)