Structuring theories on consequence

Building on the work of Goguen and Burstall on institutions and on Tarski's notion of deductive system, a categorial framework for manipulating theories in an arbitrary logic is presented. Its main contribution is the formalisation of the semantics of theory-building operations on top of a consequence relation. For that purpose, the notion of π-institution is proposed as an alternative to the notion of institution, replacing the notions of model and satisfaction by a primitive consequence operator in the definition of a logic. The resulting approach to the semantics of specification languages is intrinsically different from the original one in the sense that the ultimate denotation of a specification is taken herein to be a class of theories (sets of formulae closed for the consequence relation) and not a class of models of that logic. Adopting this point of view, the semantics of Clear-like specification building operations is analysed.