The Completeness Theorem for Monads in Categories of Sorted Sets

• Autores: Juan Carlos Soliveres Tur, Joan B. Climent Vidal
• Localización: Houston journal of mathematics, ISSN 0362-1588, Vol. 31, Nº 1, 2005, págs. 103-130
• Idioma: inglés
• Texto completo no disponible (Saber más ...)
• Resumen

  • Birkhoff's completeness theorem of equational logic 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 finitary many-sorted equational deduction, generalized the completeness theorem of Birkhoff to the completeness of finitary many-sorted equational logic and provided simultaneously a full algebraization of finitary many-sorted equational deduction. In this paper, after defining the concepts of equational class and equational theory for a monad in a category of sorted sets and the concept of projective limit-compatible congruence on a category, we prove that the lattice of product-compatible congruences on the dual of the Kleisli category of a monad in a category of sorted sets is identical to the lattice of equational theories for the same monad. In this way we obtain a completeness theorem for monads in categories of sorted sets, and therefore independent of any explicit syntactical representation of the relevant concepts, that generalizes the completeness theorem of Goguen-Meseguer and provides a full categorization of many-sorted equational deduction.