FOM: priority arguments and reverse mathematics

[Stephen G Simpson]

There has been a lot of discussion on FOM about the need for, or lack
of need for, priority arguments.  See FOM July-August-September 1999.

See also the recent posting of Peter Cholak, FOM, Wed, 28 Jun 2000
17:14:46 -0500 (EST), which concerns the question of whether a
priority argument is needed for Robert Soare's unpublished theorem
about settling-down functions of r.e. sets, mentioned by Nabutovsky
and Weinberger in their preprint "The fractal nature of Riem/Diff" (46
pages, to appear).

Now Harvey Friedman, in his FOM posting of Fri, 7 Jul 2000 03:40:15
-0400, brings up the issue of "formal criteria associated with the
necessity of using a priority argument to prove a theorem".

Harvey's first set of criteria concerns provability in fragments of
first order arithmetic.  This subject has an extensive literature and
has gone under the name "reverse recursion theory".  Some of the
researchers are Chong, Mourad, Mytilinaios, Shore, Slaman, Yang.
Reverse recursion theory has been alluded to several times here on
FOM; see my postings of Mon, 21 Jun 1999 21:36:37 -0400 (EDT) and Mon,
16 Aug 1999 14:07:56 -0400 (EDT).

Harvey says:

 > It appears that priority arguments cannot be done in the fairly
 > strong theory ISigma_1 (i.e., Sigma_1 induction).

But this is not correct, because I observed long ago that at least one
of the well known finite-injury priority arguments for solving Post's
problem (i.e., for constructing an intermediate r.e. Turing degree)
goes through in ISigma_1.  I think Mytilinaios credited me for this in
one of the early reverse recursion theory papers:

   Michael E. Mytilinaios.  Finite injury and Sigma_1 induction.
   Journal of Symbolic Logic, 54:38-49, 1989.

So Harvey's suggestion to use non-provability in ISigma_1, as a formal
criterion for needing a priority argument, cannot be right.  A more
appropriate criterion might be: non-provability in PRA (primitive
recursive arithmetic).  Or: non-provability in ISigma_0(exp).

Harvey continues:

 > It would be interesting to use, say, ISigma_0(exp) as a base theory
 > and perhaps derive ISigma_1 from some elementary recursion
 > theoretic statements, or show that this cannot be derived. 

Well, ISigma_1 is easily seen to be equivalent over ISigma_0(exp) to
"every bounded r.e. set is finite", or "every partial recursive
function with bounded domain has bounded range".  These are elementary
recursion-theoretic statements in some sense, but not in the sense
that Harvey had in mind.  Perhaps Harvey will comment further.  How
shall we explicate the notion of "elementary recursion-theoretic
statement"?  I know that Harvey himself did some interesting work long
ago on Wagner-Strong generalized recursion theories ....

Harvey's other set of criteria concerns provability in HA.
This is a new direction which I don't think has been explored.

Harvey mentions several test theorems in recursion theory:

 > a) recursively inseparable r.e. sets;
 > b) all creative sets are recursively isomorphic (Myhill);
 > c) Turing incomparable r.e. sets (Friedberg);
 > d) Friedberg enumeration theorem.

Surely (a) and (b) are doable in ISigma_0(exp).  I think Mytilinaios
showed that (c) is doable in ISigma_1.  I don't know about (d).

-- Steve