15 Pages
English

January Final version appearing in proceedings of TLCA'05

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
January 31, 2005 — Final version, appearing in proceedings of TLCA'05. Naming Proofs in Classical Propositional Logic Franc¸ois Lamarche Lutz Straßburger LORIA & INRIA-Lorraine Universitat des Saarlandes Projet Calligramme Informatik — Programmiersysteme 615, rue du Jardin Botanique Postfach 15 11 50 54602 Villers-les-Nancy — France 66041 Saarbrucken — Germany Abstract. We present a theory of proof denotations in classical propo- sitional logic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a “Boolean” category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a “real” sequential- ization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures. 1 Introduction Finding a good way of naming proofs in classical logic—a good theory of proof terms, or proof nets, or whatever—is a notoriously difficult question, and the literature about it is already quite large, and still increasing. Other logics have been helped enormously by the presence of good semantics, where by semantics we mean mathematical objects that have an independent existence from syntax.

  • logic

  • saarbrucken —


  • syntax

  • ing sequent

  • closed categories

  • has very

  • cont-cont problems

  • logic can

  • sequent calculi


Subjects

Informations

Published by
Reads 10
Language English
January31,2005—Finalversion,appearinginproceedingsofTLCA’05.NamingProofsinClassicalPropositionalLogicFranc¸oisLamarcheLutzStraßburgerLORIA&INRIA-LorraineUniversita¨tdesSaarlandesProjetCalligrammeInformatikProgrammiersysteme615,rueduJardinBotaniquePostfach15115054602Villers-le`s-NancyFrance66041Saarbru¨ckenGermanyhttp://www.loria.fr/~lamarchehttp://www.ps.uni-sb.de/~lutzAbstract.Wepresentatheoryofproofdenotationsinclassicalpropo-sitionallogic.Theabstractdefinitionisintermsofasemiringofweights,andtwoconcreteinstancesareexplored.WiththeBooleansemiringwegetatheoryofclassicalproofnets,withageometriccorrectnesscriterion,asequentializationtheorem,andastronglynormalizingcut-eliminationprocedure.Thisgivesusa“Boolean”category,whichisnotaposet.Withthesemiringofnaturalnumbers,weobtainasoundsemanticsforclassicallogic,inwhichfewerproofsareidentified.Thougha“real”sequential-izationtheoremismissing,theseproofnetshaveagriponcomplexityissues.Inbothcasesthecuteliminationprocedureiscloselyrelatedtoitsequivalentinthecalculusofstructures.1IntroductionFindingagoodwayofnamingproofsinclassicallogic—agoodtheoryofproofterms,orproofnets,orwhatever—isanotoriouslydifficultquestion,andtheliteratureaboutitisalreadyquitelarge,andstillincreasing.Otherlogicshavebeenhelpedenormouslybythepresenceofgoodsemantics,wherebysemanticswemeanmathematicalobjectsthathaveanindependentexistencefromsyntax.Linearlogicwasfoundthroughtheobservationofthecategoryofcoherencespacesandlinearmaps.Forintuitionisticlogic,ithasbeenobviousforalongtimethatallittakestogiveaninterpretationofformulasandproofsa`laBrouwer-Heyting-Kolmogorov-Curry-Howardisabi-cartesianclosedcategory...andcartesianclosedcategoriesaboundinnature.Butifwetrytoextendnaivelythesesemanticstoclassicallogic,itiswell-knownthateverythingcollapsestoaposet(aBooleanalgebra,naturally)andwearebacktotheoldsemanticsofprovability.Clearlysomethinghastobeweakened,ifweeverwantclassicallogictohaveameaningbeyondsyntax.Veryrecently,itwasfound[17]thataclassofalgebrasfromgeometrypermitsrelevantinterpretationsofclassicalproofs;inadditionproposalsforabstractcategoricalframeworkshasbeenmade;theonein[10,11]isbasedontheproofnetsof[24](whichavoidsposetcollapseisbynotidentifyingarrowcompositionwithcut-elimination),andtheonein[9]extendsthetraditionof“coherence”resultsincategorytheory,whichpredateslinearlogicbydecades.