Some properties of linear logic proved by semantic

SOMEPROPERTIESOFLINEARLOGICPROVEDBYSEMANTICMETHODSArnonAvron*DepartmentofComputerScienceRaymondandBeverlySacklerFacultyofExactSciencesTelAvivUniversityTelAviv,Israele-mail:[e-mail]eralsimplealgebraicmodelsofthemultiplicativeandmulti-plicative-additivefragmentsoflinearlogicanddemonstratethevalueofsuchmodelsbyprovingsomeunexpectedproof-theoreticalpropertiesofthesefrag-ments.I.IntroductionTheresearchdescribedbelowstartedwhenweconsideredthefollowingsimpleques-tion:IsthereasentenceAofthemultiplicativefragmentofLinearLogicsuchthat)A;Aisatheoremof(theGentzen-typeversionof)thislogic?(Themotivationforconsideringthisquestionwillbeexplainedbelow,seeIII.10(3)).Afterfailingtoproduceanexampleofsuchasentencewehavetriedtoshowbyaproof-theoreticalargumentthatitcannot*PartofthisresearchwasdonewhiletheauthorwasvisitingtheComputerScienceDepartmentofEdinburghUniversity,andwassupportedbygrantsfromtheBritishAcademyofScienceandtheUKScienceandEngineeringResearchCouncil(VisitingFellowshipnumberGR/G55471).1exist.Again,wefailed(Thishadbeendue,infact,toalackofinsight,sinceDanosandSchellinxdidprovidelatersuchanargument1).Insituationslikethisinlogiconeusuallytriestoapplysemanticalmethods.Indeedafruitfulinvestigationofalogicalsystemalmostalwaysconsistsoftwocomplementaryparts:semanticalandproof-theoretical.Ideally,thereshouldbeaperfectmatchbetweenthetwo,butevenapartialmatch(likehavingonlysoundness)isfrequentlyofgreatvalue.Inlinearlogic,however,(asfarasIknow),noseriousattempthasbeenmadeuptonowtousesemanticconsiderationsinordertosolvestrictproof-theoreticalproblems.2Thestructuresthatwereinvestigatedinthisareawereofaveryabstractcharacter(likethe\phasesemanticsof[Gi87])andwereneverappliedforsolvingconcreteproblemsthatarenotdirectlyrelatedtothem.Wehavefelt,therefore,thatthetimehascometodevelopconcretestructuresthatcanserveasmodelsforlinearlogicandbehelpfulforsolvingproblemsaboutitliketheonewedescribedabove.Thispaperhas,accordingly,twopurposes.Therstistodevelopclassesofsimple,concretemodelsoflinearlogic.3Thesecondistodemonstratetheirvaluebyusingthemtoshowseveralsomewhatunexpectedfeaturesofthemultiplicativeandthemultiplicative-additivefragmentsoflinearlogic.Amongotherthingsweshow,e.g.,thatthereisnosentenceAofthemultiplicativelanguagesuchthat)A;:::;Aisatheorem(except,ofcourse,sequentsoftheform)A),thatthereisnomultisetoftheorems[A1;:::;An](n2)ofthemultiplicativefragmentsuchthat)A1;:::;Anisalsoatheorem,andthatasequentoftheform)isprovableinthemultiplicative-additivefragmentithemultisetisasingleton(asamultiset).Itisourhopethattheinvestigationsbelowwillnallyleadtoaclassofconcrete1InamessagetotheLINEARmboxonFebruary7,1992.Inthatnotetheyprovedalso,usingtheirbasicargument,TheoremsIII.4,III.6andthe\onlyifpartofTheoremIII.8below.Theydidnotprovidealternativeproofsforthenewresultsinsection4(likeIV.2.3.),buttheywerenotawareofthoseresultsthen.Theirargument,asitis,appliedonlytothemultiplicativefragment.2Perhapsethecaseisputtoostronglyhere.Itdependsonwhatonemightcall\strictproof-theoreticalproblems.Apaperlike[BCST],forexample,certainlytreatsproof-theoreticalproblems-butnotofthekindImean.Theexamplesbelowillustrate,Ihope,whatIhaveinmind.3ForanexampleofwhatIhaveinmindwhenIspeakabout\concretemodelsversus\abstractmodels,thinkofthetwo-valuedmodelofclassicalpropositionallogicversustheclassofBooleanalgebras.2modelsoflinearlogicforwhichwehavebothsoundnessandcompleteness.II.PreliminariesII.1Notations.Weshallusuallyusethosewhichwereemployedin[Av88].Inpartic-ular,weshalluse!;+;^;and_for,respectively,linearimplication,\par,\withand\plus.Whilein[Av88]thiswasamatterofhabit(followingthetraditioninrelevancelogic),inthepresentcontextthesenotationsturnouttobeparticularlysuggestive.Weshall,inaddition,treatnegationasanindependentconnective,denotedby:.Weshall,however,follow[Gi87]inusingthesymbols;1and?forthemultiplicativeconjunctionandthetwomultiplicativepropositionalconstants.ThefullpropositionallinearlogicwillbedenotedbyLL,whileitsmultiplicativeandmultiplicative-additivefragments(withoutthepropositionalconstants)willbedenotedbyLLmandLLa,respectively.LL?mandLL?adenotethecorrespondingfragmentswiththemultiplicativeconstants.II.2Gentzen-typeformulationGLL?a.Weshallusetheconventionaltwo-sidedversioninwhichwehavemultisetsonbothsidesof).Therulesare:A)A1)1;AA;2)21;2)1;2(cut));A:A;)A;));:A():)(+))A;1)1B;2)2A+B;1;2)1;2);A;B);A+B()+)(_))A;)B;)A_B;));A);A_B);B);A_B()_)3(?))?)));?()?)(Therulesfor;^and1aredualtothosefor,respectively+;_and?.Thesethreeconnectivescanbetakenasdenedones.)II.3TheAssociatedConsequenceRelation.Thelinearconsequencerelation(de-noted‘‘LLin[Av88])whichisusuallyassociatedwithlinearlogic(andcorrespondstothesequentsofGLL)isnotanordinaryconsequencerelationintheTarskiansense.Itisnotsuitable,therefore,forsemanticalinvestigationsoftheusualtype.Weshallusethereforeinsteadthe\extensionalconsequencerelation‘LLwhichwasintroducedin[Av88].Itcanbegivenanyofthefollowingcharacterizations(theequivalencebetwe