Institution (computer Science)
   HOME

TheInfoList



OR:

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. 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
morphism In mathematics, particularly in category theory, a morphism is a structure-preserving map from one mathematical structure to another one of the same type. The notion of morphism recurs in much of contemporary mathematics. In set theory, morphisms a ...
s 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 :''This page is about the concept in mathematical logic. For the concepts in sociology, see Institutional theory and Institutional logic''. In mathematical logic, institutional model theory generalizes a large portion of first-order model theory to ...
has generalized various notions and results of
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
, 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 (called signature) that defines the (non-logic) 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 (think of symbols being replaced along the morphism), models are translated (or better: reduced) against signature morphisms. For example, in the case of a signature extension, a model of the (larger) target signature may be reduced to a model of the (smaller) source signature by just forgetting some components of the model. Let \mathbf^ denote the opposite of the category of small categories. An institution formally consists of * a category \mathbf of signatures, * a functor \mathit \colon \mathbf \to \mathbf giving, for each signature \Sigma, the set of sentences \mathit(\Sigma), and for each signature morphism \sigma \colon \Sigma \to \Sigma', the sentence translation map \mathit(\sigma) \colon \mathit(\Sigma) \to \mathit(\Sigma'), where often \mathit(\sigma)(\varphi) is written as \sigma(\varphi), * a functor \mathbf \colon \mathbf \to \mathbf^ giving, for each signature \Sigma, the category of models \mathbf(\Sigma), and for each signature morphism \sigma \colon \Sigma \to \Sigma', the reduct functor \mathbf(\sigma) \colon \mathbf(\Sigma') \to \mathbf(\Sigma), where often \mathbf(\sigma)(M') is written as M', _, * a satisfaction
relation Relation or relations may refer to: General uses *International relations, the study of interconnection of politics, economics, and law on a global level *Interpersonal relationship, association or acquaintance between two or more people *Public ...
\subseteq, for each \Sigma \in \mathbf, such that for each \sigma \colon \Sigma \to \Sigma' in \mathbf, the following satisfaction condition holds: M' \models_ \sigma(\varphi) \quad\text\quad M', _ \models_ \varphi for each M' \in \mathbf(\Sigma') and \varphi \in \mathit(\Sigma). The satisfaction condition expresses that truth is invariant under change of notation (and also under enlargement or quotienting of context). Strictly speaking, the model functor ends in the "category" of all large categories.


Examples of institutions

* Common logic * Common Algebraic Specification Language (CASL) * First-order logic * Higher-order logic * Intuitionistic logic *
Modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
* Propositional logic * Temporal logic * Web Ontology Language (OWL)


See also

*
Abstract model theory In mathematical logic, abstract model theory is a generalization of model theory that studies the general properties of extensions of first-order logic and their models. Abstract model theory provides an approach that allows us to step back and stu ...
*
Institutional model theory :''This page is about the concept in mathematical logic. For the concepts in sociology, see Institutional theory and Institutional logic''. In mathematical logic, institutional model theory generalizes a large portion of first-order model theory to ...
* Universal logic


References


Further reading

* . This was the first publication on institution theory and the preliminary version of Goguen and Burstall (1992). * * * *


External links

* *
''Formalism, Logic, Institution - Relating, Translating and Structuring''
Includes large bibliography. *{{citation , publisher=Simion Stoilow Institute of Mathematics of the Romanian Academy , url=http://www.imar.ro/~diacon/publications.html#Institutions__institution-independent , last1=Răzvan Diaconescu , title=Selected Publications , access-date=January 31, 2021. Contains recent work on institutional model theory. Theoretical computer science Model theory