一句话：通过 Galois 连接刻画可与给定可判定理论集合不相交组合的最大理论类，并否证若干开放问题。
本文研究一阶理论不相交组合所需性质，包括稳定无限性、shininess、强礼貌性和 gentleness。作者在可判定理论集合之间建立了一个 Galois 连接，该连接可为给定可判定理论集合选出能与之组合的最大可判定理论集合。利用这一框架，文章精确刻画了能与满足若干著名理论组合性质的理论集合相组合的可判定理论集合，从而加强了已有结果，并对能否改进现有组合方法以覆盖更大理论类这一长期开放问题给出了否定回答。此外，该 Galois 连接诱导出理论组合性质的完全格，可通过取交与并生成新的组合方法；作者给出了此类示例，引入新的组合定理，并将新旧方法定位于该格中。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-17374,
title = {Characterizing Sets of Theories That Can Be Disjointly Combined},
author = {Benjamin Przybocki and Guilherme V. Toledo and Yoni Zohar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776652}
}