Cut Elimination for a Logic with Definitions and Induction Raymond McDowell

Raymond Mcdowell

Description

Niveau: Supérieur

• dissertation

Cut-Elimination for a Logic with Definitions and Induction Raymond McDowell Department of Computer Science Widener University Chester, PA 19013 USA Dale Miller Department of Computer Science and Engineering 200 Pond Laboratory The Pennsylvania State University University Park, PA 16802 USA May 15, 1998 Abstract In order to reason about specifications of computations that are given via the proof search or logic programming paradigm one needs to have at least some forms of induction and some principle for reasoning about the ways in which terms are built and the ways in which computa- tions can progress. The literature contains many approaches to formally adding these reasoning principles with logic specifications. We choose an approach based on the sequent calculus and design an intuitionistic logic FO?∆IN that includes natural number induction and a notion of definition. We have detailed elsewhere that this logic has a number of applications. In this paper we prove the cut-elimination theorem for FO?∆IN, adapting a technique due to Tait and Martin-Lof. This cut-elimination proof is technically interesting and significantly extends previous results of this kind. 1 Introduction As one attempts to prove a given sequent by placing above it an inference rule, zero or more unproven sequents will arise for the premise of the inference rule and these sequents will, in general, involve some different formulas than the conclusion sequent. Such changes in sequents during the search for a proof have been used to provide a rich and flexible framework for the specification of a wide range of computations.

• order abstract


• order quantification


• quantification over


• nt ?


• logic specifications


• intuitionistic logic


• higher-order abstract

Sujets

• Dissertation
• McDowell
• Intuitionistic logic

Informations

• Publié par: profil-nechor-2012
• Nombre de lectures: 11
• Langue: English

Extrait

Cut-EliminationforaLogicwithDefinitionsandInduction RaymondMcDowell DepartmentofComputerScience WidenerUniversity Chester,PA19013USA DaleMiller DepartmentofComputerScienceandEngineering 200PondLaboratory ThePennsylvaniaStateUniversity UniversityPark,PA16802USA May15,1998 Abstract Inordertoreasonaboutspecificationsofcomputationsthataregivenviatheproofsearch orlogicprogrammingparadigmoneneedstohaveatleastsomeformsofinductionandsome principleforreasoningaboutthewaysinwhichtermsarebuiltandthewaysinwhichcomputa- tionscanprogress.Theliteraturecontainsmanyapproachestoformallyaddingthesereasoning principleswithlogicspecifications.Wechooseanapproachbasedonthesequentcalculusand designanintuitionisticlogicFOλ ΔIN thatincludesnaturalnumberinductionandanotionof definition.Wehavedetailedelsewherethatthislogichasanumberofapplications.Inthis paperweprovethecut-eliminationtheoremforFOλ ΔIN ,adaptingatechniqueduetoTait andMartin-Lo¨f.Thiscut-eliminationproofistechnicallyinterestingandsignificantlyextends previousresultsofthiskind. 1Introduction Asoneattemptstoproveagivensequentbyplacingaboveitaninferencerule,zeroormore unprovensequentswillariseforthepremiseoftheinferenceruleandthesesequentswill,ingeneral, involvesomedifferentformulasthantheconclusionsequent.Suchchangesinsequentsduringthe searchforaproofhavebeenusedtoprovidearichandflexibleframeworkforthespecificationof awiderangeofcomputations.Ofcourse,tomakeproofsearchresembleacomputationalprocess, thecutruleneedstobeavoided;thatis,whenattemptingtomodelacomputationbyconstructing aproof,itseemssensiblenottoobligethesearchtoalsosearchforlemmastoestablish.Thesearch forlemmasispartofthecreativeactivityofmathematicianswhentheylookforproofsanddoesnot seempartofthenotionofmechanicalcomputation.Thecut-eliminationtheorem,whenavailable, couldbeusedtoarguethatthesearchforcut-freeproofsisacompleteproofprocedure.The logicprogrammingparadigmcanbedefined,atleastabstractly,usingthisnotionofproofsearch, althoughafurtherrestrictiononthesearchofproofsisoftenmade.Inparticular,thenotionof 1

