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.
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' eThis 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) eThe 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).
The following are links to some relevant material available at UCSD; the third to last is the basic paper on institutions.
Below is a preliminary list of sites that feature institutions in one way or another: