Institution Theory

Institution theory is a very general mathematical study of formal logical systems—with emphasis on semantics—that is not committed to any particular concrete logical system. This is based upon a mathematical definition for the informal notion of logical system, called institution, which includes both syntax and semantics as well as the relationship between them. Because of its very high level of abstraction, this definition accommodates not only well-established logical systems but also very unconventional ones; and moreover it has served and it may serve as a template for defining new ones.

There is some criticism that the abstraction power of institutions is too much, allowing for examples that can hardly be recognised as logical systems. Institution theory is nevertheless part of the universal logic trend (Béziau, 2012) which approaches logic from a relativistic, non-substantialist perspective, that is quite different from the common reading of logic, both in philosophy and in the exact sciences. However, institution theory should not be regarded as opposed to the established tradition of logic since it includes it from a higher abstraction level. In fact the real difference may occur at the level of methodology, top-down (in the case of institution theory) versus bottom-up (in the case of conventional logic tradition). This means that, in institution theory, concepts come naturally as presumed features that a logical system might or might not exhibit, and they are defined at the most appropriate level of abstraction; hypotheses are kept as general as possible and introduced on an as-needed basis. These lead to a deeper understanding of logic phenomena that is not hindered by the largely irrelevant details of particular logical systems, but are guided by structurally-clean causality. In the exposition, after discussing the history of institution theory, its main concepts are presented. Then there is a discussion of the main contributions of institution theory, including a wide range from pure mathematical logic to applied computing science. A special point here is the institution-theoretic method for doing logic by translation, which means handling logical issues rather indirectly by transporting them across logical systems and solving them at the most appropriate place. After this some extensions of mainstream institution theory are presented briefly.

History
The Concept of Institution
Institution-independent Model Theory
Logic by Translation
Contributions to Computing Science
Extensions
References and Further Reading

1. History

a. Origins

Institution theory was introduced by Joseph Goguen and Rod Burstall in the late seventies as a response to the explosion in the population of logical systems in use in formal specification theory and practice. Formal specification is a logic-based area of computer science that aims to support reliable system development through axiomatic formalisation of their structure and functionality. At the time (and now even more) there was a great diversity of specification formalisms, each of them supported by a particular underlying logical system. Hence the need for a uniform approach to specification theory capable to develop those part of the theory that are independent of the choice of a particular logical system, and thus are common to many specification formalisms. The key step was the definition of the concept of institution in (Goguen and Burstall, 1984) intended to capture formally the structural essence of logical systems beyond specific details. Since semantics plays the primary role in formal specification, institutions lean towards the semantics side of logic, known as model theory. This aspect has permanently constituted a source of criticism from the side of syntactic and proof oriented logicians and at the same time a source of celebration from the side of the semantics oriented ones.

The concept of institution has two theoretical sources. One is the abstract model theory of Barwise (1974), and the other is the category theory of Eilenberg and Mac Lane (1945); Mac Lane (1998). While the importance of the latter in traditional areas of mathematics remains controversial, it has gained a major status in theoretical computing science (see (Goguen, 1991)) and logic. Although mathematically institutions are categorical structures
their spirit is that of abstract model theory.

b. Early Developments

The first paper on institution theory (Goguen and Burstall, 1984) introduced the main concepts and in parallel illustrated them on the example of the capture of many-sorted equational logic as an institution, at the time being the most traditional and important specification logic. Among the basics of institution theory developed there were the Galois connection between syntax and semantics as well as various concepts and results related to the structuring of specifications and programs. The latter task has been carried much further in the influential work (Sannella and Tarlecki, 1988). Another important early development was the introduction in (Tarlecki, 1986b) of the treatment of classical connectives (conjunction, disjunction, negation, and so forth) and of quantifications in abstract institutions, and also of other logic concepts such as interpolation. That was a clear indication that institution theory may reach far beyond its original goal, that of providing a very general theoretical platform for formal specification. The work (Tarlecki, 1986c) was the first paper on institution theory that developed deep results having a logic (model theory) rather than a computing science flavour. In parallel with these developments the list of logical systems captured as institutions kept growing, with quite unconventional ones being added, a process fueled mainly by the increasing diversity of computing science logics. Very often the effort to formally capture particular logical systems as institutions has lead to (re)considerations, within the respective logical setups, of some basic logical concepts, such as variable, language (or vocabulary, signature), model, sentence, and so forth. Presenting logical systems as precise and coherent mathematical objects proves to be more than a simple exercise, it has lead to new understanding of some aspects of particular logical systems.

c. Later Developments

The work (Meseguer, 1989) extended the concept of institution, that has a pronounced semantic character, to include proof-theoretic concepts, thus opening the possibility to have a general institution-theoretic approach to logical calculi.

Although the conceptual infrastructure was already in place right from the beginning of institution theory, the first substantial institution-theoretic work in the direction of doing logic by translation is (Cerioli and Meseguer, 1997). Many other works in the same direction followed, most notably (Mossakowski et al., 2009), the winner of the contest of the 2nd World Congress in Universal Logic (Xi’an, China, 2007).

An important trend within institution theory is less motivated by computing science and more by model theory research. Several important model theory methods have been developed at the level of abstract institutions and a lot of very general and yet deep results have been developed. This has resulted in a very abstract form of model theory, often refereed to as institution-independent model theory or synonymously institutional model theory. The monograph (Diaconescu, 2008) provides a snapshot of this dynamic area. Many of the institution-independent model theory results constitute high generalisations of well known results from conventional concrete model theory and can be used for obtaining easily corresponding results in less conventional logical systems. The same can be said for model theoretic concepts. A lot of theoretical computer science has been developed within institution theory based on the principle that formal specification and declarative programming languages should be based rigorously upon an underlying concrete institution. Based upon a large body of institution-theoretic developments, two modern specification languages have been designed by following this principle: CafeOBJ in Japan (Diaconescu and Futatsugi, 1998) and CASL in Europe (Astesiano et al., 2002). Both developments (the latter via the Hets environment (Mossakowski, 2005)) acknowledged the importance of logically heterogeneous environments, where several logical systems instead of only one are used via appropriate translations between them. For this, institution theory was able to accommodate a construction from algebraic geometry due to the French mathematician Alexandre Grothendieck, and flatten any such heterogeneous environment to a single institution (Diaconescu, 2002; Mossakowski, 2002), with the benefit of avoiding the rather big eort of a redevelopment of concepts and results for the heterogeneous situation. Institution theory plays the core role in the OMG standard The Ontology, Integration and Interoperability (OntoIOp).

d. Notes

Although (Goguen and Burstall, 1984) may be considered as the first prominent publication from the now rather vast institution theory literature, the seminal reference of the area is considered (Goguen and Burstall, 1992). The large time gap between these two publications is due to a very slow editorial process. Some critics consider the term ‘institution’ as uninspired since it does not convey anything about the scientific or the philosophical meaning of the concept. Goguen said that they chose this name, somehow half joking, in response to the sectarianism that was taking over the specification community at the time. Around particular specification formalisms, people were building real social institutions consisting of dedicated conferences, publication forums, user groups, and so forth.

2. The Concept of Institution

An institution is a mathematical structure that can be regarded as a template for capturing mathematically logical systems. Many argue that this template is general enough to accomodate anything that may be called ‘logic’, or at least any logical system based on satisfaction between sentences and models of any kind. The concept of institution relies heavily upon category theory concepts, but in a rather elementary way. This means that most of institution theory does not involve sophisticated or advanced levels of category theory. An institution consists of four kinds of entities: signatures, sentences, models, and the satisfaction between models and sentences. All these are considered fully abstractly and axiomatically. This means the focus is on their external properties, how they relate to the other entities, rather than what they actually are or may be.

a. Signatures

When assuming a logical context the first thing to be done is to assume a collection of symbols as primitive building blocks for the syntactic constructs. In logic this is usually called language or vocabulary. In computing science this is usually called signature, and so is in institution theory. In a signature the symbols are also usually structured, and often this gets to rather complex structures. This is especially true in the context of many modern computing science logics. But institution theory encapsulates all such information and treats signatures as fully abstract entities. In addition to this, institution theory considers that in a logical system signatures may vary. This comes from the practice of formal specification where the signatures are defined locally. Hence in any institution we have a collection of signatures rather than only one signature. However, this is not taken as a discrete collection as institution theory also considers interpretations between signatures called morphisms of signatures; these are also considered fully abstractly. The only data is that any signature morphism $\varphi$ has a source signature $\Sigma$ and a target signature $\Sigma'$ ; this is denoted $\varphi \,\colon\; \Sigma \rightarrow \Sigma'$ by employing the common mathematical notation of a function. Note that in concrete examples signature morphisms are not necessarily functions, they may be much more complex interpretations that preserve the respective structure of the signatures. Also given two signatures, in general nothing prevents the existence of more than one morphisms between them, or the non-existence of such morphisms.

