Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Characterizing Sets of Theories That Can Be Disjointly Combined

Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar

TL;DR

The paper addresses when disjoint first-order theories can be combined decidably by introducing a Galois-connection framework that maps a set of theories to the largest set that can be combined with it. This yields a closure operator and a complete lattice of theory-combination properties, enabling sharpness results for Nelson–Oppen, shiny, polite/strong politeness, and gentle, plus the construction of new combination theorems through lattice operations. Key contributions include precise maximality results (e.g., $G( rak{T})= rak{T}_{ ext{shiny}}$ for shiny, $G( rak{T}_{SI})= rak{T}_{SI}$ for stably infinite), the development of test theories, and the discovery of symmetric and higher-order combination theorems (e.g., computable-spectra, $n$-shininess, and $ rak{F}$-QG frameworks). The framework both clarifies the landscape of existing methods and provides a principled route to generate and analyze new theory-combination rules, with potential applications to SMT solvers and multi-theory reasoning.

Abstract

We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice.

Characterizing Sets of Theories That Can Be Disjointly Combined

TL;DR

The paper addresses when disjoint first-order theories can be combined decidably by introducing a Galois-connection framework that maps a set of theories to the largest set that can be combined with it. This yields a closure operator and a complete lattice of theory-combination properties, enabling sharpness results for Nelson–Oppen, shiny, polite/strong politeness, and gentle, plus the construction of new combination theorems through lattice operations. Key contributions include precise maximality results (e.g., for shiny, for stably infinite), the development of test theories, and the discovery of symmetric and higher-order combination theorems (e.g., computable-spectra, -shininess, and -QG frameworks). The framework both clarifies the landscape of existing methods and provides a principled route to generate and analyze new theory-combination rules, with potential applications to SMT solvers and multi-theory reasoning.

Abstract

We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice.

Paper Structure

This paper contains 57 sections, 78 theorems, 8 equations, 3 figures, 5 tables, 6 algorithms.

Table of Contents

  1. Introduction
  2. History of Theory Combination
  3. Our Contributions
  4. Related Work
  5. Preliminaries
  6. First-Order Logic
  7. Spectra, Löwenheim--Skolem, and Compactness
  8. Theory Combination Properties
  9. Fontaine's Lemma
  10. Lattice Theory
  11. The Galois Connection
  12. The Sharpness of Known Combination Theorems
  13. Test Theories
  14. Combination of Shiny Theories With Decidable Theories
  15. Combination of Stably Infinite Theories
  16. ...and 42 more sections

Key Result

theorem 1

Let $\Delta$ be a set of formulas over a countable signature, and let $\kappa \ge \aleph_0$. Then, $\Delta$ is satisfied by an interpretation of size $\kappa$ if and only if it is satisfied by an interpretation of size $\aleph_0$.

Figures (3)

  • Figure 1: Cardinality formulas
  • Figure 2: The lattice of theory combination properties we will examine: next to each property one finds the section which studies it; the structure of the diagram is explained in \ref{['sec-lattice']}, where a precise statement of its correctness is also given. The Galois connection reflects the lattice over the dashed line.
  • Figure 3: The example theories used to separate the theory combination properties in \ref{['fig:lattice']}

Theorems & Definitions (82)

  • theorem 1: marker2002
  • theorem 2: marker2002
  • corollary 1
  • lemma 1: Fontaine's lemma
  • proposition 1
  • proposition 2
  • proposition 3
  • Remark 3.1
  • definition 1
  • theorem 3
  • ...and 72 more