The notion of institution was created by Joseph Goguen and Rod Burstall in the late 1970s, in order to deal with the "population explosion among the logical systems used in computer science". The notion tries to capture the essence of the concept of "logical system". The use of institutions makes it possible to develop concepts of specification languages, proof calculi and even tools in a way completely independent of the underlyinglogical system. There are also morphisms that allow to relate and translate logical systems. Important applications of this are re-use of logical structure, heterogeneous specification and combination of logics. The spread of institutional model theory has generalized various notions and results of model theory, and institutions themselves have impacted the progress of universal logic.
Definition
The theory of institutions does not assume anything about the nature of the logical system. That is, models and sentences may be arbitrary objects; the only assumption is that there is a satisfaction relation between models and sentences, telling whether a sentence holds in a model or not. Satisfaction is inspired by Tarski's truth definition, but can in fact be any binary relation. A crucial feature of institutions is that models, sentences, and their satisfaction, are always considered to live in some vocabulary or context that defines the symbols that may be used in sentences and that need to be interpreted in models. Moreover, signature morphisms allow to extend signatures, change notation, and so on. Nothing is assumed about signatures and signature morphisms except that signature morphisms can be composed; this amounts to having a category of signatures and morphisms. Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved. While sentences are translated along with signature morphisms, models are translated against signature morphisms: for example, in case of a signature extension, a model of the target signature may be reduced to a model of the source signature by just forgetting some components of the model. Formally, an institution consists of
a category of signatures,
a functorSet giving, for each signature, the set of sentences, and for each signature morphism, the sentence translation map, where often is written as,
a functor Cat giving, for each signature, the category of models, and for each signature morphism, the reduct functor, where often is written as,
such that for each in the following satisfaction condition holds: if and only if for each and. The satisfaction condition expresses that truth is invariant under change of notation . Strictly speaking, the model functor ends in the "category" of all large categories.
