Institution-independent model theory (Q2469760)

The theory of institutions is a categorical abstract model theory which formalizes the intuitive notion of a logical system, including syntax, semantics, and the satisfaction relation between them. Institutions constitute a model-oriented meta-theory on logics similarly to how the theory of rings and modules constitutes a meta-theory for classical linear algebra. Another analogy can be drawn with universal algebra versus particular algebraic structures such as groups, rings, modules, or with mathematical analysis over Banach spaces versus real analysis. This is a book about doing model theory without an underlying logical system. This approach is based upon the theory of institutions, which has witnessed a vigorous and systematic development over the past two decades and which provides an ideal framework of true abstract model theory. Also, this book is far from being a complete encyclopedia of institution-independent model theory. The book consists of four parts. The first part contains the basic institution theory including the concepts of institution and institution morphism, and several model-theoretic fundamental concepts such as model amalgamation, (elementary) diagrams, inclusion systems, and free models. The author develops an internal logic for abstract institutions, which includes a semantic treatment of Boolean connectives, quantifiers, atomic sentences, substitutions, and elementary homomorphisms, all of them in an institution-independent setting. The second part is the core of the institution-independent model-theoretic study because it develops the main model-theoretic methods and results in an institution-independent setting. The first method considered in this part is that of ultraproducts. The author develops a fundamental ultraproducts theorem in an institution-independent setting and explores some of its immediate consequences, such as ultrapower embeddings and compactness. The chapter on saturated models starts by developing sufficient conditions for directed colimits of homomorphisms to retain the elementarity. This rather general version of Tarski's elementary chain theorem is a prerequisite for a general result about the existence of saturated models, later used for developing other important results. Also, the author develops the complementary result on uniqueness of saturated models. Here the necessary concept of cardinality of a model is handled categorically with the help of elementary extensions, a concept given by the method of diagrams. The author develops an important application for the uniqueness of saturated models, namely a generalized version of the remarkable Keisler-Shelah result in first-order model theory, ``two models are elementarily equivalent if and only if they have isomorphic ultrapowers''. A good application of the existence result for saturated models is seen in preservation results, such as ``a theory has a set of universal axioms if and only if its class of models is closed under sub-models''. The author develops a generic preservation-by-saturation theorem. Such preservation results might lead us straight to their axiomatizability versions. One way is to assume the Keisler-Shelah property for the institution and to use a direct consequence of the fundamental ultraproducts theorem which may concisely be read as ``a class of models is elementary if and only if it is closed under elementary equivalence and ultraproducts''. Another method to obtain an important class of axiomatizability results is by expressing the satisfaction Horn sentences as categorical injectivity. This leads to general quasi-variety theorems, such as ``a class of models is closed under products and sub-models if and only if it is axiomatizable by a set of (universal) Horn sentences'', and variety theorems, such as ``a class of models is closed under products and sub-models and homomorphic images if and only if it is axiomatizable by a set of (universal) atoms''. All axiomatizability results presented are collected under the abstract concept of Birkhoff institution. The next topic is interpolation. The institution-independent approach brings several significant upgrades to the conventional formulation. The author develops three main methods for obtaining the interpolation property, the first two having rather complementary application domains. The first one is based upon a semantic approach to interpolation and exploits the Birkhoff-style axiomatizability properties of the institution, while the second, inspired by the conventional methods of first-order logic, is via Robinson consistency. The third one is a borrowing method across institutions. The author next treats definability, again with two rather complementary methods, via Birkhoff-style axiomatizability and via interpolation. While the latter represents a generalization of Beth's theorem of conventional first-order model theory, the former reveals a causality relationship between axiomatizability and definability. The final chapter of the second part of the book is devoted to possible worlds (Kripke) semantics and to extensions of the satisfaction relation of abstract institutions to modal satisfaction. By applying the general ultraproducts method to possible worlds semantics, the author develops the preservation of modal satisfaction by ultraproducts together with its semantic compactness consequence. The third part of the book is devoted to special modern topics in institution theory, such as Grothendieck constructions on systems of institutions with applications to heterogeneous multi-logic frameworks, and an extension of institutions with proof-theoretic concepts. For the Grothendieck institutions the author develops a study of lifting of important properties, such as theory colimits, model amalgamation, and interpolation, from the level of the local institutions to the global Grothendieck institution. Also, the author presents a rather striking application of the interpolation result for Grothendieck institutions, which leads, for example, to a quite surprising interpolation property in the Horn fragment of conventional first-order logic. The chapter on proof theory for institutions introduces the concept of proof in a simple way that suits the model theory, explores proof-theoretic versions of compactness and internal logic, and presents general soundness results for institutions with proofs. The final part of this chapter develops a general sound and complete Birkhoff-style proof system with applications significantly wider than those of the Horn institutions. The last part presents a few of the multitude of applications of institution-independent model theory to computer science, especially in the areas of formal specification and logic programming. This includes structured specifications over arbitrary institutions, the lifting of a complete calculus from the base institution to structured specifications, Herbrand theorems and modularization for logic programming, and semantics of logic programming with pre-defined types. The concepts introduced and the results obtained are illustrated in the main text by their applications to the model theory of conventional logic (which includes first-order logic but also fragments and extensions of it).