Stable Infiniteness Removes Hidden Cardinality Conflicts

The requirement that each component theory be stably infinite can seem excessive. A Nelson–Oppen input contains only finitely many terms, so why should every satisfiable constraint need an infinite model?

The reason is not that the input needs infinitely many values. The reason is that the Nelson–Oppen decision procedure communicates only equalities and disequalities between shared variables. It does not communicate the cardinality of the rest of each theory’s domain. Stable infiniteness ensures that this missing information cannot prevent the local models from being merged.

The solvers agree only on named values

After purification, a combined constraint has the form

$${\Gamma }_1\wedge {\Gamma }_2,$$

where ${\Gamma }_i$ uses only the signature ${\Sigma }_i$, apart from a finite set of shared variables

$$V=\{x_1,\dots ,x_n\}.$$

Nelson–Oppen chooses an arrangement $\alpha$ of $V$. For every pair $x_i,x_j$, the arrangement contains either

$$x_i=x_j\text{or}{x}_i\ne x_j.$$

Each theory solver then checks its own constraint with the same arrangement:

$${\Gamma }_1\wedge \alpha \text{ is }{\mathcal{T}}_1\text{-satisfiable},{\Gamma }_2\wedge \alpha \text{ is }{\mathcal{T}}_2\text{-satisfiable}.$$

The arrangement fixes which shared variables denote the same element. If it has $k$ equivalence classes, it also implies the lower bound

$$|D|\ge k.$$

It says nothing about unnamed elements. In particular, it cannot express that one local model requires exactly two domain elements while another requires exactly three.

Local satisfiability can hide a global conflict

Without stable infiniteness, agreement on $\alpha$ does not suffice to construct one model for the combined theory.

Two elements cannot be three elements

Let ${\mathcal{T}}_2$ require every model to have exactly two elements:

$$\exists a\exists b(a\ne b\wedge \forall x(x=a\vee x=b)).$$

Let ${\mathcal{T}}_3$ require every model to have exactly three elements:

$$\exists a\exists b\exists c(a\ne b\wedge a\ne c\wedge b\ne c\wedge \forall x(x=a\vee x=b\vee x=c)).$$

The constraint $\top$ is satisfiable in each theory separately. There are no shared variables, so the only arrangement is also $\top$. Both local solvers therefore return SAT.

Their union is nevertheless unsatisfiable: a common domain would have to satisfy

$$|D|=2\text{and}|D|=3.$$

Three shared values exceed a two-element theory

Let ${\mathcal{T}}_1$ be a theory over

$${\Sigma }_1=\{f_1,a,b\}$$

whose interpretations have domains of size at most two. This restriction can be expressed by the axiom

$$\forall u\forall v\forall w(u=v\vee u=w\vee v=w).$$

Let ${\mathcal{T}}_2$ impose no cardinality restriction and use the disjoint signature

$${\Sigma }_2=\{f_2\}.$$

Consider the purified constraints

$$\begin{array}{rl}{F}_1& :=f_1(x)\ne f_1(y),\\ F_2& :=f_2(x)\ne f_2(z)\wedge f_2(y)\ne f_2(z).\end{array}$$

Each constraint is satisfiable in its own theory. For $F_1$, choose a two-element domain with $x\ne y$ and interpret $f_1$ as the identity. For $F_2$, choose a two-element domain with $x=y\ne z$ and again use the identity function. Neither solver derives a shared equality, so equality exchange alone reaches a fixed point without exposing a conflict.

In the combined formula, however, unequal function values force unequal arguments:

$$\begin{array}{rl}{f}_1(x)\ne f_1(y)& ⟹x\ne y,\\ f_2(x)\ne f_2(z)& ⟹x\ne z,\\ f_2(y)\ne f_2(z)& ⟹y\ne z.\end{array}$$

Hence,

$$F_1\wedge F_2\models x\ne y\wedge x\ne z\wedge y\ne z,$$

so every combined model requires at least three elements:

$$|D|\ge 3.$$

