Abstract. We divide attempts to give the structural proof theory of modal logics into two kinds, those pure formulations whose inference rules characterise modality completely by means of manipulations of boxes and diamonds, and those labelled formulations

PuritythroughUnravelling

RobertHeinandCharlesStewart

TechnischeUniversit¨atDresden,Germany

Abstract.Wedivideattemptstogivethestructuralprooftheoryofmodallogicsintotwokinds,thosepureformulationswhoseinferencerulescharacterisemodalitycompletelybymeansofmanipulationsofboxesanddiamonds,andthoselabelledformulationsthatleveragetheuseoflabels

ingivinginferencerules.Thewidespreadadoptionoflabelledformula-tionsisdrivenbytheirabilitytomodelfeaturesofthemodeltheoryofmodallogicinitsprooftheory.

Wedescribehereanapproachtothestructuralprooftheoryofmodallogicthataimstobringunderoneroofthebene tsofboththepureandthelabelledformulations.Weintroducetwoproofcalculi,onela-

belledsequentformulationandonepureformulationinthecalculusofstructuresthatareshowntobeinasystematiccorrelation,wherethelattercalculususesdeepinferencewithshapedmodalrulestocaptureinapuremannerthemanipulationsthattheformercalculationsmediatesthroughtheuseoflabels.

Wesituatethisworkwithinalargerinvestigationintotheprooftheoryofmodallogicthatsolvesproblemsthatexistedwiththeearlierinves-tigationbasedonpre xmodalrules.Weholdthisdevelopmentprovidesyetstrongerevidencejustifyingtheclaimthatgood,pureprooftheoryformodallogicneedsdeepinference.

1Introduction

Modallogicisanessentialpartofbothcomputationallogicandphilosophicallogic,forreasonsamongwhichwebringattentionto:

1.Modalitiesallowpartsofpropositionstobemarkedashavingdi erentse-manticstootherparts,forexampleinthewaythatvarious avoursoflinearlogicusethe”!”and”?”modalitiestoindicatewherestructuralidentitiesarevalid;

2.Modalpropositionallogicallowsincreasedexpressivityoverclassicalpropo-sitionallogic,butinacontrolledmannerallowingmanyuseful,decidablelanguagestobeformulated,bycontrasttothesituationinpredicatelogic;

3.Modallogiccapturesanotionoflocalitythathasprovenespeciallyusefulinthetheoryofconcurrency,duetothecloserelationshipofmodelinvarianceandbisimulation,aclosenessthathasresultedinthefundamentalcharac-terisationofbisimulationinHennessy-Milnerlogic;

4.Classicalmodallogiciswellsuitedtoalgebraicsemantics,sinceifweregardclassicalpropositionallogicasreceivingitsmostfundamentalsemanticsin