Repository | Series | Book | Chapter
Complete categorical deduction for satisfaction as injectivity
pp. 157-172
Abstract
Birkhoff (quasi-)variety categorical axiomatizability results have fascinated many scientists by their elegance, simplicity and generality. The key factor leading to their generality is that equations, conditional or not, can be regarded as special morphisms or arrows in a special category, where their satisfaction becomes injectivity, a simple and abstract categorical concept. A natural and challenging next step is to investigate complete deduction within the same general and elegant framework. We present a categorical deduction system for equations as arrows and show that, under appropriate finiteness requirements, it is complete for satisfaction as injectivity. A straightforward instantiation of our results yields complete deduction for several equational logics, in which conditional equations can be derived as well at no additional cost, as opposed to the typical method using the theorems of constants and of deduction. At our knowledge, this is a new result in equational logics.
Publication details
Published in:
Futatsugi Kokichi, Jouannaud Jean-Pierre, Meseguer José (2006) Algebra, meaning, and computation: essays dedicated to Joseph A. Goguen on the occasion of his 65th birthday. Dordrecht, Springer.
Pages: 157-172
DOI: 10.1007/11780274_9
Full citation:
Roşu Grigore (2006) „Complete categorical deduction for satisfaction as injectivity“, In: K. Futatsugi, J. Jouannaud & J. Meseguer (eds.), Algebra, meaning, and computation, Dordrecht, Springer, 157–172.