FOM: Kreisel's "unwinding" program

[Solomon Feferman]

In his posting of yesterday (March 1, 19:00) Steve Simpson reviewed
Angus MacIntyre's essay, "The strength of weak systems".  The review
concerns many matters, but since I have not read the essay itself, I just
want to comment on one of these.  Apparently MacIntyre spoke favorably of
the work of Kreisel in the 1950s demonstrating the formalizability of
analytic number theory in PA (Peano Arithmetic) and using his
results on the unwinding of proofs in PA to obtain concrete information
about results obtained by analytic methods.  In particular, Kreisel
claimed in various places to have obtained three or four level
(depending on how you count) exponential bounds for the first change of
sign in pi(x) - li(x), proved without bounds by Littlewood using
non-constructive 
arguments [it went one way if R.H., the Riemann Hypothesis, is true,
another if false].  I have examined Kreisel's arguments in detail in a
paper entitled "Kreisel's 'unwinding' program", and have found them to be
seriously wanting if not suspicious as to their grounds.  As I say in my
article, which was published in the volume "Kreiseliana" (P. Odifreddi, 
ed., A.K. Peters, Ltd., 1996), and which can also be found at my ftp
site

ftp://gauss.stanford.edu/pub/papers/feferman/

under the rubric 'unwind', the "expected details are either problematic 
or simply missing".  This is why I called specifically for a
re-examination of the formalization of results like Littlewood's in weak
subsystems of PA, in a recent posting (referred to by Simpson).  What the
foundational significance of such work may be is another matter that I will
try to take up on another occasion.  

Let me add some more personal remarks vis a vis the evaluation of
Kreisel's work. At the beginning of my article I said that Kreisel "did
perhaps more than anyone else to promote the development of proof theory
and the metamathematics of constructivity in the last forty-odd years"
through "his own contributions (individual and collaborative) and his
extraordinary personal influence."  In particular, he and I were very
close colleagues for close to twenty years, and he greatly influenced my
own development as a logician during that period.  But his increasingly
critical views of foundational work in general, and of 
individual logicians in particular, led to his estrangement from
practically all of his former collaborators, myself included.  Since the
1970s, his views have had a baleful impact on our field and have led some
on the outside to a serious mis-evaluation of its achievements.  There is
no need to formulate this in terms of general intellectual interest vs.
mathematical interest, but what has apparently resulted in such essays as
MacIntyre's (if Simpson's report is accurate) is an unfortunate snobbism
or dismissal of foundational work, and that only applications of logic to
"real", "hard" mathematics is to be valued.  Let me make clear that this
has nothing to do with my own great appreciation of the latter through the
work of MacIntyre, van den Dries, Wilkie, Zilber, Hrushovski and others,
which had its roots in the pioneering model-theoretic work of Tarski and 
Abraham Robinson.  The excitement and drive of their research programs is
palpable (as is evidenced by the current convocations at MSRI) and cannot
be gainsaid.  Let us hope the non-logical mathematicians value their work
as much as these logicians admire current hard-core mathematics.  

--Sol Feferman