arXiv · 2406.18912
The nonexistence of unicorns and many-sorted L\"owenheim-Skolem theorems
Abstract
Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are strongly finitely witnessable and smooth are called strongly polite and can be effectively combined with other theories. Toledo, Zohar, and Barrett conjectured that stably infinite and strongly finitely witnessable theories are smooth and therefore strongly polite. They called counterexamples to this conjecture unicorn theories, as their existence seemed unlikely. We prove that, indeed, unicorns do not exist. We also prove versions of the L\"owenheim-Skolem theorem and the {\L}o\'s-Vaught test for many-sorted logic.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Benjamin Przybocki, Guilherme Toledo, Yoni Zohar, Clark Barrett. 2024-06-27. The nonexistence of unicorns and many-sorted L\"owenheim-Skolem theorems. https://arxiv.org/abs/2406.18912
Cite the original work for its findings. Save a collection to share your selection of sources.