20 Pages
English

Workshop on “Classical Logic and Computation” July Venice Italy

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
Workshop on “Classical Logic and Computation” — July 15, 2006 — Venice, Italy What could a Boolean category be? Lutz Straßburger INRIA Futurs, Projet Parsifal Ecole Polytechnique — LIX — Rue de Saclay — 91128 Palaiseau Cedex — France Abstract. In its most general meaning, a Boolean category should be to categories what a Boolean algebra is to posets. In a more specific mean- ing a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Carte- sian closed category captures the proofs in intuitionistic logic and a *- autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this talk I will sketch a series (with increasing strength) of possible such axiomatisations, all based on the notion of *-autonomous category. There will be some focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures. 1 Introduction This work is mainly motivated by the question how to identify proofs in classical propositional logic. These are usually presented as syntactic objects within some deductive system (e.g., tableaux, sequent calculus, resolution, . . . ). Here we will take the point of view that these syntactic objects (also known as proof trees) should be considered as concrete representations of certain abstract proof ob- jects, and that such an abstract proof object can be represented

  • between ?

  • category theory

  • proofs written

  • autonomous category

  • ?b ?

  • classical logic

  • has recently

  • parigot's ?µ-calculus


Subjects

Informations

Published by
Reads 9
Language English
Workshopon“ClassicalLogicandComputation”—July15,2006—Venice,ItalyWhatcouldaBooleancategorybe?LutzStraßburgerINRIAFuturs,ProjetParsifalE´colePolytechniqueLIXRuedeSaclay91128PalaiseauCedexFrancehttp://www.lix.polytechnique.fr/~lutzAbstract.Initsmostgeneralmeaning,aBooleancategoryshouldbetocategorieswhataBooleanalgebraistoposets.Inamorespecificmean-ingaBooleancategoryshouldprovidetheabstractalgebraicstructureunderlyingtheproofsinBooleanLogic,inthesamesenseasaCarte-sianclosedcategorycapturestheproofsinintuitionisticlogicanda*-autonomouscategorycapturestheproofsinlinearlogic.However,recentworkhasshownthatthereisnocanonicalaxiomatisationofaBooleancategory.InthistalkIwillsketchaseries(withincreasingstrength)ofpossiblesuchaxiomatisations,allbasedonthenotionof*-autonomouscategory.Therewillbesomefocusonthemedialmap,whichhasitsorigininaninferenceruleinKS,acut-freedeductivesystemforBooleanlogicinthecalculusofstructures.1IntroductionThisworkismainlymotivatedbythequestionhowtoidentifyproofsinclassicalpropositionallogic.Theseareusuallypresentedassyntacticobjectswithinsomedeductivesystem(e.g.,tableaux,sequentcalculus,resolution,...).Herewewilltakethepointofviewthatthesesyntacticobjects(alsoknownasprooftrees)shouldbeconsideredasconcreterepresentationsofcertainabstractproofob-jects,andthatsuchanabstractproofobjectcanberepresentedbyaresolutionprooftreeandasequentcalculusprooftree,orevenbyseveraldifferentsequentcalculusprooftrees.Underthispointofviewthemotivationforthisworkistoprovideanab-stractalgebraictheoryofproofs.AlreadyLambek[Lam68,Lam69]observedthatsuchanalgebraictreatmentcanbeprovidedbycategorytheory.Forthis,itisnecessarytoacceptthefollowingpostulatesaboutproofs:foreveryprooffofconclusionBfromhypothesisA(denotedbyf:AB)andeveryproofgofconclusionCfromhypothesisB(denotedbyg:BC)thereisauniquelydefinedcompositeproofgfofconclusionCfromhypothesisA(denotedbygf:AC),thiscompositionofproofsisassociative,foreachformulaAthereisanidentityproof1A:AAsuchthatforf:ABwehavef1A=f=1Bf.
Undertheseassumptions1theproofsarethearrowsinacategorywhoseobjectsaretheformulasofthelogic.Whatremainsistoprovidetherightaxiomsforthe“categoryofproofs”.ItseemsthatfindingtheseaxiomsisparticularlydifficultforthecaseofBooleanlogic.Forintuitionisticlogic,Prawitz[Pra71]proposedthenotionofproofnormalizationforidentifyingproofs.Itwassoondiscoveredthatthisno-tionofidentitycoincideswiththenotionofidentitythatresultsfromtheaxiomsofaCartesianclosedcategory(see,e.g.,[LS86]).Infact,onecansaythattheproofsofintuitionisticlogicarethearrowsinthefree(bi-)cartesianclosedcate-gorygeneratedbythesetofpropositionalvariables.Analternativewayofrepre-sentingthearrowsinthatcategoryisviatermsinthesimply-typedλ-calculus:arrowcompositionisnormalizationofterms.Thisobservationiswell-knownasCurry-Howard-correspondence[How80].Inthecaseoflinearlogic,therelationto*-autonomouscategories[Bar79]wasnoticedimmediatelyafteritsdiscovery[Laf88,See89].Inthesequentcal-culuslinearlogicproofsareidentifiedwhentheycanbetransformedintoeachothervia“trivial”rulepermutations[Laf95].Formultiplicativelinearlogicthiscoincideswiththeproofidentificationsinducedbytheaxiomsofa*-autonomouscategory[Blu93,SL04].Therefore,wecansafelysaythataproofinmultiplica-tivelinearlogicisanarrowinthefree*-autonomouscategorygeneratedbythepropositionalvariables[BCST96,LS04,Hug05].Butforclassicallogicnosuchwell-acceptedcategoryofproofsexists.Wecandistinguishtwomainreasons.First,ifwestartfromaCartesianclosedcategoryandaddaninvolutivenegation2,wegetthecollapseintoaBooleanalgebra,i.e.,anytwoproofsf,g:ABareidentified.Foreveryformulatherewouldbeatmostoneproof(see,e.g.,[LS86]ortheappendixof[Gir91]fordetails).Alternatively,startingfroma*-autonomouscategoryandaddingnaturaltrans-formationsAAAandAt,i.e.,theproofsforweakeningandcontraction,yieldsthesamecollapse.3Thesecondreasonisthatcuteliminationinthesequentcalculusforclassicallogicisnotconfluent.Sincecuteliminationistheusualwayofcomposingproofs,thismeansthatthereisnocanonicalwayofcomposingtwoproofs,letaloneassociativityofcomposition.Consequently,foravoidingthesetwoproblems,wehavetoacceptthat(i)cartesianclosedcategoriesmightnotprovideanabstractalgebraicaxiomatisa-tionforproofsinclassicallogic,andthat(ii)thesequentcalculusisnottherightframeworkforinvestigatingtheidentityofproofsininclassicallogic.1Itcan(andshould)bearguedthattheseassumptionsarealreadytostrongforareasonabletheoryofproofs.However,inthispaperwefollowtheapproachinducedbytheseassumptions,andseewhereitwillbringus.2i.e.,anaturalisomorphismbetweenAandthedouble-negationofA(inthispaperdenotedbyA¯)3SincewearedealingwithBooleanlogic,wewillusethesymbolsandtforthetensoroperation(usually)andtheunit(usually1orI)ina*-autonomouscategory.2