On the completeness theorem of many-sorted equational logic and the equivalence between Hall algebras and Binabou theories

• Autorzy: Vidal J. , Tur J.
• Języki publikacji: EN

Abstrakty

EN

The completeness theorem of equational logic of Birkhoff asserts the coincidence of the model-theoretic and proof- theoretic consequence relations. Goguen and Meseguer, giving a sound and adequate system of inference rules for many-sorted deduction, founded ultimately on the congruences on Hall algebras, generalized the completeness theorem of Birkhoff to the completeness theorem of many-sorted equational logic. In this paper, after simplifying the specification of Hall algebras as given by Goguen-Meseguer, we obtain another many-sorted equational calculus from which we prove that the inference rules of abstraction and concretion due to Goguen-Meseguer are derived rules. Finally, after defining the Bienabou algebras for a set of sorts S we prove that the category of Bienabou algebras for S is equivalent to the category of Hall algebras for S and isomorphic to the category of Bienabou theories for S, i.e., the many-sorted counterpart of the category of Lawvere theories, hence that Hall algebras and Bienabou theories are equivalent.

Słowa kluczowe

EN

Hall algebra; Binabou algebra; Many-sorted algebra; term; equation; many-sorted equanational completness; Binabou theory

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2006
• Tom: Nr 40
• Strony: 127--158
• Opis fizyczny: Bibliogr. 5 poz.

Twórcy

autor

Vidal J.

autor

Tur J.

• Universidad de Valencia Departamento de Logica y Filosofia de la Ciencia E-46071 Valencia, Spain,

Bibliografia

• [1] J. Bénabou, Structures algebriques dans les categories, Cahiers de Topologie et Géometrie Différentielle, 10 (1968), pp. 1-126.
• [2] G. Birkhoff, On the structure of abstract algebras, Proceedings of the Cambridge Philosophical Society, 31 (1935), pp. 433-454.
• [3] J. Climent and J. Soliveres, On the morphisms and transformations of Tsuyoshi Fujiwara (as a concretion of a bidimensional many-sorted general algebra and its application to the equivalence between clones and algebraic theories), manuscript, 2002.
• [4] J. Goguen and J. Meseguer, Completeness of many-sorted equational logic, Houston Journal of Mathematics, 11 (1985), pp. 307-334.
• [5] F. W. Lawvere, Functorial semantics of algebraic theories, Dissertation. Columbia University, 1963.