Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems

Benjamin Przybocki, Guilherme Toledo, Yoni Zohar, Clark Barrett

TL;DR

This work resolves the unicorn conjecture by showing that any countable-signature theory that is both stably infinite and strongly finitely witnessable must be smooth, thereby eliminating the existence of unicorn theories and enabling a tight characterization of strongly polite theories. It then develops robust many-sorted extensions of foundational model-theoretic results, including downward/upward/combined Löwenheim–Skolem theorems and a Łoś–Vaught test, tailored to multi-sorted frameworks and SMT practice. The key technical advance blends compactness and Skolem methods with Ramsey-theoretic generalizations to control cardinalities across multiple sorts, yielding precise cardinality-alignment results essential for theory combination and decidability. Collectively, these results streamline proving that a theory can be combined with others in SMT, and provide practical criteria for identifying shiny and strongly polite theories in multi-sorted settings.

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öwenheim-Skolem theorem and the Łoś-Vaught test for many-sorted logic.

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems

TL;DR

This work resolves the unicorn conjecture by showing that any countable-signature theory that is both stably infinite and strongly finitely witnessable must be smooth, thereby eliminating the existence of unicorn theories and enabling a tight characterization of strongly polite theories. It then develops robust many-sorted extensions of foundational model-theoretic results, including downward/upward/combined Löwenheim–Skolem theorems and a Łoś–Vaught test, tailored to multi-sorted frameworks and SMT practice. The key technical advance blends compactness and Skolem methods with Ramsey-theoretic generalizations to control cardinalities across multiple sorts, yielding precise cardinality-alignment results essential for theory combination and decidability. Collectively, these results streamline proving that a theory can be combined with others in SMT, and provide practical criteria for identifying shiny and strongly polite theories in multi-sorted settings.

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öwenheim-Skolem theorem and the Łoś-Vaught test for many-sorted logic.
Paper Structure (8 sections, 8 theorems, 4 equations, 1 figure)

This paper contains 8 sections, 8 theorems, 4 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Many-sorted first-order logic
  4. Model-theoretic properties
  5. Notation
  6. The nonexistence of unicorns
  7. Motivating the proof
  8. Ramsey's theorem and generalizations

Key Result

theorem thmcountertheorem

A set of $\Sigma$-formulas $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable.

Figures (1)

  • Figure 1: How we move from interpretation to interpretation

Theorems & Definitions (11)

  • theorem thmcountertheorem: Compactness Theorem Monzano93
  • lemma thmcounterlemma
  • lemma thmcounterlemma: The Tarski--Vaught test
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem thmcountertheorem
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • lemma thmcounterlemma: BarTolZoh2
  • theorem thmcountertheorem
  • ...and 1 more