Institution-Independent Model Theory

ISBN-13: 9783764387075 / Angielski / Miękka / 2008 / 376 str.

Razvan Diaconescu

Opis

This book develops model theory independently of any concrete logical system or structure, within the abstract category-theoretic framework of the so called 'institution theory'. The development includes most of the important methods and concepts of conventional concrete model theory at the abstract institution-independent level. Consequently it is easily applicable to a rather large diverse collection of logics from the mathematical and computer science practice.

Spis treści

1. Introduction.- 2. Categories.- 2.1 Basic Concepts.- 2.2 Limits and Co-limits.- 2.3 Adjunctions.- 2.4 2-categories.- 2.5 Indexed Categories and Fibrations.- 3. Institutions.- 3.1 From concrete logic to Institutions.- 3.2 Examples of institutions.- 3.3 Morphisms and Comorphisms.- 3.4 Institutions as Functors.- 4. Theories and Models.- 4.1 Theories and Presentations.- 4.2 Theory (co-)limits.- 4.3 Model Amalgamation.- 4.4 The method of Diagrams.- 4.5 Inclusion Systems.- 4.6 Free Models.- 5. Internal Logic.- 5.1 Logical Connectives.- 5.2 Quantifiers.- 5.3 Substitutions.- 5.4 Representable Signature Morphisms.- 5.5 Satisfaction by Injectivity.- 5.6 Elementary Homomorphisms.- 6. Model Ultraproducts.- 6.1 Filtered Products.- 6.2 Fundamental Theorem.- 6.3 Los Institutions.- 6.4 Compactness.- 6.5 Finitely Sized Models.- 7. Saturated Models.- 7.1 Elementary Co-limits.- 7.2 Existence of Saturated Models.- 7.3 Uniqueness of Saturated Models.- 7.4 Saturated Ultraproducts.- 8. Preservation and Axiomatizability.- 8.1 Preservation by Saturation.- 8.2 Axiomatizability by Ultraproducts.- 8.3 Quasi-varieties and Initial Models.- 8.4 Quasi-Variety Theorem.- 8.5 Birkhoff Variety Theorem.- 8.6 General Birkhoff Axiomatizability.- 9. Interpolation.- 9.1 Semantic interpolation.- 9.2 Interpolation by Axiomatizability.- 9.3 Interpolation by Consistency.- 9.4 Craig-Robinson Interpolation.- 9.5 Borrowing Interpolation.- 10. Definability.- 10.1 Explicit implies implicit definability.- 10.2 Definability by Interpolation.- 10.3 Definability by Axiomatizability.- 11. Possible Worlds.- 11.1 Internal Modal Logic.- 11.2 Ultraproducts of Kripke models.- 12. Grothendieck Institutions.- 12.1 Fibred and Grothendieck Institutions.- 12.2 Theory Co-limits and Model Amalgamation.- 12.3 Interpolation.- 13. Institutions with Proofs.- 13.1 Free Proof Systems.- 13.2 Compactness.- 13.3 Proof-theoretic Internal Logic.- 13.4 The Entailment Institution.- 13.5 Birkhoff Completeness.- 14. Specification.- 14.1 Structured Specifications.- 14.2 Specifications with Proofs.- 14.3 Predefined Types.- 15. Logic Programming.- 15.1 Herbrand Theorems.- 15.2 Unification.- 15.3 Modularization.- 15.4 Constraints.- A Table of Notation.- Bibliography.- Index

Blurb

A model theory that is independent of any concrete logical system allows a general handling of a large variety of logics. This generality can be achieved by applying the theory of institutions that provides a precise mathematical formulation for the intuitive concept of a logical system. Especially in computer science, where the development of a huge number of specification logics is observable, institution-independent model theory simplifies and sometimes even enables a concise model-theoretic analysis of the system. Besides incorporating important methods and concepts from conventional model theory, the proposed top-down methodology allows for a structurally clean understanding of model-theoretic phenomena. As a consequence, results from conventional concrete model theory can be understood more easily, and sometimes even new results are obtained.