A R lgebraic elativization AND A L rrow ogic ILLC Dissertation Series 1995-3 institute/or logic, language computation and For further information about ILLC-publications, please contact Institute for Logic, Language and Computation Universiteit van Amsterdam Plantage Muidergracht 24 1018 TV Amsterdam phone: +31-20-5256090 fax: +31-20-5255101 e-mail: [email protected] A R lgebraic elativization and A L rrow ogic Academisch Proefschrift ter verkrijging van de graad van doctor aan de Universiteit van Amsterdam, op gezag van de Rector Magnificus Prof.dr P.W.M. de Meijer in het openbaar te verdedigen in de Aula der Universiteit (Oude Lutherse Kerk, ingang Singel 411, hoek Spui) op vrijdag 3 februari te 13.00 uur door Maarten Johannes Marx geboren te Amsterdam. Promotors: Prof.dr. J.F.A.K. van Benthem Prof dr. I. Nemeti Co-promotor: Dr. J.M.F Masuch CIP-GEGEVENS KONINKLUKE BEBLIOTHEEK, DEN HAAG Marx, Maarten Johannes Algebraic relativization and arrow logic / Maarten Johannes Marx. - Amsterdam : Institute for Logic, Language and Computation. - (ILLC dissertation series ; 1995-3) Proefschrift Universiteit van Amsterdam. - Met lit. opg., reg. ISBN 90-74795-15-3 NUGI811 Trefw.: algebra / logica. Copyright © 1995 by Maarten Marx Cover: Saint Sebastian by Egon Schiele ISBN: 90-74795-15-3 C ontents Acknowledgments vii Introduction 1 1 Main themes 5 LI Arrow logic is the modal logic of transitions...................... 5 1.2 Cylindric modal logic is the modal logic of assignments........................ 7 1.3 Relativization............................................................................................ 10 1.4 Fine structure of definability.................................................................... 10 1.5 BAO’s and general modal logic ............................................................... 11 2 The Algebras and the Logics 13 2.1 BAO’s, general modal logic and Kripke frames....................................... 13 2.2 Review of basic duality theory.................................................................. 18 2.3 Relativization and the logical core............................................................ 23 2.4 Relation algebras, arrow logic and arrow frames.................................... 25 2.5 Cylindric algebras, cylindric modal logic and alpha frames.................. 36 3 Decidability 45 3.1 Filtrations................................. .4 5 3.2 Relativized relation algebras . . .5 0 3.3 Relativized cylindric algebras........................ .5 2 3.4 Concluding remarks.......................................... .5 5 4 Representation &: Axiomatization 57 4.1 Axiomatizing BAO’s by representing frames . . 57 4.2 Relativized relation algebras........................ ................................. 58 4.3 Reducts of relativized relation algebras...... ................................. 69 4.4 Adding the difference operator................................................................. 74 4.5 Representing BAO’s as algebras of relations.......................................... 85 4.6 Concluding remarks............................................................................ . . 95 5 Amalgamation & Interpolation 97 5.1 Amalgamation, interpolation and definability . . .9 8 5.2 Zigzag products.......................... . 104 5.3 Preservation................................ .110 5.4 Applications to relation and cylindric algebras............ .113 5.5 Concluding remarks......................................................... .118 5.6 Appendix: Reformulation of (S)AP with applications . .118 6 Applications to Arrow Logic 127 6.1 Introduction...................................................................................................127 6.2 The core language..........................................................................................130 6.3 Expansions of the core language..................................................................133 6.4 Two-Sorted arrow logic.................................................................................144 6.5 Concluding remarks.......................................................................................150 Bibliography 151 Index 159 List of symbols 161 Samenvatting 165 vi A cknowledgments Zonder de enorme steun en het grote vertrouwen van mijn promotors en copromotor was dit proefschrift er nooit gekomen. Ik wil hen hiervoor oprecht danken. Michael Masuch dank ik vooral voor het vertrouwen wat hij in mij stelde om een voor hem en mij onbekende weg in te slaan en mij daarop voort te laten gaan. Ik dank Johan van Benthem voor zijn zeer bijzondere aandacht en voor de unieke wijze waarop hij een verzameling ideeen hielp omvormen tot een geheel. Nemeti 1st van befogadott a magyarok csaladjaba! Koszonom neki, es vele egyiitt az egesz LGS-nek a bizalmat, biztatast es tamogatast. Mijn tijd als AIO heb ik als zeer bijzonder ervaren. Ik heb erg genoten van de lessen die ik volgde bij de logici en taalkundigen aan de faculteit der wijsbegeerte en aan het FWI. Dank aan alien die mij zo voortreffelijk hebben onderwezen. Koszonom az LGS minden tagjanak a kituno legkort, amiben Budapesten dolgoztunk. A1 mijn collegas op het CCSOM wil ik hartelijk danken voor de prettige werksfeer die er altijd heerste op ons kleine instituutje. Speciale dank gaat uit naar Hajnal Andreka, Ildiko Sain, Andras Simon, Yde Venema, Szabolcs Mikulas, Agnes Kurucz en Laszlo Polos voor hun geduld en hun uitvoerige en waardevolle commentaar op eerdere versies van dit proefschrift. Een bijzondere rol in de totstandkoming van dit proefschrift is gespeeld door de “snelkookpan”. Ik dank alle aanwezigen, Marianne, de Natasha’s, Johan, Yde, Szabolcs, Lennert, Arriette, Maarten, Jerry, Michiel, Andras en Peter voor de leuke en vruchtbare vrijdagmiddagen. Tenslotte dank ik het NWO en Tempus voor de beurzen waarmee ik verscheidene malen naar het buitenland kon reizen en Jaap en Breanndan voor hun technische steun bij het vervaardigen van dit manuscript. Naast de kring van bijzondere mensen met wie ik heb mogen samenwerken zijn ook mijn familie en vrienden van groot belang voor mij geweest. Een aantal wil ik persoonlijk danken. Ik dank mijn ouders, mijn zus Mieke, Martin, Zsofia, mijn vriendjes Sanne, Laura, Mark en Severin, de jongens van “Pussy Twister”, en Anna, Kati, Peter en Adrika in Budapest. Tot slot dank ik alle anderen met wie ik deze jaren gelachen, gedronken, herrie gemaakt of geslapen heb. Jullie warmte betekent zeer veel voor mij. Amsterdam Maarten Marx December, 1994. I ntroduction Parsimony in applying logic When one wants to use logic to formalize a problem in such diverse fields as philosophy, linguistics or computer science, the first difficulty one encounters is the following: What is the appropriate logic which fits my specific problem? There are two parameters in the above question which have to be made clear: appro­ priateness and fit. Assume that one has indeed good reasons to use formal logic1. It is easy to make the first criterion precise: the logic should contain enough ex­ pressive power to give an accurate description of the problem. A good example is Propositional Dynamic Logic (PDL) (cf. Harel [Har84]), which is expressive enough to formalize the regular programming constructions. Another example is first-order (FO) logic, which is expressive enough to capture most of mathematical reasoning. Whether a logic fits a specific problem, is a question which seems harder to answer. While the appropriateness criterion asks for enough expressive power, a good fit could mean that there is not too much. In this view, the two criteria become necessary and sufficient conditions on the expressive power of a logic. Clearly, there is more to say about fit, but we stay with expressive power for a moment. The expressive power of a logic is closely connected to its complexity. In the article titled Sources of Complexity: Content versus Wrapping, J. van Benthem describes this situation as follows: Any description of a subject carries its own price in terms of complexity. To understand what is being described, one has to understand the mechanism of the language or logic employed, adding the complexity of the encoder to the subject matter being encoded. Put more succinctly, “complexity is a package of subject matter plus analytic tools”. ([Ben94b], p.l) Since one of the main advantages of a formalized problem is that one can make definite statements about the complexity of the problem, a close fit between the complexity of the encoder and that of the subject matter seems to be a sine qua non. As van Benthem describes: ... working logicians in linguistics or computer science often have the gut feeling that the styles of reasoning they are analyzing are largely decidable (...), but it is hard to give any mathematical underpinning of these working intuitions. ([Ben94b], p.9) Could it be that the logic they used is appropriate, but does not fit in the sense that it contains an excess of expressive power? After all, when proving decidability, one proves decidability of the encoder, not of the subject matter. ’In the broad sense that a syntax and a semantics are precisely defined, so that a mathematical investigation of that logic itself becomes possible. 2 Introduction Two good examples of logics, carefully designed for the problem at hand, are the above mentioned PDL and the Lambek Calculus (cf. Lambek [Lam58], van Benthem [Ben88]). Both are decidable. Both2 can be viewed as a fragment of Relation Alge­ bra, which is undecidable. Besides being decidable, these two logics have found many applications besides their original purposes. This brings us to a second point one should make about the fitness condition, and which might conflict with the previous one. How close should the fit between logical language and problem be? If we use only binary relations in the description of the problem, should we then abandon unary predicates in our logic? Should we always include all Booleans? One should be liberal here, and allow “natural” logics, which are rich enough to express the original problem, but which fit well with respect to complexity. To conclude, when designing a logic for a specific problem, it seems to pay off to do one’s conceptual homework Instead of taking the well-driven paths and diving straight into deep water, assuming a beginner’s mind seems to be more fruitful: What are the operations needed? What are the objects to be modeled and how much mathematical structure is needed to model them? What are the models? etc. If the conceptual homework is done well at this early stage of the work, there is reason to be confident in the complexity results later on. In subsequent chapters, we will investigate decidable versions of relation algebra (cf. e.g., Jonsson [Jon91] or Maddux [Mad91b], for an introduction) and of first-order logic (with finitely or infinitely many variables). Stating and motivating the results, we will hardly refer to applications, letting the future decide whether these weakened logics can indeed play a role as sketched above. The results presented here can be viewed as additions to the tool- box of the ap­ plied logician. Since these two logics are well-known and frequently used, it seems indispensable to have “computationally well-behaved” versions of them as well. ARROW Logic. As is well known, the classical models for relation algebras are not finitely axiomatizable (Monk [Mon64], Andreka [And91a]), their equational theory is highly undecidable (Tarski-Givant [TG87], Andreka et al. [AKN+94]), and the corre­ sponding logic does not even have the weakest form of Craig Interpolation (Sain -Simon [SS94]). Almost the only positive thing one can mention is its enormous expressive power. (E.g., in Tarski -Givant [TG87] it is shown that this formalism is expressive enough to formalize set theory.) The research project of looking for weakened decidable versions of relation algebra became known under the name of Arrow Logic (cf. van Benthem [Ben91a], Venema [Ven91], [Ven94]). If we take the name “arrow logic” in its original sense, it stands roughly for the whole landscape of possible semantic modelings for the “logic of tran­ sitions”, using the language of relation algebras. The ideas and techniques, we use for obtaining and investigating this landscape are not restricted to arrow logic in the sense described above, but can be used for almost every family of modal logics (including FO logic). For this reason, we will also use 2 When forgetting for a moment the Kleene * in PDL.