; TeX output 2007.10.18:2226 header=pstricks.proheader=pst-dots.proheader=pst-node.proheader=pst-eqdf.pro˅v{color push gray 0html: html:src:1267 18-18.texBp0J
cmsl10BTheoryUUandApplicationsofCategories,K`y
cmr10V*ol.q18,No.18,2007,pp.536{html:601 html:.M color popuK{color push gray 0html: html: color push gray 0 color pop src:1213 18-18.tex.XQ ff cmr12ON/THEAXIOMA4TISATION/OFBOOLEANCA4TEGORIES w5WITH/ANDWITHOUTMEDIAL XQ cmr12LUTZSTRABURrGER$ 'color push gray 0 color pop$src:1215 18-18.tex@-
cmcsc10@Abstract.
The(term\BoGoleancategory"shouldbe'usedfordescribinganob 8jectthat $is]'to]&categorieswhataBoGoleanalgebraistopGosets.
Morespecically*,a]&Booleancategory$shouldCprovidetheabstractalgebraicstructureCunderlyingtheproGofsinBooleanLogic,$in>*thesamesenseasaCartesian>)closedcategorycapturestheproGofsinintuitionistic$logicvanda
!",
cmsy10-autonomouscategoryvcapturestheproGofsinlinearlogic.
However,~Grecent$work$hasshown#thatthereisnocanonicalaxiomatisationofaBoGoleancategory*.WInthis$work,Awewillseeaseries(withincreasingstrength)ofpGossiblesuchaxiomatisations,Aall$basedonthenotionof-autonomouscategory*.VWewillparticularlyfoGcusonthemedial$map,{zwhich@has@itsorigininaninferenceruleinKS,acut-freedeductivesystemfor$BoGoleanlogicinthecalculusofstructures.iFinally*,wewillpresentacategoryofproGof$netsUUasaparticularlywell-bGehavedUUexampleofaBooleancategory*.shtml: html:91.IntrodCductionsrc:1238 18-18.texThe:questions;A@ cmti12A\WhatV7isV6aprffoof=?"andA\WhenV6areV7twoprffoofstheV7same?"are:fundamenrtal forxproSofxtheoryV.oButforthemostprominenrtlogic,BoSolean(orclassical)propSositionallogic,wrestillhavenosatisfactoryanswers.src:1243 18-18.texThisisnotonlyemrbarrassingforproSoftheoryitself,butalsoforcomputerscience,whereBoSoleanpropositionallogicplarysama jorroleinautomatedreasoningandlogicprogramming.Y1AlsonthedesignmandvrericationofhardwrareisbasedonBoSoleanlogic.Evrery
areainwhichproSofsearchisemployedcanbSenetfromabSetterunderstandingoftheconceptofproSofinBooleanlogic,BandthefamousNP-vrersus-coNPcproblemcanbereducedtothequestionwhetherthereisashort(i.e.,zpSolynomialsize)proSofforevreryBoSoleantautology[%html:CR79 html:].src:1253 18-18.texUsuallyproSofsarestudiedassynrtacticob jectswithinsomedeductivresystem(e.g.,tableaux,@sequenrtw'calculus,resolution,A.T..)._ThispapSertakresw&thepoinrtw&ofviewthatthesesynrtacticFmob jects(alsoFnknownasproSoftrees)shouldbeFnconsideredasconcreterepresen-tationseofcertainabstractproSofob jects,mandethatsucrhanabstractproofob jectcanberepresenrted0=byaresolutionproSoftreeandasequentcalculusproSoftree,UorevenbyseveraldierenrtsequentcalculusproSoftrees.src:1261 18-18.texFVrom athis `pSoinrtofviewthemotivXationforthiswrorkistoprorvideanabstractalgebraic
"!color push gray 0ff ff HE ReceivedUUbytheeditors2006-06-12and,inrevisedform,2007-10-05. T*ransmittedUUbyR.Blute.Publishedon2007-10-18. 2000UUMathematicsSub 8jectClassication:q03B05,03G05,03F03,18D15,18D35. KeyϟwordsϠandphrases:.BoGoleancategory*,^*-autonomouscategory,^proGoftheory,^classicallogic,proGof nets. c
UYLutzUUStraburger,2007.qPermissiontocopyforprivqateusegranted. color pop color push gray 0 ֔536M color pop *˅v{color push gray 0html: html:src:1326 18-18.tex
ONUUTHEAXIOMA*TISATIONUUOFBOOLEANCA*TEGORIESWITHANDWITHOUTMEDIAL(537M color popuK{theory]of]proSofs. AlreadyLamrbek][html:Lam68 html:,html:Lam69 html:]]observredthatsuchan]algebraictreat- menrtcanbSeprovidedbycategorytheoryV. Forthis,kitisnecessarytoacceptthefollowingpSostulatesaboutproofs: color push gray 0!",
cmsy10 color pop_forc evrerycproSofg cmmi12fofconclusionBfromhrypSothesisA(denotedbryfS:
A"8!"7B )and_evreryproSofg7ofconclusionCpfromhrypSothesisBcع(denotedbygÍ: BX!URC ܞ)thereisa_uniquelyhdenedicompSositeproofg
fgofconclusioniCfromhrypothesisiA(denoted_brygÊfS: AUR!C ܞ),color push gray 0 color pop_src:1272 18-18.texthiscompSositionofproofsisassociativre,color push gray 0 color pop_src:1273 18-18.texfor_eacrh_formulaAthere_isanidentityproSof_12 cmmi8Ar:A5!Asucrhthat_forfS:
A!B_wrehavefP1A=URfQ=1B.4fG.src:1277 18-18.texUnder4these5assumptionstheproSofsarethearrorwsinacategorywhoseob jectsaretheformrulae]of]thelogic.Whatremainsistoprorvidetherighrtaxiomsforthe\categoryofproSofs".src:1281 18-18.texItseemsthatndingtheseaxiomsisparticularlydicultforthecaseofBoSoleanlogic.(FVorinrtuitionisticlogic,hPrawitz[ html:Pra71 html:]propSosedthenotionofAprffoofnormalizationforMidenrtifyingMproSofs.b5ItwassoSonMdiscoveredthatthisMnotionofidentityMcoincideswiththeSnotionofidenrtityTthatSresultsfromtheaxiomsofaCartesianclosedcategory(see,e.g.,[%html:LS86 html:]).Infact,onecansarythattheproSofsofintuitionisticlogicarethearrowsintheW'free(bi-)CartesianclosedcategorygeneratedW(brythesetofpropSositionalvXariables.Analternativrewayofrepresentingthearrowsinthatcategoryisviatermsinthesimply-typSed-calculus:arrorwcompSositionisnormalizationofterms.wThisobservXationiswell-knownastheCurry-Horward-correspSondence[html:How80 html:].src:1295 18-18.texInVtheVcaseoflinearlogic,t2therelationto-autonomouscategories[html:Bar79 html:]wrasnoticedimmediatelyafteritsdiscorvery[#html:Laf88 html:,html:See89 html:].SInthesequenrtcalculuslinearlogicproSofsareӕidenrtiedwhenӖtheycanbSetransformedinrtoeachotherviaӖ\trivial"rulepSermutations[html:Laf95 html:].wFVormmrultiplicativellinearlogicthiscoincideswiththeproSofidenrticationsinducedbryktheaxiomslofa-autonomouscategory[html:Blu93 html:,$html:SL04 html:].T)Therefore,\wrecansafelysarythat?ca?bproSofinmrultiplicative?clinearlogicisanarrorwinthefree-autonomouscategorygeneratedbrythepropSositionalvXariables[html:BCST96 html:,&html:LS06 html:,%html:Hug05a html:].src:1306 18-18.texButforclassicallogicnosucrhwell-acceptedcategoryofproSofsexists.\WVecandis-tinguishtrwomainreasons.'First,ifwestartfromaCartesianclosedcategoryandaddanjLinrvolutivejMnegationhtml:2|{Y cmr81 html:,5wegetthejMcollapseintoajMBoSoleanalgebra,5i.e.,anryjMtwoproSofsf ;gÍ: _A
o!B?are:idenrtied.@FVor9everyformula9therewould9bSeatmostoneproSof(see,e.g.,[%html:LS86 html:,p.67]wortheappSendixofv[html:Gir91 html:]fordetails).MAlternativrelyV,startingfroma-autonomousUcategoryandTaddingnaturaltransformationsA{!A^AandUA{!CN cmbx12Ct, i.e.,theproSofsforwreakeningandconrtraction,yieldsthesamecollapse.html:22 html:
"!color push gray 0ff ff HE-
^ٓR cmr71 html: html: i.e.,UUanaturalisomorphismbGetweenUU
b>
cmmi10Aandthedouble-negationofA(inthispaperdenotedbyfx䍑A)
^2 html: html: SinceawearebdealingwithBoGoleanlogic,webwillusethesymbGolsb^andF"V
cmbx10FtforthetensoropGeration (usuallyUU1,
stmary10s)UUandtheunit(usuallyF1orFI)ina-autonomouscategory*. color pop color push gray 0M color pop ˅v{color push gray 0html: html:src:1405 18-18.tex538 HPLUTZUUSTRABURGERM color popuK ύsrc:1322 18-18.texThesecondreasonisthatcuteliminationinthesequenrtcalculusforclassicallogicis not*econ
uenrt.Sincecuteliminationistheusual*fwayofcompSosingproofs,PthismeansthattherejisnocanonicalkwrayjofcompSosingtrwojproofs,letkaloneassociativitryofcomposition.src:1327 18-18.texConsequenrtlyV,ford-avoidingd.thesetwod.problems,wehaved-toacceptthat(i)CartesianclosedcategoriesdonotprorvideanabstractalgebraicaxiomatisationforproSofsinclassicallogic,8andlthatl(ii)thesequenrtcalculusisnottherighrtframeworklforinvestigatingtheidenrtityofproSofsinclassicallogic.src:1333 18-18.texTheredharvealreadydbSeenseveralaccountsfordaproSoftheoryforclassicallogicbasedontheaxiomsofCartesianclosedcategories.-TherstwrereprobablyPrarigot's-calculusr[ html:Prar92 html:]andGirard'sLC[html:Gir91 html:]. iTheworkonpSolarizedproofnetsbryLau-renrt_[ html:Lau99 html:, html:Lau03 html:]showsthatthereisinfactnotmuchdierencebSetweenthetwo.Later,the2category-theoretic1axiomatisationsunderlyingthisproSoftheoryhasbSeenin-vrestigatedqandthecloserelationshiptocontinuations[#html:Thi97 html:,'html:SR98 html:]hasbSeenestablished,culminatinginSelinger'sAcffontrolDcategories[!html:Sel01 html:].Horwever,?bystickingtotheaxiomsofCartesianclosedcategories,onehastosacricethepSerfectsymmetryofBooleanlogic.src:1348 18-18.texInAthispapSer,'wre@willgotheoppositewrayV.InAtheattemptofgoing@fromaBooleanalgebra,`to,_aBoSoleancategorywreinsistonkreepingthesymmetrybSetrween^,`and_.BydoingEthiswrehavetoleavetherealmofCartesianclosedcategories.ThatthisisverywellpSossiblehasrecenrtlybeenshorwnbyseveralauthors[1html:DP04 html:,'html:FP04c html:,)html:LS05a html:].*However,thefact{that{allthreepropSosalsconsiderablydierfromeacrhothersuggeststhattheremighrtbSenocanonicalwrayofgivingacategoricalaxiomatisationforproofsinclassicallogic.src:1358 18-18.texWVeowilloprorvideaseriesofpSossiblesucrhaxiomatisationswithincreasingstrength.Theydwilldallbuildonthestructureofa-autonomouscategoryinwhicrheverydob jecthasa_monoid`(andacomonoid)structure.lInthisrespSectitwillcloselyfollorwthewrorkof['html:FP04c html:]and[)html:LS05a html:],butwilldierfrom[1html:DP04 html:].src:1365 18-18.texThe6approacrh7thatwe7takehere7ismainlymotivXatedbrytheinrvestigation6inthecom-plexitry7cofproSofs.EventuallyV,JagoSod7ctheoryofproSof7didenticationshouldneveridentifytrwoproSofsifoneisexponenrtiallybiggerthantheother.src:1377 18-18.texThe,mainproSof-theoreticinspirationforthiswrork,comesfromthesystemIR6 cmss12ISKS~f[%html:BT01 html:],whicrhAisaAdeductivesystemforBoSoleanlogicAwithintheformalismofthecalculusofstructures[html:Gug07 html:, html:GS01 html:,%html:BT01 html:].iAremarkXablefeatureofthecut-freevrersionofISKS 5,whicrhkisjcalledIKS,wisthatitcan(cut-free)pSolynomiallysimrulatenotonlysequenrtcalculusandtableauxsystemsbutalsoresolutionandFVrege-HilbSertsystems[-html:Gug04a html:,#html:BG07 html:].ThismeansthatifatautologyhasapSolynomialsizeproofin anryofthesesystems,thenithasaCcut-freeCpSolynomialsizeproofCinIKS.NThisabilitryofIKS&isaconsequenceoftrwoCfeatures:html: html:color push gray 0\h1. color pop_src:1389 18-18.texADeffepinference 尹:IInsteads ofdecompSosingtheformrulaealongtheirrootconnectivres_inrtoysubformulaeduringtheconstructionofxaproSof,'OinIKS inferencerulesareapplied_deepinsideformrulaeinthesamewayasweknowitfromtermrewriting.-html: html:color push gray 0\h2. color pop_src:1393 18-18.texThetrwoinferencerulesAswitchXandAmeffdial,whichloSokasfollows:cVW_r html: html: yՍ_5Ff(A_B )^C ܞgEW_r Is_5Ҟ33 ff Tގy_5FfA_(BE^C ܞ)g αand yՍFf(A^B )_(CF^DS)gE Im33 ff u4yFf(A_C ܞ)^(BE_DS)g
;I(1) color push gray 0M color pop *<˅v{color push gray 0html: html:src:1480 18-18.tex
ONUUTHEAXIOMA*TISATIONUUOFBOOLEANCA*TEGORIESWITHANDWITHOUTMEDIAL(539M color popuK{_src:1403 18-18.texwhereFfgstandsforanarbitrary(pSositivre)formulacontextandA,B ,C ܞ,andD _areformrulavXariables.
html: html:L-
cmcsc10LFromdeepinferencetoalgebra.src:1409 18-18.texDeepinferenceallorwsustoestablishtherela-tionshipTbSetrweenproSoftheorySandalgebrainamuchcleanerwaySthanthisispSossiblewithEshallorwinferenceformalismslikethesequentcalculus.ThereasonisthatfromaderivXationinadeepinferenceformalismonecandirectly\readothemorphisms".TVakreforexamplethefollorwingderivXationinsystemIKSֹ:+ y html: html:>Ս 5R(A2K cmsy80x^B )_(CF^DS)E Ir 5R33 ff by n(A^B )_(CF^DS)E y Im n33 ff _Ǝy n(A_C ܞ)^(BE_DS)I(2),dsrc:1420 18-18.texwhereA,/A209,0B ,C ܞ,andD`arearbitraryformrulae,0andIrљisanryinferenceruletakingA20vtoA.8Incategory-theoreticlanguagethiswrouldbSewrittenasacompositionofmaps:T (A20x^B )_(CF^DS)y (Js6 cmss8Jr9^Bd)_(C ^D