FOM: FOM, unwinding and elimination of analytical methods
Ulrich Kohlenbach
kohlenb at brics.dk
Wed Mar 4 08:19:16 EST 1998
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
More information about the FOM
mailing list