FOM: priority arguments in applied recursion theory; proof cleansing

[Stephen G Simpson]

This is a response to parts 1A-1N of Robert Soare's angry FOM posting
of 2 Aug 1999 12:54:07.

Concerning the so-called Simpson's Thesis, Soare asked angrily:

 > Which is it Mr. Simpson, ST or ST'?  It doesn't really matter
 > because they are BOTH REFUTABLE.
 
 [ Soare's emphasis. By the way, does anybody know what ST' stands
 for?  Does it stand for ``Soare's Thesis''?  :-) ]

My answer is that ``it'' is ST (Simpson's Thesis), not Soare's
distorted version.  The concise statement of Simpson's Thesis is:

  ``Priority methods are almost completely absent from applied
  recursion theory.''

[ By the way, I would like to remark that it wasn't my idea to call
this statement ``Simpson's Thesis''.  So far as I can tell, it was
Soare who first started calling it a ``thesis''.  This was in Soare's
COMP-THY posting of 9 July 1999, which is accessible as part of the
ongoing discussion of the CTA meeting (``Computability Theory and
Applications'') at <http://www.math.psu.edu/simpson/cta/>.  After
that, Harvey Friedman in his 19 Jul 1999 12:33:44 FOM posting
``Invitation to Soare'' started calling it ``Simpson's Thesis'', and
the name stuck. ]

To provide some context, let me quote the entire passage surrounding
the original statement of Simpson's Thesis.  Here it is:

 > Obviously the organizers of the CTA meeting were concerned with a
 > distinction between *pure* recursion theory, i.e. the study of
 > structural questions concerning r.e. degrees, r.e. sets, etc., and
 > *applied* recursion theory, i.e. recursion theory connected to
 > issues and programs in f.o.m. and other areas, including: recursive
 > mathematics, intuitionistic mathematics, constructive mathematics,
 > reverse mathematics, theoretical computer science, undecidable
 > problems in mathematics, etc.
 > 
 > Historically, the pure/applied dichotomy has been fairly stark.
 > For example, priority methods were originated by Friedberg and
 > Muchnik to produce an incomparable pair of r.e. degrees, and
 > difficult priority arguments remain a hallmark of pure recursion
 > theory.  But priority methods are almost completely absent from
 > applied recursion theory.  (Below I will point out an exception to
 > this rule.)
 > 
 > At the CTA meeting, the pure/applied distinction was also much in
 > evidence.  Although the organizers tried to include a lot of
 > applied recursion theory talks and to bridge the pure/applied gap,
 > there was very little actual connection between the two domains.
 > There were only a few points of intellectual contact between the
 > pure recursion theory talks and the applied recursion theory talks.
 > (Below I will mention some of these points of contact.)

This is from my original 21 Jun 1999 21:36:37 FOM posting entitled
``an unusual recursion theory meeting; impressions of CTA talks''.
This is the posting that started it all, i.e., the one where the
so-called Simpson's Thesis first appeared.  Thus, in order to discuss
Simpson's Thesis as originally stated, we need to ask how prevalent
priority methods are in the various areas of ``applied recursion
theory'' as enumerated above.  These areas are:

  recursive mathematics

  intuitionistic mathematics

  constructive mathematics
 
  reverse mathematics

  theoretical computer science

  undecidable problems in mathematics

  et cetera

So let me comment briefly on each of these areas, and then we can
discuss them individually in future postings.

recursive analysis:

  No priority arguments.  See the books of Aberth and
  Pour-El/Richards.  See also my FOM posting of 22 Jul 1999 20:32:42.

recursive algebra and combinatorics:
  
  There are quite a few priority arguments (see e.g. the Handbook of
  Recursive Mathematics), but I suspect that many of them can easily
  be eliminated; see the Metakides/Nerode example in my FOM posting of
  22 Jul 1999 20:32:42.  See also the discussion of ``proof
  cleansing'' below.

intuitionistic and constructive mathematics:

  No priority arguments.  See for instance the books by Beeson,
  Troelstra/van Dalen, Bishop/Bridges, etc.

reverse mathematics:

  No priority arguments.  See my definitive book ``Subsystems of
  Second Order Arithmetic'' <http://www.math.psu.edu/simpson/sosoa/>.
  See also my refutation below of Soare's claims about alleged
  priority arguments in reverse mathematics.

theoretical computer science:

  It's hard to get a handle on this, but Fenner 3 Aug 1999 12:38:58
  says the ratio of papers that use priority arguments to those that
  don't is very small.  And he isn't aware of significant use of
  priority arguments in computational complexity theory other than
  collapsing degrees, where he is an expert.  I concede however that
  there are at least some priority arguments here, and I don't know
  whether they can easily be eliminated.

undecidable problems in mathematics:

  No priority arguments.

et cetera:

  Let's talk more about this later.  :-)

So, in sum, Simpson's Thesis as originally formulated seems to be
by-and-large correct.  But I am open to discussion.

Now I will comment on Soare's alleged refutation of Simpson's Thesis.
According to Soare,

 > In only a few days computability theorists have gathered nearly TWO
 > HUNDRED references to refute Simpson's Thesis (ST), including a
 > NUMBER IN REVERSE MATHEMATICS (Simpson's OWN research area), with
 > hundreds more to come.  These references are posted on the web
 > page, www.cs.uchicago.edu/~soare/lectures/applications.html

 [ Soare's emphasis ]

and I have looked several times at this hastily compiled and
still-evolving web page.  The current version of it is available as
<http://www.math.psu.edu/simpson/cta/applications-990729.html>.

There is a lot to say about Soare's ``applications'' web page, but the
main point I want to make here is that it does not contradict
Simpson's Thesis.  In fact, considering that it is apparently the best
Soare can do, I regard it as additional tentative *confirmation* of
Simpson's Thesis.

Let me elaborate:

1. Soare's ``applications'' web page starts with some thoughtful
   comments by Carl Jockusch on five places ``where priority arguments
   play a role in interactions of computability with other areas''.
   Note however that Jockusch speaks not of *applications* but of
   *interactions*.  And that is exactly what they are: interactions,
   not applications, in areas such as recursive Ramsey theory.  We
   know from Soare's COMP-THY posting that even Jockusch himself does
   not want to refer to these results as ``applied recursion theory''.
   See also my discussion of the applications/connections distinction
   and Jockusch's views in FOM 15 Jul 1999 22:33:53.

2. The rest of Soare's ``applications'' web page consists largely of
   an unstructured jumble of excerpts from the publication lists of
   various recursion theorists, including Soare himself.  With
   reference to Simpson's Thesis, this jumble is unconvincing, because
   there is little or no indication of the results and methods that
   constitute the alleged so-called ``applications''.  Furthermore,
   there is little or no attempt to distinguish among

     a. *applications* of priority arguments,
     b. *applications* of other recursion-theoretic techniques,
     c. *interactions* involving priority arguments,
     d. *interactions* involving other recursion-theoretic techniques,
     f. places where priority methods are hard to eliminate,
     e. places where priority methods are easy to eliminate.

   These and other distinctions are of course crucial for a serious
   discussion of Simpson's Thesis.  To quote from my FOM posting of 15
   Jul 1999 22:33:53,

    > If we are going to compile lists of ``applications'' of
    > recursion theory, such as Soare's compilation at
    > <http://www.cs.uchicago.edu/~soare/lectures/applications.html>,
    > then we ought to classify them carefully and distinguish various
    > features, just as the applied model theorists do.  For each
    > ``application'' of recursion theory, we need to say what the
    > field of application is, whether the statement of the result or
    > only the proof involves recursion-theoretic concepts, which
    > recursion-theoretic concepts and/or methods and/or results are
    > used, whether the recursion-theoretic concepts and/or methods
    > and/or results can be eliminated, what are the costs of
    > eliminating them, etc.  There are many distinctions to be made,
    > and these distinctions are of essential scientific importance.
    > It is misleading to lump everything together as ``applications''
    > without further qualification.

   Soare says these distinctions don't matter, but in fact they do
   matter.  They matter a lot.

3. Soare claims on his web page and in FOM 2 Aug 1999 12:54:07 that

    > If one specifically desires applications of the priority method
    > to Reverse Mathematics, then Mytilinaios and Slaman used a
    > priority argument in their Reverse Mathematics paper, "On a
    > question of Brown and Simpson," and solved a problem posed by
    > Brown and Simpson in 1993.

   But this claim by Soare is incorrect.  I happen to be familiar with
   this area!  The result in question is that BCT-II does not imply
   RCA_0^+.  The Mytilinaios/Slaman proof of this result uses the low
   basis theorem but does not use a priority argument.  (With regard
   to the low basis theorem, see below.)  There is a priority argument
   in the Mytilinaios/Slaman paper, but it doesn't address reverse
   mathematics.

   By the way, this paper was published around the time of the OJ
   trial, if I am not mistaken.

   By the way, an even more interesting reverse mathematics problem
   that was studied in the Brown/Simpson paper is still not completely
   solved.  Namely, what does it take to prove the open mapping
   theorem for separable Banach spaces?  Is the open mapping theorem
   for separable Banach spaces provable in RCA_0?

4. Soare claims on his ``applications'' web page and in FOM 2 Aug 1999
   12:54:07 that Leo Harrington used a priority argument to prove an
   (unpublished) result in reverse mathematics.  This is incorrect, as
   I pointed out in my FOM posting of 3 Aug 1999 20:56:31 on Sigma11
   choice.  And, as mentioned there, I am planning two further FOM
   postings which will explain exactly what Harrington did and how it
   is related to reverse mathematics, among other things.

5. Soare claims on his ``applications'' web page and in FOM 2 Aug 1999
   12:54:07 that Donald Martin's original 1975 proof of Borel
   determinacy is a priority argument.  I'm skeptical about this, but
   unfortunately I don't have Martin's paper handy to check.  Did
   Martin himself say that it is a priority argument?

   In any case, I once presented Martin's streamlined ``purely
   inductive'' 1985 proof of Borel determinacy in a graduate course on
   Borel sets, and I can tell you that there is absolutely no priority
   argument there.  (In the same course I presented Harvey Friedman's
   streamlined 1981 proof of his 1969 result that Borel determinacy
   needs aleph_1 cardinals.  This pair of results is one of my
   favorite chapters of set theory.)

6. Soare claims in FOM 2 Aug 1999 12:54:07 that a result in Reed
   Solomon's 1998 thesis about the reverse mathematics of ordered
   groups uses a priority argument.  I checked with Reed about this
   and he says that Jeff Hirst has eliminated the priority argument.

Finally, an interesting issue that is bound to come up often in any
discussion of Simpson's Thesis is the so-called ``proof cleansing''
issue, i.e., elimination of priority arguments.  Soare claims to think
this issue is unimportant.  He asks rhetorically:

  > If the priority method proved a theorem FIRST, what does it MATTER
  > whether later on there is ANOTHER (maybe even better, simpler,
  > shorter) proof?

  [ Soare's emphasis. ]

I have two answers to this question.  (1) It matters, if we want to
discuss Simpson's Thesis in a systematic and scientifically honest
way.  (2) It matters, if we are interested in finding the ``right''
proofs of our theorems.

Regarding Simpson's Thesis, my experience tells me that some recursion
theorists sometimes resort to priority arguments prematurely and don't
bother to investigate whether their proofs can be simplified/improved.
I suspect this is because recursion theorists as a group have a large
investment in priority arguments, so large that they don't *want* to
eliminate them, even when this would result in a better, simpler,
shorter proof of a better result.  This seems to happen quite often,
especially in applied recursion theory.  In order to discuss
meaningful aspects of Simpson's Thesis, we need to be aware of this
phenomenon.

On the other hand, an important theorem of applied recursion theory is
the low basis theorem, and according to Soare,

  > Jockusch and Soare first proved the often applied Low Basis
  > Theorem with a priority argument ....

However, none of the *published* proofs of the low basis theorem use a
priority argument.  This includes both the original Jockusch/Soare
1972 proof and the proof in Soare's 1987 book, not to mention the
proof in section VIII.2 of my 1998 book ``Subsystems of Second Order
Arithmetic'' <http://www.math.psu.edu/simpson/sosoa/>.

Thus the low basis theorem seems to be a case where the authors
*started* their thought process with priority arguments -- perfectly
natural, since priority arguments are a powerful technique in pure
recursion theory and they are experts at it -- but *ended* by
publishing a non-priority proof, which they evidently regarded as
simpler, shorter, better.

Should we count these cases as priority arguments in applied recursion
theory, for Simpson's Thesis purposes?  I think not.  But I suspect
that this pattern occurs quite often in both pure and applied
recursion theory.  More generally, it occurs throughout mathematics,
because cleaning up proofs prior to publication is something that many
of us like to do.

-- Steve