- 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
```

- Consider example:

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

- Purify, introduce new constants:
- Purified:

```
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$.
- Then we must have $F \implies x_1 = y_1$ or $F = x_2 = y_2$.
- Generalize to $n$ disjuncts.
- Inutitively, if $F$ implies a disjunction of equalities, then it implies at least one equality.
- LIA is not convex: suppose $F = 1 \leq x \leq 2$. Then 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.
- See that in the case of LIA, If we want $A \implies B$ to be true, if we view $A, B$ as sets, then we want $\lnot A \lor B$to be the whole space, which means that $B$ covers whatever $A$ used to cover, so we need $A \subseteq B$.
- 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.

- 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$.