FOM: constructivity; priority arguments; recursive counterexamples

[Stephen G Simpson]

This is a follow-up to Harvey's postings of Thu, 13 Jul 2000 10:35:35
-0400 and Fri, 7 Jul 2000 03:40:15 -0400.

1. NON-CONSTRUCTIVITY OF PRIORITY ARGUMENTS

A key remark in Harvey's posting is that, although the elements of
recursive function theory (Enumeration Theorem, S-m-n Theorem, etc)
are constructive, priority arguments are highly non-constructive.

This remark seems absolutely correct.  But, as Harvey notes, it would
be nice to have precise results to back it up.  Can we show that some
standard results that are standardly proved with priority arguments
are not provable constructively?  For example, can we show that the
Friedberg/Muchnik Theorem is not provable in HA?

Harvey appears to be saying that the Friedberg Enumeration Theorem is
inherently non-constructive:

 > It is straightforward to show that any reasonable formulation of
 > the existence of a one-one partial enumeration of the partial
 > recursive functions cannot be proved constructively; e.g., in HA =
 > Heyting Arithmetic.

Harvey, could you please indicate how to show this?

Harvey goes on to ask:

 > To what extent can technically sophisticated techniques from
 > recursion theory be used to provide constructive information?

By "technically sophisticated techniques from recursion theory", I
assume Harvey means priority arguments.  

My gut feeling has always been that priority arguments are
constructively useless.  They have no constructive content.  They
start out with a constructive focus, but then they veer off into
massive and overwhelming non-constructivity.  For example, Friedberg
gives an explicit enumeration of the r.e. sets in question, but his
proof that they have the desired property (Turing incomparability) is
inductive, with a non-constructive division into cases at every step
of the way.

2. RECURSIVE COUNTEREXAMPLES

Harvey goes on to discuss the methodology of "recursive
counterexamples".  These counterexamples are foundationally
interesting, because they are the standard means of showing that
certain specific mathematical theorems are "computably false", i.e.,
that they fail in the omega-model of computable (i.e., recursive)
sets.

[ For general background on this topic, look up "recursive
counterexamples" in the index of my book Subsystems of Second Order
Arithmetic, 1999, http://www.math.psu.edu/simpson/sosoa/.  See also
the Handbook of Recursive Mathematics, 1999, edited by Ershov,
Goncharov, Nerode, and Remmel. ]

Harvey observes that, when recursive counterexamples are obtained by
directly encoding a complete r.e. set -- corresponding to ACA_0 in
reverse mathematics -- one usually obtains constructive information.
For example, one can prove *constructively* that there is a recursive
bounded sequence of rational numbers with no recursive limit point.

I would also point out that the same applies to a more sophisticated
class of recursive counterexamples, where one encodes an effectively
inseparable pair of r.e. sets -- corresponding to WKL_0 in reverse
mathematics.  For example, this technique can be used to prove
*constructively* that there exists a recursive formally real field
with no recursive total ordering. (See the discussion in Section IV.4
of my book.)

Harvey continues:

 > there are also plenty of examples of such statements which
 > are normally proved using a priority argument.

I find this statement questionable.  Harvey, could you please give an
example of this?  

I do not ask this question idly or lightly.  My strong impression
based on experience is that priority arguments used to obtain
recursive counterexamples are often or always unnecessary or illusory.
I am aware that recursion theorists often say they are using a
priority argument to obtain a recursive counterexample, but in the
cases I know of, it turns out that the so-called priority argument is
better viewed as or replaced by a straightforward coding argument.  An
example of this (Downey/Kurtz/Hatzikiriakou/Simpson -- about orderings
of Abelian groups) is presented in my FOM posting of 13 Aug 1999.
Other examples are in my book.  E.g., Section IV.4, about orderings of
fields, and Section III.4, about bases of vector spaces.

Some recursion theorists are under the impression that reverse
mathematics consists largely of the metamathematics of priority
arguments.  This is not the case.  There are no priority arguments in
my definitive book on reverse mathematics.

Harvey asks:

 > In these cases does one get a constructive proof of the original
 > statement in any reasonable sense?

If a priority argument is used, the proof is non-constructive, so the
answer to Harvey's question is no.  But the answer becomes yes, when
the priority argument is replaced by a (usually easier) coding
argument.  The coding argument is fully constructive.  This is
illustrated by the examples mentioned above.

This is a good reason to avoid the use of priority arguments for
obtaining recursive counterexamples.  Fortunately, it seems that, in
these foundationally interesting applications of recursion theory, one
can often or always avoid priority arguments.  

See also the discussion of "priority arguments in applied recursion
theory", FOM, July/August/September, 1999.

-- Steve