“goal-directedsearch”thatseemstobeanaturalaspectofthelogicprogrammingparadigmhas beenformulatedusingthetechnicalnotionofuniformproof[18,17].Toretaincompletenessof uniformproofs,restrictionsonlogicalformulasneedtomaintained.Forexample,completenessof uniformproofscanbeachievedinclassicallogicbyrestrictingtoHornclauses[19];inintuitionistic logicbyrestrictingtohereditaryHarropformulas[18];andinlinearlogicbychoosingtheproper logicalconnectives[1,17]. Therearenumerousexamplesofspecifyingcomputationswithintheselogicsandwithusing meta-theoreticpropertiesofthoselogicstoinferpropertiesofcomputations.Weonlymentiona fewoftheseexampleshere.Intuitionisticlogichasbeenusedtospecifyboththedynamicandstatic semanticsoffunctionalprogramminglanguages[10],andtheoremsthatrelatethesetwosemantics (suchassubjectreductionortypepreservation)arerenderedassimpleconsequencesoftheproof theoryofintuitionisticlogic[14].In[17],variouslinearlogicencodingsofsimpleobjectswith statearegivenandprovedequivalentwithinlinearlogic.Alsointhatpaper,asmallprogramming languagewithreferencesisspecified,andtechniquesforprovingtheequivalenceoftwoprograms aregivenbasedonresolutionwithinlinearlogic.In[2],Chirimarprovidestwospecificationsofthe operationalsemanticsoftheDLXRISCprocessor[20],onecapturingitssequential,machinecode semanticsandtheothercapturingitsconcurrent,pipe-linedsemantics.Usingsimplepropertiesof proofsinlinearlogic,heisabletoformallyshowtheequivalenceofthosetwospecifications. MovingfromtheclassicaltheoryofHornclauses(thelogicalfoundationsofProlog)toallof linearlogic(asintheForumspecificationlanguage[17])greatlyincreasestheexpressivepowerof thelogicprogrammingparadigm.WhileHornclausesare,ofcourse,powerfulenoughtospecifyall computations,suchspecificationsneedtorepresentmostofthedynamicsofacomputationwithin atomicformulas,thatis,withinthenon-logicallayerofthelanguage.Asaresult,deepproperties oftheambientlogic,suchascut-elimination,areofonlylimitedusewhenreasoningaboutHorn clausespecificationssincesuchpropertiesonlysupplymeaningforthelogicalconstants.Asmore expressivelogicsareused,moredynamicsofacomputationcanbecapturedbyvariousaspects ofthelogic,andthisincreasesthelikelihoodthatpropertiesofthelogiccanbeusedtoderive propertiesofthespecifiedcomputations. Thereisadifference,however,betweenspecifyingacomputationandreasoningaboutacom- putation,and,inparticular,reasoningaboutcomputationoftenrequiresinductionandsomeway toconsideringallpossiblepathsthatagivencomputationcouldproceedoragivenobjectcould havebeenconstructed.Intheliterature,therehavebeenvariousapproachestoprovidingforthese missingfeatures.Withintypetheory,forexample,inductionoverdatastructuresandoverproofs canbeusedforreasoningaboutcomputations[21].Withinlogicprogramming,therearevarious waystoturntheclosedworldassumptionintoaproofprinciple,suchasSLDNF[4].Inthispa- per,weconsideranotherapproachthatintroducesnewinferencerulesintothesequentcalculusof intuitionisticlogic.Inparticular,weaddtothesequentcalculusaruleforinductiononnatural numbersandinferencerulesfortreatinglogicspecificationsasdefinitionsinsteadofastheories. OurapproachtodefinitionsfollowslinesdevelopedbySchroeder-Heister[25],Eriksson[5],Girard [9],andSta¨rk[28]. Ourneedsforreasoningaboutspecifications,however,forcedustodevelopasingleextension tointuitionisticlogic,calledFOλ ΔIN (pronounced“fold-n”),thatgoesbeyondthelogicsstudiedin previousworks.Inparticular,weneededonelogicthatallowedfornotonlyinductionanddefinitions butalsoforhigher-orderquantification(butnotpredicatequantification)sincewewishedtotreat higher-orderabstractsyntax[23].Whendesigninganewsequentcalculustobeusedforreasoning, 2

