[FOM] Recursive but not p.r. computable functions

[Alasdair Urquhart]

As a follow-up to Allen Hazen's posting
of 13 February, I would like to mention that
I proved that the implication-conjunction 
fragment of the relevant logic R, though
decidable, has no primitive recursive decision
procedure (JSL Vol. 64 (1999), 1774-1802).
This problem is a special case of the
decision problem for LR mentioned by Allen 
Hazen.

The last section of my paper showing this result
has a discussion of complexity questions connected
with Dickson's Lemma (the key lemma in proving
the Hilbert basis theorem).  It's possible to
extract a fast-growing non-p.r. computable function
of a natural sort from Dickson's Lemma (see Lemma
11.2 of my paper, discussing a result of McAloon).

These ideas are closely connected with the reverse
mathematics of the Hilbert basis theorem.  
I strongly recommend Steve Simpson's beautiful paper
analysing the logical strength of the Hilbert basis
theorem (JSL 53, 961-974).

Functions such as those arising from Dickson's Lemma,
though mathematically natural, require a fairly
sophisticated reduction to prove they are not p.r.
I don't know of a function satisfying the two demands of 
Peter Smith, namely that (a) it's natural, and 
(b) the fact that it is not p.r. is easy to demonstrate.  

Alasdair Urquhart