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 attempts to "formalize the informal" concept of logical system.
[1] The use of institutions makes it possible to develop concepts of specification languages (like structuring of specifications, parameterization, implementation, refinement, and development), proof calculi, and even tools in a way completely independent of the underlying logical system.
There are also morphisms that allow to relate and translate logical systems.
Important applications of this are re-use of logical structure (also called borrowing), and 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.
[2][3] The theory of institutions does not assume anything about the nature of the logical system.
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 (called signature) that defines the (non-logic) symbols that may be used in sentences and that need to be interpreted in models.
Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved.
The satisfaction condition expresses that truth is invariant under change of notation (and also under enlargement or quotienting of context).