Complete Categorical Deduction for Satisfaction as Injectivity

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 ract 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.

• Type: Conference
• Year: 2006
• Where: BIRTHDAY
• Authors: Grigore Rosu
• Keywords: Applied Computing, BIRTHDAY 2006, Complete Deduction, Equational Logics, Quasi-)variety Categorical Axiomatizability