nLab institution

Idea

The concept of an institution provides an abstract category-theoretic rendering of the informal concept of a logical system. It was introduced 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 $\langle\Sigma , S, M, \models\rangle$ with

• $\Sigma$ a category of “signatures”,

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

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

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

subject to the following satisfaction condition:

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

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

Examples

…

Applications

…

Related entries

• abstract model theory

• Beth definability theorem

• Grothendieck fibration

• signature

• computer science

• Joseph Goguen

Links

• The late Joseph Goguen’s page on institutions.

• A Bremen based community homepage: Flirts.

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

• Răzvan Diaconescu, Institution Theory, Internet Encyclopedia of Philosophy

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)