FOM: sour grapes vis a vis Reverse Mathematics

[Stephen G Simpson]

This FOM posting consists of some reactions to Angus Macintyre's essay
"The Strength of Weak Systems", which was published as part of the
proceedings of a symposium on Wittgenstein(!), published by Kluwer,
1986, pages 43-59.  Macintyre acknowledges "advice" from Kreisel.
Indeed, Kreisel's influence is readily apparent; see below.

For a long time Harvey has been promising an FOM posting in response
to Macintyre.  I'm diving in now because I got tired of waiting for
Harvey.

Macintyre's essay consists of a string of pointed but sloppy comments
on various aspects of contemporary research in mathematical logic and
f.o.m.  I have been told that Macintyre's custom is to pontificate on
such matters while drinking beer in dimly lit pubs surrounded by
junior colleagues who are in no position to contradict him.  That
scenario perfectly matches the style and tone of the essay under
discussion.  It's a shame that Macintyre has been unwilling or unable
to subject his views to public give-and-take here in the light of day
provided by the FOM list.  Although I disagree with many of
Macintyre's opinions, I respect his mathematical contributions, and I
believe that a dialogue with Macintyre here on the FOM list would be
interesting and productive.

The overall point that Macintyre seems to be driving at is that,
according to Macintyre, contemporary research in mathematical logic
and f.o.m. is deficient because almost none of it contributes to what
he calls "effective understanding".  Macintyre reserves his most
sarcastic and scathing comments for Reverse Mathematics, a subject
that I have been closely identified with.  Hence this posting.

Reading between the lines, it seems clear that Macintyre's notion of
"effective understanding" refers to core mathematical subjects such as
number theory and algebraic geometry.  In other words, to put it
crudely, Macintyre regards f.o.m. as no damn good because it isn't
number theory.  Do I detect a noxious aroma of f.o.m.-bashing?  In any
case, I think that Macintyre's viewpoint is easily seen to be rather
peculiar when viewed in the light of day.  Macintyre's viewpoint has
been advocated here on the FOM list by Lou van den Dries, who insists
that G"odel is small potatoes compared to any of dozens of 20th
century core mathematicians.  This doesn't square with normal criteria
of general intellectual interest.  See also the FOM brawl on general
intellectual interest (December 1997).  Macintyre and van den Dries
are completely off base.

In his introduction, Macintyre summarizes as follows:

  "One intended moral of the paper is that induction may be an
  all-purpose proof method in arithmetic, without being a masterly
  method for the discovery of new resources of argument."

In this connection, I think Macintyre fails to take account of the
views of Poincare about the creative role of induction (see for
instance Harvey's posting of 15 Oct 1997 03:15:39).

A very short section of Macintyre's essay is devoted to set theory.
He begins with a Tragesser-like comment (see Tragesser's FOM posting
of 20 Feb 1998 11:38:18) concerning set-theoretic formalization of
mathematics:
  
  "Who can deny that the translation distorts hopelessly our intuitive
  resonances to mathematical situations?"

This criticism strikes me as wrong-headed, just like the romantic or
Marxist critique of capitalism and the Industrial Revolution on the
grounds that they alienate us from our pre-industrial roots.  The
plain facts are that capitalism doesn't prevent us from taking
vacations in the countryside, and set-theoretic foundations need not
play havoc with "intuitive resonances" that may have been obtained
elsewhere.

On the same page Macintyre criticizes large cardinals on the grounds
that they do not contribute to core mathematics:

  "none of the large cardinal systems can reasonably be called
  *strong* if that carries any hint of relevance to the central parts
  of mathematics."

Inexcusably, Macintyre omits all mention of Harvey Friedman's finite
combinatorial theorems which require large cardinals.  (For the latest
results in this direction, see Harvey's web page at
http://www.math.ohio-state.edu/~friedman/.)

In a very short section on the G"odel incompleteness phenomenon,
Macintyre touts Kreisel's work.  He says:

  "not until Kreisel's 1950's papers [Kr2,Kr4] on the mathematical
  significance of consistency proofs, did one have a realistic
  appraisal, in terms of conservative extensions, of the power of
  complex analysis in analytic number theory.  No G"odel phenomenon is
  to be expected there."

If I'm not mistaken, the first sentence above refers to some early
work of Kreisel concerning formalization of analysis within
conservative extensions of PA.  (See also recent FOM postings by
Feferman 27 Feb 1998 08:57:15, Shipman 25 Feb 1998 17:03:56, and
myself 25 Feb 1998 14:14:59.)  But Macintyre's second sentence baffles
me.  Why does Macintyre think there is no G"odel phenomenon in
analytic number theory?  The formal systems in question certainly do
exhibit the incompleteness phenomenon.  Is Macintyre engaging in
wishful thinking, like van den Dries's discussion of the "G"odel
horizon" (16 Oct 1997 23:21:25)?

A large part of Macintyre's essay consists of a review of work in
applied model theory and bounded arithmetic.  I find this work
interesting, but I don't have anything new to say here.

The part of Macintyre's essay that offended me most is the last
section, on Reverse Mathematics.  Before responding, let me briefly
summarize the big picture provided by this research program.

Reverse Mathematics consists of a series of case studies in
formalization of mathematics within subsystems of second order
arithmetic with restricted induction.  It turns out that, for a great
many specific key mathematical theorems t, there is a weakest natural
system S(t) in which t is provable.  In each case, "weakest natural"
is validated by showing that t is logically equivalent to the
principal set existence axiom of S(t), equivalence being proved in a
weak base system.  Furthermore, the systems S(t) that arise frequently
are few in number, principally the following:

  1. RCA_0 (Delta^0_1 comprehension plus Sigma^0_1 induction)
  2. WKL_0 (RCA_0 plus weak K"onig's lemma)
  3. ACA_0 (arithmetical comprehension)
  4. ATR_0 (arithmetical transfinite recursion)
  5. Pi^1_1-CA_0 (Pi^1_1 comprehension)

For example, the theorem that every continuous f:[0,1] -> R has a
maximum is equivalent to WKL_0 over RCA_0.  Also equivalent to WKL_0
over RCA_0 are: the Cauchy-Peano existence theorem for solutions of
ordinary differential equations; the Heine-Borel compactness of [0,1];
the theorem that every countable commutative ring has a prime ideal;
the Hahn-Banach theorem for separable Banach spaces; the Brouwer and
Schauder fixed point theorems; etc etc.  These results for WKL_0 are
of interest with respect to Hilbert's program of finitistic
reductionism, because WKL_0 is conservative over primitive recursive
arithmetic for Pi^0_2 sentences.  See
http://www.math.psu.edu/simpson/papers/hilbert/.  Moreover, just as
WKL_0 embodies finitistic reductionism, there are similar
correspondences to other foundational programs: ACA_0 embodies
predicative mathematics, and ATR_0 embodies predicative reductionism.

Macintyre does not indicate or discuss the scope and nature of the
results above.  Instead, he criticizes some of them on the grounds
that he "cannot be surprised" by them.  In this I hear the voice of
Kreisel.  Kreisel's voice is saying: "sour grapes".  In the 1960's
Kreisel was intensely interested in subsystems of second order
arithmetic and their role in f.o.m.  Unfortunately, Kreisel never came
up with the idea of Reverse Mathematics, was never able to do anything
coherent along these lines, and was very upset by my work in this area
in the 1970's and 1980's.  The inspiration for my work goes back to
some early papers of Harvey Friedman.  Perhaps Kreisel would claim to
have influenced Harvey.  I'll let Harvey comment on this if he wishes
to do so.

Macintyre takes a gratuitous dig at Harvey's program of so-called
calibration of mathematical texts, by asserting that it is based on
what Macintyre calls a "classical logical error."  But it is Macintyre
himself who has committed a logical error.  Macintyre says:

  "*No* living mathematical text will use the full range of
  quantification in the Cauchy-Peano Theorem, and will apply the
  theorem only as a convenience."

Here Macintyre is ignoring the logical requirement of simplicity.  In
order to make our formulations useful, we keep them simple.  This is
more than a matter of "convenience".  It is a logical necessity.  The
idea of Harvey's calibration program is to analyze mathematical texts
as they are, not as Macintyre might wish they would be if encumbered
by incomprehensible and unnecessary hypotheses.

As a final criticism of Reverse Mathematics and Harvey's calibration
program, Macintyre compares them unfavorably and inappropriately to a
half-baked idea of Thom.  Macintyre ends his essay as follows:

  "This is not to say that I object to all dramatic formulations in
  terms of fundamental mathematical principles.  I recall from 1979
  Professor Thom asserting that there are only about four theorems
  (methods) in mathematics.  The implicit function theorem was one,
  and the sense of the claim here is evident ....  For examples of the
  life involved, one can read the masterly [A].  Thom's remark may be
  an exaggeration, but he has unerringly drawn attention to one of the
  most supple of mathematical methods, beside which Friedman's axioms
  are pale stuff."

Unfortunately, "the masterly [A]" is omitted from Macintyre's list of
references (more sloppiness!), so Macintyre's point concerning the
implicit function theorem falls flat.  In any case, it is clear that
Macintyre is comparing apples to oranges.  For one thing, Reverse
Mathematics is *not* an exaggeration; it is a mathematical research
program with many precise results to back up its claims.  For another,
Reverse Mathematics is serious f.o.m. research concerning the question
of which set-existence axioms are appropriate for mathematics.  By
comparison, the Thom/Macintyre 4-fold scheme amounts to nothing more
than pointless bar-room chatter.

-- Steve