资源描述：
《SMM Applied Proof Theory Proof Interpretations and Their Use in Mathematics》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、SpringerMonographsinMathematicsU.KohlenbachAppliedProofTheory:ProofInterpretationsandTheirUseinMathematicsUlrichKohlenbachTechnischeUniversitätDarmstadtFBMathematikSchloßgartenstr.764289DarmstadtGermanykohlenbach@mathematik.tu-darmstadt.deISBN978-3-540-77532-4e-ISBN978-3-540-77533-
2、1DOI10.1007/978-3-540-77533-1SpringerMonographsinMathematicsISSN1439-7382LibraryofCongressControlNumber:2008920614MathematicsSubjectClassification(2000):03F03,03F10,03B30,41A10,41A52,47H9,47H10c2008Springer-VerlagBerlinHeidelbergThisworkissubjecttocopyright.Allrightsarereserved,whe
3、therthewholeorpartofthematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation,broadcasting,reproductiononmicrofilmorinanyotherway,andstorageindatabanks.DuplicationofthispublicationorpartsthereofispermittedonlyundertheprovisionsoftheGermanCop
4、yrightLawofSeptember9,1965,initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.ViolationsareliabletoprosecutionundertheGermanCopyrightLaw.Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply,evenintheabsenceofaspecificstate
5、ment,thatsuchnamesareexemptfromtherelevantprotectivelawsandregulationsandthereforefreeforgeneraluse.Coverdesign:WMXDesignGmbH,HeidelbergPrintedonacid-freepaper987654321springer.comForGabrieleandKatharinaPrefaceThisbookgivesanintroductiontoso-calledproofinterpretations,morespecifical
6、lyvariousformsofrealizabilityandfunctionalinterpretations,andtheiruseinmathe-matics.Whereasearliertreatmentsofthesetechniques(e.g.[366,266,122,369,7])emphasizefoundationalandlogicalissuesthefocusofthisbookisonapplicationsofthemethodstoextractneweffectiveinformationsuchascomputableu
7、niformboundsfromgiven(typicallyineffective)proofs.Thislineofresearch,whichhasitsrootsinG.Kreiselspioneeringworkonunwindingofproofsfromthe50s,hasinmorerecentyearsdevelopedintoafieldofmathematicallogicwhichhasbeencalled(suggestedbyD.Scott)proofmining.Theareaswhereproofminingbasedonpro
8、ofinterpretationshasbeenap