In the case of concrete institutions, of examples, one has to define precisely what are the signatures and their morphisms. Let us consider the simple example of (the institution of) classical propositional logic, which we denote by $\mathit{PL}$ . Here a signature is just a set $P$ , traditionally referred to as a set of ‘propositional variables’. It is important that $P$ , although arbitrary, is a fixed set. Another set $P'$ gives another signature. And any function $\varphi \,\colon\; P \rightarrow P'$ is a signature morphisms. Note that the Boolean connectors $\wedge$ , $\neg$ , etc, although they contribute to the building of the propositional logic statements, are not part of the signatures.

The only property that institution theory considers for signatures and their morphisms is that when

$\varphi \,\colon\; \Sigma \rightarrow \Sigma'$

and

$\varphi' \,\colon\; \Sigma' \rightarrow \Sigma''$

there exists another signature morphism

$\varphi;\varphi' \,\colon\; \Sigma \rightarrow \Sigma''$

called the composition of $\varphi$ and $\varphi'$ . This composition should satisfy some associativity and identity laws, hence very compactly we say that in any institution the signatures and their morphisms form a category. In our $\mathit{PL}$ example this is just the most standard category, the category $\mathit{\mathrm{SET}}$ of sets with functions as morphisms, with the composition $\varphi;\varphi'$ being just the set theoretic composition $\varphi' \circ \varphi$ , i.e.

$(\varphi;\varphi')(x) = (\varphi' \circ \varphi)(x) = \varphi' (\varphi (x))$

b. Sentences

In any particular logical system once a language (signature) is assumed, we can have logical statements or sentences. The collection of sentences is dependent on the assumed language (signature). In institution theory this very basic principle is reflected by a designated function ( $\mathrm{Sen}$ ) that maps each signature to a set (of presumed sentences). At the abstract level one does not bother what this function is, it is considered fully abstractly. For each signature $\Sigma$ we just call the elements of $\mathrm{Sen}(\Sigma)$ as ‘ $\Sigma$ -sentences’. However, the concrete institutions need to define these. For instance, given a $\mathit{PL}$ signature $P$ (which is just a set), $\mathrm{Sen}(P)$ is the set of all formulæ built from $P$ by using the connectors $\wedge$ and $\neg$ . If

$P = \{ \pi_1, \pi_2 \}$

then for example

$(\neg \pi_1) \wedge \pi_2 \in \mathrm{Sen}(P)$

Since semantically the other propositional logic connectors such as implication $\Rightarrow$ , disjunction $\vee$ , etc. can be expressed in terms of $\wedge$ and $\neg$ , the latter two are enough to get all the expressivity power of propositional logic.

The signature morphisms reflect at the level of sentences as translation mappings. That is, for any signature morphism $\varphi \,\colon\; \Sigma \rightarrow \Sigma'$ there exists a function

$\mathrm{Sen}(\varphi) \,\colon\; \mathrm{Sen}(\Sigma)\rightarrow \mathrm{Sen}(\Sigma')$

For abstract institutions $\mathrm{Sen}(\varphi)$ is considered abstractly, but in concrete institutions we have to define it. Usually $\mathrm{Sen}(\varphi)$ just replaces the symbols in $\Sigma$ -sentences according to $\varphi$ . For example, given the only existing $\mathit{PL}$ signature morphism

$\varphi \,\colon\; P \rightarrow P'$

where $P$ is as above and $P' = \{ \pi \}$ then

$\mathrm{Sen}(\varphi)((\neg \pi_1)\wedge \pi_2) = (\neg \pi) \wedge \pi$

. In other situations things are not that straightforward. For instance in many sorted quantified logics the translation of quantified sentences gets a little sophisticated due to the management of the first order variables (for example to make sure that a translated variable does not clash with an existing constant of the target signature). From our example we may note easily a very simple coherence property of the sentence translation: for any composition of signature morphisms $\varphi;\theta$ we have that for each sentence $\rho$ ,

$\mathrm{Sen}(\varphi;\theta)(\rho) = \mathrm{Sen}(\theta)(\mathrm{Sen}(\varphi)(\rho))$

If we add also that the identity signature morphisms (i.e. those keeping everything as it is) always get mapped to identity functions then in category theory terminology we can just say that $\mathrm{Sen}$ is a functor from the category $\mathrm{Sig}$ of the signatures to the category $\mathit{\mathrm{SET}}$ of sets and functions. At the level of abstract institutions this property of the $\mathit{PL}$ sentence translations is given as an axiom that characterises the sentence part of the general definition of institution.

c. Models

On the semantics shore, each signature can be interpreted as a collection of models. In general for each signature $\Sigma$ there can be several models (called $\Sigma$ -models), an aspect that gives model theory its relativistic character. For instance, the models of a $\mathit{PL}$ signature $P$ are the valuations of the ‘propositional variables’ of $P$ to the truth values $0$ and $1$ , which is the same as the subsets of $P$ (by retaining only the elements of $P$ that are valuated to $1)$ . Like with signatures and sentences, at the abstract level, that of the definition of the concept of institution, the models are also considered fully abstractly. Like for signatures, but unlike for sentences (of a given signature), we also consider morphisms between models. This yields the same kind of mathematical structure for the collection of the $\Sigma$ -models like in the case of $\mathrm{Sig}$ , that of a category. Hence let $\mathrm{Mod}(\Sigma)$ denote the category of the $\Sigma$ -models and their morphisms. In the case of $\mathit{PL}$ , $\mathrm{Mod}(P)$ has the particularity that given two models $M$ and $N$ there exists at most one morphism $M \rightarrow N$ ; this happens only when $M \subseteq N$ (here we regard the $P$ -models as subsets of $P$ rather than valuations to $\{ 0,1 \}$ ).

The fact that in general $\mathrm{Mod}(\Sigma)$ is defined as a category rather than set (like $\mathrm{Sen}(\Sigma)$ is), besides the morphisms aspect, has a rather subtle set-theoretic aspect. The $\Sigma$ -models may be so many that they may not constitute a set anymore. In examples this is closely related to the fact that there does not exists ‘the set of all sets’, which would be a violation of one of the axioms of formal set theory. However, this does not necessarily happen always, for example in $\mathit{PL}$ the $P$ -models do form a set.

Another important difference between the syntax and semantics sides of the definition of institution occur at the level of the translations induced by the signature morphism. This phenomenon can be best understood when looking at concrete examples, such as $\mathit{PL}$ . Given a $\mathit{PL}$ signature morphism $\varphi \,\colon\; P \rightarrow P'$ the corresponding translation mapping goes from $\mathrm{Mod}(P')$ to $\mathrm{Mod}(P)$ , opposite the direction the sentence translation goes. Namely, each $P'$ -model $M'$ gets reduced to the $P$ -model $M' \circ \varphi$ (here for convenience we regard $\mathit{PL}$ -models as valuations rather than subsets). This is a very important feature of the semantics, called the contravariance of the reduction. The use of the name ‘reduction’ instead of ‘translation’ is in fact meant to convey this aspect. This terminological choice can be easily understood when considering $\varphi$ to be an inclusion $P \subseteq P'$ : as the valuation function, $M' \circ \varphi$ is just the restriction of $M'$ to $P$ . Thus, at the general level, for any signature morphism $\varphi\,\colon\; \Sigma \rightarrow \Sigma'$ there is a model reduct functor

