Characterizing Sets of Theories That Can Be Disjointly Combined

TL;DR

This paper characterizes the properties of first-order theories that enable their disjoint combination, introduces a Galois connection to identify maximal decidable theory sets, and develops a lattice framework for generating new combination methods.

Contribution

It provides a precise characterization of decidable theories suitable for disjoint combination and introduces a lattice structure to systematically generate and analyze new theory combination methods.

Findings

Established a Galois connection for theory sets

Characterized sets of theories compatible with known combination properties

Developed a lattice framework for creating new combination methods

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.