A Universe of Sorts

§ Implementing Nelson Oppen

Two theories are disjoint of they do not share predicates and function symbols, except for $=$ .

Transform a formula in $\Sigma_1 \cup \Sigma_2$ into an equisatisfiable formula $F_1 \land F_2$ with $F_1 \in T_1$ and $F_2 \in T_2$
Introduce fresh symbols for shared subterms.
Algorithmically, to purify a formula $f(x_1, \dots)$ to be in theory $T_1$ :

repeat until fixpoint:
      u = gesym()
      Purify[f(..., t, ...)] => Purify[f(..., u, ...)] /\ u = t

x + 2 == y, f(Store(A, x, 3)[y - 2]) != f(y - x + 1)

Functions:  f(v1) != f(v2)
Arrays:     v1 == v3[v4], v3 == Store(x, y, v5)
Arithmetic: x + 2 == y, v2 == y - x + 1, v4 == y - 2, v5 == 2

Let $F$ be a conjunctive formula.
Let $F \implies x_1 = y_1 \lor x_2 = y_2$ (ie, the formula is a tautology, so it's true in all models).
Then we must have $F \implies x_1 = y_1$ or $F = x_2 = y_2$ .
Inutitively, if $F$ implies a disjunction of equalities, then it implies at least one equality. (Generalize to $n$ disjuncts.)

Another way to look at the LIA thing: $A \implies B$ is us saying that $x \in A \implies x \in B$ for arbitrary $x$ , and thus we need $A \subseteq B$ !.
Let us now view this in terms of $F \implies H_1 \lor H_2$ .
$F$ is a conjunctive formula, so it is geometricaly a convex set.
$H_1, H_2$ are equalities of the form $x_i = y_i$ , so they are hyperplanes.
To have $F \implies H_1 \lor H_2$ be true, we need $F \subset H_1 \cup H_2$ .
We now want that $F \subset H_1 \cup H_2$ , which can only happen if $F \subset H_1$ or $F \subset H_2$ , since a convex set can be a subset of hyperplanes only if it is contained in any hyperplane! Otherwise, we can "interpolate" a point $x_1 \in H_1$ and $x_2 \in H_2$ and get a point $(x_1 + x_2) / 2$ that lies in neither.
For a (non) example, we can take $F$ a square: $x \geq 0 \land x \leq 1 \land y \geq 0 \land y \leq 1$ . But a point being in a square does not imply equality of the point to any coordinate!
So we must have a tight constraint, ie, the convex set must itself be a point.
If the convex set itself is a point, like $x \geq 1 \land x \leq 1 \land y \geq 1 \land y \leq 1$ , then we can indeed have a disjunction of equalities it implies, and only one of these disjncts will be true!

For a example, we can take $F$ a square: $x \geq 0 \land x \leq 1 \land y \geq 0 \land y \leq 1$ . But a point being in a square in the integers does imply facts about coordinates! For example, it implies that $x = 1 \lor x = 2$ .
However, we cannot conclude from this that "point in square implies $x = 1$ " or "point in square implies $x = 2$ " in all models (ie, the two statements are not tautologies).
Example 2 of LIA is not convex: suppose $F = 1 \leq x \leq 2$ . Then, to be convex, we have $F \implies x = 1 \lor x = 2$ . But, $F$ does not imply either $x = 1$ or $x = 2$ .
Convexity reduces what we need to handle: If we want to show $x_1 = y_1 \lor x_2 = y_2$ , we can try to prove each disjunct first.
Another intuition: membership in a bounded set in LIA has a finite disjunctive formula that witnesses it, by enumerating integer points in the bounded set. This can be used as the disjunctive RHS.
But such a splitting is necessarily forcing a case split :)
On the other hand, in the case of rationals, there is no such finite disjuntive formula, so any implied equalities really do hold in all models (points that are in the sets)

Suppose a theory $T$ has a non-trivial model, and is convex.
Then we need to show that it's stably infinite.
Theory $T$ is stably infinite iff for every ground quantifier free formula $F$ that is satisfiable, there is an infinite model.
So we are given a ground formaul $F$ that's true in some model $M$ of $T$ , and we need to show that it's true in an infinite model.
If the model $M$ is the trivial model $M = {*}$ , then the formula $F$ must hold in a larger model (why?)
Suppose size of $M \geq 2$ .
We will build an infinite model for $F$ by compactness.
For every $n \in N$ , we know that $M^{\log_2 n}$ will have cardinality greater than or equal to $n$ .