$\mathrm{Mod}(\varphi)\,\colon\; \mathrm{Mod}(\Sigma')\rightarrow \mathrm{Mod}(\Sigma)$

By taking into account that $\mathrm{Mod}(\Sigma')$ and $\mathrm{Mod}(\Sigma)$ are categories rather than sets, $\mathrm{Mod}(\varphi)$ is functor rather than function. The behaviour of the model reduct functors with respect to the composition of the signature morphisms is perfectly similar to what happens in the case of the sentence translations, of course modulo the contravariance aspect:

$\mathrm{Mod}(\varphi;\varphi')(M'') = \mathrm{Mod}(\varphi)(\mathrm{Mod}(\varphi')(M''))$

All these can be formulated compactly just by saying that $\mathrm{Mod}$ is a contravariant functor from $\mathrm{Sig}$ to the category $\mathit{\mathrm{CAT}}$ of categories and functors.

d. Satisfaction

At the heart of the semantic concept of truth, promoted by Tarski (1944) and employed by institution theory, lies the satisfaction relation between models and sentences. For example, in $\mathit{PL}$ given a signature $P$ , a $P$ -model $M$ and a $P$ -sentence $\rho$ , we may evaluate $\rho$ for the valuation $M$ as a truth value $0$ or $1$ by applying the well known truth table of classical propositional logic inductively on the structure of $\rho$ . Then we say that $M$ satisfies $\rho$ , written $M \models \rho$ , if and only if the evaluation of $\rho$ in $M$ yields $1$ . Note that we speak about satisfaction only when the model and the sentence belong to the same signature.

Since in the definition of institutions signatures, sentences and models are fully abstract, the satisfaction of sentences by models is fully abstract too. Thus for each signature $\Sigma$ there is a satisfaction relation between $\Sigma$ -models and $\Sigma$ sentences, denoted $\models_\Sigma$ . This is subject of an axiom known as the Satisfaction Condition whose meaning is often informally explained as the invariance of truth with respect to the change of notation: for each signature morphism $\varphi \,\colon\; \Sigma\rightarrow \Sigma'$ , each $\Sigma$ -sentence $\rho$ and each $\Sigma'$ -model $M'$ ,

$\mathrm{Mod}(\varphi)(M') \models_\Sigma \rho \text{ if and only if } M' \models_{\Sigma'} \mathrm{Sen}(\varphi)(\rho).$

In concrete institutions one always has to define the satisfaction relation, commonly done by induction on the structure of the sentences (like in the case of $\mathit{PL}$$ . This principle, known as truth functionality, means that given a semantic context (model) the truth value of any compound sentence is determined from the truth values of its components. Truth functionality provides also the common method to establish the Satisfaction Condition in concrete institutions, by induction on the structure of the sentences. While in some cases this is an easy task ( $\mathit{PL}$ is such an example) in other cases it can be highly non-trivial. Especially in the case of quantified logics the induction step corresponding the quantifications poses some technical problems, requiring some compositionality property for the models (see (Diaconescu, 2008)).

Our presentation of the mathematical definition of the concept of institution may be summarised as follows. An institution is a tuple $(\mathrm{Sig},\mathrm{Sen},\mathrm{Mod},\models)$ where $\mathrm{Sig}$ is a category, $\mathrm{Sen}$ is a functor $\mathrm{Sig} \rightarrow \mathit{\mathrm{SET}}$ , $\mathrm{Mod}$ is a contravariant functor $\mathrm{Sig} \rightarrow \mathit{\mathrm{CAT}}$ , and for each signature $\Sigma$ , $\models_\Sigma$ is a relation between $\Sigma$ -models and $\Sigma$ -sentences such that the Satisfaction Condition holds. Note that besides the Satisfaction Condition, the definition of institution includes other axioms encapsulated by the several categories and functors that are part of the definition.

e. Concrete Institutions

The institution theory literature (which includes part of the specification theory literature) contains countless examples of logical systems that have been formally captured as institutions. Among these there are first, second, higher order logics, logics with some form of partiality for the functions such as partial algebra and various dialects of order sorted algebras, non-classical logics such as intuitionistic ones, a wide diversity of modal logics, fuzzy and many valued logics, and so forth. All these institutions admit also many-sorted variants. Many examples of institutions arose on the basis of various combinations between other institutions. Several institutions related to programming look rather divorced from the common perception of what is a logical system, some of these being presented in (Sannella and Tarlecki, 2012).

f. Notes

The traditional style of doing logic has a rather global approach to signatures, they usually do not vary, and when they do this would be just extensions. By contrast, institution theory is genuinely multi signature oriented, with signature morphisms being a rather primitive concept. Moreover in concrete examples the institution-theoretic view is that these can be broader than extensions, they may rename and even collapse elements. This widening of the concept of signature morphism serves the purpose of specification theory but is also very convenient for abstraction. Having signature morphisms as a primitive concept is also crucial for the development of various important logic concepts at the abstract level, for example, quantification, interpolation, method of diagrams, saturated models, and so forth. Moreover, the generality of the concept of signature morphism in institution theory accommodates even first-order substitutions like in (Găină and Petria, 2010), or substitutions of propositional variables by compound propositions like in (Voutsadakis, 2002).

The Satisfaction Condition had appeared for the first time as an axiom in (Barwise, 1974), but in a much less abstract context than institution theory. Although in logic this appears as an indisputable property of logical systems, in computing science there was some criticism of being too strong and thus preventing some logical systems, albeit very marginal, from being institutions. More precisely, the critics of the Satisfaction Condition argued that the implication from the right to the left would be enough. Counter-criticism to this argues that in the absence of the full Satisfaction Condition as an equivalence, almost all general institution theory results both in model theory and in computing science become impossible. In defence of the Satisfaction Condition (Goguen, 1991) argues that those counterexamples arise due to some heavy incoherence between the respective concepts of signature morphism and satisfaction relation, that under a meaningful fix of the respective concept of signature morphism the Satisfaction Condition is rescued.

3. Institution-independent Model Theory

The institution-theoretic approach to model theory tends to be rather comprehensive, here we present some rudiments of it. This reading of this section may sometimes require some technical inclination from the side of the reader.

a. The Galois Connection between Syntax and Semantics

Given a signature $\Sigma$ in an institution we let

for each $E\subseteq \mathrm{Sen}(\Sigma)$ , $E^* = \{ M \in \mathrm{Mod}(\Sigma) \mid M \models_\Sigma \rho \mbox{ for each } \rho\in E \}$ , and
for each $\mathcal{M}\subseteq \mathrm{Mod}(\Sigma)$ , $\mathcal{M}^* = \{ \rho\in \mathrm{Sen}(\Sigma) \mid M \models_\Sigma \rho \mbox{ for each } M \in \mathcal{M} \}$ .

These give what is called a Galois connection between the subsets of $\mathrm{Sen}(\Sigma)$ and those of $\mathrm{Mod}(\Sigma). The \(*$ operators allow also for the definition of semantic consequence: given any set $E$ of $\Sigma$ -sentences and any $\Sigma$ -sentence $\rho$ we say that $\rho$ is a semantic consequence of $E$ , written $E \models \rho$ , when $\rho \in E^{**}$ (that is every model that satisfies every sentence in $E$ satisfies $\rho$ too).

b. Logical Connectors

The semantics of the Boolean connectors can be formally defined in institutions also by using the $*$ operators. A $\Sigma$ -sentence $\rho$ is a conjunction of the $\Sigma$ -sentences $\rho_1$ and $\rho_2$ when $\rho^* = \rho_1^* \cap \rho_2^*$ . Or, $\rho'$ is a negation of $\rho$ when $\rho'^* = \mathrm{Mod}(\Sigma) \setminus \rho^*$ . And similarly for disjunction, implication, etc. Note that, unlike their syntactic correspondents that are unique, the semantic conjunction, negation, implication, etc. are unique only up to semantic equivalence, which means that from this point of view sentences satisfied by the same models are indistinguishable. The definition of the Boolean connectors can be extended at the level of the whole institution: for example an institution has conjunctions when any two of its sentences have a conjunction, and so on.

c. Quantifiers

The institution theoretic treatment of quantifiers is semantic and relies crucially upon the concept of signature morphism essentially by assimilating valuations of variables with model expansions along the extension of the signature with the respective variables. While in concrete institutions one may discuss about valuations of variables $X$ into models $M$ as functions from $X$ to some underlying set theoretic carrier of $M$ , in the abstract setup this is not possible due to the lack of explicit set theoretic structures. However by assimilating the variables $X$ with the signature extensions $\Sigma \rightarrow \Sigma+X$ obtained by adding them to the respective signatures, we may note that for any $\Sigma$ -model $M$ , there is a canonical one-to-one correspondence between the valuations $X \rightarrow M$ and the $\Sigma+X$ -models $M'$ such that their reducts to $\Sigma$ are just $M$ . This trick implies that variables can become part of the signatures, which breaks with the habit of traditional approaches to logic of keeping variables separated from the language (signature). The point of this separation is to avoid some clash between $X$ and the entities of $\Sigma$ . However this can be achieved differently without separating variables from the signatures, which anyway from the formal perspective poses several difficulties. The idea is very simple and comes from the practice of specification languages. One has just to qualify properly the variables by their signature context. For example a variable for a signature $\Sigma$ in the institution of many sorted first order logic would be a triple $(x,s,\Sigma)$ where $x$ is the name, $s$ the sort/type, and $\Sigma$ the signature of the variable. A signature $\Sigma$ becoming part of the data defining the variables $X$ prevents, by formal set theory reasons, any clash between $\Sigma$ and $X$ when adjoining $X$ to $\Sigma$ .

Hence at the level of abstract institutions a variable for a signature $\Sigma$ is just a signature morphism $\chi \,\colon\; \Sigma \rightarrow \Sigma$ . Note that in the concrete situations variables-as-signature-morphisms support concepts of variables at the same level with the signatures, hence it is rather powerful. For example if the signature allows for higher order functions, then one can have variables for those. However often the intended variables are significantly more particular than what the respective concept of signature provides. This is one of the reasons why not any signature morphism can be considered as representing a variable. Another reason is that in concrete institutions the signature morphism representing variables are extensions, and moreover they are extensions with entities that have a proper qualification, as discussed above. A standard way to realize these restrictions abstractly is to have an abstract designated subclass $\mathcal{D}$ of signature morphism as variables. Given $(\chi \,\colon\; \Sigma \rightarrow \Sigma')$ in $\mathcal{D}$ , a $\Sigma$ -sentence $\rho$ is a universal $\chi$ -quantification of a $\Sigma'$ -sentence $\rho'$ when for each $\Sigma$ -model $M$ , $M \models_\Sigma \rho$ if and only if $M' \models_{\Sigma'} \rho'$ for all $\Sigma'$ -models $M'$ such that $M = \mathrm{Mod}(\chi)(M')$ . Existential quantification is defined similarly. It is said that the institution has universal/existential $\mathcal{D}$ -quantifications when any sentence $\rho'$ as above has a universal/existential $\chi$ -quantification for any $\chi\in \mathcal{D}$ as above.

In logic in general and in model theory in particular it is well known that quantification by first-order variables has very good and desirable properties. This kind of quantification is captured at the abstract level by requiring that any signature morphism $(\chi \,\colon\; \Sigma \rightarrow \Sigma')$ in $\mathcal{D}$ is representable, which essentially means that there exists a $\Sigma$ -model $M_\chi$ such that there is a one-to-one correspondence between the $\Sigma'$ -models $N'$ with $\mathrm{Mod}(\chi)(N') = N$ and the $\Sigma$ -model morphisms $M_\chi \rightarrow N$ . The idea behind this is that in concrete situations valuations of variables can be represented by model morphisms from a ‘free model’ over the variables. In other words, when $\chi$ is a signature extension $\Sigma \rightarrow \Sigma + X$ as discussed above, $M_\chi$ is the $\Sigma$ -model freely generated by $X$ , in standard actual situations being a term model over $X$ .

d. Diagrams

The method of diagrams is a widely pervasive method in model theory (see for example (Chang and Keisler, 1990)). Its institution-theoretic abstraction of Diaconescu (2004b) also plays an important role in many institution-independent model theory developments. In essence, the diagram of given a model $M$ represents a kind of comprehensive syntactic characterisation of $M$ . The institution-theoretic definition introduced in (Diaconescu, 2004b) axiomatises a category theoretic one-to-one correspondence between the model morphisms $M \rightarrow N$ and the models satisfying an abstractly designated set of sentences $E_M$ . The signature $Sigma_M$ of $E_M$ is not the signature $\Sigma$ of the model $M$ , instead there is an abstractly designated signature morphism

$\iota_{\Sigma,M} \,\colon\; \Sigma \rightarrow \Sigma_M$

In the concrete examples in which the models have an underlying set theoretic structure, $\iota_{\Sigma,M}$ is usually the extension of $\Sigma$ with the elements of the underlying carrier of $M$ that are adjoined to $\Sigma$ as new constants.

The most typical examples come from classical first order model theory. Let $\iota_{\Sigma,M}$ be as described above, and let $M_M$ be the $\Sigma_M$ model that expands $M$ by interpreting the new constants by themselves. Then $E_M$ is the set of all atoms that are satisfied by $M_M$ . This corresponds to the case when the model morphisms are those that preserve the structure of the models, if we change the concept of model morphism then the diagram should change also. For example if we consider the elementary embeddings as model morphisms then $E_M$ is much larger, consisting of all first order sentences that are satisfied by $M_M$ . And so on. The narrower the class of model morphisms considered, the larger the corresponding diagrams.

The existence of institution-theoretic diagrams in concrete logical systems is a mark of coherence between the syntax (the kind of sentences involved) and the semantics (the concept of model morphism employed). For example non-hybrid modal logics lack diagrams because there is an unbalance between the syntax and the semantics (Kripke structures), in the sense that the syntax is too weak to express aspects of the semantics. On the other hand, the hybrid (modal) logics do have diagrams because they have more expressive power with respect to the Kripke frames.

e. Ultraproducts

The method of ultraproducts is a most important and remarkably powerful one in conventional model theory (Chang and Keisler, 1990). This has been realised at the abstract level of institution theory beginning with (Diaconescu, 2003), on the basis of the previously established concept of categorical ultraproduct (introduced perhaps first time in (Matthiessen, 1978)) and applied to the categories of models $\mathrm{Mod}(\Sigma)$ in institutions. This requires some familiarity with categorical limits and colimits. A filter $F$ on a set $I$ is a set of subsets of $I$ , such that $J \cap J' \in F$ when $J,J' \in F$ and $J'\in F$ when $J\in F$ and $J \subseteq J'$ . $F$ is an ultrafilter when in addition $F$ satisfies the property that for each $J\subseteq I$ , $J \in F$ if and only if its complementary $I \setminus J \not\in F$ . Let us consider a family $(M_i)_{i\in I}$ of $\Sigma$ -models in an institution and a filter $F$ on $I$ . For any $J\in F$ let us denote the direct product of $(M_i)_{i\in J}$ by $M_J$ . If $\mathrm{Mod}(\Sigma)$ has direct products then for any $J \subseteq J'$ in $F$ there is a canonical projection

$p_{J'\supseteq J} \,\colon\; M_{J'} \rightarrow M_J$

Then any colimit

$\mu = \{ \mu_J \,\colon\; M_J \rightarrow M_F \mid J \in F \}$

of the diagram

$\{ p_{J'\supseteq J} \mid J\subseteq J', J\in F \}$

is called an $F$ -product of $(M_i)_{i\in I}$ . When $F$ is ultrafilter, $F$ -products are called ultraproducts. Due to the uniqueness up to isomorphisms of categorical direct products and of colimits it follows that $F$ -products are unique only up to isomorphisms too.

The foundation of the ultraproducts method in first-order model theory is constituted by a result in (Ło´s, 1955) which gives a ‘preservation’ property for the satisfaction by ultraproducts of models that is common to all sentences in first-order logic. This has been highly generalised in institution theory by decomposing it into a puzzle of general preservation results across connectors (Boolean, modalities) and quantifiers. Concrete instances of this result and of some of its extensions provide for free an ultraproducts method for a variety of logical systems, including unconventional ones for which such development was otherwise difficult to envisage.

A typical application of ultraproducts is the derivation of the compactness of the semantic consequence without having to resort to a proof system and a related completeness argument, which in general is technically very difficult. An institution is said to be compact when for each semantic consequence $E \models_\Sigma \rho$ , where $E$ is a set of sentences and $\rho$ is a single sentence, there exists a finite set $E_0 \subseteq E$ such that $E_0 \models_\Sigma \rho$ . In the presence of the preservation of the satisfaction relation under the ultraproduct construction of models, if in addition the institution has conjunctions and negations, we get the compactness of the institution. When adjoined to the institution-theoretic generalisation of the fundamental ultraproducts result of (Ło´s, 1955), this remarkably general property gives an abstract compactness result, which can be instantiated with little eort to a wide variety of concrete logical systems. The eciency of this path to compactness has become transparent for example in (Diaconescu and Stefaneas, 2007) in the case of a wide class of quantified modal systems.

f. Interpolation and Definability

Interpolation is an important property of logical systems which has a strikingly elementary formulation but which is usually very difficult to establish. Its common semantic version sounds like this:

given a $\Sigma_1$ -sentence $\rho_1$ and a $\Sigma_2$ -sentence $\rho_2$ , if $\rho_1 \models_{\Sigma_1 \cup \Sigma_2} \rho_2$ then there exists a $\Sigma_1 \cap \Sigma_2$ -sentence $\rho_0$ (called interpolant) such that $\rho_1 \models_{\Sigma_1} \rho_0$ and $\rho_0 \models_{\Sigma_2} \rho_2$ .

In other words, any semantic consequence is established by means of symbols that are common to both sentences. In institution theory interpolation is considered in a form that generalizes several aspects of its common formulation. First, the signature inclusions that appear implicitly in the formulation of interpolation are abstracted to arbitrary signature morphisms. Then the common formulation of interpolation corresponds to the situation when the institution comes with the signature morphisms restricted to inclusions only. However the generalisation of interpolation to arbitrary signature morphism allows in the concrete situations for consideration of signature morphisms that may rename or even collapse syntactic entities. While such extended form of interpolation may be unusual in conventional logic, it is used in specification theory. A second generalisation of the concept of interpolation replaces individual sentences by finite sets of sentences. While in logics that have conjunction (such as classical propositional, first-order logics, and so forth) this does not mean anything, it is very meaningful in logics lacking conjunctions, such as equational or Horn clause logics. In the latter ones interpolation may fail artificially due to unrealistic single sentence style formulation. These get us to the following definition of interpolation. A commuting square of signature morphisms like below

is an interpolation square when for any finite sets $E_1\subseteq\mathrm{Sen}(\Sigma_1)$ and $E_2\subseteq\mathrm{Sen}(\Sigma_2)$ such that

$\mathrm{Sen}(\theta_1)(E_1) \models_{\Sigma'} \mathrm{Sen}(\theta_2)(E_2)$

there exists a finite set

$E_0 \subseteq\mathrm{Sen}(\Sigma_0)$

such that

$E_1 \models_{\Sigma_1} \mathrm{Sen}(\varphi_1)(E_0)$

and

$\mathrm{Sen}(\varphi_2)(E_0)\models_{\Sigma_2} E_2$

Such commuting squares are meant to emulate the intersection-union of signatures from the common formulation of interpolation, with $\Sigma_0$ in the role of $\Sigma_1 \cap \Sigma_2$ and $\Sigma'$ in the role of $\Sigma_1 \cup \Sigma_2$ . However in the common formulation of interpolation it is important that $\Sigma_1 \cup \Sigma_2$ is the lowest signature above $\Sigma_1$ and $\Sigma_2$ . In the generalised formulation of interpolation this property appears as a category theoretic condition, that the commuting square is a pushout in the category $\mathrm{Sig}$ of the signatures of the institution. But when considering interpolation as a property of the institution as a whole, it is in general not meaningful to look for interpolation in all pushout squares. This leads to another generalisation layer in the formulation of interpolation, which restricts abstractly the range of $\varphi_1$ and $\varphi_2$ to designated subclasses of signature morphisms. Thus, given $\mathcal{L}$ and $\mathcal{R}$ subclasses of signature morphisms, the institution has $(\mathcal{L},\mathcal{R})$ -interpolation when each pushout of a span $(\varphi_1,\varphi_2)$ of signature morphisms with $\varphi_1\in \mathcal{L}$ and $\varphi_2\in \mathcal{R}$ is an interpolation square.

Institution-theoretic interpolation has been established at the general level in relation to several different causes. One cause can be an axiomatizability property of the institution, like in (Diaconescu, 2004a). A typical example here is many sorted equational logic which has $(\mathcal{L},\mathcal{R})$ -interpolation with $\mathcal{L}$ being the injective signature morphisms and $\mathcal{R}$ being all signature morphisms. Another cause can be the Robinson consistency property, like in (Găină and Popescu, 2007). An instance of this is many sorted first order logic which has $(\mathcal{L},\mathcal{R})$ -interpolation when either $\mathcal{L}$ of $\mathcal{R}$ consists of signatures morphisms that are injective on the sorts. And yet another cause can be the existence of an adequate translation to an institution that has well established interpolation properties, like in (Diaconescu, 2012b).

Definability is one of the traditional important consequences of interpolation. The concept of definability has been approached in institution theory by Petria and Diaconescu (2006) in a rather similar way to interpolation, by abstracting the new (presumably definable) symbols for signatures to arbitrary abstract signature morphisms. The institution-theoretic study of definability in (Petria and Diaconescu, 2006) revealed that, besides interpolation, axiomatizability properties (considered in the generalised form introduced in (Diaconescu, 2004a)) may constitute a primary cause for definability.

g. Layered Completeness

The concept of institution can be enhanced with a proof theoretic structure (Meseguer, 1989) by adding for each signature $\Sigma$ an entailment relation $\vdash_\Sigma$ between sets of $\Sigma$ -sentences and single $\Sigma$ -sentences subject to the following axioms:

$E \vdash_\Sigma \rho$ when $\rho\in E$ ;
If $E \vdash_\Sigma \gamma$ for each $\gamma\in \Gamma$ and $\Gamma \vdash_\Sigma \rho$ then $E \vdash_\Sigma \rho$ ; and
For each signature morphism $\varphi \,\colon\; \Sigma \rightarrow \Sigma'$ if $E \vdash_\Sigma \rho$ then $\mathrm{Sen}(\varphi)(E) \vdash_{\Sigma'} \mathrm{Sen}(\varphi)(\rho)$ .

The entailment system $\vdash$ is sound for the respective institution when $E \vdash_\Sigma \rho$ implies $E \models_\Sigma \rho$ and is complete when the reverse implication holds. These are institution-theoretic generalisations of the common concepts of soundness and completeness from logic and model theory. Soundness is an obligatory property that is also easy to establish in the concrete situations. Completeness is very desirable but hard to establish; completeness results are difficult ones.

The institution-theoretic approach to completeness results is a layered one based upon the observation that usually proof systems can usually be deconstructed into several layers that correspond to the structure of the sentences involved, and that completeness can be developed at each layer relative to the completeness at the previous one. This means that at each layer the respective entailment system is considered fully abstract, and hence the proof rules that build the next layer come in a form that is independent of the previous layers. The total completeness
result is thus obtained as a combination of smaller independent completeness results, each of them having the potential to be reused in other contexts.

For instance, let us consider the case of the completeness of Horn clause logic with equality, the fragment of first order logic with equality that restricts the sentences to those of the form $(\forall X)H \Rightarrow C$ , where $H$ is a finite conjunction of (equational and relational) atoms and $C$ is a single atom. This completeness can be decomposed into three layers. At the base layer we consider the institution that has as sentences only equational $t=t'$ and relational $\pi(t_1,\dots,t_n)$ atoms. For that we have a complete proof system defined by

$\vdash t=t$ for each term $t$ ;
$t =t' \vdash t' = t$ for all terms $t,t'$ ;
$\{ t=t', t'=t'' \} \vdash t = t'$ for all terms $t,t',t''$ ;
$\{ t_i = t'_i \mid 1\leq i\leq n \} \vdash \sigma(t_1,\dots,t_n) = \sigma(t'_1,\dots, t'_n)$ for any function symbol $\sigma$ of arity $n$ ; and
$\{ t_i = t'_i \mid 1\leq i\leq n \} \cup \pi(t_1,\dots,t_n) \vdash \pi(t'_1,\dots,t'_n)$ for any relation symbol $\pi$ or arity $n$ .

At the next layer we add the sentences of the form $H \Rightarrow C$ where $H$ is a finite conjunctions of atoms and $C$ is a single atom and extend the proof system with the meta-rule

$\Gamma \cup H \vdash C$ if and only if $\Gamma \vdash H \Rightarrow C$ .

The crucial point here is that this step does not depend upon the previous layer, meaning that information can be completely encapsulated, allowing the addition of implications over an arbitrary institution endowed with a complete entailment system. Then the completeness at the new layer is obtained. The final layer consists of adding the universal quantification to the sentences and a rule and a meta-rule to the proof system.

$(\forall X)\rho \vdash (\forall Y)\theta(\rho)$ for any substitution $\theta$ of variables $X$ with terms over the variables $Y$ ; and
$\Gamma \vdash _\Sigma (\forall X)\rho$ if and only if $\Gamma \vdash_{\Sigma+X} \rho$ .

This step can be also developed independently of the previous layer, over an institution endowed with a complete entailment system considered fully abstractly. This requires however an abstract treatment of substitutions. The completeness at the final upper layer is also obtained. By instantiating now the base layer to the one of the atoms in first-order logic with equality and the final layer to universal first-order quantification we get a complete proof system for Horn clause logic with equality. But all the compound completeness results can be also used separately on different instances of the abstract institutions, thus obtaining complete proof systems in various different logical systems. For example we can obtain a complete proof system for the universal fragment of first-order logic, that is, sentences of the form $(\forall X)\rho$ where $\rho$ is a quantifier-free sentence, just by replacing the mid layer above by the proof system of propositional logic.

h. Notes

The institution-theoretic concept of diagrams introduced by Diaconescu (2004b) is significantly simpler than a previously introduced one in (Tarlecki, 1986a,c). Since (Diaconescu, 2004b) this has been used rather intensively in many institution theory works.

The many-sorted first-order logic instance of the general interpolation result of (Găină and Popescu, 2007) represents an elegant solution by means of institution theory to a question about the limits of interpolation in many-sorted first-order logic that stayed as conjecture for several years. The layered completeness was introduced by Borzyszkowski (2002) within the context of the study of complete calculi for structured specifications. The example discussed here comes from Codescu and Găină (2008). Other works on layered completeness include (Găină and Petria, 2010) (two layers), (Găină et al., 2012) (four layers).

Other important model theory methods that have been developed at the level of abstract institutions include saturated models (Diaconescu and Petria, 2010), forcing (Găină and Petria, 2010), omitting types (Găină, 2014). These have lead to remarkable high generalisations of deep model theory results including downwards Löwenheim-Skolem in (Găină, 2014) and the Keisler-Shelah characterisation of first-order elementary equivalence as isomorphism under ultrapowers in (Diaconescu and Petria, 2010).

4. Logic by Translation

Institution theory is very well positioned with respect to the logic-by-translation paradigm because of its perspective on logical systems as mathematical objects/structures. Concepts of structure preserving mappings between institutions, when regarded as mathematical structures, constitute mathematical formalisations for translation concepts. The importance of this idea has been recognised right from the beginnings of institution theory.

a. Morphisms and Comorphisms

Institutions as mathematical structures invite several concepts of ‘morphisms’, or structure preserving mappings between institutions. All of them define three components, corresponding to the translations of the signatures, of the sentences, and of the models. Moreover in each case an axiom that represents an invariance property of the satisfaction relation with respect to these translations is imposed.

The original structure preserving mapping between institutions has been defined by Goguen and Burstall (1992), and called just morphism of institutions. Given institutions $\mathcal{I}$ and $\mathcal{I}'$ a morphism $\mathcal{I}' \rightarrow \mathcal{I}$ consists of

a functor $\Phi \,\colon\; \mathrm{Sig}' \rightarrow \mathrm{Sig}$ translating $\mathcal{I}'$ -signatures to $\mathcal{I}$ -signatures;
for each $\mathcal{I}'$ -signature $\Sigma'$ a sentence translation $\alpha_{\Sigma'} \,\colon\; \mathrm{Sen}(\Phi(\Sigma')) \rightarrow \mathrm{Sen}'(\Sigma')$
for each $\mathcal{I}'$ -signature $\Sigma'$ a model translation/reduct $\beta_{\Sigma'} \,\colon\; \mathrm{Mod}'(\Sigma') \rightarrow \mathrm{Mod}(\Phi(\Sigma'))$

such that both $\alpha$ and $\beta$ are natural transformations (this is a category theory notion, ‘naturality’ in this context meaning a coherence property of the component translations with respect to the signature morphisms) and such that the following Satisfaction/Translation Condition holds for each $\Sigma'$ -model $M'$ and each $\Phi(\Sigma')$ -sentence $\rho$ : $! M' \models'_{\Sigma'} \alpha_{\Sigma'}(\rho) \mbox{ if and only if } \beta_{\Sigma'}(M') \models_{\Phi(\Sigma')} \rho.$

Institution morphisms have the flavour of ‘projecting’ from a more complex institution to a simpler one, like the following morphism from first-order to propositional logic. This maps any first-order logic signature to its set of sentences (each sentence being regarded as a propositional variable in a propositional logic signature), $\alpha_{\Sigma'} (\rho)$ is just the first-order sentence $\rho$ , and $\beta_{\Sigma'} (M')$ being just the propositional logic model consisting of all $\Sigma'$ -sentences that hold in $M'$ .

By reversing the translation of the signatures we get the concept of comorphism of institutions which has the flavour of an ‘embedding’ of a simpler institution into a more complex one. A comorphism $\mathcal{I} \rightarrow \mathcal{I}'$ consists of

a functor $\Phi \,\colon\; \mathrm{Sig} \rightarrow \mathrm{Sig}'$ translating $\mathcal{I}$ -signatures to $\mathcal{I}'$ -signatures;
for each $\mathcal{I}$ -signature $\Sigma$ a sentence translation $\alpha_{\Sigma} \,\colon\; \mathrm{Sen}(\Sigma) \rightarrow \mathrm{Sen}'(\Phi(\Sigma))$ ; and
for each $\mathcal{I}$ -signature $\Sigma$ a model translation/reduct $\beta_{\Sigma} \,\colon\; \mathrm{Mod}'(\Phi(\Sigma)) \rightarrow \mathrm{Mod}(\Sigma)$ .

such that both $\alpha$ and $\beta$ are natural transformations and the following Satisfaction/Translation Condition holds for each $\Phi(\Sigma)$ -model $M'$ and each $\Sigma$ -sentence $\rho$ :

$M' \models'_{\Phi(\Sigma)} \alpha_{\Sigma}(\rho) \mbox{ if and only if } \beta_{\Sigma}(M') \models_{\Sigma} \rho.$

The embedding of propositional logic into first-order logic can be captured as a comorphism that interprets any set of propositional variables as a first-order signature that has only relation symbols of arity zero; note that both $\alpha$ and $\beta$ are identities.

The level of preservation of institution-theoretic structure by morphisms and comorphisms is equal, so just from the viewpoint of institutions as mathematical structures one cannot say which of these is more adequate to play the role of morphisms for the category of institutions. This means that there can be at least two categories that have institutions as their objects, both of them equally legitimate from the perspective of structure. This constitutes a good example of the idea, prevalent in category theory, that a category is best described by its morphisms rather than its objects. The conceptual symmetry between institution morphisms and comorphisms got a formal explanation by Arrais and Fiadeiro (1996) where it is showed that a categorical adjunction between the categories of the signatures of two institutions $\mathcal{I}$ and $\mathcal{I}'$ determine a canonical one-to-one correspondence between the morphisms $\mathcal{I}' \rightarrow \mathcal{I}$ and the comorphisms $\mathcal{I} \rightarrow \mathcal{I}'$ .

b. Encodings

Besides embeddings of simpler logics into more complex ones, the concept of comorphism supports also ‘encodings’ of more complex logics into simpler ones. Famous cases such as the translation of classical propositional logic into intuitionistic by Kolmogorov (1925) or the standard translation of modal logic into first-order logic by van Bentham (1988) can be presented as comorphisms. Most often the cost representing the difference in complexity is payed at the level of translation of the signatures, $\Phi$ mapping signatures to theories in the target institution. This can be explained as a comorphism $\mathcal{I} \rightarrow \mathcal{I}'^{\mathrm{th}}$ where $\mathcal{I}'^{\mathrm{th}}$ denotes the canonically defined institution of $\mathcal{I}'$ -theories, that has as signatures the pairs $(\Sigma,E)$ where $\Sigma$ is an $\mathcal{I}'$ -signature and $E$ a set of $\Sigma$ -sentences. (Note that ‘theories’ here are mere sets of sentences rather than sets of sentences closed under some consequence relation as meant in some logical studies.) The comorphism $\mathcal{I} \rightarrow \mathcal{I}'^{\mathrm{th}}$ are sometimes called theoroidal comorphisms. The two encodings mentioned above represent a notable exception, as they can be presented as plain rather than theoroidal comorphisms (Goguen and Ro¸su, 2002), in both cases the encoding cost being payed at the level of the translation of the sentences.

c. Borrowing

Comorphism-based encodings between institutions represent the main tool for the institution theoretic approach to the logic-by-translation paradigm. Suppose we want to establish a property $P$ in an institution $\mathcal{I}$ but due to various reasons this is rather difficult. Then we can look for a suitable encoding $\mathcal{I} \rightarrow \mathcal{I}'$ such that the translation of $P$ along the encoding can be established in $\mathcal{I}'$ , and moreover such that we can reflect back to $\mathcal{I}$ this conclusion in the form of $P$ . In this case we say that $P$ is ‘borrowed’ from $\mathcal{I}'$ along the encoding. This requires the respective encoding to satisfy some specific properties that are conducive for the borrowing process. The institution theory literature abounds of such examples, that include interpolation, definability, diagrams, saturated models, etc.

One especially important case is that of the borrowing of a consequence relation. Let $P$ be a consequence $E \models_\Sigma \rho$ to be established. If it holds then by a simple argument relying upon the Satisfaction Condition of the comorphism we have that

$\alpha_\Sigma (E) \models_{\Phi(\Sigma)} \alpha_\Sigma (\rho)$

holds too. If $\mathcal{I}'$ comes equipped with a complete proof system then

$\alpha_\Sigma (E) \models'_{\Phi(\Sigma)} \alpha_\Sigma (\rho)$

may be established by proof theoretic means. Now in order to get the conclusion back to $\mathcal{I}$ we need a reflection property for the semantic consequence, which does not happen in general. However a standard way to ensure this is to check that the comorphism is conservative, which means that for any $\Sigma$ -model $M$ there exists a $\Phi(\Sigma)$ -model $M'$ such that $\beta_\Sigma (M') = M$ .

d. Notes

The importance of comorphisms and other types of structure preserving mappings between institutions has been understood gradually, with the paper (Goguen and Ro¸su, 2002) presenting a systematic comparative overview of the different notions of morphisms between institutions. That paper also fixed a lot of current terminology, including for example the term ‘comorphism’.

The work (Mossakowski et al., 2005) gave the institution-theoretic answer for the contest question of the 1st World Congress on Universal Logic (Montreux, Switzerland, 2005), namely what is the identity of a logic? The answer was that it is an equivalence class of institutions under equivalence of institutions. Briefly, the concept of equivalence of institutions proposed by Mossakowski et al. (2005) is a comorphisms (or alternatively a morphism) that consists of categorical equivalences at all levels.

The borrowing of a consequence relation is the foundation for formal verification by translation within the context of logic-based formal system specification. A specification based upon a source institution $\mathcal{I}$ may have very good expressivity and readability but $\mathcal{I}$ may lack adequate proof support. The solution is to shift the formal verification process across an encoding to an institution $\mathcal{I}'$ that is supported by good theorem proving tools, such as theorem provers, proof assistants, and so forth. Within the context of the heterogenous specification paradigm this has become a rather standard practice (Mossakowski, 2005), which is very economical since it makes good use of existing tools instead of building new ones.

5. Contributions to Computing Science

The contribution of institution theory to computing science is manifold, the most basic one being that it sets a standard style of developing new specification languages that requires at the beginning to define a logical system captured as institution and then develop all the language constructs solidly and rigorously backed by corresponding mathematical entities in the underlying institution.

a. Structured Specifications

Software systems tend to be very complex, and likewise their formal specifications. One key device for the management of this complexity is a structuring mechanism for specifications that allows to develop them in modular way. It has been noticed that structuring systems are largely, if not completely, independent of the logical systems underlying specification formalisms. Hence the idea to study the structuring of specifications and programs at a conceptual level that abstracts away the details of logical systems and instead exploits some of their compositionality properties. This has been the original motivation for institution theory.

Given an institution, considered abstractly, a structured specification is just a term formed by applying a specific fixed set of building operators to blocks consisting of finite set of sentences in the institutions (called basic, flat or unstructured specifications). Then by induction on the structure of a specification $\mathit{SP}$ one may calculate its signature $\mathrm{Sig}(\mathit{SP})$ and its class of models $\mathrm{Mod}(\mathit{SP})$ . Seminal works such as (Sannella and Tarlecki, 1988) have proposed a core set of specification-building operators consisting of renaming (translations), sum, hiding (derivation) which can express most of the concrete structuring operations in the actual specification languages. Often an initial semantics operator is added in order to deal with initial semantics specification modules. A lot of results have been developed on this conceptual basis, providing an uniform and solid foundation for modular software development. A particularly remarkable one is the layered completeness result of Borzyszkowski (2002) that lifts a proof system (considered in the form of an abstract entailment system) from the base institution to structured specifications; under a set of general conditions expressed as properties of the base institution, the completeness of the former yields the completeness of the latter.

A later development by Diaconescu (2012a) proposes an even more abstract approach that avoids particular choices of sets of specification building operators. This abstracts the (structured) specifications as signatures in an abstract ‘upper level’ institution $\mathcal{I}'$ , the relationship to the base institution $\mathcal{I}$ (representing the underlying logic) being axiomatised as a special kind of institution morphism, whose sentence translations are identities, and whose model translations/reducts are inclusions.

b. Heterogeneous Specifications

The increasing complexity of current systems has led to an understanding of the limitations of specification formalisms based upon single logical systems. Hence the emergence of the heterogeneous specification environments based on multiple logical systems. A standard view of such heterogeneous logical environments, actually realised by CafeOBJ (Diaconescu and Futatsugi, 1998) and Hets (Mossakowski, 2005), is as diagrams of institutions that are linked by comorphisms. However this raises the difficult question of how to lift specification theory to the heterogenous level. The answer comes from a category-theoretic construction that originated from algebraic geometry by Grothendieck (1963), and that can be replicated to institutions in order to ‘flatten’ a diagram of institutions to a single institution that retains all data provided by the respective diagram of institutions. This construction is known as the Grothendieck institution associated to the respective diagram. The main idea is to aggregate together all institutions of the diagrams into a big institution and label all the entities by their origin (node or edge in the diagram). This means that a signature of the Grothendieck institution is a pair $(i,\Sigma)$ where $i$ is a node in the diagram and $\Sigma$ is an signature in the institution at $i$ . A signature morphism $(i,\Sigma) \rightarrow (i',\Sigma')$ in the Grothendieck institution is a pair $(u,\varphi)$ where $u$ is an edge in the diagram $i \rightarrow i'$ and $\varphi$ is a signature morphism in the institution at $i'$ from the translation of $\Sigma$ across the institution comorphisms at $u$ to $\Sigma'$ . The $(i,\Sigma)$ -sentences are just the $\Sigma$ -sentences (at $i$ ) and likewise the models, but the translations of both sentences and models across $(u,\varphi)$ make use of the respective translations given by the comorphism at $u$ and the local translations corresponding to $\varphi$ . The Grothendieck institution satisfaction relation $\models_{(i,\Sigma)}$ is just $\models_\Sigma$ of the institution at $i$ .

A series of properties required by specification theory have been gradually established for Grothendieck institutions. These results usually provide sets of sucient (and often necessary) conditions for lifting of institution-theoretic properties from the local level of the component institutions to the global level of the Grothendieck institution.

c. Ontologies

Computer science ontologies can be regarded as logic-based formal specifications. On the basis of this observation Goguen (2006) introduces the institution-theoretic trend in theory of ontologies which represents more or less a rephrasing of well established specification theory concepts and results in an ontology theoretic setup. This has brought several notable gains for ontologies, such as very well developed structuring technologies and the Grothendieck institution approach to logical heterogeneity (Kutz et al., 2010).

This line of development plays the core role in the OMG standard Ontology, Modeling and Specification Integration and Interoperability (OntoIOp).

d. Logic Programming

The Herbrand theorems as foundations of the logic-programming paradigm have been developed at the level of abstract institutions by Diaconescu (2004c). This has opened the possibility to develop logic programming over non-conventional logical structures, thus providing solid foundations for the combination of logic programming and other computing paradigms. Particularly important results in this line of developments are the Herbrand-based foundations for constraint solving (Diaconescu, 2008), which show that at the denotational level constraint solving is just an instance of plain (abstract) logic programming, and logic programming for services (Ţuţu and Fiadeiro, 2015b) that extends the original approach over a concept of generalized substitution system (Ţuţu and Fiadeiro, 2015a).

e. Notes

The work on the specification language Clear (Burstall and Goguen, 1980) was very influential and preceded the institution-theoretic structuring of specifications. Another particularly influential work in this area was (Diaconescu et al., 1993).

Grothendieck institutions, preceded by an attempt by Diaconescu (1998) to lift ‘by-hand’ specification theory concepts and results to the heterogeneous level, have been originally introduced by Diaconescu (2002) but in a slightly improper way using institution morphisms at the edges of the diagram representing the heterogeneous environment; that was soon corrected by Mossakowski (2002) to comorphisms.

The treatment of variables as signature extensions outlined in Sec. 3.c plays a key role in the institution-independent study of logic programming. It is an essential feature of the institutional approach to Herbrand theorems, one that has enabled the development of some of the most fundamental semantic concepts to logic programming, like query and solution, in arbitrary institutions. Despite such mild assumptions, the logic-programming semantics of services (Ţuţu and Fiadeiro, 2015b) does not fit into the framework proposed in (Diaconescu, 2004c). This has led to an upgrade of the original approach, to Herbrand theorems over a concept of generalized substitution system (Ţuţu and Fiadeiro, 2015a) that extends institutions by allowing for direct representations of variables and substitutions, much in the spirit of context institutions (Pawlowski, 1996). The connection between the substitution-system-based and the original institution-independent approach to logic programming was studied in depth in (Ţuţu and Fiadeiro, 2015c).

6. Extensions

While non-classical logics can be captured properly as institutions, some of their fine aspects may be beyond the conventional institution theory. For example, the institutions of many-valued logics handle the ternary aspect of the satisfaction relation by adjoining truth value to the sentences; in this way we get a binary satisfaction relation. While this works well with respect to most aspects of many-valued logics, it cannot handle graded (non-binary) consequences. The same with modal logics, the conventional concept of institution does not allow for a general semantics of modalities. These shortcomings have been overcome by extensions of the definition of institution towards non-classical aspects of logics.

a. Many-valued Truth

The many-valued extension of institution theory is very simple, just replace the binary truth values with any set $L$ of truth values. The satisfaction relation becomes a function

$\models_\Sigma \,\colon\; \mathrm{Sen}(\Sigma) \times \mathrm{Mod}(\Sigma) \rightarrow L$

that for each sentence and model gives a truth value interpreted as a satisfaction degree. The Satisfaction Condition gets rephrased as

$(\mathrm{Mod}(\varphi)(M') \models_\Sigma \rho) = (M' \models_{\Sigma'} \mathrm{Sen}(\varphi)(\rho)).$

Very often it is necessary that $L$ comes as a partial order of some kind, such as lattice. In order to get a genuine many-valued implication one needs even more, that $L$ is a residuated lattice.

b. Modalities

The stratified institutions of Aiguier and Diaconescu (2007) refine institutions by considering models with states. Thus each model $M$ comes equipped with a designated set $[\![ M ]\!]$ , and this is subject to several coherent conditions. In the case of Kripke models $M$ , $[\![ M ] \!]$ gives the set of the possible worlds.

c. Notes

The idea to extend the definition of institution to many-valued truth arose at the beginning of institution theory (Mayoh, 1985) motivated by research in data base theory; this was already mentioned in (Goguen and Burstall, 1992). Later works on many-valued institutions include (Eklund and Helgesson, 2010; Diaconescu, 2013, 2014).

7. References and Further Reading

a. Primary Sources

Răzvan Diaconescu. Institution-independent Model Theory. Birkhäuser, 2008.
Joseph Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.
Joseph Goguen and Grigore Ro¸su. Institution morphisms. Formal Aspects of Computing, 13:274–307, 2002.
José Meseguer. General logics. In H.-D. Ebbinghaus et al., editors, Proceedings, Logic Colloquium, 1987, pages 275–329. North-Holland, 1989.
Till Mossakowski, Joseph Goguen, Răzvan Diaconescu, and Andrzej Tarlecki. What is a logic? In Jean-Yves Béziau, editor, Logica Universalis, pages 113–133. Birkhäuser, 2005. 19
Till Mossakowski, Răzvan Diaconescu, and Andrzej Tarlecki. What is a logic translation? Logica Universalis, 3(1):59–94, 2009.
Donald Sannella and Andrzej Tarlecki. Foundations of Algebraic Specifications and Formal Software Development. Springer, 2012.

b. Secondary Sources

Marc Aiguier and Răzvan Diaconescu. Stratified institutions and elementary homomorphisms. Information Processing Letters, 103(1):5–13, 2007. 01.
Arrais and José L. Fiadeiro. Unifying theories in different institutions. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Recent Trends in Data Type Specification, volume 1130 of Lecture Notes in Computer Science, pages 81–101. Springer, 1996.
Edigio Astesiano, Michel Bidoit, Hélène Kirchner, Berndt Krieg-Brückner, Peter Mosses, Don Sannella, and Andrzej Tarlecki. CASL: The common algebraic specification language. Theoretical Computer Science, 286(2):153–196, 2002.
Tomasz Borzyszkowski. Logical systems for structured specifications. Theoretical Computer Science, 286(2):197–245, 2002.
Rod Burstall and Joseph Goguen. The semantics of Clear, a specification language. In Dines Bjorner, editor, 1979 Copenhagen Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 292–332. Springer, 1980.
Maura Cerioli and José Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997.
Mihai Codescu and Daniel Găină. Birkhoff completeness in institutions. Logica Universalis, 2(2):277–309, 2008.
Răzvan Diaconescu. Extra theory morphisms for institutions: logical semantics for multi-paradigm languages. Applied Categorical Structures, 6(4):427–453, 1998. A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997.
Răzvan Diaconescu. Grothendieck institutions. Applied Categorical Structures, 10(4):383–402, 2002. Preliminary version appeared as IMAR Preprint 2-2000, ISSN 250-3638, February 2000.
Răzvan Diaconescu. Institution-independent ultraproducts. Fundamenta Informaticæ, 55(3-4):321–348, 2003.
Răzvan Diaconescu. An institution-independent proof of Craig Interpolation Theorem. Studia Logica, 77(1):59–79, 2004a.
Răzvan Diaconescu. Elementary diagrams in institutions. Journal of Logic and Computation, 14(5):651–674, 2004b.
Răzvan Diaconescu. Herbrand theorems in arbitrary institutions. Information Processing Letters, 90:29–37, 2004c.
Răzvan Diaconescu. An axiomatic approach to structuring specifications. Theoretical Computer Science, 433:20–42, 2012a.
Răzvan Diaconescu. Borrowing interpolation. Journal of Logic and Computation, 22(3):561–586, 2012b.
Răzvan Diaconescu. Institutional semantics for many-valued logics. Fuzzy Sets and Systems, 218:32–52, 2013.
Răzvan Diaconescu. Graded consequence: an institution theoretic study. Soft Computing, 18(7):1247–1267, 2014.
Răzvan Diaconescu and Kokichi Futatsugi. CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, volume 6 of AMAST Series in Computing. World Scientific, 1998.
Răzvan Diaconescu and Marius Petria. Saturated models in institutions. Archive for Mathematical Logic, 49(6):693–723, 2010.
Răzvan Diaconescu and Petros Stefaneas. Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science, 379(1):210–230, 2007.
Răzvan Diaconescu, Joseph Goguen, and Petros Stefaneas. Logical support for modularisation. In Gerard Huet and Gordon Plotkin, editors, Logical Environments, pages 83–130. Cambridge, 1993. Proceedings of a Workshop held in Edinburgh, Scotland, May 1991. 20
Patrick Eklund and Robert Helgesson. Monadic extensions of institutions. Fuzzy Sets and Systems, 161:2354–2368, 2010.
Joseph Goguen. Types as theories. In George Michael Reed, Andrew William Roscoe, and Ralph F. Wachter, editors, Topology and Category Theory in Computer Science, pages 357–390. Oxford, 1991. Proceedings of a Conference held at Oxford, June 1989.
Joseph Goguen. Data, schema, ontology and logic integration. Journal of IGPL, 13(6):685–715, 2006.
Joseph Goguen and Rod Burstall. Introducing institutions. In Edward Clarke and Dexter Kozen, editors, Proceedings, Logics of Programming Workshop, volume 164 of Lecture Notes in Computer Science, pages 221–256. Springer, 1984.
Daniel Găină. Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally. Logica Universalis, 8(3): 469–498, 2014.
Daniel Găină and Marius Petria. Completeness by forcing. Journal of Logic and Computation, 20(6):1165–1186, 2010.
Daniel Găină and Andrei Popescu. An institution-independent proof of Robinson consistency theorem. Studia Logica, 85(1): 41–73, 2007.
Daniel Găină, Kokichi Futatsugi, and Kazuhiro Ogata. Constructor-based logics. J. of Universal Computer Science, 18 (2204–2233), 2012.
Oliver Kutz, Till Mossakowski, and Dominik Lücke. Carnap, Goguen, and the hyperontologies – logical pluralism and heterogeneous structuring in ontology design. Logica Universalis, 4(2):255–333, 2010.
Brian Mayoh. Galleries and institutions. Technical Report DAIMI PB-191, Aarhus University, 1985.
Till Mossakowski. Comorphism-based Grothendieck logics. In K. Diks and W. Rytter, editors, Mathematical foundations of computer science, volume 2420 of Lecture Notes in Computer Science, pages 593–604. Springer, 2002.
Till Mossakowski. Heterogeneous specification and the heterogeneous tool set. Habilitation thesis, University of Bremen, 2005.
Wieslaw Pawlowski. Context institutions. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Recent Trends in Data Type Specification, volume 1130 of Lecture Notes in Computer Science, pages 436–457. Springer, 1996.
Marius Petria and Răzvan Diaconescu. Abstract Beth definability in institutions. Journal of Symbolic Logic, 71(3):1002–1028, 2006.
Donald Sannella and Andrzej Tarlecki. Specifications in an arbitrary institution. Information and Control, 76:165–210, 1988.
Andrzej Tarlecki. On the existence of free models in abstract algebraic institutions. Theoretical Computer Science, 37:269–304, 1986a.
Andrzej Tarlecki. Bits and pieces of the theory of institutions. In David Pitt, Samson Abramsky, Axel Poigné, and David Rydeheard, editors, Proceedings, Summer Workshop on Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 334–360. Springer, 1986b.
Andrzej Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33(3):333–360, 1986c.
Ionuţ Ţuţu and José L. Fiadeiro. From conventional to institution-independent logic programming, 2015a.
Ionuţ Ţuţu and José L. Fiadeiro. Service-oriented logic programming, 2015b.
Ionuţ Ţuţu and José L. Fiadeiro. Revisiting the institutional approach to Herbrand’s theorem. In Algebra and Coalgebra in Computer Science, Leibniz International Proceedings in Informatics. Schloss Dagstuhl, 2015c.
George Voutsadakis. Categorical abstract algebraic logic: Algebrizable institutions. Applied Categorical Structues, 10: 531–568, 2002.

c. Auxiliary Non-Institutional Sources

Jon Barwise. Axioms for abstract model theory. Annals of Mathematical Logic, 7:221–265, 1974. 21
Jean-Yves Béziau, editor. Universal Logic: an Anthology. Studies in Universal Logic. Springer Basel, 2012.
Chen-Chung Chang and H. Jerome Keisler. Model Theory. North Holland, Amsterdam, 1990.
Samuel Eilenberg and Saunders Mac Lane. General theory of natural equivalences. Transactions of the American Mathematical Society, 58:231–294, 1945.
Joseph Goguen. A categorical manifesto. Mathematical Structures in Computer Science, 1(1):49–67, March 1991. Joseph Goguen. Programming Research Group Technical Monograph PRG–72, Oxford University, March 1989.
Alexandre Grothendieck. Catégories fibrées et descente. In Revêtements étales et groupe fondamental, Séminaire de Géométrie Algébraique du Bois-Marie 1960/61, Exposé VI. Institut des Hautes Études Scientifiques, 1963. Reprinted in Lecture Notes in Mathematics, Volume 224, Springer, 1971, pages 145–94.
Andrei N. Kolmogorov. On the principle of the excluded middle. Matematicheskii Sbornik, 32(646–667), 1925. (in Russian).
Jerzy Ło´s. Quelques remarques, théorèmes et problèmes sur les classes définissables d’algèbres. In Mathematical Interpretation of Formal Systems, pages 98–113. North-Holland, Amsterdam, 1955.
Saunders Mac Lane. Categories for the Working Mathematician. Springer, second edition, 1998.
Günter Matthiessen. Regular and strongly finitary structures over strongly algebroidal categories. Canadian Journal of Mathematics, 30:250–261, 1978.
Alfred Tarski. The semantic conception of truth. Philos. Phenomenological Research, 4:13–47, 1944.
Johan van Bentham. Modal Logic and Classical Logic. Humanities Press, 1988.

Author Information

Răzvan Diaconescu
Email: Razvan.Diaconescu@imar.ro
Simion Stoilow Institute of Mathematics of the Romanian Academy
Romania

Institution Theory

Table of Contents

1. History

a. Origins

b. Early Developments

c. Later Developments

d. Notes

2. The Concept of Institution

a. Signatures

b. Sentences

c. Models

d. Satisfaction

e. Concrete Institutions

f. Notes

3. Institution-independent Model Theory

a. The Galois Connection between Syntax and Semantics

b. Logical Connectors

c. Quantifiers

d. Diagrams

e. Ultraproducts

f. Interpolation and Definability

g. Layered Completeness

h. Notes

4. Logic by Translation

a. Morphisms and Comorphisms

b. Encodings

c. Borrowing

d. Notes

5. Contributions to Computing Science

a. Structured Specifications

b. Heterogeneous Specifications

c. Ontologies

d. Logic Programming

e. Notes

6. Extensions

a. Many-valued Truth

b. Modalities

c. Notes

7. References and Further Reading

a. Primary Sources

b. Secondary Sources

c. Auxiliary Non-Institutional Sources

Author Information

An encyclopedia of philosophy articles written by professional philosophers.