FOM: Soare on Sigma11 choice

[Stephen G Simpson]

This is a response to part of Robert Soare's extremely long FOM
posting of 2 Aug 1999 12:54:07.

Soare's account of results related to Sigma11 choice is seriously
incorrect.  Soare said

 > In Reverse Mathematics ITSELF, Leo Harrington [1979] proved that
 > that boldface Sigma-1-1 axiom of choice does not imply lightface
 > Sigma-1-1 dependent choices.
 ...
 > Harrington and Steel explain ... how a priority argument is the
 > right method to use in order to MAKE the EARLIER boldface Steel
 > proof more "EFFECTIVE," a typical use of the priority method
 > applied by Harrington and others many times, to effectivize a
 > noneffective result.

 [Soare's emphasis]

and this is incorrect on three counts:

 1. The result in question (i.e., existence of an omega-model of
    [boldface] Sigma11 choice in which [lightface] Sigma11 dependent
    choice fails) is due to neither Leo Harrington nor John Steel, but
    to Harvey Friedman.  It was originally stated and proved in
    Friedman's Ph.D. thesis, MIT, 1967.
    
 2. Friedman's proof of the result in question does not use anything
    like a priority argument.  Rather, it is an ingenious application
    of Friedman's omega-model version of G"odel's second
    incompleteness theorem.

Points 1 and 2 are well documented in the literature.  I am good
friends with all of these people (Harrington, Steel, Friedman), and I
have personal knowledge that at least Steel, and probably also
Harrington, is very well aware of points 1 and 2 and will readily
acknowledge them, if asked.  See also the full exposition, with
bibligraphic references, of this and many related results in sections
VIII.5 and VIII.6 of my book ``Subsystems of Second Order Arithmetic''
<http://www.math.psu.edu/simpson/sosoa/>.

In a few days I plan to post another message on FOM giving my account
of the history of this and related results, from my viewpoint as a
spectator and participant, right up to the present.

Soare has said that he tried very hard to verify all of the facts in
his extremely long posting of 2 Aug 1999 12:54:07.  But somehow his
verification process misfired, on this issue at least.

 3. Soare notwithstanding, the result in question is *not* part of
    Reverse Mathematics.  Rather, it is an independence result for
    certain subsystems of second order arithmetic.  The systems in
    question, Sigma11 choice and Sigma11 dependent choice, are *not*
    among the small number of ``basic systems'' that have arisen
    repeatedly in Reverse Mathematics, as equivalents of many
    different mathematical theorems.  (It is true however that inner
    omega-models of Sigma11 choice have been used as a technical
    device for certain proofs in Reverse Mathematics.)

All of this is laid out in great detail in my book ``Subsystems of
Second Order Arithmetic''.  Later I will post something on FOM
concerning the relationship between Reverse Mathematics and subsystems
of second order arithmetic.  Apparently a serious misunderstanding of
just this issue is what caused Soare to ``shoot from the lip'' here.

A couple of days ago, Soare sent me an aggressive private e-mail
complaining that he hasn't been able to properly inform himself about
Reverse Mathematics, because the library at his university does not
have a copy of my book.  And unfortunately, Soare is very angry with
me these days, so angry that I wasn't able to give him the instant
enlightenment which he sought.  My suggestion for Soare now would be
to visit my book's web page at
<http://www.math.psu.edu/simpson/sosoa/>, where chapter one and
ordering information are available.

-- Steve