itisimportanttoestablishacut-eliminationtheoremsincethisoneresultcanbeusedtoshow theconsistencyofthelogicaswellasthattheconsequencerelationisclosedundermodusponens. ThekeyfeaturesofFOλ ΔIN (induction,definitions,andhigher-orderquantification)interactin complicatedways,sopreviouscut-eliminationproofsforlogicswiththesefeaturesinisolationdo notcarryovertothisnewsystem.Thebulkofthispaperisapresentationofaproofofcut- eliminationforFOλ ΔIN . Thepaperisorganizedasfollows.Inthenextsection,webrieflydescribesomeusesthat havebeenmadeofFOλ ΔIN .Insection3weintroducethelogicandsomeofitsbasicproperties. WeproceedinSection4togiveanoverviewofthecut-eliminationproof.Section5specifiesthe reductionrulesthatwillbeusedtoeliminateapplicationsofthecutrule.Thisisfollowedby asectionwhichprovidessomeauxiliarydefinitionsandtheirproperties.Section7containsthe proofofcut-elimination.Weconcludewithabriefcomparisonofourworkwithrelatedworkof Martin-Lo¨fandSchroeder-Heister. 2ApplicationsofFOλ ΔIN OneuseofFOλ ΔIN hasbeentoreasonaboutHornclauseprograms.Forexample,Hornclauses canbeusedtospecifyapredicatethatrelatesalisttoitslengthandanotherpredicatethatrelates twolistsiftheyarepermutationsofeachother.ItisaneasymattertogiveaproofinFOλ ΔIN that iftwolistsarepermutationsofeachother,thenthosetwolistshavethesamelength[13,Chapter 2].ManysimilartheoremscanbefoundthroughoutMcDowell’sdissertation[13]. Asweshallsee,theintegrationofdefinitionsintosequentcalculusmakesitpossibletoperform acaseanalysisonpossiblewaysthataspecifiedcomputationcanprogress.Ifexploitedproperly, itispossibletocapturenotionssuchassimulationandbisimulationbetweentwoprocesses.The paper[16]showshowthiscanbeaccomplishedinabstracttransitionsystemsandCCS. AfinalareawhereFOλ ΔIN hasbeenusedtoreasonaboutspecificationsisintheareaoflogical frameworksandhigher-orderabstractsyntax.Logicalframeworkshavebeensuccessfullyusedto givehigh-level,modular,andformalspecificationsofmanyimportantjudgmentsintheareaof programminglanguagesandinferencesystems.Thesejudgments,suchas“thetermMdenotes aprogram”,“theprogramMevaluatestothevalueV”,and“theprogramMhastypeT”,are representedbypredicatesinthespecificationlogicorbytypesinadependenttypecalculus.One oftheadvantagesofsuchformalspecificationsisthattheyallowlogicalandmathematicalanalyses tobeusedtoprovepropertiesaboutthespecifiedsystems.Giventhespecificationofevaluation forafunctionalprogramminglanguage,forexample,wemaywishtoprovethatthelanguageis deterministicorthatevaluationpreservestypes. Onechallengeinreasoningaboutsuchspecificationscentersontheuseofhigher-orderabstract syntax,anelegantanddeclarativeencodingofabstractionandsubstitution[23].Withmostap- proachestosyntacticrepresentation,thedetailsofvariablebindingandsubstitutionmustbecare- fullyaddressedthroughoutaspecification,andtheoremsaboutsubstitutionandboundvariables candominatethesystemanalyses.Withhigher-orderabstractsyntax,ontheotherhand,these featuresarespecifiedconciselyandtheirbasicpropertiesfollowimmediatelyfromthespecification logic.However,reasoningwithinalogicalframeworkaboutsystemsrepresentedinhigher-order abstractsyntaxhasbeendifficultsincethelogicsthatsupportthisnotionofsyntaxdonotprovide facilitiesforthefundamentaloperationsofcaseanalysisandinduction.Moreover,higher-order abstractsyntaxleadstotypesandrecursivedefinitionsthatdonotgiverisetomonotoneinductive 3

