[FOM] Recursive but not p.r. computable functions
urquhart at cs.toronto.edu
Mon Feb 17 11:07:48 EST 2003
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
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.
More information about the FOM