A 2-CATEGORICAL FRAMEWORK FOR THE SYNTAX AND SEMANTICS OF MANY-SORTED EQUATIONAL LOGIC

作者：Climent Vidal Juan; Soliveres Tur Juan

来源：Reports on Mathematical Logic, 2010, 45: 37-95.

• Many-sorted set
• many-sorted algebra
• Ehresmann-Grothendieck construction
• Kleisli category for a monad
• many-sorted term
• clone
• many-sorted algebraic theory
• Hall algebra
• Benabou algebra
• polyderivor
• transformation of polyderivors

For, not necessarily similar, single-sorted algebras Fujiwara defined, through the concept of family of basic mapping-formulas between single-sorted signatures, a notion of morphism which generalizes the ordinary notion of homomorphism between algebras. Subsequently he also defined an equivalence relation, the relation of conjugation, on the families of basic mapping-formulas. In this article we extend the theory of Fujiwara to the, not necessarily similar, many-sorted algebras, by defining the concept of polyderivor between many-sorted signatures under which are subsumed the standard signature morphisms, the derivors of Goguen-Thatcher-Wagner, and the basic mapping-formulas of Fujiwara. After this, by means of the homomorphisms between Benabou algebras, we define the composition of polyderivors from which we get the category Sig(p partial derivative), of many-sorted signatures and polyderivors. Next, by defining the notion of transformation between polyderivors, which generalizes the relation of conjugation of Fujiwara, we endow the category Sig(p partial derivative) with a 2-category structure. From this we obtain a 2-category Spf(p partial derivative), of many-sorted specifications, in which we prove that, for every set of sorts S, the specifications B-S, of Benabou for S, and H-S, of Hall for S, are equivalent, and, after defining a pseudo-functor Alg(p partial derivative)(sp) from Spf(p partial derivative) to Cat, we prove that, for every set of sorts S, the categories Alg(H-S), of Hall algebras for S, and Alg(B-S), of Benabou algebras for S, are equivalent. These last equivalences were used in an earlier article to give an alternative proof of the Completeness Theorem of many-sorted Equational Logic based on the categories Alg(B-S), which are isomorphic to the categories BThf(S), of finitary many-sorted algebraic theories for S. Therefore, in this case, Alg(p partial derivative)(sp) provides a justification for the existence of such alternative proofs.

• 出版日期2010