June Final version for the proceedings of CSL'09

Description

Niveau: Supérieur, Doctorat, Bac+8
June 22, 2009 — Final version for the proceedings of CSL'09 Expanding the realm of systematic proof theory Agata Ciabattoni1, Lutz Straßburger2, and Kazushige Terui3 1Technische Universtat Wien, Austria 2INRIA Saclay–Ile-de-France, France 3RIMS, Kyoto University, Japan Abstract. This paper is part of a general project of developing a sys- tematic and algebraic proof theory for nonclassical logics. Generaliz- ing our previous work on intuitionistic-substructural axioms and single- conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert ax- ioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level P ?3 of the hierarchy into inference rules in multiple-conclusion (hy- per)sequent calculi, which enjoy cut-elimination under a certain con- dition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than P ?3. The case study of Abelian and Lukasiewicz logic is outlined. 1 Introduction Since the axiomatisation of classical propositional logic by Hilbert in 1922, such axiomatic descriptions (nowadays called Hilbert-systems) have been successfully used to introduce and characterize logics. Ever since Gentzen's seminal work it has been an important task for proof theorists to design for these logics de- ductive systems that admit cut-elimination.

• conclusion setting


• linear logic


• coming up


• axiom ? ?


• conclusion sequent


• every axiom


• generated rules


• iff ?c ?


• into structural


• pin iff

Sujets

• Kyoto University
• Straßburger
• Linear logic
• Coming Up

Informations

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

Extrait

June22,2009—FinalversionfortheproceedingsofCSL’09 Expandingtherealmofsystematicprooftheory AgataCiabattoni 1 ,LutzStraßburger 2 ,andKazushigeTerui 3 1 TechnischeUniversta¨tWien,Austria 2 INRIASaclay– ˆ Ile-de-France,France 3 RIMS,KyotoUniversity,Japan Abstract.Thispaperispartofageneralprojectofdevelopingasys- tematicandalgebraicprooftheoryfornonclassicallogics.Generaliz- ingourpreviousworkonintuitionistic-substructuralaxiomsandsingle- conclusion(hyper)sequentcalculi,wedefineahierarchyonHilbertax- iomsinthelanguageofclassicallinearlogicwithoutexponentials.We thengiveasystematicproceduretotransformaxiomsuptothelevel 0 P 3 ofthehierarchyintoinferencerulesinmultiple-conclusion(hy- per)sequentcalculi,whichenjoycut-eliminationunderacertaincon- dition.Thisallowsasystematictreatmentoflogicswhichcouldnotbe dealtwithinthepreviousapproach.Ourmethodalsoworksasaheuristic principleforfindingappropriaterulesforaxiomslocatedatlevelshigher 0 than P 3 .ThecasestudyofAbelianand Lukasiewiczlogicisoutlined. 1Introduction SincetheaxiomatisationofclassicalpropositionallogicbyHilbertin1922,such axiomaticdescriptions(nowadayscalledHilbert-systems)havebeensuccessfully usedtointroduceandcharacterizelogics.EversinceGentzen’sseminalwork ithasbeenanimportanttaskforprooftheoriststodesignfortheselogicsde- ductivesystemsthatadmitcut-elimination.Theadmissibilityofcutiscrucial toestablishimportantpropertiesofcorrespondinglogicssuchasconsistency, decidability,conservativity,interpolation,andisalsothekeytomakeasystem suitableforproofsearch.Asdesignersofdeductivesystemscouldneverkeep pacewiththespeedoflogiciansandpractitionerscomingupwithnewlogics, generaltoolstoautomatethisdesignprocessandextractsuitablerulesoutof axiomswouldbeverydesirable.Workinthisdirectionaree.g.[7,20,19]. Ageneralprojectofsystematicandalgebraicprooftheoryfornonclassical logicswasrecentlylaunchedin[3,4]whereHilbertaxiomsinthelanguageof fullLambekcalculusFL(i.e.,intuitionisticnoncommutativelinearlogicwithout exponentials)havebeenclassifiedintothesubstructuralhierarchy( P n , N n ) n ∈ N , withtheaimtoconquestthewholehierarchyfrombottomtotop.Theworkin[3] successfullydealtwiththeaxiomsuptolevel N 2 .Itgaveaproceduretotrans- formthemintostructuralrulesinthesingle-conclusionsequentcalculus,and algebraicallyproved(astrongerformof)cut-eliminationforFLextendedwith thegeneratedruleswhichsatisfythesyntacticconditionofacyclicity.Then, [4]expandedtherealmtothelevel P 3 0 ,asubclassof P 3 inthecommutative setting,byusingthesingle-conclusionhypersequentcalculus[2].Theaimto continuetheconquerfurtherfacedaseriousobstacle:Asshownin[3],“strong”