La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

Cut Elimination for a Logic with Definitions and Induction Raymond McDowell

De
28 pages
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


Voir plus Voir moins

Vous aimerez aussi

Cut-EliminationforaLogicwithDefinitionsandInductionRaymondMcDowellDepartmentofComputerScienceWidenerUniversityChester,PA19013USADaleMillerDepartmentofComputerScienceandEngineering200PondLaboratoryThePennsylvaniaStateUniversityUniversityPark,PA16802USAMay15,1998AbstractInordertoreasonaboutspecificationsofcomputationsthataregivenviatheproofsearchorlogicprogrammingparadigmoneneedstohaveatleastsomeformsofinductionandsomeprincipleforreasoningaboutthewaysinwhichtermsarebuiltandthewaysinwhichcomputa-tionscanprogress.Theliteraturecontainsmanyapproachestoformallyaddingthesereasoningprincipleswithlogicspecifications.WechooseanapproachbasedonthesequentcalculusanddesignanintuitionisticlogicFOλΔINthatincludesnaturalnumberinductionandanotionofdefinition.Wehavedetailedelsewherethatthislogichasanumberofapplications.Inthispaperweprovethecut-eliminationtheoremforFOλΔIN,adaptingatechniqueduetoTaitandMartin-Lo¨f.Thiscut-eliminationproofistechnicallyinterestingandsignificantlyextendspreviousresultsofthiskind.1IntroductionAsoneattemptstoproveagivensequentbyplacingaboveitaninferencerule,zeroormoreunprovensequentswillariseforthepremiseoftheinferenceruleandthesesequentswill,ingeneral,involvesomedifferentformulasthantheconclusionsequent.Suchchangesinsequentsduringthesearchforaproofhavebeenusedtoprovidearichandflexibleframeworkforthespecificationofawiderangeofcomputations.Ofcourse,tomakeproofsearchresembleacomputationalprocess,thecutruleneedstobeavoided;thatis,whenattemptingtomodelacomputationbyconstructingaproof,itseemssensiblenottoobligethesearchtoalsosearchforlemmastoestablish.Thesearchforlemmasispartofthecreativeactivityofmathematicianswhentheylookforproofsanddoesnotseempartofthenotionofmechanicalcomputation.Thecut-eliminationtheorem,whenavailable,couldbeusedtoarguethatthesearchforcut-freeproofsisacompleteproofprocedure.Thelogicprogrammingparadigmcanbedefined,atleastabstractly,usingthisnotionofproofsearch,althoughafurtherrestrictiononthesearchofproofsisoftenmade.Inparticular,thenotionof1
“goal-directedsearch”thatseemstobeanaturalaspectofthelogicprogrammingparadigmhasbeenformulatedusingthetechnicalnotionofuniformproof[18,17].Toretaincompletenessofuniformproofs,restrictionsonlogicalformulasneedtomaintained.Forexample,completenessofuniformproofscanbeachievedinclassicallogicbyrestrictingtoHornclauses[19];inintuitionisticlogicbyrestrictingtohereditaryHarropformulas[18];andinlinearlogicbychoosingtheproperlogicalconnectives[1,17].Therearenumerousexamplesofspecifyingcomputationswithintheselogicsandwithusingmeta-theoreticpropertiesofthoselogicstoinferpropertiesofcomputations.Weonlymentionafewoftheseexampleshere.Intuitionisticlogichasbeenusedtospecifyboththedynamicandstaticsemanticsoffunctionalprogramminglanguages[10],andtheoremsthatrelatethesetwosemantics(suchassubjectreductionortypepreservation)arerenderedassimpleconsequencesoftheprooftheoryofintuitionisticlogic[14].In[17],variouslinearlogicencodingsofsimpleobjectswithstatearegivenandprovedequivalentwithinlinearlogic.Alsointhatpaper,asmallprogramminglanguagewithreferencesisspecified,andtechniquesforprovingtheequivalenceoftwoprogramsaregivenbasedonresolutionwithinlinearlogic.In[2],ChirimarprovidestwospecificationsoftheoperationalsemanticsoftheDLXRISCprocessor[20],onecapturingitssequential,machinecodesemanticsandtheothercapturingitsconcurrent,pipe-linedsemantics.Usingsimplepropertiesofproofsinlinearlogic,heisabletoformallyshowtheequivalenceofthosetwospecifications.MovingfromtheclassicaltheoryofHornclauses(thelogicalfoundationsofProlog)toalloflinearlogic(asintheForumspecificationlanguage[17])greatlyincreasestheexpressivepowerofthelogicprogrammingparadigm.WhileHornclausesare,ofcourse,powerfulenoughtospecifyallcomputations,suchspecificationsneedtorepresentmostofthedynamicsofacomputationwithinatomicformulas,thatis,withinthenon-logicallayerofthelanguage.Asaresult,deeppropertiesoftheambientlogic,suchascut-elimination,areofonlylimitedusewhenreasoningaboutHornclausespecificationssincesuchpropertiesonlysupplymeaningforthelogicalconstants.Asmoreexpressivelogicsareused,moredynamicsofacomputationcanbecapturedbyvariousaspectsofthelogic,andthisincreasesthelikelihoodthatpropertiesofthelogiccanbeusedtoderivepropertiesofthespecifiedcomputations.Thereisadifference,however,betweenspecifyingacomputationandreasoningaboutacom-putation,and,inparticular,reasoningaboutcomputationoftenrequiresinductionandsomewaytoconsideringallpossiblepathsthatagivencomputationcouldproceedoragivenobjectcouldhavebeenconstructed.Intheliterature,therehavebeenvariousapproachestoprovidingforthesemissingfeatures.Withintypetheory,forexample,inductionoverdatastructuresandoverproofscanbeusedforreasoningaboutcomputations[21].Withinlogicprogramming,therearevariouswaystoturntheclosedworldassumptionintoaproofprinciple,suchasSLDNF[4].Inthispa-per,weconsideranotherapproachthatintroducesnewinferencerulesintothesequentcalculusofintuitionisticlogic.Inparticular,weaddtothesequentcalculusaruleforinductiononnaturalnumbersandinferencerulesfortreatinglogicspecificationsasdefinitionsinsteadofastheories.OurapproachtodefinitionsfollowslinesdevelopedbySchroeder-Heister[25],Eriksson[5],Girard[9],andSta¨rk[28].Ourneedsforreasoningaboutspecifications,however,forcedustodevelopasingleextensiontointuitionisticlogic,calledFOλΔIN(pronounced“fold-n”),thatgoesbeyondthelogicsstudiedinpreviousworks.Inparticular,weneededonelogicthatallowedfornotonlyinductionanddefinitionsbutalsoforhigher-orderquantification(butnotpredicatequantification)sincewewishedtotreathigher-orderabstractsyntax[23].Whendesigninganewsequentcalculustobeusedforreasoning,2
itisimportanttoestablishacut-eliminationtheoremsincethisoneresultcanbeusedtoshowtheconsistencyofthelogicaswellasthattheconsequencerelationisclosedundermodusponens.ThekeyfeaturesofFOλΔIN(induction,definitions,andhigher-orderquantification)interactincomplicatedways,sopreviouscut-eliminationproofsforlogicswiththesefeaturesinisolationdonotcarryovertothisnewsystem.Thebulkofthispaperisapresentationofaproofofcut-eliminationforFOλΔIN.Thepaperisorganizedasfollows.Inthenextsection,webrieflydescribesomeusesthathavebeenmadeofFOλΔIN.Insection3weintroducethelogicandsomeofitsbasicproperties.WeproceedinSection4togiveanoverviewofthecut-eliminationproof.Section5specifiesthereductionrulesthatwillbeusedtoeliminateapplicationsofthecutrule.Thisisfollowedbyasectionwhichprovidessomeauxiliarydefinitionsandtheirproperties.Section7containstheproofofcut-elimination.WeconcludewithabriefcomparisonofourworkwithrelatedworkofMartin-Lo¨fandSchroeder-Heister.2ApplicationsofFOλΔINOneuseofFOλΔINhasbeentoreasonaboutHornclauseprograms.Forexample,Hornclausescanbeusedtospecifyapredicatethatrelatesalisttoitslengthandanotherpredicatethatrelatestwolistsiftheyarepermutationsofeachother.ItisaneasymattertogiveaproofinFOλΔINthatiftwolistsarepermutationsofeachother,thenthosetwolistshavethesamelength[13,Chapter2].ManysimilartheoremscanbefoundthroughoutMcDowell’sdissertation[13].Asweshallsee,theintegrationofdefinitionsintosequentcalculusmakesitpossibletoperformacaseanalysisonpossiblewaysthataspecifiedcomputationcanprogress.Ifexploitedproperly,itispossibletocapturenotionssuchassimulationandbisimulationbetweentwoprocesses.Thepaper[16]showshowthiscanbeaccomplishedinabstracttransitionsystemsandCCS.AfinalareawhereFOλΔINhasbeenusedtoreasonaboutspecificationsisintheareaoflogicalframeworksandhigher-orderabstractsyntax.Logicalframeworkshavebeensuccessfullyusedtogivehigh-level,modular,andformalspecificationsofmanyimportantjudgmentsintheareaofprogramminglanguagesandinferencesystems.Thesejudgments,suchas“thetermMdenotesaprogram”,“theprogramMevaluatestothevalueV”,and“theprogramMhastypeT”,arerepresentedbypredicatesinthespecificationlogicorbytypesinadependenttypecalculus.Oneoftheadvantagesofsuchformalspecificationsisthattheyallowlogicalandmathematicalanalysestobeusedtoprovepropertiesaboutthespecifiedsystems.Giventhespecificationofevaluationforafunctionalprogramminglanguage,forexample,wemaywishtoprovethatthelanguageisdeterministicorthatevaluationpreservestypes.Onechallengeinreasoningaboutsuchspecificationscentersontheuseofhigher-orderabstractsyntax,anelegantanddeclarativeencodingofabstractionandsubstitution[23].Withmostap-proachestosyntacticrepresentation,thedetailsofvariablebindingandsubstitutionmustbecare-fullyaddressedthroughoutaspecification,andtheoremsaboutsubstitutionandboundvariablescandominatethesystemanalyses.Withhigher-orderabstractsyntax,ontheotherhand,thesefeaturesarespecifiedconciselyandtheirbasicpropertiesfollowimmediatelyfromthespecificationlogic.However,reasoningwithinalogicalframeworkaboutsystemsrepresentedinhigher-orderabstractsyntaxhasbeendifficultsincethelogicsthatsupportthisnotionofsyntaxdonotprovidefacilitiesforthefundamentaloperationsofcaseanalysisandinduction.Moreover,higher-orderabstractsyntaxleadstotypesandrecursivedefinitionsthatdonotgiverisetomonotoneinductive3
operators,makinginductiveprinciplesdifficulttofind.In[14]theauthorshaveshownthatthesedifficultiescanbeovercomewithinFOλΔIN.See[13,14]formoreonhowFOλΔINcanbeusedasameta-logicforanintuitionisticandlinearlogicalframework.ThePiderivationeditorofEriksson[6]wasdesignedforthefinitarycalculusofpartialinductivedefinitions[5].BecauseofFOλΔIN’scloserelationshipwiththefinitarycalculusofpartialinductivedefinitions,thePieditorcanbeusedtoconstructFOλΔINderivations.ThemanyexamplesofspecificationsandproofsinFOλΔINreportedin[13,14]wereconstructedusingthiseditor.Dependenttypedλ-calculihavebeenusedtospecifycomputationsinwaysanalogoustothelogicprogrammingsettingpresentedhere[22].Schu¨rmannandPfenning[26]presentedameta-logicforsuchadependenttypedλ-termsthatcanbeusedtoreasonabouthigher-orderdeductionsinwayssimilartousesofFOλΔIN[14].3TheLogicFOλΔINThebasiclogicisanintuitionisticversionofasubsetofChurch’sSimpleTheoryofTypes[3]inwhichmeta-levelformulaswillbegiventhetypeo.Thelogicalconnectivesare,>,,,,τ,andτ.Thequantificationtypesτ(andthusthetypesofvariables)arerestrictedtonotcontaino.ThusFOλΔINsupportsquantificationoverhigher-order(non-predicate)types,acrucialfeatureforhigher-orderabstractsyntax,buthasafirst-orderprooftheorysincethereisnoquantificationoverpredicatetypes.WewillusesequentsoftheformΓ−→B,whereΓisafinitemultisetofformulasandBisasingleformula.ThebasicinferencerulesforthelogicareshowninTable1.Inthe∀Rand∃Lrules,yisaneigenvariablethatisnotfreeinthelowersequentoftherule.Themulticut(mc)ruleisageneralizationofcutduetoSlaney[27],andisusedtosimplifythepresentationofthecut-eliminationproof.Weintroducethenaturalnumbersviatheconstantsz:ntforzeroands:ntntforsuccessorandthepredicatenat:nto.TherightandleftrulesforthisnewpredicateareΓ−→natIΓ−→natznatRΓ−→nat(sI)natR−→BzBj−→B(sj)BI,Γ−→CnatI,Γ−→CnatL.Intheleftrule,thepredicateB:ntorepresentsthepropertythatisprovedbyinduction,andjisaneigenvariablethatisnotfreeinB.ThethirdpremiseVofthatinferencerulewitnessesthefactthat,ingeneral,Bwillexpressapropertystrongerthan(Γ)C.BecausetheinductionpredicateBinthenatLruleisnotnecessarilyasubformulaoftheformulaCoranyformulainΓ,thesubformulapropertydoesnotholdforFOλΔIN.Infact,wecanderivethefollowinginferencerulefromtheinductionrule:−→BB,Γ−→CnatI,Γ−→C.Thisderivedruleresemblesthecutrulebutrequiresanatassumption.AlthoughFOλΔINdoesnothavethesubformulaproperty,thecut-eliminationtheoremstillprovidesastrongbasisforreasoningaboutproofsinFOλΔIN[13,14,16].Infact,theformulationofthenatLruleandthefailureofthesubformulapropertyreflectthefactthatinactualmathematicalpractice,findingthe4
Table1:InferencerulesforthecoreofFOλΔIN,Γ−→B⊥LΓ>>RB,Γ−→DC,Γ−→DB[t/x],Γ−→CBC,Γ−→D∧LBC,Γ−→DLx.B,Γ−→C∀LΓ−→BΓ−→C∧RΓ−→B[y/x]∀RΓ−→BCΓ−→∀x.BB,Γ−→DC,Γ−→D∨LB[y/x],Γ−→C∃LBC,Γ−→Dx.B,Γ−→CΓ−→B[t/x]ΓΓBBC∨RΓΓBCC∨RΓ−→∃x.B∃RΓ−→BC,Γ−→DB,Γ−→CBC,Γ−→D⊃LΓ−→BC⊃RA,Γ−→Ainit,whereAisatomicB,B,BΓ,ΓCCcLΔ1−→B1∙∙∙Δn−→BnB1,...,Bn,Γ−→Cmc,wheren0Δ1,...,Δn,Γ−→C5
properinductionhypothesisrequiresinsightandcreativity;theyarenotsimplyrearrangementsofthesubformulasoftheconclusion.Asaresult,anyimplementationofFOλΔINwillnecessarilybeinteractive,atleastfortheinventionofmanyinductionhypotheses.4Adefinitionalclauseiswrittenx¯[pt¯=B],wherepisapredicateconstant,everyfreevariableoftheformulaBisalsofreeinatleastoneterminthelistt¯ofterms,andallvariablesfreeint¯arecontainedinthelistx¯ofvariables.Sinceallfreevariablesinpt¯andBareuniversallyquantified,weoftenleavethesequantifiersimplicitwhendisplayingdefinitionalclauses.Theatomicformulapt¯iscalledtheheadoftheclause,andtheformulaBiscalledthebody.Thesymbol=4isusedsimplytoindicateadefinitionalclause:itisnotalogicalconnective.Adefinitionisa(perhapsinfinite)setofdefinitionalclauses.Thesamepredicatemayoccurintheheadofmultipleclausesofadefinition:itisbesttothinkofadefinitionasamutuallyrecursivedefinitionofthepredicatesintheheadsoftheclauses.DefinitionsareemployedinFOλΔINvialeftandrightintroductionrulesforatomicformulas.Ifweimposenorestrictionsondefinitions,thecut-eliminationtheoremdoesnothold[24].Twodifferentapproacheshavebeentakentoretaintheadmissibilityofcut.First,ifthestructuralruleofcontractionisremovedorrestricted(asitisinlinearlogic,forexample),cut-eliminationcanbeestablished[9,25].Anotherapproach,moreappropriateforuseheresincewewishtoworkwithinanintuitionisticsetting,istorestricttheoccurrencesofimplicationswithinthebodyofdefinitions.In[25],Schroeder-Heisterprovedthecut-eliminationtheoremforanintuitionisticlogicinwhichnoimplicationsareallowedwithindefinitions.Hereweshallallowimplicationsinthebodyofdefinitionsiftheyaresuitablystratified.Towardthatendweassumethateachpredicatesymbolpinthelanguagehasassociatedwithitanaturalnumberlvl(p),thelevelofthepredicate.Thefollowingdefinitionextendsthenotionofleveltoformulasandderivations.Definition1GivenaformulaB,itslevellvl(B)isdefinedasfollows:1.lvl(pt¯)=lvl(p)2.lvl()=lvl(>)=03.lvl(BC)=lvl(BC)=max(lvl(B),lvl(C))4.lvl(BC)=max(lvl(B)+1,lvl(C))5.lvl(x.B)=lvl(x.B)=lvl(B).GivenaderivationΠofΓ−→B,lvl(Π)=lvl(B).4Weshallnowrequirethatforeverydefinitionalclausex¯[pt¯=B],lvl(B)lvl(p).ThelogicFOλΔINhasusesdefinitionsinleftandright-introductionrulesforatoms;thefollowingrelationwillbeusefulfordescribingthoseinferencerules.Definition2Letthefour-placerelationdfn(ρ,A,σ,B)bedefinedtoholdfortheformulasAandBandthesubstitutionsρandσifthereisaclausex¯[A0=4B]inthegivendefinitionsuchthat=A0σ.TherightandleftrulesforatomsareΓ−→defR,wheredfn(²,A,θ,B)AΓ6
{Bσ,Γρ−→|dfn(ρ,A,σ,B)}A,Γ−→CdefL,where²istheemptysubstitutionandtheboundvariablesx¯inthedefinitionalclausesarechosentobedistinctfromthevariablesfreeinthelowersequentoftherule.Specifyingasetofsequentsasthepremiseshouldbeunderstoodtomeanthateachsequentinthesetisapremiseofthe4rule.Therightrulecorrespondstothelogicprogrammingnotionofbackchainingifwethinkof=indefinitionalclausesasreverseimplication.Theleftruleissimilartodefinitionalreflection[25](nottobeconfusedwithanothernotionofreflectionoftenconsideredbetweenameta-logicandobject-logic)andtoaninferenceruleusedbyGirardinhisnoteonfixedpoints[9].NoticethatinthedefLrule,thefreevariablesoftheconclusioncanbeinstantiatedinthepremises.ThenumberofpremisesofthedefLrulemaybezeroormaybeinfinite.IftheformulaAdoesnotunifywiththeheadofanydefinitionalclause,thenthenumberofpremiseswillbezero.Inthiscase,Aisanunprovableformulalogicallyequivalentto,anddefLcorrespondstothe⊥Lrule.IftheformulaAdoesunifywiththeheadofadefinitionalclause,thenumberofpremisescouldbeinfinite,sincethedomainsofthesubstitutionsρandσmayincludevariablesthatarenotfreeinAandB.Ingeneralwewishtoworkwithinferenceruleswithafinitenumberofpremises.ThiscanbeachievedbyrestrictingdefinitionstohaveonlyafinitenumberofclausesandtorestricttheuseofdefLruletothoseformulasAsuchthatforeverydefinitionalclausethereisafinite,completesetofunifiers(CSU)[11]ofAandtheheadoftheclause.ConsiderthefollowinginferenceruleduetoEriksson[5]{Bθ,Γθ−→|θCSU(A,A0)forsomeclausex¯[A0=4B]}A,Γ−→CdefLCSU,wherethevariablesx¯arechosentobedistinctfromthevariablesfreeinthelowersequentoftherule.WhentheCSUsanddefinitionarefinite,thisrulewillhaveafinitenumberofpremises.Noticethatinfirst-orderlogics,aCSUwillhaveatmostonemember,namelythemostgeneralunifier(MGU).Proposition3TherulesdefLanddefLCSUareinteradmissible,thatis,ifFOλΔINisformulatedwitheitherdefLordefLCSU,theotherruleisadmissibleinthatformulation.ProofGiventhesetofderivations¾½B,θΠ,Bθ,Γθ−→θCSU(A,A0)forsomeclausex¯[A0=4B]wecan4constructaderivationofA,Γ−→CusingdefLasfollows.Foranydefinitionalclausex¯[A0=B]andsubstitutionsρandσsuchthat=A0σ,thesubstitution(σ(y)ifyFV(A0)ρσ(y)=ρ(y)otherwisewillbeaunifierofAandA0.ThusforsomeθCSU(A,A0)thereisasubstitutionθ0suchthatρσisθθ0.(NoticethatcompositionofsubstitutionisdefinedsothatA(θθ0)=()θ0.)WecanthususeΠθ,Bθ0asthepremisederivationofBσ,Γρ−→fordefL.(WewillformallydefinewhatitmeanstoapplyasubstitutiontoaderivationinDefinition5.Fornowitisenoughtoknowthat7
ityieldsaderivationwhoseendsequentisobtainedbyapplyingthesubstitutiontotheendsequentoftheoriginalderivation.)Giventhesetofderivations¾½Πρ,σ,B,Bσ,Γρ−→dfn(ρ,A,σ,B)wecanconstructaderivationofA,Γ−→CusingdefLCSUasfollows.Foranydefinitionalclausex¯[A0=4B]andsubstitutionθCSU(A,A0),dfn(θ,A,θ,B)holds.WecanthususeΠθ,θ,BasthepremisederivationofBθ,Γθ−→fordefL.ObservethatseveraloftherulesofFOλΔINmayhavevariablesthatarefreeinthepremisebutnotintheconclusion:thisresultsfromtheeigenvariableyof∀Rand∃L,thetermtof∀Land∃R,thecutformulasB1,...,Bnofmc,theinductionpredicateBofnatL,andthesubstitutionsρandσofdefL.Weviewthechoiceofsuchvariablesasarbitraryandidentifyallderivationsthatdifferonlyinthechoiceofvariablesthatarenotfreeinend-sequent.Wedefineanordinalmeasurewhichcorrespondstotheheightofaderivation:Definition4GivenaderivationΠwithpremisederivations{Πi}i,themeasureht(Π)istheleastupperboundof{ht(Πi)+1}i.Substitutionsarefinitemapsfromvariablestoterms.Itiscommontoviewsubstitutionsasmapsfromtermstotermsbyapplyingthesubstitutiontoallfreevariablesofaterm.Wecanthenextendthemappinginturntoformulasandmultisetsbyapplyingittoeveryterminaformulaandeveryformulainamultiset.Thefollowingdefinitionextendssubstitutionsyetagaintoapplytoderivations.Sinceweidentifyderivationsthatdifferonlyinthechoiceofvariablesthatarenotfreeintheend-sequent,wewillassumethatsuchvariablesarechosentobedistinctfromthevariablesinthedomainofthesubstitutionandfromthefreevariablesoftherangeofthesubstitution.Thusapplyingasubstitutiontoaderivationwillonlyaffectthevariablesfreeintheend-sequent.Definition5IfΠisaderivationofΓ−→Candθisasubstitution,thenwedefinethederivationΠθofΓθ−→asfollows:1.SupposeΠendswiththedefLrule¾½Πρ,σ,BBσ,Γ0ρ−→dfn(ρ,A,σ,B)A,Γ0−→CdefL.Observethatifdfn(ρ0,Aθ,σ0,B)thendfn(θρ0,A,σ0,B).ThusΠθis½¾Πθρ00,B0000Bσ,Γθρ−→Cθρdfn(ρ0,Aθ,σ0,B)Aθ,Γ0θ−→defL.2.IfΠendswithanyotherruleandhaspremisederivationsΠ1,...,Πn,thenΠθalsoendswiththesameruleandhaspremisederivationsΠ1θ,...,Πnθ.Lemma6ForanysubstitutionθandderivationΠofΓ−→C,ΠθisaderivationofΓθ−→.8
ProofThislemmastatesthatDefinition5iswell-constructed,andfollowsbyinductiononµ(Π).ObservethatifΠendswiththedefRrule0ΓΠΓ−→AdefR,thendfn(²,A,σ,B),andsoitisalsotruethatdfn(²,Aθ,σθ,B).Therefore0θΠΓθ−→BσθdefRΓθ−→isavalidderivation.Lemma7ForanyderivationΠandsubstitutionθ,ht(Π)ht(Πθ).ProofTheproofofthislemmaisasimpleinductiononht(Π).ThemeasuresmaynotbeequalbecausewhenthederivationsendwiththedefLrule,someofthepremisederivationsofΠmaynotbeneededtoconstructthepremisederivationsofΠθ.Ourlogicdoesnotcontainaweakeningrule;insteadweallowextraassumptionsintheaxioms.Thefollowingdefinitionprovidesmeta-levelweakeningonderivations.Sinceweidentifyderivationsthatdifferonlyinthechoiceofvariablesthatarenotfreeintheend-sequent,wewillassumethatsuchvariablesarechosentobedistinctfromthefreevariablesoftheweakeningformulas.Definition8IfΠisaderivationofΓ−→CandΔisamultisetofformulas,thenwedefinethederivationw,Π)ofΓ,Δ−→Casfollows:1.IfΠendswiththedefLrule¾½Πρ,σ,BBσ,Γ0ρ−→A,Γ0−→CdefL,thenw,Π)is½¾wρ,Πρ,σ,B)Bσ,Γ0ρ,Δρ−→LfedA,Γ0,Δ−→C.2.IfΠendswiththenatLruleΠ1Π2Π3−→BzBj−→B(sj)BI,Γ−→CnatLnatI,Γ−→C,thenw,Π)isΠ1Π2w,Π3)−→BzBj−→B(sj)BI,Γ,Δ−→CnatLnatI,Γ,Δ−→C.9
3.IfΠendswiththemcruleΠ1ΠnΠ0Δ1−→B1∙∙∙Δn−→BnB1,...,Bn,Γ−→CcmΔ1,...,Δn,Γ−→C,thenw,Π)isΠ1Πnw,Π0)Δ1−→B1∙∙∙Δn−→BnB1,...,Bn,Γ,Δ−→CcmΔ1,...,Δn,Γ,Δ−→C.4.IfΠendswithanyotherruleandhaspremisederivationsΠ1,...,Πn,thenw,Π)alsoendswiththesameruleandhaspremisederivationsw,Π1),...,w,Πn).Thefollowinglemmascanbeprovedbyinductiononthemeasureofthegivenderivation.Lemma9ForanymultisetΔofformulasandderivationΠofΓ−→C,w,Π)isaderivationofΓ,Δ−→C.Lemma10ForanyderivationΠandmultisetΔofformulas,ht(Π)=ht(w,Π)).Lemma11ForanyderivationΠ,multisetΔofformulas,andsubstitutionθ,w,Π)θandwθ,Πθ)arethesamederivation.Lemma12ForanyderivationΠandmultisetsΔandΔ0offormulas,w,w0,Π))andwΔ0,Π)arethesamederivation.4OverviewoftheCut-EliminationProofGentzen’sclassicproofofcut-eliminationforfirst-orderlogic[7]usesaninductioninvolvingthenumberoflogicalconnectivesinthecutformula.Acutonacompoundformulaisreplacedbycutsonitssubformulas,whichnecessarilycontainalowernumberofconnectives.Forexample,thederivationΠ1Π2Π3Δ−→B1Δ−→B2B1,Γ−→CΔ−→B1B2∧RB1B2,Γ−→C∧LcmΔ,Γ−→CisreducedtoΠΠ31Δ−→B1B1,Γ−→CcmΔ,Γ−→C.01
Bytheinductionhypothesis,thiscutonB1iseliminable,hencetheoriginalcutonB1B2isalsoeliminable.Infirst-orderlogic,whenthecutformulaisatomic,thecutcaneasilyberemovedbypermutingthecutuptowardtheleavesoftheproof;eventuallyaninitialruleisreached,atwhichpointtheremovalofthecutistrivial.InFOλΔIN,however,therulesfornaturalnumbersanddefinitionsactonatoms,sotheatomiccaseisnotsimple.Consider,forexample,thederivation¾½Π1Πρ,σ,DΔ−→defRDσ,Γρ−→defLΔ−→AA,Γ−→CΔ,Γ−→Cmc.TheobviousreductionforthisisacutbetweenΠ1andtheappropriatepremiseofthedefLrule;however,isaformulaofarbitrarycomplexity,andsowillingeneralhaveagreaternumberofconnectivesthantheatomA,whichhaszero.Thusadifferentinductionmeasureisneeded.Schroeder-Heisterprovescut-eliminationforseverallogicswithdefinitions[24,25]byincludingthenumberofusesofthedefLruleinthederivationaspartoftheinductionmeasure.However,thelogicsheconsidersdonotcontaininduction;theinclusionofthenatRandnatLrulesinFOλΔINcomplicatesthingsfurther.ThederivationΠ1Π2Π3Π4Δ−→natI−→BzBj−→B(sj)B(sI),Γ−→CΔ−→nat(sI)natRnat(sI),Γ−→CnatLcmΔ,Γ−→Ccanbereducedinanumberofways,butthereductionsareallvariationsofthederivationΠ2Π3Π3[I/j]Π1−→BzBj−→B(sj)BI−→B(sI)Δ−→natInatI−→B(sI)natLΠ4cmΔ−→B(sI)B(sI),Γ−→CcmΔ,Γ−→C.Here,thecutontheatomicformulanat(sI)isreplacedbytwocuts,oneontheatomnatIandtheotherontheformulaB(sI).Itisnotclearwhatinductionmeasurecanbeusedhere.Forthefirstcut,theatomnatIcontainsnologicalconnectives,butthisistrueoftheoriginalcutformulanat(sI)aswell.ThenumberofnatRrulesintherightsubderivationofthecuthasgonedownbyone,buttheduplicationofΠ3mightoffsetthis.Forthesecondcut,thecutformulaB(sI)isnotrelatedatalltotheoriginalcutformula;itcertainlycanhavenofewerconnectivesthantheatomnat(sI).Andthoughitsleftpremiseisshorterthantheleftpremiseoftheoriginalcut,itisunclearhowtheheightsoftherightpremisescompare.Itshouldbenoted,however,thatthecomplicatingfactorhereisnotthepresenceofaninductionrule,butouruseofthenatpredicateintheinductionrule.IfweremovethenatRrulesfromthelogicandreformulatetheinductionruletobe−→BzBj−→B(sj)BI,Γ−→CΓ−→Cind,11