This contradicts the restriction $|D|\le 2$ imposed by ${\mathcal{T}}_1$. Thus, $F_1$ is ${\mathcal{T}}_1$-satisfiable and $F_2$ is ${\mathcal{T}}_2$-satisfiable, but $F_1\wedge F_2$ is not $({\mathcal{T}}_1\cup {\mathcal{T}}_2)$-satisfiable. The missing information is the domain size needed by the combined disequalities.

The local answers are individually correct. The error lies in inferring global satisfiability from them. Equality exchange cannot reveal the incompatible requirements on unnamed parts of the domains.

Infinite models provide enough room to align

Now suppose both theories are stably infinite. If the two purified constraints are satisfiable under the same arrangement, choose infinite local models

$$\begin{array}{rlrl}{\mathcal{M}}_1& \models {\mathcal{T}}_1,& {\mathcal{M}}_1& \models {\Gamma }_1\wedge \alpha ,\\ {\mathcal{M}}_2& \models {\mathcal{T}}_2,& {\mathcal{M}}_2& \models {\Gamma }_2\wedge \alpha .\end{array}$$

The standard model-theoretic construction takes these models at a common sufficiently large infinite cardinality $\kappa$:

$$|D_1|=|D_2|=\kappa .$$

Because both models satisfy the same arrangement, their shared values have the same equality pattern. There is therefore a bijection between the values denoted by the shared variables:

$$x_i^{{\mathcal{M}}_1}⟷x_i^{{\mathcal{M}}_2}.$$

Only finitely many values are prescribed by $V$. Since both domains have the same infinite cardinality, this partial correspondence can be extended to a bijection

$$h:D_2\to D_1.$$

Transport the interpretation of every ${\Sigma }_2$-symbol along $h$. The transported ${\mathcal{T}}_2$-model now uses domain $D_1$ and assigns every shared variable the same value as ${\mathcal{M}}_1$.

The signatures are disjoint apart from equality, so the two interpretations can now be placed on the same domain without assigning incompatible meanings to a private symbol:

$$\mathcal{M}{\upharpoonright }_{{\Sigma }_1}={\mathcal{M}}_1,\mathcal{M}{\upharpoonright }_{{\Sigma }_2}=h({\mathcal{M}}_2).$$

The resulting model $\mathcal{M}$ satisfies both ${\Gamma }_1$ and ${\Gamma }_2$. This is the merge step for which stable infiniteness is needed.

Infinity removes an upper bound, not a lower bound

The shared disequalities already communicate how many distinct named values are required. If an arrangement contains

$$x_1\ne x_2,x_1\ne x_3,x_2\ne x_3,$$

then both solvers know that at least three domain elements are necessary.

The dangerous information is an uncommunicated finite upper bound such as $|D|\le 2$. A stably infinite theory cannot force such a bound whenever its local constraint is satisfiable, because that constraint also has an infinite model. Stable infiniteness therefore makes the arrangement’s finite lower bound the only relevant cardinality condition.

This is why “large enough” is not used as a fixed finite requirement. Different inputs may demand arbitrarily many distinct shared values, and finite-domain theories may permit incompatible sets of cardinalities. Infinite models provide a uniform amount of slack.

The requirement belongs to the combination theorem

Stable infiniteness is not required to decide satisfiability inside an individual theory. A finite-domain theory may have an excellent decision procedure. The condition is needed by the standard Nelson–Oppen inference

$$\begin{array}{rl}& {\Gamma }_1\wedge \alpha \text{ is }{\mathcal{T}}_1\text{-satisfiable},\\ & {\Gamma }_2\wedge \alpha \text{ is }{\mathcal{T}}_2\text{-satisfiable}\end{array}⟹{\Gamma }_1\wedge {\Gamma }_2\text{ is }({\mathcal{T}}_1\cup {\mathcal{T}}_2)\text{-satisfiable}.$$

Nor is stable infiniteness logically necessary for every specially designed theory combination. Finite-domain theories can be combined by procedures that exchange additional cardinality information. They simply fall outside the guarantee of the standard Nelson–Oppen construction.

The missing step is therefore model compatibility: equality arrangements align the finitely many values that the theories name, while stable infiniteness ensures that the unnamed remainder of their domains can also be made compatible.