Machine-checked Cut-elimination for Display Logic

Machine-checkedCut-eliminationforDisplayLogicJeremyE.DawsonandRajeevGoreyDepartmentofComputerScienceandAutomatedReasoningGroupAustralianNationalUniversityCanberraACT0200,[e-mail]@arp.anu.edu.au7November2006AbstractBelnap'sDisplayLogicisageneralisedsequent-styleframeworkwhichisabletocapturemanydierentlogicsinoneuniformsetting.Itsmainattractionsaretwofold:a\displaypropertywhichallowseveryformulatobeintroducedasthewholeoftheleftorrightsideofasequent,andasinglecut-eliminationtheoremwhichworksforall\properdisplaycalculi.Belnap'soriginalproofofthistheoremisshortandsuccinct,butithasbeencriticisedbysomeasbeingtooinformal.Theonlyotherpublishedproofturnsouttocontainanerror.ModerninteractiveproofassistantslikeNqthm,HOL,Isabelle,CoqandPVSinvariablytracetheiroriginstothesimply-typedlambda-calculusofChurch(althoughMizarisanexception).SuchtoolshavematuredtothepointwheredeeptheoremsinlogicandmathematicslikeGodel'sIncompletenessTheoremandtheFourColourTheoremcanbeexpressedandprovedbyexpertusersusingthesesystems.Here,wepresentanewproofofcut-eliminationforalldisplaycal-culiwhichdoesnotreplyontheusualdoubleinductiononthegradeandweightofacut.Simultaneously,wepresentahigh-leveldescrip-tionofhowweusedtheproofassistantIsabelletondandcheckthisproof.Webelievethattheuseofsuchproofassistantswillsoonbecomecommon-placeasproofsbecomemoreandmorecomplicated.SupportedbyanAustralianResearchCouncilLargeGrantySupportedbyanAustralianResearchCouncilQEIIFellowship1Contents1Introduction32LogicalFrameworksandInteractiveProofAssistants63RelatedWorkonMechanisedProofTheory74RelationAlgebras,RA,andIsabelle/HOL94.1RelationAlgebras.............................94.2TheDisplayCalculusRA.......................94.3IsabelleanditsHOLtheory.......................104.4DeepandShallowEmbeddings.....................115ADeepEmbeddingofRAinIsabelle/HOL115.1RepresentingFormulae,Structures,SequentsandRules.......115.2RepresentingDerivationsasTrees....................145.3HandlingSubstitutionsExplicitly....................155.4ReasoningAboutDerivations......................165.5ReasoningAboutDerivability......................186AnOperationalViewofCut-Elimination206.1PrincipalCutsandBelnap'sConditionC8...............216.2TransformingArbitraryCutsIntoPrincipalOnes...........227ADirectProofofCut-Admissibility(Weak-Normalisation)247.1FunctionsforReasoningAboutCuts..................247.2DealingWithPrincipalCuts......................247.3MakingACut(Left)Principal.....................267.4TurningOneCutIntoSeveralLeft-PrincipalCuts..........287.5PuttingItAllTogether.........................297.6TracingBelnap'sConditionsoftheDisplayCalculus.........348Wansing'sStrongNormalisationProof359Discussion3810ANewProofofStrongNormalisation3810.1PreliminaryDenitionsandResultsforStrongNormalization....3810.2DeningStronglyNormalisingDerivations...............3910.3VariousWell-FoundedOrderings....................4010.4InheritingStrongNormalisationfromImmediateSubtrees......4310.5ReasoningAboutCut-Reductions....................4510.6Strong-Normalisation...........................4710.7MakingACut(Left)Principal.....................4810.8DealingWithPrincipalCuts......................5410.9Cut-EliminationViaStrongNormalisation...............5511ConclusionandFurtherWork5812Appendix:Kracht'sFormulationofBelnap'sConditions6021IntroductionSequentcalculi[37]providearigorousbasisformeta-theoreticstudiesoflogics.Thecentraltheoremiscut-elimination,whichstatesthatdetoursthroughlemmatacanbeavoided,andallowsustoprovemanyimportantmeta-theoreticpropertieslikeconsistency,interpolation,andBethdenabil-ityinastraightforwardway[38].Cut-freesequentcalculiarealsousefulforautomateddeduction[19],nonclassicalextensionsoflogicprogramming[35],andstudyingthedeepconnectionsbetweencutelimination,lambda-calculiandfunctionalprogramming[20].Sequentcalculi,andtheirextensions,thereforeplayanimportantroleinbothlogicandtheoreticalcomputersci-ence.DisplayLogic[5]isageneralisedsequentframeworkfornon-classicallog-ics,basedonGentzen'ssequentcalculus[37].Sinceitisnotreallyalogic,weprefertheterm\displaycalculianduseitfromnowon.DisplaycalculiextendGentzen'slanguageofsequentswithextra,complex,n-arystruc-turalconnectives,inadditiontoGentzen'ssolestructuralconnective,the\comma.WhereasGentzen'commaisusuallyassumedtobeassociative,commutativeandinherentlypoly-valent,nosuchimplicitassumptionsaremadeaboutthen-arystructuralconnectivesindisplaycalculi.Propertiessuchasassociativityareexplicitlystatedasstructuralrules.Suchexplicitstructuralrulesmakedisplaycalculimoremodularthantraditionalsequent-stylecalculi:thelogicalrulesremainconstantanddif-ferentlogicsareobtainedbytheadditionordeletionofstructuralrulesonly.Displaycalculithereforeprovideanextremelyelegantsequentframeworkfor\logicengineering,encompassingavastrangeofsubstructurallogicslikethebi-intuitionisticandbi-classicalversionsoftheLambekcalculus,linearlogic,relevantlogic,BCK-logic,andtheirmodalandtenselogicalexten-sions,inauniformway[40,17].Themostremarkable