Characterizing Sets of Theories That Can Be Disjointly Combined
summary
Proves an exact characterization of which decidable first‑order theories over disjoint signatures can be disjointly combined, showing Nelson–Oppen’s stable infiniteness, shininess/strong politeness, gentleness and related methods are optimal and cannot be strictly weakened. Constructs decidable “test” theories using the halting function f to force properties (finite model property, etc.) and reduce undecidability, exhibits a Galois connection giving a complete lattice of closed combination classes, derives new sharp theorems including a symmetric computable spectra method and a single maximally hard decidable theory.
AI-written summary · about
chapters (11)
- 0:00Theory combination intro
- 2:05Nelson-Oppen and stable infiniteness
- 3:30Shininess and polite combination
- 5:58Central question and negative results
- 7:03Galois connection framework
- 10:55Sharpness with test theories
- 14:24Maximally difficult theories
- 15:48New combination methods
- 18:33Lattice of combination properties
- 19:56Conclusion and future work
- 21:43Q&A
related talks
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
53mIntroduction to Intuitionistic Type Theory
27mFunctorial Semantics for Partial Theories
25mLocally Nameless Sets
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
15mSemantics of Sets of Programs
15mClosing Remarks
11mLocal algebraic effect theories