nLab
institution

Contents

Context

Model theory

Category theory

Contents

Idea

The concept of an institution provides an abstract category-theoretic rendering of the informal concept of a logical system. It was introduecd by Burstall and Goguen in the 1970s in order to get a grip on the proliferation of specification logics in programming and constitutes a genuine contribution of theoretical computer science to general logic and abstract model theory.

Definition

Definition

An institution is a quadruple Σ,S,M,\langle\Sigma , S, M, \models\rangle with

  • Σ\Sigma a category of “signatures”,

  • S:ΣSetS:\Sigma\to Set a functor assigning to an object XΣX\in \Sigma the set S(X)S(X) of “sentences” of signature XX ,

  • M:Σ opCatM:\Sigma^{op} \to Cat is a functor assigning to an object XΣ opX\in\Sigma^{op} the category of “X-structures” and

  • \models is a family of “satisfaction” relations specifying for each signature XX and XX-structure 𝔄\mathfrak{A} the set of sentences Th(𝔄)S(X)Th(\mathfrak{A})\subseteq S(X) “holding in 𝔄\mathfrak{A}”,

subject to the following satisfaction condition:

Given a morphism of signatures φ:XX\varphi:X\to X' and a sentence eS(X)e\in S(X), the sentence S(φ)(e)S(\varphi)(e) i.e. the “φ\varphi-translation” of ee into an XX'-sentence, holds in a X’-structure 𝔄\mathfrak{A}' (in signs: 𝔄S(φ)(e)\mathfrak{A}'\models S(\varphi)(e)) precisely if ee holds in M(φ)(𝔄)M(\varphi)(\mathfrak{A}'):

𝔄S(φ)(e)iffM(φ)(𝔄)e. \mathfrak{A}'\models S(\varphi)(e) \; iff \; M(\varphi)(\mathfrak{A}')\models e\quad .

Examples

Applications

References

One of the original sources is

  • J. Goguen, R. Burstall, Institutions: Abstract model theory for specification and programming , J. ACM 39 no.1 (1992) pp.95–146. (ps-preprint)

A high level introduction

A monograph on the subject is

  • Răzvan Diaconescu, Institution-independent Model Theory , Birkhäuser Basel 2008.

More specific research papers are

  • M. Aiguier, F. Barbier, An institution-independent Proof of the Beth Definability Theorem , Studia Logica 85 no. 3 (2007) pp.333-359. (pdf)

  • Răzvan Diaconescu, Grothendieck institutions , App. Cat. Struc. 10 no.4 (2002) pp.383–402.

  • Lucanu, D., Li, Y. F., & Dong, J. S. (2006). Semantic web languages–towards an institutional perspective. In Algebra, Meaning, and Computation (pp. 99-123). Springer, Berlin, Heidelberg. (pdf)

  • Bao, J., Tao, J., McGuinness, D. L., & Smart, P. (2010). Context representation for the semantic web. (pdf)

Last revised on September 21, 2018 at 11:27:40. See the history of this page for a list of all contributions to it.