Central and East European
Society for Phenomenology

Repository | Series | Book | Chapter

225391

Complete categorical deduction for satisfaction as injectivity

Grigore Roşu

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.