Formally, an institution consists of
- 'Sign' a category of signatures,
- a functor sen:Sign -> Set giving, for each signature Σ, the set of sentences sen(Σ), and for each signature morphismΣ:Σ ->Σ', the sentence translation map sen(σ):sen(Σ) -> sen(Σ'), where often sen(σ)(φ) is written as Σ(φ),
- a functor Mod:Sign^{op} -> Cat giving, for each signatureΣ, the category of models Mod(Σ), and for each signature morphismΣ:Σ ->Σ', the reduct functor Mod(σ):Mod(Σ') -> Mod(Σ), where often Mod(σ)(M') is written as M'|_{σ},
- a satisfaction relation {\models_{Σ}}\subseteq|{Mod(Σ)|× sen(Σ)} for eachΣ\in Sign,
see this Wiki page.
