A 2-categorial generalization of the concept of institution (Q993499)

The theory of institutions was started about three decades ago by Goguen and Burstall as a categorical abstract model theory in order to provide a general uniform model-theoretic framework for developing concepts and result in computer science and logic in a way that is free from the often irrelevant details of concrete logical systems. Such concepts and results would be thus applicable to a wide variety of logical systems. The central concept of institution theory is that of an institution, which provides a category-theoretic formalization for the notion of logical system that includes syntax, semantics, and the satisfaction relation between them. This paper refines the traditional concepts of institution with a 2-categorical dimension by replacing the signatures category by a 2-category, the model and sentence functors with pseudo-functors and the satisfaction relation by a pseudo-extranatural transformation. The authors present at length a motivating example which represents a 2-categorical extension of the equational logic institution.