Abstract The theory of stratified institutions is a general axiomatic approach to model theories where the satisfaction is parameterized by states of the models. In this paper we further develop this theory by introducing a new technique for representing stratified institutions, which is based on projecting to such simpler structures. On the one hand this can be used for developing general results applicable to a wide variety of already existing model theories with states, such as those based on some form of Kripke semantics. On the other hand this may serve as a template for defining new such model theories. In this paper we emphasize the former application of this technique by developing general results on model amalgamation and on the existence diagrams for stratified institutions. These are two most useful properties to have in institution theoretic model theory.

We propose stratified institutions (a decade old generalised version of the theory of institutions of Goguen and Burstall) as a fully abstract model theoretic approach to modal logic. This allows for a uniform treatment of model theoretic aspects across the great multiplicity of contemporary modal logic systems. Moreover Kripke semantics (in all its manifold variations) is captured in an implicit manner free from the sometimes bulky aspects of explicit Kripke structures, also accommodating other forms of concrete semantics for modal logic systems. The conceptual power of stratified institutions is illustrated with the development of a modal ultraproducts method that is independent of the concrete details of the actual modal logical systems. Consequently, a wide array of compactness results in concrete modal logics may be derived easily.

This special issue contains papers related to Universal Logic and Computation. The work on this special issue started about three years ago with the intention to dedicate it to Jean-Yves Béziau on the occasion of his 50th anniversary which actually took place a couple of years ago in the middle of the process of preparing this special issue. I think even now it is not too late to dedicate it to Jean-Yves, who has been and still is a main promoter of this quite revolutionary new trend in logic, known as Universal Logic. He has done this especially by building from scratch a quite amazing academic infrastructure in support of Universal Logic. This includes a dedicated World Congress and School (until now there have been five such events), a book series (Studies in Universal Logic, Springer Basel) and a journal (Logica Universalis, Springer Basel). Although Universal Logic has been clearly recognized as a trend in mathematical logic since about one decade only, it had a presence here and there since much longer. Universal Logic ideas can be traced back to the work of Paul Herz in 1922. In fact there is a whole string of famous names in logic that have been involved with Universal Logic in the last century, including Paul Bernays, Kurt Gödel, Alfred Tarski, Haskell Curry, Jerzy Łoś, Roman Suszko, Saul Kripke, Dana Scott, Dov Gabbay, etc. Universal Logic is not a new super-logic, but it is rather a body of general theories of logical structures, similarly, universal algebra is a general theory of algebraic structures. Within the last century mathematical logic has witnessed the birth of a multitude of unconventional logical systems, such as intuitionistic, modal, multiple valued, paraconsistent, non-monotonic logics, etc. Moreover, a big number of new logical systems have appeared in computer science, especially in the area of formal methods. The universal logic trend constitutes a response to this new multiplicity by the development of general concepts and methods applicable to a great variety of logical systems.

We define and develop the concept of quasi-variety for models of hybrid logics and we apply this for determining initial semantics for classes of hybrid logics theories. The hybrid logic is considered here in a very general sense, internal to abstract institutions (in the sense of the so-called institution theory of Goguen and Burstall). This means our result is applicable to a wide variety of hybrid logics including, e.g. those resulting from the various kinds of combinations between conventional hybrid logics and various other logical systems.

A ‘hybridization’ of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By ‘hybridized institutions’ we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated $\mathcal{FOL}$ ) as a ‘hybridization’ process of abstract encodings of institutions into $\mathcal{FOL}$ , which may be seen as an abstraction of the well-known standard translation of modal logic into $\mathcal{FOL}$ . The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover, we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to $\mathcal{FOL}$ .

