Graph-Based Logic and Sketches II Finite-Product C

arXiv:math/9612220v1[math.LO]19Dec1996GRAPH-BASEDLOGICANDSKETCHESII:FINITE-PRODUCTCATEGORIESANDEQUATIONALLOGIC(PRELIMINARYREPORT)ATISHBAGCHIANDCHARLESWELLSAbstract.Itisshownthattheprooftheoryforsketchesandformsprovidedin[BagchiandWells,1996]isstrongenoughtoproduceallthetheoremsoftheentail-mentsystemformultisortedequationallogicprovidedin[GoguenandMeseguer,1982].1.IntroductionIn[Wells,1990]thesecondauthorintroducedthenotionofform,agraph-basedmethodofspecificationofmathematicalstructuresthatgeneralizesEhresmann’ssketches.In[BagchiandWells,1996],theauthorsproducedastructureforformswhichprovidesauniformprooftheorybasedonfinite-limitconstructionsformanytypesofforms,includingalltypesofsketchesandalsoformsthatcanspecifyhigher-orderstructuresincartesianclosedcategoriesandtoposes(amongmanyothers).Theparameterintheprooftheorythatdeterminesthetypesofconstructionsthatcanbemadeistheconstructorspace.Forexample,theconstructorspaceforcarte-sianclosedcategories(withspecifiedstructure)isthefinite-limittheoryCCCforcartesianclosedcategories.Inparticularfortheconcernsofthepresentpaper,theconstructorspaceforstructuresthatcanbespecifiedbyfiniteproductsisafinite-limittheoryFinProdforcategorieswithspecifiedfiniteproducts.Thistheoryisdescribedexplicitlyin[BagchiandWells,1996].EachfiniteproductformFisgivenbyasyntacticcategorydenotedbySynCat[FinProd,F].Thelogicalstructurein[BagchiandWells,1996]identifiesastatementasapotentialfactorizationinSynCat[FinProd,F],whichisadiagramoftheformhypclaimconclaimhypcon//wksp(1)ResearchatMSIissupportedinpartbyNSFgrantDMS-9022140.12ATISHBAGCHIANDCHARLESWELLSandthetheoremthatthegivenstatementistrueasanactualfactorizationhypclaimconclaimverifxxxxxxxxxxxxxhypcon//wkspofthediagram(1).In[GoguenandMeseguer,1982],GoguenandMeseguerproducedasoundandcompleteentailmentsystemformultisortedequationallogic.Inthispaper,weverifythatthetheoremsofthatlogicforaparticularsignatureandequationsalloccurasactualfactorizationsinSynCat[FinProd,F],whereFisaFinProdforminduced(inamannertobedescribed)bythegivensignatureandequations.Wealsocomparetheexpressivepowersofthesetwosystems.2.Preliminaries2.1.Lists.GivenasetA,List[A]denotesthesetoflistsofelementsofA,includingtheemptylist.ThekthentryinalistwofelementsofAisdenotedbywkandthelengthofwisdenotedbyLength[w].Therangeofw,denotedbyRng[w],isthesetofelementsofAoccurringasentriesinw.Iff:A→Bisafunction,List[f]:List[A]→List[B]isbydefinitionf“mappedover”List[A]:IfwisalistofelementsofA,thenthekthentryofList[f](w)isbydefinitionf(wk).ThismakesListafunctorfromthecategoryofsetstoitself.2.2.Signatures.2.2.1.Expressionsandterms.Inthedescriptionthatfollowsofthetermsandequa-tionsforasignature,weuseanotationthatspecifiesthevariablesofatermorequationexplicitly.Inparticular,onemayspecifyvariablesthatdonotactuallyappearintheexpression.Forthisreason,theformalismweintroduceinthedefini-tionsbelowdistinguishesanexpressionsuchasf(x,g(y,x),z)fromaterm,whichisanexpressiontogetherwithaspecifiedsetoftypedvariables;inthiscasethatsetcouldbeforexample{x,y,z,w}.Thisformalismisequivalenttothatof[GoguenandMeseguer,1982].2.2.2.Definition.Apair(Σ,Ω)ofsetstogetherwithtwofunctionsInp:Ω→List[Σ]andOutp:Ω→Σiscalledasignature.GivenasignatureS:=(Σ,Ω),elementsofΣarecalledthetypesofSandtheelementsofΩarecalledtheoperationsofS.2.2.3.Notation.GivenasignatureS=(Σ,Ω),wewilldenotethesetΣoftypesbyTypes[S]andthesetΩofoperationsbyOprns[S].Foranyf∈Ω,thelistInp[f]iscalledtheinputtypelistoffandthetypeOutp[f]istheoutputtypeoff.2.2.4.Remark.Theinputtypelistoffisusuallycalledthearityoff,andtheoutputtypeoffisusuallycalledsimplythetypeoff.GRAPH-BASEDLOGICANDSKETCHESII32.2.5.Definition.AnoperationfofasignatureSiscalledaconstantifandonlyifInp[f]istheemptylist.2.2.6.Definition.AtypeγofasignatureSissaidtobeinhabitedifandonlyifeithera)thereisaconstantofoutputtypeγinS,orb)thereisanoperationfofoutputtypeγforwhicheverytypeinInp[f]isinhab-ited.Thetypeγissaidtobeemptyifandonlyifitisnotinhabited.2.3.Termsandequations.Inthissection,wedefinethetermsandequationsofagivensignature.2.3.1.Assumptions.Inthesedefinitions,wemakethefollowingassumptions,usefulforbookkeepingpurposes.A.1WeassumethatwearegivenasignatureSforwhichTypes[S]={σi|i∈I}forsomeordinalI.A.2Foreachi∈I,weassumethereisanindexedsetVbl[σi]:={xij|j∈ω}whoseelementsarebydefinitionvariablesoftypeσi.Inthissetting,xijisthejthvariableoftypeσi.A.3Thesetofvariablesisorderedbydefiningxijxkl:⇔(eitherikori=kandjlWealsodefineVbl[S]:=∪i∈ωVbl[σi].2.3.2.Definition.Foranytypeτ,anexpressionoftypeτisdefinedrecursivelyasfollows.Expr.1Avariableoftypeτisanexpressionoftypeτ.Expr.2IffisanoperationwithInp[f]=(γi|i∈1..n)andOutp[f]=τ,and(ei|i∈1..n)isalistofexpressionsforwhicheacheiisoftypeγi,thenf(ei|i∈1..n)isanexpressionoftypeτ.2.3.3.Notation.ThetypeofavariablexisdenotedbyType[x],sothatinthenotationof2.3.1,Type[xij]=σi.Thisnotationwillbeextendedtoincludelistsandsetsofvariables:IfW:={x12,x13,x21,x32},thenType[W]=σ1×σ1×σ2×σ3.(NotethatthisdependsontheorderinggivenbyA.1.)ThetypeofanexpressionewillbedenotedbyType[e].ThusthefunctionTypeisoverloaded:i