1. Motivation

The enormous and still growing diversity of logics used in computer science presents a formidable challenge. One approach to bringing some order to this chaos is to formalize the notion of "a logic" and then systematically study general properties of logics using this formalization, including the representation, implementation, and translation of logics. This is the purpose of the theory of institutions, as developed and applied in a literature that now has hundreds of papers.

The original application of institutions defined powerful mechanisms for structuring theories over any logical system; this was applied in the module systems of languages in the OBJ family, including BOBJ, CafeOBJ, Maude, CASL, and OBJ3, each of which has a different logic, under the name "parameterized programming," and it was later extended to module systems for programming languages. The module systems of Ada, C++, Lotos, and ML were all influenced by these ideas, which are most nearly fully implemented in the so-called signatures, structures, and functors of SML.

Institutions have also been applied to the semantics of databases and ontologies, e.g. for the semantic web. Here the main contribution of institutions is to formalize the notion of translation from one logic to another in such as way as to preserve truth, and to provide a number of basic results about such translations, such as when they preserve the modular structure of an ontology; see Data, Schema, Ontology, and Logic Integration.

My own recent research applies ideas from institution theory to cognitive linguistics and cognitive semantics. For example, Information Integration in Institutions brings the symbolic conceptual spaces of Fauconnier and the geometrical conceptual spaces of Gardenfors into a single unified framework by viewing the latter as models of the former; this requires extending theories beyond logic to include elements of continuous mathematics, such as derivatives. A detailed analysis of some metaphors of time as space is given in Mathematical Models of Cognitive Space and Time.

Many logical systems have been shown to be institutions, including first order logic (with first order structures as models), many sorted equational logic (with abstract algebras as models), Horn clause logic, many variants of higher order and of modal logic, and much more. Institutions are also increasingly used in mathematical logic, e.g., in the study of fibring, which is a (originally non-institutional) way of combining logics due to Dov Gabbay, and in the study of institution independent logical properties. Logical results obtained include very general versions of Craig interpolation, Robinson consistency, Beth definability, and Herbrand universe theorems; these results cover all logics where these results are known, and yield new results for many other logics, e.g. in research by Rãzvan Diaconescu and his students. Recent work is adding support for proof theory to institutions, by treating proofs as morphisms of sentences; see What is a Logic? for some details.

2. Introduction

Tarski's "semantic definition of truth" provides a familiar starting point for understanding the formal notion of institution (but see also the short philosophical discussion of institutions and Peirce's triadic semiotics). The most significant ingredient of Tarski's approach is a relation of satisfaction between first order sentences and models, denoted |=. For example, Tarski defined the semantics of conjunction with a formula like

M |= (P and Q)   =   (M |= P) & (M |= Q)
where (just for the moment) "and" is syntactic conjunction, "&" is semantic conjunction, M is a model, and P,Q are formulae. Institutions generalize and abstract this dyadic satisfaction to a triadic relation for arbitrary logics.

Many applications of logic, especially in computer science, require the vocabularies from which sentences are built (such as predicate and function symbols) to vary from one case to another in such a way that truth is conserved under translations among such vocabularies. This requires formalizing the notions of vocabulary and of translations among vocabularies, as well as the effects of such translations on sentences and models, each of which must be conceived of as parameterized by the vocabularies that they use.