We present a generic method for establishing interpolation properties by ‘borrowing’ across logical systems. The framework used is that of the so-caled ‘institution theory’ which is a categorical abstract model theory providing a formal definition for the informal concept of ‘logical system’ and a mathematical concept of ‘homomorphism’ between logical systems. We develop three different styles or patterns to apply the proposed borrowing interpolation method. These three ways are illustrated by the development of a series of concrete interpolation results for logical systems that are used in mathematical logic or in computing science, some of these interpolation properties apparently being new results. These logical systems include fragments of (classical many sorted) first-order logic with equality, preordered algebra and its Horn fragment, partial algebra, higher order logic. Applications are also expected for many other logical systems, including membership algebra, various types of order sorted algebra, the logic of predefined types, etc., and various combinations of the logical systems discussed here.

We give a logic-independent semantics for predefined (data) types within the categorical abstract model theoretic framework of the theory of institutions. We develop a generic interpolation result for this semantics, which can be easily applied to various concrete situations from the theory and practice of specification and programming. Our study of interpolation is motivated by a number of important applications to computing science, especially in the area of structured specifications.

Abstract This paper studies definability within the theory of institutions, a version of abstract model theory that emerged in computing science studies of software specification and semantics. We generalise the concept of definability to arbitrary logics, formalised as institutions, and we develop three general definability results. One generalises the classical Beth theorem by relying on the interpolation properties of the institution. Another relies on a meta Birkhoff axiomatizability property of the institution and constitutes a source for many new actual definability results, including definability in (fragments of) classical model theory. The third one gives a set of sufficient conditions for ‘borrowing’ definability properties from another institution via an ‘adequate’ encoding between institutions. The power of our general definability results is illustrated with several applications to (many-sorted) classical model theory and partial algebra, leading for example to definability results for (quasi-)varieties of models or partial algebras. Many other applications are expected for the multitude of logical systems formalised as institutions from computing science and logic.

Institutions with proof-theoretic structure, here called ‘institutions with proofs’, provide a complete formal notion for the intuitive notion of logic, including both the model and the proof theoretic sides. This paper introduces a concept of proof rules for institutions and argues that the proof systems of the actual institutions with proofs are freely generated by their presentations as systems of proof rules. We also show that proof-theoretic quantification, an institutional refinement of the (meta-)rule of Generalization from classical logic, can also be added freely to any proof system. By applying these universal properties, we are able to provide some general compactness results for proof systems and some general soundness results for institutions with proofs. We also discuss several open problems and further research directions.

We generalize the method of diagrams from conventional model theory to a simple institution-independent (i.e. independent of the details of the actual logic formalized as an institution) framework based on a novel categorical concept of elementary diagram of a model. We illustrate the power of our institution-independent method of elementary diagrams by developing several applications to institution liberality, institution-independent quasi-varieties, and limits and colimits of presentation models. The results obtained are illustrated systematically with examples from several different specification logics. In the introduction we also discuss the relevance of our institution-independent approach to the model theory of algebraic specification and computing science, but also to conventional and abstract model theory.

Equational deduction is generalised within a category-based abstract model theory framework, and proved complete under a hypothesis of quantifier projectivity, using a semantic treatment that regards quantifiers as models rather than variables, and valuations as model morphisms rather than functions. Applications include many- and order-sorted (conditional) equational logics, Horn clause logic, equational deduction modulo a theory, constraint logics, and more, as well as any possible combination among them. In the cases of equational deduction modulo a theory and of constraint logic the completeness result is new. One important consequence is an abstract version of Herbrand's Theorem, which provides an abstract model theoretic foundation for equational and constraint logic programming.

This paper surveys several different variants of order sorted algebra (abbreviatedOSA), comparing some of the main approaches (overloaded OSA, universe OSA, unified algebra, term declaration algebra,etc.), emphasising motivation and intuitions, and pointing out features that distinguish the original ‘overloaded’ OSA approach from some later developments. These features include sort constraints and retracts; the latter is particularly useful for handling multiple data representations (including automatic coercions among them). Many examples are given, for most of which, runs are shown on the OBJ3 system. This paper also significantly generalises overloaded OSA by dropping the regularity and monotonicity assumptions, and by adding signatures of non-monotonicities, which support simple semantics for some aspects of object oriented programming. A number of new results for this generalisation are proved, including initiality, variety, and quasi-variety theorems. Axiomatisability results àlaBirkhoff are also proved for unified algebras.