Workshop on “Classical Logic and Computation” July Venice Italy

Lutz Strassburger

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

Sujets

• École polytechnique
• Straßburger
• Category theory
• Autonomous category
• Classical logic

Informations

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

Extrait

Workshopon“ClassicalLogicandComputation”—July15,2006—Venice,Italy WhatcouldaBooleancategorybe? LutzStraßburger INRIAFuturs,ProjetParsifal E ´ colePolytechnique—LIX—RuedeSaclay—91128PalaiseauCedex—France http://www.lix.polytechnique.fr/~lutz Abstract.Initsmostgeneralmeaning,aBooleancategoryshouldbeto categorieswhataBooleanalgebraistoposets.Inamorespecificmean- ingaBooleancategoryshouldprovidetheabstractalgebraicstructure underlyingtheproofsinBooleanLogic,inthesamesenseasaCarte- sianclosedcategorycapturestheproofsinintuitionisticlogicanda*- autonomouscategorycapturestheproofsinlinearlogic.However,recent workhasshownthatthereisnocanonicalaxiomatisationofaBoolean category.InthistalkIwillsketchaseries(withincreasingstrength)of possiblesuchaxiomatisations,allbasedonthenotionof*-autonomous category.Therewillbesomefocusonthemedialmap,whichhasits origininaninferenceruleinKS,acut-freedeductivesystemforBoolean logicinthecalculusofstructures. 1Introduction Thisworkismainlymotivatedbythequestionhowtoidentifyproofsinclassical propositionallogic.Theseareusuallypresentedassyntacticobjectswithinsome deductivesystem(e.g.,tableaux,sequentcalculus,resolution,...).Herewewill takethepointofviewthatthesesyntacticobjects(alsoknownasprooftrees) shouldbeconsideredasconcreterepresentationsofcertainabstractproofob- jects,andthatsuchanabstractproofobjectcanberepresentedbyaresolution prooftreeandasequentcalculusprooftree,orevenbyseveraldifferentsequent calculusprooftrees. Underthispointofviewthemotivationforthisworkistoprovideanab- stractalgebraictheoryofproofs.AlreadyLambek[Lam68,Lam69]observedthat suchanalgebraictreatmentcanbeprovidedbycategorytheory.Forthis,itis necessarytoacceptthefollowingpostulatesaboutproofs: –foreveryprooffofconclusionBfromhypothesisA(denotedbyf:A → B) andeveryproofgofconclusionCfromhypothesisB(denotedbyg:B → C)thereisauniquelydefinedcompositeproofg ◦ fofconclusionCfrom hypothesisA(denotedbyg ◦ f:A → C), –thiscompositionofproofsisassociative, –foreachformulaAthereisanidentityproof1 A :A → Asuchthatfor f:A → Bwehavef ◦ 1 A =f=1 B ◦ f.

Undertheseassumptions 1 theproofsarethearrowsinacategorywhoseobjects aretheformulasofthelogic.Whatremainsistoprovidetherightaxiomsfor the“categoryofproofs”. Itseemsthatfindingtheseaxiomsisparticularlydifficultforthecaseof Booleanlogic.Forintuitionisticlogic,Prawitz[Pra71]proposedthenotionof proofnormalizationforidentifyingproofs.Itwassoondiscoveredthatthisno- tionofidentitycoincideswiththenotionofidentitythatresultsfromtheaxioms ofaCartesianclosedcategory(see,e.g.,[LS86]).Infact,onecansaythatthe proofsofintuitionisticlogicarethearrowsinthefree(bi-)cartesianclosedcate- gorygeneratedbythesetofpropositionalvariables.Analternativewayofrepre- sentingthearrowsinthatcategoryisviatermsinthesimply-typedλ-calculus: arrowcompositionisnormalizationofterms.Thisobservationiswell-knownas Curry-Howard-correspondence[How80]. Inthecaseoflinearlogic,therelationto*-autonomouscategories[Bar79] wasnoticedimmediatelyafteritsdiscovery[Laf88,See89].Inthesequentcal- culuslinearlogicproofsareidentifiedwhentheycanbetransformedintoeach othervia“trivial”rulepermutations[Laf95].Formultiplicativelinearlogicthis coincideswiththeproofidentificationsinducedbytheaxiomsofa*-autonomous category[Blu93,SL04].Therefore,wecansafelysaythataproofinmultiplica- tivelinearlogicisanarrowinthefree*-autonomouscategorygeneratedbythe propositionalvariables[BCST96,LS04,Hug05]. Butforclassicallogicnosuchwell-acceptedcategoryofproofsexists.Wecan distinguishtwomainreasons.First,ifwestartfromaCartesianclosedcategory andaddaninvolutivenegation 2 ,wegetthecollapseintoaBooleanalgebra, i.e.,anytwoproofsf,g:A → Bareidentified.Foreveryformulatherewould beatmostoneproof(see,e.g.,[LS86]ortheappendixof[Gir91]fordetails). Alternatively,startingfroma*-autonomouscategoryandaddingnaturaltrans- formationsA → A ∧ AandA → t,i.e.,theproofsforweakeningandcontraction, yieldsthesamecollapse. 3 Thesecondreasonisthatcuteliminationinthesequentcalculusforclassical logicisnotconfluent.Sincecuteliminationistheusualwayofcomposingproofs, thismeansthatthereisnocanonicalwayofcomposingtwoproofs,letalone associativityofcomposition. Consequently,foravoidingthesetwoproblems,wehavetoacceptthat(i) cartesianclosedcategoriesmightnotprovideanabstractalgebraicaxiomatisa- tionforproofsinclassicallogic,andthat(ii)thesequentcalculusisnottheright frameworkforinvestigatingtheidentityofproofsininclassicallogic. 1 Itcan(andshould)bearguedthattheseassumptionsarealreadytostrongfora reasonabletheoryofproofs.However,inthispaperwefollowtheapproachinduced bytheseassumptions,andseewhereitwillbringus. 2 i.e.,anaturalisomorphismbetweenAandthedouble-negationofA(inthispaper denotedbyA ¯ ) 3 SincewearedealingwithBooleanlogic,wewillusethesymbols ∧ andtforthetensor operation(usually  )andtheunit(usually1orI)ina*-autonomouscategory. 2