Complete Categorical Deduction for Satisfaction as Injectivity
Joseph Goguen was my ( Grigore's) PhD adviser at the University of California at San Diego (UCSD) during the period October 1996 to August 2000. We also collaborated frequently after I finished my PhD. A Symposium to honor Joseph Goguen on his 65th birthday on June 28, 2006 was held at the Department of Computer Science and Engineering at UCSD in June 27–29, 2006. I warmly dedicate the paper below to Joseph, for his teachings and friendship.
- Complete Categorical Deduction for Satisfaction as Injectivity
- Grigore Rosu
- Festschrift in Honor of Joseph Goguen, LNCS 4060, pp 157-172. 2006.
- 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.