operators,makinginductiveprinciplesdifficulttofind.In[14]theauthorshaveshownthatthese difficultiescanbeovercomewithinFOλ ΔIN .See[13,14]formoreonhowFOλ ΔIN canbeusedas ameta-logicforanintuitionisticandlinearlogicalframework. ThePiderivationeditorofEriksson[6]wasdesignedforthefinitarycalculusofpartialinductive definitions[5].BecauseofFOλ ΔIN ’scloserelationshipwiththefinitarycalculusofpartialinductive definitions,thePieditorcanbeusedtoconstructFOλ ΔIN derivations.Themanyexamplesof specificationsandproofsinFOλ ΔIN reportedin[13,14]wereconstructedusingthiseditor. Dependenttypedλ-calculihavebeenusedtospecifycomputationsinwaysanalogoustothe logicprogrammingsettingpresentedhere[22].Schu¨rmannandPfenning[26]presentedameta-logic forsuchadependenttypedλ-termsthatcanbeusedtoreasonabouthigher-orderdeductionsin wayssimilartousesofFOλ ΔIN [14]. 3TheLogicFOλ ΔIN ThebasiclogicisanintuitionisticversionofasubsetofChurch’sSimpleTheoryofTypes[3]in whichmeta-levelformulaswillbegiventhetypeo.Thelogicalconnectivesare⊥,>,∧,∨,⊃,∀ τ , and∃ τ .Thequantificationtypesτ(andthusthetypesofvariables)arerestrictedtonotcontaino. ThusFOλ ΔIN supportsquantificationoverhigher-order(non-predicate)types,acrucialfeaturefor higher-orderabstractsyntax,buthasafirst-orderprooftheorysincethereisnoquantificationover predicatetypes.WewillusesequentsoftheformΓ−→B,whereΓisafinitemultisetofformulas andBisasingleformula.ThebasicinferencerulesforthelogicareshowninTable1.Inthe∀R and∃Lrules,yisaneigenvariablethatisnotfreeinthelowersequentoftherule.Themulticut (mc)ruleisageneralizationofcutduetoSlaney[27],andisusedtosimplifythepresentationof thecut-eliminationproof. Weintroducethenaturalnumbersviatheconstantsz:ntforzeroands:nt→ntforsuccessor andthepredicatenat:nt→o.Therightandleftrulesforthisnewpredicateare Γ−→natI Γ−→natz natR Γ−→nat(sI) natR −→BzBj−→B(sj)BI,Γ−→C natI,Γ−→C natL . Intheleftrule,thepredicateB:nt→orepresentsthepropertythatisprovedbyinduction,and jisaneigenvariablethatisnotfreeinB.Thethirdpremise V ofthatinferencerulewitnessesthe factthat,ingeneral,Bwillexpressapropertystrongerthan(Γ)⊃C. BecausetheinductionpredicateBinthenatLruleisnotnecessarilyasubformulaoftheformula CoranyformulainΓ,thesubformulapropertydoesnotholdforFOλ ΔIN .Infact,wecanderive thefollowinginferencerulefromtheinductionrule: −→BB,Γ−→C natI,Γ−→C. Thisderivedruleresemblesthecutrulebutrequiresanatassumption.AlthoughFOλ ΔIN does nothavethesubformulaproperty,thecut-eliminationtheoremstillprovidesastrongbasisfor reasoningaboutproofsinFOλ ΔIN [13,14,16].Infact,theformulationofthenatLruleandthe failureofthesubformulapropertyreflectthefactthatinactualmathematicalpractice,findingthe 4

Table1:InferencerulesforthecoreofFOλ ΔIN ⊥,Γ−→B ⊥L Γ−→> >R B,Γ−→DC,Γ−→D B[t/x],Γ−→C B∧C,Γ−→D ∧L B∧C,Γ−→D ∧L ∀x.B,Γ−→C ∀L Γ−→BΓ−→C ∧R Γ−→B[y/x] ∀R Γ−→B∧CΓ−→∀x.B B,Γ−→DC,Γ−→D ∨L B[y/x],Γ−→C ∃L B∨C,Γ−→D∃x.B,Γ−→C Γ−→B[t/x] Γ− Γ → −→ B∨ B C ∨R Γ− Γ → −→ B C ∨C ∨R Γ−→∃x.B ∃R Γ−→BC,Γ−→DB,Γ−→C B⊃C,Γ−→D ⊃L Γ−→B⊃C ⊃R A,Γ−→A init,whereAisatomic B, B, B Γ ,Γ − − → → C C cL Δ 1 −→B 1 ∙∙∙Δ n −→B n B 1 ,...,B n ,Γ−→C mc,wheren≥0 Δ 1 ,...,Δ n ,Γ−→C 5

