FOM: FOM, unwinding and elimination of analytical methods

[Ulrich Kohlenbach]

I would like to add a view comments to the ongoing discussion about Kreisel's
"unwinding program" and "elimination of analytical methods". 
In a recent posting S. Feferman wrote: 

>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.  

I agree with Sol's view and find the polemic against FOM-oriented logic 
expressed in some writings of Kreisel particular unfortunate since in my view 
there is no real conflict between "FOM-style" proof theory and the attempt to 
investigate specific proofs with the aim to obtain general insights (resulting 
eventually in a "theory of proofs") in how the logical/mathematical structure 
of a given proof and the "ideal principles" used in it relate to the  
the computational/arithmetical content of the proof.  

Let me explain this by referring to some work of mine in the context of 
approximation theory (see my papers "Effective moduli from ineffective 
uniqueness proof...", APAL 64, pp.27-94(1993), "New effective moduli of 
uniqueness and uniform a priori estimates for constants of strong unicity",
J.Numer.Funct.Anal. and Optimiz. 14, pp. 581-606 (1993), and as a survey 
"Analysing proofs in analysis", in: Logic: From Foundations to Applications, 
OUP (1996)):    

Using among other things a variant of Goedel's functional interpretation I 
analysed a couple of (essentially two) classical non-constructive proofs for 
the uniqueness of best Chebycheff approximation. Lets call these two proofs 
p1 and p2. P1 is the proof which can be found in almost all textbooks and 
goes back to Tonelli (1908)/de La Vallee Poussin (1917) while p2 is due to 
Borel(1905)/Young(1907). Both p1 and p2 essentially use the so-called 
alternation theorem AT which can be seen to imply WKL. Using an appropriate 
arithmetical context, AT follows from the theorem of the attainment of 
the maximum of f in C[0,1] (and hence from WKL). 
Both proofs differ only in their relatively small constructive endpieces 
and by any mathematical standards the endpiece of p1 is even more elementary 
and elegant than that of p2 (thats, I guess, the reason why 90% of all 
textbooks present p1). 
Nevertheless the unwindings of p1 and p2 are quite different mainly   
w.r.t. the complexity of the unwinding but also w.r.t. to the quality of the 
data obtained (uniform constants of strong unicity). 
And it is p1 which is very complicated to unwind and produces a less good 
constant of strong unicity. 
A very interesting FOM-point here (perhaps more interesting than that the best 
resulting bounds also improved known results in approximation theory, see my 
paper in J. Numer. Funct.Anal.and Optimiz 14,1993 mentioned above, note also 
that even the plain EXISTENCE of uniform constants of strong unicity for 
Chebycheff approx. was shown only in 1976 by analysts!) for me is that this 
different behaviour can be completely explained by a proof-theoretic 
meta-result which just "predicts" this to be happen (the result I am 
referring to is: thm.4.17 in my paper "Effective bounds from ineffective 
proofs in analysis" in JSL 57,1992):   

P2 applies AT in a slightly different form AT* to obtain the uniqueness, 
and AT* (which still implies WKL and is even in a certain sense 
"more nonconstructive") has a specific logical form which allows to treat 
it as an AXIOM in the process of unwinding p2 (this fact that various 
non-constructive principles can be treated directly as axioms and don't 
contribute to the extractable bounds is a distinguished feature of the 
method of "monotone functional interpretation" as discussed in my paper 
"Analysing proofs in analysis", see above). 
In contrast to this AT itself has a slightly more complicated logical 
structure. One still can analyse proofs using lemmas of this more general 
type but then (thats the content of the thm.4.17 mentioned above) the PROOFS 
of these lemmas matter since a QUANTITATIVE version of (a constructive 
epsilon-weakening, corresponding to the Bishop-style constructive substitutes 
of classical theorems, of) the lemmas is needed for the final result. Thats 
why one has to unwind the whole non-constructive proof of AT as well in the 
case of p1 which can be avoided for p2. 

After the extraction of the data which strengthen the original uniqueness 
theorem quantitatively one can also obtain (both for p1 and for p2) a 
purely arithmetical proof of these results which can be carried out e.g. 
in some subsystem of intuitionistic arithmetic (in the language of functionals 
of finite type). However this "elimination of analytical methods" comes after 
the extraction of the constructive content of the proof (the bounds). 
The elimination of analytical methods is achieved again by monotone functional 
interpretation which allows to replace lemmas of the type AT* (including WKL) 
by certain epsilon-weakenings which are provable by elementary means. 
This technique also can be used to obtain short proofs of  proof-theoretic 
conservation results of WKL relatively to (even extremely weak) fragments of 
classical arithmetic in all finite types generalizing H. Friedman's classical 
result (see e.g. my paper "Mathematically strong subsystems of analysis...", 
Arch.Math.Logic 36, pp.31-41(1996), to which S. Feferman referred to in a 
recent posting, and subsequent ones on the "program" of what I call 
polynomially bounded analysis, see my paper "Proof Theory and Computational 
Analysis" which can be downloaded from my homepage). 
I should stress that the method of monotone functional interpretation doesn't 
cause any significant blow up in the length of the proof since normalization
is not needed unless one wants to perform the final passage to a first-order 
system like PRA (instead of its conservative finite type extension PRA^omega).  

So we have here a nice interplay of FOM (in particular of reverse mathematics) 
and the "unwinding program": 

FOM-results yield the a-priori existence of some reasonable (at 
least prim. rec.) content of the uniqueness proofs discussed above since 
the only higher function existence principle used is WKL which can be 
eliminated from proofs of certain classes of formulas (including the 
uniqueness theorems). 
However for a feasible and faithful unwinding one has to design a method 
which directly deals with the non-constructive principles at hand, namely AT, 
AT* and allows a perspicuous extraction of data without performing any 
elimination of analytical principles. 
The resulting method can be used not only to prove general 
meta-results on uniqueness theorems in a very general sense but also to 
strengthen "pure" FOM-results concerning WKL (see above) etc. 

Already the bare fact that there actually exist non-trivial specific proofs 
(p1 and p2) which use essentially (in the sense of ordinary mathematics) 
WKL although FOM tells that its elimination is possible in principle is in 
my view of FOM-interest: The conservation results for e.g. WKL(_0) and 
RCA(_0) are highly non-trivial even for single specific proofs! 

I suspect that even Kreisel was and is somehow interested in this 
FOM(?)-aspect of unwindings: 
he still stresses the insights obtained by Girard's unwindings of 
proofs of van der Waerden's theorem although this work is obsolete from 
an ordinary mathematical point of you because of S. Shelah's subsequent 
much better prim. rec. bound (obtained without any reference to logic). 

Ulrich Kohlenbach 
Research Assistant Professor
Department of Computer Science
University of Aarhus Denmark
http://www.brics.dk/~kohlenb/
Research interests: Proof theory with applications to FOM, Mathematics and 
                    Computer Science