Institutions accomplish this formalization by passing from "vocabularies" to signatures, which are abstract objects, and from "translations among vocabularies" to abstract mappings between objects, called signature morphisms; then the parameterization of sentences by signatures is given by as assignment of a set Sen(S) of sentences to each signature S, and a translation Sen(f) from Sen(S) to Sen(S') for each signature morphism f: S -> S', while the parameterization of models by signatures is given by an assignment of a class Mod(S) of models for each signature S, and a translation Mod(S') -> Mod(S) for each f: S -> S' (please note the contravariance here). More technically, an institution consists of an abstract category Sign, the objects of which are signatures, a functor Sen: Sign -> Set, and a contravariant functor Mod: Sign -> Setop (more technically, we might uses classes instead of sets here). Satisfaction is then a parameterized relation |=S between Mod(S) and Sen(S), such that the following satisfaction condition holds, for any signature morphism f: S -> S', any S-model M, and any S'-sentence e:

M |=S f(e)   iff   f(M) |=S' e
This condition expresses the invariance of truth under change of notation.

Some of the first, and most useful, results in the theory of institutions concern the duality between theories and model classes. Given a signature S, an S-theory is a set of S-sentences, and an S-model class is a class of S-models. Every S-theory T determines an S-model class T, which contains all the S-models that satisfy all its sentences, and every S-model class V determines an S-theory V, which contains all the S-sentences satisfied by all the models in V. These two operations define the particular kind of duality between model classes and theories that is known as a Galois connection, and the closure of a theory T is the theory T••, while the closure of a model class V is V••. A theory is closed iff it equals its closure; intuitively, a closed theory already contains all the consequences of its sentences. Among many small results that can be proved is the fact that the closure of a closed theory (or model class) is equal to itself.

An institution morphism from an institution I to another I' consists of a functor F: Sign -> Sign', a natural transformation a: F;Sen' => Sen, and a natural transformation b: Mod => F;Mod', such that, for any S-model M and F(S)-sentence e,

M |=S aS(e)   iff   bS(M) |=F(S) e
The intuition for institution morphisms is that they are truth preserving translations from one logical system to another. More technically, for any signature S, letting S' = F(S), then aS maps S-sentences to S'-sentences, and bS maps S'-models to S-models, in a way that is consistent with respect to the satisfaction relation. One important class of examples consists of inclusion institution morphisms, for which F, aS and bS are each an inclusion. For example, there is an inclusion morphism from Horn clause logic to first order logic. A more general notion of subinstitution allows these functions to be injective. An example is the translation from (many sorted) equational logic into (unsorted) first order logic, in which equality is treated as a special relation. Of course, there are many other examples; and there are also many examples that are not subinstitution morphisms. In addition, there are several variants of the institution morphism notion, useful under different circumstances, one of which is the co-morphism (see Institution Morphisms).

3. Some Local Literature

The following are links to some relevant material available at UCSD; the third to last is the basic paper on institutions.

  1. [New] Three Flirtations, abstract of talk at the Fifth FLIRTS Meeting, 1-2 October 2005, in Bremen, Germany. (FLIRTS is an acronym for "Formalism, Logic, Institution - Relating, Translating and Structuring".) The slides for the presentation by Till Mossakowski and Joseph Goguen, on An Institutional View on the Curry-Howard-Tait Isomorphism are also available.
  2. [New] Mathematical Models of Cognitive Space and Time, constructs mathematical models for reasoning about space and time, and metaphors of time as space, using the language of unified concept theory, especially frames and frame blending. Slides of talk Mathematical models of cognitive space and time at University of Bremen, Center for Research on Spatial Cognition, 30 September 2005, Bremen, Germany (does not have the most recent results, but does have some pictures).
  3. [Newly Revised] What is a Logic?, by Till Mossakowski, Joseph Goguen, Razvan Diaconescu, and Andrzej Tarlecki, Logica Universalis, ed. Jean-Yves Beziau (Birkhauser, 2005), pages 113-133. Proceedings of First World Conference on Universal Logic, 26 March to 3 April 2005, Montreaux, Switzerland. Defines an equivalence relation on institutions such that the equivalence classes define a notion of "a logic"; in addition, several interesting invariants are defined for this notion, including a new Lindenbaum category construction and a model cardinality spectrum. To handle proof theory, traditional categorical logic is extended to use sets of sentences instead of single sentences as objects.
  4. [Newly Revised] Information Integration in Institutions, for Jon Barwise memorial volume edited by Larry Moss, Indiana University Press. This paper unifies and/or generalizes several approaches to information, including the information flow theory of Barwise and Seligman, the formal conceptual analysis of Wille, the lattice of theories approach of Sowa, the categorical general systems theory of Goguen, and the cognitive semantic theories of Fauconnier, Turner, Gardenfors, and others. Its rigorous approach uses category theory to achieve independence from any particular choice of representation, and institutions to achieve independence from any particular choice of logic. Corelations, cocones, and colimits over arbitrary diagrams provide a very general formalization of information integration, and Grothendieck constructions extend this to several kinds of heterogeneity. Examples from databases, ontologies, cognitive semantics and other areas are treated. An unusual way to institutionalize databases is given in an appendix, inspired by C.S. Peirce's triadic semiotics. A postscript version is also available.
  5. [New] Data, Schema, Ontology, and Logic Integration, to appear in book edited by Walter Carnielli, Miguel Dionisio, and Paulo Mateus; postscript version also available. Extended abstract appears in Proceedings, CombLog'04 Workshop, edited by Walter Carnielli, Miguel Dionisio, and Paulo Mateus, pages 21-31; held 28-30 July 2004, in Lisbon, Portugal; keynote address. Motivation and theory for a "data integration chain," from data to schema to ontology to ontology language to ontology logic integration; main new ideas are abstract schema, abstract schema species, and abstract schema morphism.
  6. Institution Morphisms, by Joseph Goguen and Grigore Rosu, in Formal Aspects of Computing 13, 2002, pages 274-307; special issue edited by Don Sannella, in honor of the retirement of Rod Burstall. This paper brings greater order to the chaotic menagerie of different genres and species of morphisms between institutions, by exploring their basic properties and some important relationships among them, and by giving them systematic suggestive names.
  7. Composing Hidden Information Modules over Inclusive Institutions, by Joseph Goguen and Grigore Rosu. Semantics for specification combining operations that can hide information; necessary and sufficient conditions for using only visible consequences of hidden information to be safe; applications to programming language module systems. In From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl, Springer Lecture Notes in Computer Science, vol. 2635, edited by Olaf Owe, Stein Krogdahl and Tom Lyche, 2004, pages 96-123.
  8. An Implementation-Oriented Semantics for Module Composition, by Joseph Goguen and Will Tracz, in Foundations of Component-based Systems, edited by Gary Leavens and Murali Sitaraman, Cambridge, April 2000, pages 231-263. Considers horizontal and vertical module composition, with laws relating them, using a purely set theoretic version of institutions, in a way that applies to any imperative programming, specification language pair.
  9. Logical Support for Modularisation , with Rãzvan Diaconescu and Petros Stefaneas. In Logical Environments, edited by Gerard Huet and Gordon Plotkin (Proceedings of a Workshop held in Edinburgh, May 1991), Cambridge, 1993, pages 83-130. Studies properties of logical that support the definition, combination, parameterisation and reuse of modules. Results give connections among preservation of conservative extension under pushouts, distributive laws for information hiding over sums, and Craig interpolation.
  10. Institutions: Abstract model theory for specification and programming, by Joseph Goguen and Rod Burstall, in Journal of the ACM, 39, No. 1, Jan. 1992, pages 95-146. This is the basic paper, giving the basic definitions and results.
  11. Some Fundamental Algebraic Tools for the Semantics of Computation, Part 3: Indexed Categories, by Andrzej Tarlecki, Rod Burstall and Joseph Goguen. Theoretical Computer Science, 91, 1991, pp 239-264. Includes a discussion of generalized institutions that uses Grothendieck flattening.
  12. Introducing Institutions, by Joseph Goguen and Rod Burstall, in Logics of Programs (Carnegie-Mellon University, June 1983), Springer, Lecture Notes in Computer Science, Volume 164, 1984, pages 221-256.

4. Other Links

Below is a preliminary list of sites that feature institutions in one way or another:

To research projects index page
To philisophical discussion of institutions and Peirce's triadic semiotics
Maintained by Joseph Goguen
Last modified: Fri Jan 6 07:46:59 PST 2006