properinductionhypothesisrequiresinsightandcreativity;theyarenotsimplyrearrangementsof thesubformulasoftheconclusion.Asaresult,anyimplementationofFOλ ΔIN willnecessarilybe interactive,atleastfortheinventionofmanyinductionhypotheses. 4 Adefinitionalclauseiswritten∀x¯[pt ¯ =B],wherepisapredicateconstant,everyfreevariable oftheformulaBisalsofreeinatleastoneterminthelistt ¯ ofterms,andallvariablesfreeint ¯ are containedinthelistx¯ofvariables.Sinceallfreevariablesinpt ¯ andBareuniversallyquantified, weoftenleavethesequantifiersimplicitwhendisplayingdefinitionalclauses.Theatomicformula pt ¯ iscalledtheheadoftheclause,andtheformulaBiscalledthebody.Thesymbol= 4 isused simplytoindicateadefinitionalclause:itisnotalogicalconnective.Adefinitionisa(perhaps infinite)setofdefinitionalclauses.Thesamepredicatemayoccurintheheadofmultipleclauses ofadefinition:itisbesttothinkofadefinitionasamutuallyrecursivedefinitionofthepredicates intheheadsoftheclauses. DefinitionsareemployedinFOλ ΔIN vialeftandrightintroductionrulesforatomicformulas. Ifweimposenorestrictionsondefinitions,thecut-eliminationtheoremdoesnothold[24].Two differentapproacheshavebeentakentoretaintheadmissibilityofcut.First,ifthestructuralrule ofcontractionisremovedorrestricted(asitisinlinearlogic,forexample),cut-eliminationcanbe established[9,25].Anotherapproach,moreappropriateforuseheresincewewishtoworkwithin anintuitionisticsetting,istorestricttheoccurrencesofimplicationswithinthebodyofdefinitions. In[25],Schroeder-Heisterprovedthecut-eliminationtheoremforanintuitionisticlogicinwhich noimplicationsareallowedwithindefinitions.Hereweshallallowimplicationsinthebodyof definitionsiftheyaresuitablystratified.Towardthatendweassumethateachpredicatesymbol pinthelanguagehasassociatedwithitanaturalnumberlvl(p),thelevelofthepredicate.The followingdefinitionextendsthenotionofleveltoformulasandderivations. Definition1GivenaformulaB,itslevellvl(B)isdefinedasfollows: 1.lvl(pt ¯ )=lvl(p) 2.lvl(⊥)=lvl(>)=0 3.lvl(B∧C)=lvl(B∨C)=max(lvl(B),lvl(C)) 4.lvl(B⊃C)=max(lvl(B)+1,lvl(C)) 5.lvl(∀x.B)=lvl(∃x.B)=lvl(B). GivenaderivationΠofΓ−→B,lvl(Π)=lvl(B). 4 Weshallnowrequirethatforeverydefinitionalclause∀x¯[pt ¯ =B],lvl(B)≤lvl(p). ThelogicFOλ ΔIN hasusesdefinitionsinleftandright-introductionrulesforatoms;thefollowing relationwillbeusefulfordescribingthoseinferencerules. Definition2Letthefour-placerelationdfn(ρ,A,σ,B)bedefinedtoholdfortheformulasAand Bandthesubstitutionsρandσifthereisaclause∀x¯[A 0 = 4 B]inthegivendefinitionsuchthat Aρ=A 0 σ. Therightandleftrulesforatomsare Γ−→Bθ defR,wheredfn(²,A,θ,B) A→−Γ 6

