克莱瑟的“重心转移”及当代证明挖掘.pdf

Studies in Logic,Vol.16,No.3(2023):135PII:16743202(2023)03000135Kreisels“Shift of Emphasis”andContemporary Proof Mining*Ulrich KohlenbachAbstract.The contemporary“proof mining”paradigm has its historical roots in GeorgKreisels program of“unwinding of proofs”.In this paper we elaborate on the tremendousinfluence Kreisels ideas have had and still have on this applied reorientation of proof theoryand discuss some logical aspects of“proof mining”.1IntroductionThe story above began and ended with shifts away from traditionallogical aims.(106,p.401)A price paid by those(of us)later pursuing proof theory has been todiscoversuitableideasforadaptingconsistencyproofstoaimsrewardingfor a broader view,naturally,not an unduly high price for those(of us)attracted by such activity.(108,pp.4344)Starting in the early 50s,Kreisel argued that prooftheoretic methods which hadbeen developed in the course of Hilberts consistency program could be used for concrete mathematical goals different and independent from their original foundationalmotivation.Kreisels writings on this topic,in particular in connection with his concept of“unwinding of proofs”,span over a period of 60 years and contain numerousimportant insights and suggestions on how such a reorientation of traditional prooftheoryfrom foundational aims to applications incore mathematics could be achieved.In this paper,we revisit some of Kreisels main themes from the perspective of thecurrent“proof mining”program which has been pursued,e.g.,by the present authorandmany collaboratorsas a modern and more systematic version of KreiselsoriginalReceived 20220319Ulrich KohlenbachDepartment of Mathematics,Technische Universitt Darmstadtkohlenbachmathematik.tudarmstadt.de*An earlier version of this paper was originally submitted in January 2018 as an invited contributionto a volume“Intuitionism,Computation,and Proof:Selected themes from the research of G.Kreisel,inM.Antonutti Marfori and M.Petrolo(eds.)”but withdrawn in March 2022 when that volume still hadnotmaterialized.Sincethenthepaperhasbeenupdatedandexpendedtoreflectsomenewdevelopmentsin proof mining since 2018.The author is grateful to Thomas Powell,Andrei Sipo and an anonymous referee for commentingon earlier versions of this paper which led to an improved presentation.2Studies in Logic,Vol.16,No.3(2023)“unwinding”program and which has the area of nonlinear analysis as its prominentfield for applications(see 70,72 for surveys).As we will see,the importance ofKreisels insights for the development of the proof mining paradigm can hardly beoverstated.2The Shift of Emphasis in Hilberts Program2.1Kreisels quest for applications of proof theoryBehind Kreisels quest for unwinding mathematically useful but hidden contentby the logical analysis of proofs is his general conviction thatthevalidityofatheorem,infact,thevalidityofaproof,isonlyasmallpart of the significant knowledge contained in the proof:it just happensto be the part which is most easily put into words.(101,p.164)Kreisel did not reject the significance of foundational research in principle.In fact,he writes:Nobody denies that,at various periods of history,people experimented with dubious principles It cannot be repeated too often that therecan be and have been realistic doubts In particular,certain precursorsof the concepts mentioned above(sets,lawless sequences)were indeeddubious in a realistic sense,and their foundational analyses were by nomeans superfluous.(97,pp.171172)However,on the same pages of that paper he states:1.There are no realistic doubts concerning the concepts used in current mathematical practice and concerning their basic properties formulated in the usual axiomatic systems.2.Thereis,inmyopinion,nohintofevidencefortheassumptionthatany analysis of the usual concepts or of their basic properties could improve in any general way on the mere recognition of their validity.(97,pp.171172)Beginningintheearly50s,healreadyaimedatclearmathematicalusesofprooftheoretic methods for which he expected relevant success.In 90,91,92,Kreiselstressed the mathematical significance of the actual proof reductions achieved in thecontext of1.Gentzens consistency proof for Peano Arithmetic PA based on cutreductionsandsubsequentlybyAckermann(1)usingHilbertssubstitutionmethodand2.Herbrandsreductionofpredicatelogic(resp.opentheoriesT)topropositionallogic(resp.the quantifierfree fragment of T)by Herbrands theorem.Ulrich Kohlenbach/Kreisels“Shift of Emphasis”and Contemporary Proof Mining3The first correct syntactic proof of Herbrands theorem had also been obtainedby the substitution method in 48.Later,e.g.,in 95 he also discusses the potential of Gdels functional interpretation(used by Gdel again in the context of a consistency proof for PA)to unwindproofswhileinhisownworkinthisdirectionhealwaysgavepreferencetoHerbrandstheoremandthesubstitutionmethod(notethoughthatfunctionalinterpretationmaybe viewed as a modular“high level”generalization of Herbrands theorem,see 29,38,129).With regard to all these different methods which have been developed in thecourse of the consistency program,Kreisels novel approach was todescribe pragmatic uses of“consistency”proofs independent of(dubious)epistemological claims.(98,p.113)Already in 1958,Kreisel states on a similar note:There is a different general program which does not seem to sufferthe defects of the consistency program:To determine the constructive(recursive)content or the constructive equivalent of the nonconstructiveconcepts and theorems used in mathematics,particularly arithmetic andanalysis.(92,p.155)At the same time he stresses already in the opening sentence of 92 that the methodsdeveloped in the course of the consistency program can be used for this:The principal aim of the present paper is to sketch some mathematical applications of the work of the Hilbert school in the foundations ofmathematics.(92,p.155)2.2Examples and instances of Kreisels questOne such use,made already in 91,is to characterize the provably total functions(andin the presence of function parametersalso the provably total type2functionals)of PA as the(0)recursive ones using Ackermanns method.Inthe course of this,Kreisel developed his socalled nocounterexample interpretation(n.c.i)and showed how this could be used to unwind the computational content ofproofs of theorems in mathematics.As a firstpedagogical example,he treats theCauchy property of bounded monotone sequences of reals to extract a bound on then.c.i.of this statement.In 132,Tao rediscovered the n.c.i.in special cases andincidentally treated exactly the same example where he uses the term“metastability”instead of“n.c.i.”.In fact,from Kreisels analysis one immediately obtains Taos“finite convergence principle”which can be seen as a constructive and even finitaryequivalent to the usual monotone convergence principle.This is also true for the4Studies in Logic,Vol.16,No.3(2023)advanced quantitative metastability results that have been obtained by proof miningin the areas of ergodic theory,fixed point theory and convex optimization,see 70,Section 2.6,for a discussion of this point.Sometimes,the metastable version is“enriched”,i.e.,formulated with additional bounding data.The latter guarantee that thefinitary version not only(classically)implies back the convergence of the sequencein question but also that the limit has the properties stated in the original theorem.Werefer the interested reader to,e.g.,Remarks 3.6 and 3.11 in 85.Aftertreatingthemonotoneconvergenceprinciple,Kreiselshowshowonecanusing the n.c.i.“give a systematic discussion”(91,p.52)on why from Littlewoods proof that there are infinitely many sign changes of(n)li(n)it is possibleto extract a bound on such a sign change n.In 90,91,the n.c.i.is presented as an instance of the concept of an interpretation of a formal system(in the situation at hand that being PA).Kreisel lists fourconditions to be satisfied by such an interpretation of which the condition()impliesthat the interpretation should respect the modus ponens rule in a certain technicalsense.However,as discussed in detail in 59,the n.c.i.respects modus ponens onlyif one uses the full class of(0)recursive functionals.By contrast,while forthe fragment PAn+1of Peano arithmetic with 0n+1induction only,the n.c.i.interpretation can be solved by(0.Another type of generalization was recently obtained in 75 where resultson the proximal point algorithm PPA and its Halperntype variant HPPA could beeasily generalized on the level of“mined”proofs obtained in the setting of monotoneoperators to operators which are allowed to be nonmonotone in a controlled way(socalled comonotone operators,see 10)since the property of monotonicity was onlyusedinsomeapproximateway.Finally,theminingofaproofinthecontextofpursuitevasion games in 83 made it possible to eliminate a compactness assumption whichwas crucially used in the original proof.Yet another generalization of a given proofon the level of the finitary analysis of an original proof can be found in 24 where aprevious miningof a strong convergenceproofin the context of Hilbert spaces,whichproceeded via bypassing a sequential weak compactness argument,was generalizedto the setting of CAT(0)spaces where even the qualitative strong convergence resultwas new.5Purity of Methods and Other Logical IdealsLegalistically,Gdels papers only settle questions about the possibilityofpurityofmethod.Butinspectionoftheargumentssuggestsquitestrongly that the whole ideal of purity of method is suspect,even when itcan be achieved.”(101,p.164)5.1Introduction:purity of methods and computational costsKreisel repeatedly criticized the logical ideal of“Methodenreinheit”(“purityof method”)as a central component in Hilberts foundational program.WhileasKreiselarguesin101Gdelscompletenesstheoremstatesthatinfirstorderlogic,purity of method is achievable in principle,Gdels incompleteness theorem is presented by Kreisel to have established the opposite for number theory.As(the prooftheoretic form of)Herbrands theorem and subsequently Gentzens Hauptsatz show,to establish a logic validity one not only does not have to use tools outside the logicalcalculus but one can even avoid the use of lemmas(“direct proofs”).The latter,however,comes at the price of a nonelementary increase in the size of the proof and theloss of a conceptual understanding of a proof.For number theory(and other parts ofcore mathematics),in practice,the Gdel incompleteness phenomenon almost neveroccurs and soin principleone can also provide“pure”proofs.But as indicated inthe citation from Kreisel at the beginning of this section,it is problematic to strive forpure proofs as a general ideal since what is lost isknowledge of relations between the objects referred to in the theorem stated and other things in short,the kind of knowledge obtained byUlrich Kohlenbach/Kreisels“Shift of Emphasis”and Contemporary Proof Mining23looking at those objects from a broader point of view.In the case of theprime number theorem,by looking at the natural numbers as embeddedin the complex plane.(103,pp.7475)Now,while methods such as substitution,Herbrandanalyses and cutelimination,which have a close connection to the quest for direct“pure”proofs,do play amajorrolealsoinKreiselsunwindingprogram,theemphasisinthelatterasalreadyindicated in Section 2is quite different,namely on extracting witnessing data forstatements rather than on verifying these data by pure methods.For functionalinterpretations,the primary techniques in contemporary proof mining,the distinctionbetween these different goals is even more apparent as these interpretations clearlydistinguish between them.5.2A representative case study:weak Knigs lemmaAs an early example,let us recall the treatment of WKLbased proofs by thecombination of functional interpretation and majorization(subsequently phrased as“monotone functional interpretation”)as developed in 52,53 and applied to proofsin approximation theory in 52,54,55:WKL is first rewritten as a sentence of theform considered already in Section 2(with =1,=0 and s(x)=11).Consider now a proof relative to extensional Peano arithmetic over all finite typesEPAEPA+WKL f1k0Bqf(f,k)withquantifierfreeBqf(containingonlyf,xfree).Byeliminationofextensionality,one first reduces things the weakly extensional setting of WEPA(needed to applythefunctionalinterpretation).Themonotonefunctionalinterpretation(combinedwithnegative translation)now asks for a majorant for the Skolemized form 11111x1,z0Aqf(x,(x),z)()of,whichusing the truth of()is simply given by 111,to compute a boundand so(by bounded search ordue to monotonicityimmediately)to produce a witnessing term tf Bqf(f,t(f)for the conclusion provably in WEHA+(),i.e.,using a uniform version UWKLeven of WKL.Instead of focusing on the extraction of t one can also use this approach to eliminate WKL from the original proof:by the deduction theorem(whichapplies to EPAbut not to WEPA)one obtains(using subsequently eliminationofextensionality)WEPA WKL f1k0Bqf(f,k)24Studies in Logic,Vol.16,No.3(2023)and soWEPA 1f(x1,z0Aqf(x,(x),z)k0Bqf(f,k).The monotone functional interpretation can now be used to extract a uniform bounds(f)on“z”withWEHA 1f(x1z 0s(f)Aqf(x,(x),z)k0Bqf(f,k).Since one can construct(uniformly in z)a z 1 such thatWEHA x1z0 z z Aqf(x,z(x),z),this givesWEHA f1k0Bqf(f,k).One now can use either functional interpretation or modified realizability to extract awitnessing term t.5.3Conceptual discussionOf course,the elimination of WKL via the extraction of s and the extraction oft are closely related and in some cases may happen almost simultaneously.But ingeneral,experience in proof mining shows that it is usually very helpful to focus onthe extraction of t and to freely use WKL and even UWKL for its verification.Inpractice,moreover,proofs will not use WKL as such but specific theorems T(e.g.,in the case of Chebycheff approximation the fact that there is a best approximatingpolynomial whichby the Chebycheff alternation theoremhas an alternant)whichcan directly be seen to have the form so that there is not even the need to prove Tfrom WKL(and then to eliminate WKL from the proof).Even when dealing with nonstandard axioms of the form as mentioned inSection 2(e.g.,the axioms F and FXin 56 and 65 which are not true in therespective full settheoretic models S,S,X)there is(modulo some technicalitiesrelated to the failure of the deduction theorem)the possibility for a prooftheoreticelimination of these axioms from proofs(of suitable classes of theorems A)but thereis no need to carry this out:one can simply reason in Bezems model M(resp.itsextension M,X)which satisfies F(resp.FX)to get the validity of the extractedbound in Mand from there(using mild type restrictions in A)in S.As indicated above,in many cases,by additional prooftheoretic arguments,onecan actually guarantee that a constructive verification of the extracted term can inprinciple be achieved but even when one might be interested in this due to foundational