This paper is available on arxiv under CC BY-SA 4.0 DEED license. Authors: (1) Tomáš Jakl, Czech Academy of Sciences and Czech Technical University; (2) Dan Marsden, School of Computer Science University of Nottingham; (3) Nihil Shah, Department of Computer Science University of Oxford. Table of Links Abstract & Introduction Prelimenaries FVM Theorems for Positive Existential Fragments FVM Theorems for Counting Logic FVM Theorems for The Full Logic Abstract FVM Theorems for Products Adding Equality and Other Enrichment Conclusions, Acknowledgments & References Appendix A FVM theorems for coproducts Appendix B Proofs Omitted from Section III Appendix C Proofs Omitted from Section IV Appendix D Proofs Omitted from Section V Appendix E Proofs Omitted from Section VI Appendix F Proofs Omitted from Section VII Abstract We present a categorical theory of the composition methods in finite model theory – a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman–Vaught–Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments. I. INTRODUCTION Composition methods constitute a family of techniques in finite model theory for understanding the logical properties of complex structures [1]. One works in a modular fashion, building a structure out of simpler components. The larger structure can then be understood in terms of the logical properties of its parts, and how they behave under the operations used in the construction The first result of this type was proved by Mostowski [2], who showed that the first-order theory of the product of two structures A×B is determined by the first-order theories of A and B. Later, Feferman and Vaught famously proved a very general result for first-order logic, which included showing that the same holds true for infinite products and infinite disjoint unions of structures of the same type [3]. Since then many more Feferman–Vaught–Mostowski (FVM) theorems1 have been shown for various operations, logics and types of structures. These theorems have important applications in the theory of algorithms [4], for example in the development of algorithmic meta-theorems such as Courcelle’s theorem [5]. For our purposes, the typical form of an FVM theorem for a fixed n-ary operation H and logics is as follows. Given structures and L1, . . . , Ln+1 A1, . . . , An B1, . . . , Bn, Here denotes equivalence with respect to the logic . Typically, is either one or two. For example, writing ≡F O for equivalence in first-order logic, Mostowski’s result is given in the form of (1) as: ≡L L n A key tool in finite model theory for establishing that two structures are logically equivalent is that of a model comparison game. Examples of such games are the Ehrenfeucht– Fraïssé [6], [7], pebbling [8] and bisimulation games [9], establishing equivalence in fragments of first order and modal logic. FVM theorems are typically proven using these games, building a winning strategy for the composite structure out of winning strategies for the components. Despite their usefulness, working with model comparison games often requires intricate combinatorial arguments that have to be carefully adapted with even the slightest change of problem domain. To mitigate the difficulty with using game arguments directly, finite model theorists introduced higherlevel methods such as locality arguments or 0–1 laws to establish model equivalences or inexpressibility. The recently introduced game comonad framework [10], [11] provides a new such tool. This provides a unifying formalism for reasoning about model comparison games, using categorical methods. The definition of a comonad enables a transfer of results from the formally dual theory of monads, commonly encountered in the categorical semantics of computation and universal algebra [12], [13], [14]. Game comonads are designed to encapsulate a particular model comparison game, and are the key abstraction allowing us to give uniform results, whilst avoiding making arguments specific to a particular logic or its corresponding game. The early work on game comonads focused on capturing many important logics [15], [16], [17], laying the foundations for further developments. More recent results recover classical theorems from finite model theory, as well as completely new results [18], [19], [20], [21]. See [22] for a recent survey and [23] for an axiomatic formulation. Until now, there has been no account of the composition method with the game comonad framework. We close this gap by introducing a novel method for proving FVM theorems within the game comonad approach, giving results uniformly in the classes of structures, operations and logics involved. Instantiating the abstract results for our example game comonads yields concrete FVM theorems with respect to three typical fragments of first-order logic: the positive existential fragment, i.e. the fragment of firstorder logic of formulas not using universal quantification or negations, counting logic, i.e. the extension of first-order logic with counting quantifiers, full first-order logic. Conventionally, proving an FVM theorem involves cleverly combining several winning model-comparison game strategies to form a winning strategy on the composite structures. In our game comonads approach, we only need to find a collection of morphisms of a specified form to obtain an FVM theorem for the positive existential logic. This collection of morphisms is a formal witness to a combination of strategies. Perhaps surprisingly, to witness equivalence in the counting logic, the same collection of morphisms only has to satisfy two additional axioms which coincide with the standard definition of Kleisli law [25]. Although of practical interest, the FVM theorems in Sections III and IV are relatively straightforward to prove. We present them in detail for pedagogical reasons to develop the ideas gradually. The abstract FVM theorem for the full fragment is more technically challenging. This theorem shows that two additional assumptions suffice to extend an FVM theorem from counting logic to the full logic. We can rephrase these assumptions categorically as showing the operation lifts to a parametric relative right adjoint over an appropriate category. Surprising connections arise with classical results in monad theory, generalizing the notion of bilinear map and its classifying tensor product from ordinary linear algebra [26], [27].

Too Long; Didn't Read

Get VPN and ad blocker with a single subscription	

A Categorical Account of Composition Methods in Logic: Abstract & Introduction

Too Long; Didn't Read

EScholar: Electronic Academic Papers for Scholars

Share Your Thoughts

About Author

TOPICS

THIS ARTICLE WAS FEATURED IN...

A Categorical Account of Composition Methods in Logic: Abstract & Introduction

Too Long; Didn't Read

EScholar: Electronic Academic Papers for Scholars

Share Your Thoughts

About Author

TOPICS

THIS ARTICLE WAS FEATURED IN...

RELATED STORIES