{Bσ,Γρ−→Cρ|dfn(ρ,A,σ,B)} A,Γ−→C defL , where²istheemptysubstitutionandtheboundvariablesx¯inthedefinitionalclausesarechosen tobedistinctfromthevariablesfreeinthelowersequentoftherule.Specifyingasetofsequents asthepremiseshouldbeunderstoodtomeanthateachsequentinthesetisapremiseofthe 4 rule.Therightrulecorrespondstothelogicprogrammingnotionofbackchainingifwethinkof= indefinitionalclausesasreverseimplication.Theleftruleissimilartodefinitionalreflection[25] (nottobeconfusedwithanothernotionofreflectionoftenconsideredbetweenameta-logicand object-logic)andtoaninferenceruleusedbyGirardinhisnoteonfixedpoints[9].Noticethatin thedefLrule,thefreevariablesoftheconclusioncanbeinstantiatedinthepremises. ThenumberofpremisesofthedefLrulemaybezeroormaybeinfinite.IftheformulaAdoes notunifywiththeheadofanydefinitionalclause,thenthenumberofpremiseswillbezero.Inthis case,Aisanunprovableformulalogicallyequivalentto⊥,anddefLcorrespondstothe⊥Lrule. IftheformulaAdoesunifywiththeheadofadefinitionalclause,thenumberofpremisescouldbe infinite,sincethedomainsofthesubstitutionsρandσmayincludevariablesthatarenotfreeinA andB.Ingeneralwewishtoworkwithinferenceruleswithafinitenumberofpremises.Thiscan beachievedbyrestrictingdefinitionstohaveonlyafinitenumberofclausesandtorestricttheuse ofdefLruletothoseformulasAsuchthatforeverydefinitionalclausethereisafinite,complete setofunifiers(CSU)[11]ofAandtheheadoftheclause.Considerthefollowinginferenceruledue toEriksson[5] {Bθ,Γθ−→Cθ|θ∈CSU(A,A 0 )forsomeclause∀x¯[A 0 = 4 B]} A,Γ−→C defL CSU , wherethevariablesx¯arechosentobedistinctfromthevariablesfreeinthelowersequentofthe rule.WhentheCSUsanddefinitionarefinite,thisrulewillhaveafinitenumberofpremises. Noticethatinfirst-orderlogics,aCSUwillhaveatmostonemember,namelythemostgeneral unifier(MGU). Proposition3TherulesdefLanddefL CSU areinteradmissible,thatis,ifFOλ ΔIN isformulated witheitherdefLordefL CSU ,theotherruleisadmissibleinthatformulation. ProofGiventhesetofderivations ¾½ B,θ Π , Bθ,Γθ−→Cθ θ∈CSU(A,A 0 )forsomeclause∀x¯[A 0 = 4 B] wecan 4 constructaderivationofA,Γ−→CusingdefLasfollows.Foranydefinitionalclause ∀x¯[A 0 =B]andsubstitutionsρandσsuchthatAρ=A 0 σ,thesubstitution ( σ(y)ify∈FV(A 0 ) ρ σ (y)= ρ(y)otherwise willbeaunifierofAandA 0 .Thusforsomeθ∈CSU(A,A 0 )thereisasubstitutionθ 0 suchthat ρ σ isθ◦θ 0 .(NoticethatcompositionofsubstitutionisdefinedsothatA(θ◦θ 0 )=(Aθ)θ 0 .)Wecan thususeΠ θ,B θ 0 asthepremisederivationofBσ,Γρ−→CρfordefL.(Wewillformallydefinewhat itmeanstoapplyasubstitutiontoaderivationinDefinition5.Fornowitisenoughtoknowthat 7

ityieldsaderivationwhoseendsequentisobtainedbyapplyingthesubstitutiontotheendsequent oftheoriginalderivation.) Giventhesetofderivations ¾½ Π ρ,σ,B , Bσ,Γρ−→Cρ dfn(ρ,A,σ,B) wecanconstructaderivationofA,Γ−→CusingdefL CSU asfollows.Foranydefinitionalclause ∀x¯[A 0 = 4 B]andsubstitutionθ∈CSU(A,A 0 ),dfn(θ,A,θ,B)holds.WecanthususeΠ θ,θ,B asthe premisederivationofBθ,Γθ−→CθfordefL. ObservethatseveraloftherulesofFOλ ΔIN mayhavevariablesthatarefreeinthepremisebut notintheconclusion:thisresultsfromtheeigenvariableyof∀Rand∃L,thetermtof∀Land ∃R,thecutformulasB 1 ,...,B n ofmc,theinductionpredicateBofnatL,andthesubstitutionsρ andσofdefL.Weviewthechoiceofsuchvariablesasarbitraryandidentifyallderivationsthat differonlyinthechoiceofvariablesthatarenotfreeinend-sequent. Wedefineanordinalmeasurewhichcorrespondstotheheightofaderivation: Definition4GivenaderivationΠwithpremisederivations{Π i } i ,themeasureht(Π)istheleast upperboundof{ht(Π i )+1} i . Substitutionsarefinitemapsfromvariablestoterms.Itiscommontoviewsubstitutionsas mapsfromtermstotermsbyapplyingthesubstitutiontoallfreevariablesofaterm.Wecanthen extendthemappinginturntoformulasandmultisetsbyapplyingittoeveryterminaformulaand everyformulainamultiset.Thefollowingdefinitionextendssubstitutionsyetagaintoapplyto derivations.Sinceweidentifyderivationsthatdifferonlyinthechoiceofvariablesthatarenotfree intheend-sequent,wewillassumethatsuchvariablesarechosentobedistinctfromthevariables inthedomainofthesubstitutionandfromthefreevariablesoftherangeofthesubstitution.Thus applyingasubstitutiontoaderivationwillonlyaffectthevariablesfreeintheend-sequent. Definition5IfΠisaderivationofΓ−→Candθisasubstitution,thenwedefinethederivation ΠθofΓθ−→Cθasfollows: 1.SupposeΠendswiththedefLrule ¾½ Π ρ,σ,B Bσ,Γ 0 ρ−→Cρ dfn(ρ,A,σ,B) A,Γ 0 −→C defL . Observethatifdfn(ρ 0 ,Aθ,σ 0 ,B)thendfn(θ◦ρ 0 ,A,σ 0 ,B).ThusΠθis ½¾ Π θ◦ρ 0 ,σ 0 ,B 0000 Bσ,Γθρ−→Cθρ dfn(ρ 0 ,Aθ,σ 0 ,B) Aθ,Γ 0 θ−→Cθ defL . 2.IfΠendswithanyotherruleandhaspremisederivationsΠ 1 ,...,Π n ,thenΠθalsoendswith thesameruleandhaspremisederivationsΠ 1 θ,...,Π n θ. Lemma6ForanysubstitutionθandderivationΠofΓ−→C,ΠθisaderivationofΓθ−→Cθ. 8

ProofThislemmastatesthatDefinition5iswell-constructed,andfollowsbyinductiononµ(Π). ObservethatifΠendswiththedefRrule 0 Γ− Π →Bσ Γ−→A defR , thendfn(²,A,σ,B),andsoitisalsotruethatdfn(²,Aθ,σ◦θ,B).Therefore 0 θΠ Γθ−→Bσθ defR Γθ−→Aθ isavalidderivation. Lemma7ForanyderivationΠandsubstitutionθ,ht(Π)≥ht(Πθ). ProofTheproofofthislemmaisasimpleinductiononht(Π).Themeasuresmaynotbeequal becausewhenthederivationsendwiththedefLrule,someofthepremisederivationsofΠmay notbeneededtoconstructthepremisederivationsofΠθ. Ourlogicdoesnotcontainaweakeningrule;insteadweallowextraassumptionsintheaxioms. Thefollowingdefinitionprovidesmeta-levelweakeningonderivations.Sinceweidentifyderivations thatdifferonlyinthechoiceofvariablesthatarenotfreeintheend-sequent,wewillassumethat suchvariablesarechosentobedistinctfromthefreevariablesoftheweakeningformulas. Definition8IfΠisaderivationofΓ−→CandΔisamultisetofformulas,thenwedefinethe derivationw(Δ,Π)ofΓ,Δ−→Casfollows: 1.IfΠendswiththedefLrule ¾½ Π ρ,σ,B Bσ,Γ 0 ρ−→Cρ A,Γ 0 −→C defL , thenw(Δ,Π)is ½¾ w(Δρ,Π ρ,σ,B ) Bσ,Γ 0 ρ,Δρ−→Cρ Lfed A,Γ 0 ,Δ−→C. 2.IfΠendswiththenatLrule Π 1 Π 2 Π 3 −→BzBj−→B(sj)BI,Γ−→C natL natI,Γ−→C, thenw(Δ,Π)is Π 1 Π 2 w(Δ,Π 3 ) −→BzBj−→B(sj)BI,Γ,Δ−→C natL natI,Γ,Δ−→C. 9

3.IfΠendswiththemcrule Π 1 Π n Π 0 Δ 1 −→B 1 ∙∙∙Δ n −→B n B 1 ,...,B n ,Γ−→C cm Δ 1 ,...,Δ n ,Γ−→C, thenw(Δ,Π)is Π 1 Π n w(Δ,Π 0 ) Δ 1 −→B 1 ∙∙∙Δ n −→B n B 1 ,...,B n ,Γ,Δ−→C cm Δ 1 ,...,Δ n ,Γ,Δ−→C. 4.IfΠendswithanyotherruleandhaspremisederivationsΠ 1 ,...,Π n ,thenw(Δ,Π)alsoends withthesameruleandhaspremisederivationsw(Δ,Π 1 ),...,w(Δ,Π n ). Thefollowinglemmascanbeprovedbyinductiononthemeasureofthegivenderivation. Lemma9ForanymultisetΔofformulasandderivationΠofΓ−→C,w(Δ,Π)isaderivation ofΓ,Δ−→C. Lemma10ForanyderivationΠandmultisetΔofformulas,ht(Π)=ht(w(Δ,Π)). Lemma11ForanyderivationΠ,multisetΔofformulas,andsubstitutionθ, w(Δ,Π)θandw(Δθ,Πθ) arethesamederivation. Lemma12ForanyderivationΠandmultisetsΔandΔ 0 offormulas, w(Δ,w(Δ 0 ,Π))andw(Δ∪Δ 0 ,Π) arethesamederivation. 4OverviewoftheCut-EliminationProof Gentzen’sclassicproofofcut-eliminationforfirst-orderlogic[7]usesaninductioninvolvingthe numberoflogicalconnectivesinthecutformula.Acutonacompoundformulaisreplacedby cutsonitssubformulas,whichnecessarilycontainalowernumberofconnectives.Forexample,the derivation Π 1 Π 2 Π 3 Δ−→B 1 Δ−→B 2 B 1 ,Γ−→C Δ−→B 1 ∧B 2 ∧R B 1 ∧B 2 ,Γ−→C ∧L cm Δ,Γ−→C isreducedto ΠΠ 31 Δ−→B 1 B 1 ,Γ−→C cm Δ,Γ−→C. 01

Bytheinductionhypothesis,thiscutonB 1 iseliminable,hencetheoriginalcutonB 1 ∧B 2 isalso eliminable.Infirst-orderlogic,whenthecutformulaisatomic,thecutcaneasilyberemovedby permutingthecutuptowardtheleavesoftheproof;eventuallyaninitialruleisreached,atwhich pointtheremovalofthecutistrivial. InFOλ ΔIN ,however,therulesfornaturalnumbersanddefinitionsactonatoms,sotheatomic caseisnotsimple.Consider,forexample,thederivation ¾½ Π 1 Π ρ,σ,D Δ−→Bθ defR Dσ,Γρ−→Cρ defL Δ−→AA,Γ−→C Δ,Γ−→C mc . TheobviousreductionforthisisacutbetweenΠ 1 andtheappropriatepremiseofthedefLrule; however,Bθisaformulaofarbitrarycomplexity,andsowillingeneralhaveagreaternumberof connectivesthantheatomA,whichhaszero.Thusadifferentinductionmeasureisneeded. Schroeder-Heisterprovescut-eliminationforseverallogicswithdefinitions[24,25]byincluding thenumberofusesofthedefLruleinthederivationaspartoftheinductionmeasure.However,the logicsheconsidersdonotcontaininduction;theinclusionofthenatRandnatLrulesinFOλ ΔIN complicatesthingsfurther.Thederivation Π 1 Π 2 Π 3 Π 4 Δ−→natI −→BzBj−→B(sj)B(sI),Γ−→C Δ−→nat(sI) natR nat(sI),Γ−→C natL cm Δ,Γ−→C canbereducedinanumberofways,butthereductionsareallvariationsofthederivation Π 2 Π 3 Π 3 [I/j] Π 1 −→BzBj−→B(sj)BI−→B(sI) Δ−→natInatI−→B(sI) natL Π 4 cm Δ−→B(sI)B(sI),Γ−→C cm Δ,Γ−→C. Here,thecutontheatomicformulanat(sI)isreplacedbytwocuts,oneontheatomnatIand theotherontheformulaB(sI).Itisnotclearwhatinductionmeasurecanbeusedhere.Forthe firstcut,theatomnatIcontainsnologicalconnectives,butthisistrueoftheoriginalcutformula nat(sI)aswell.ThenumberofnatRrulesintherightsubderivationofthecuthasgonedown byone,buttheduplicationofΠ 3 mightoffsetthis.Forthesecondcut,thecutformulaB(sI)is notrelatedatalltotheoriginalcutformula;itcertainlycanhavenofewerconnectivesthanthe atomnat(sI).Andthoughitsleftpremiseisshorterthantheleftpremiseoftheoriginalcut,it isunclearhowtheheightsoftherightpremisescompare. Itshouldbenoted,however,thatthecomplicatingfactorhereisnotthepresenceofaninduction rule,butouruseofthenatpredicateintheinductionrule.IfweremovethenatRrulesfromthe logicandreformulatetheinductionruletobe −→BzBj−→B(sj)BI,Γ−→C Γ−→C ind , 11