- A theory is stably infinite iff every satisfiable quantifier free formula is satisfiable in an infinite model.
- EUF and arithmetic are stably infinite.
- Bitvectors are not stably infinite, since they don't have infinite models. (i.e. the structure is itself finite)
- Theory of strings of bounded length (structure is finite).

- Consider $1 \leq 2 \land f(x) \neq f(2) \land f(x) \neq f(1)$ in $T_E \cup T_Z$ (equality, integers).
- Separate, introduce new variable $y = 2, z = 1$.
- The array part becomes $f(x) \neq f(y) \land f(z) \neq f(z)$.
- The integer part becomes $1 \leq 2 \land y = 2 \land z = 1$.
- So, the two theories "communicate" via variables.

- Suppose we have $F = F_1 \land F_2$
- If either $F_1, F_2$ are are UNSAT, then $F$ is UNSAT.
- But if both $F_1, F_2$ are SAT, not guaranteed that the whole thing is SAT.

- Let $S$ be a set of terms with $\sim$ an equivalence relation.
- Then we write $F[\sim] \equiv (\land_{t \sim s} t = s) \land (\land_{t \not \sim s} t \neq s)$.
- For elements that are not related, we force disequality!

- Take two disjoint theories $T_1, T_2$
- That is, theories $T_1, T_2$ with signatures $S_1, S_2$ such that $S_1 \cap S_2 = \emptyset$ so no common symbols.
- Let $F$ be a conjunction of literals from $T_1 \cup T_2$.
- Convert $F$ to separate form: $F_1 \land F_2$.
- Guess a coordinating. equivalence relation $\sim$ over $vars(F_1) \cap vars(F_2)$.
- Run $DP_1(F_1 \land F[\sim])$, and $DP_2(F_1 \land F[\sim])$.
- If both solvers are SAT, then return SAT, since we have found a common assignment.
- Otherwise, F is UNSAT.
- CLAIM: this is a correct algorithm!

- For the proof, we need to know the reduct of a model to a smaller signature, and the notion of a model homomorphism.

- Let us a have a model $(M, S, T)$ where $M$ is the model, $S$ is the signature (tells us what the functions and predicates are), and $T$ is the theory (tells us what the axioms are.
- Then, for any subset $S' \subseteq S$, it's possible to build $(M, S')$ as a reduct of $(M, S)$.
- For example, $(Z, +, 0)$ is a reduct of $(Z, +, 0, 1, \times)$.

- Let $F_1$ be an $S_1$ model, and $F_1$ has variables $V_1$ (mutatis mutandis for $F_2$).
- Claim: $F_1 \land F_2$ is satisfiable
there exist $m_1 \models F_1$, $m_2 \models F_2$ such that $m_1 \sim m_2$ on $S_1 \cap S_2$(i.e. $m_1|_{S_1 \cap S_2, V_1 \cap V_2}$ is isomorphic as a $S_1 \cap S_2$ model to $m_2|_{S_1 \cap S_2, V_1 \cap V_2}$).*if and only if*

- If $F_1 \land F_2$ is SAT, then there's a $S_1 U S_2$ model $M$. Let $m_1 \equiv M|_{S_1}$, (ditto $M_2$).
- Clearly, the restriction of the large model $M$ to $S_1$ will continue to model $F_1$, and ditto $F_2$, hence done.

- Idea: embed $(m_2, S_2)$ as a submodel of $(m_1, S_1)$ via the isomorphism $h$.
- This "just works", since they agree on the variables.
- Let $h$ be the iso $m_1 \sim_{S_1 \cap S_2} m_2$
- Let $M \equiv m_1$
- Let $M|S_1 = m_1$
- For $v_2 \in V_2, v \not in V_1$, define $M(v_2) \equiv h^{-1}(m_2(v_2))$.
- For $f_2 \in S_2, f \not in S_1$, define $M(f_2, a \in m_1 , \dots, z \in m_1) \equiv h^{-1}(f(h(a), h(b), \dots, h(z)))$.
- So we push $a, \cdots, z$ forward via $h$, evaluate $f_2$, then pull value back.

- The key point is the sheaf-condition, which says that they agree on the intersection.
- Intuitively, this shows that we can form a pushout.

- Let $F_1$ be an $S_1$ model, and $F_1$ has variables $V_1$ (mutatis mutandis for $F_2$).
- Claim: $F_1 \land F_2$ is satisfiable
there exist $m_1 \models F_1$, $m_2 \models F_2$ such that:*if an only if* - (a) $|m_1| = |m_2|$ (underlying sets have same size)
- (b) For each variable $x, y \in V_1 \cap V_2$, we have that $m_1 \models x = y$ iff $m_2 \models x = y$.

- Pick $m_1 = M|_{S_1}$, $m_2 = M|_{S_2}$. Clearly, same underlying set so same cardinality, and same model, so witnesses same equalities.

- Key idea: Since the models have the same cardinality, we can build the iso piecewise:
- Let $h : m_1[V_1 \cap V_2] to m_2[V_1 \cap V_2]$ be an empty iso from the values that $V_1 \cap V_2$ take in $m_1$ to the values that $V_1 \cap V_2$ take in $m_2$.
- Start by updating $h$ such that $h(m_1(v)) = m_2(v)$.
- This is injective, bcause suppose $h(m_1(v)) = h(m_1(v'))$. Then this means that $m_2(v) = m_2(v')$, which implies $m_1(v) = m_1(v')$, and thus we are done.
- The condition that $m_1 \models x = y$ iff $m_2 \models x = y$ ensures that $h$ remains an iso.
- This is onto since we've exhausted every variable in $V_1 \cap V_2$.
- Since $h$ is bijective, we have that $|m_1[V_1 \cap V_2]| = |m_2[V_2 \cap V_2]|$. Since |m
*1| = |m*2|, this implies that we can extend $h$ arbitrarily to a bijective function on all of $m_1, m_2$. - Clearly, by construction $h$ is an iso, and we thus apply previous theorm!

- If we agree on variables, then we have the seed of an iso that witnesses that things are equal for ground formulae
- Then since we have same cardinality, we can extend to full iso!

- Let $T_1$ be stably infinite $S_1$ theory (mutatis mutandis).
- Let $F_1$ be a $S_1$ formula with variables $V_1$ (mutatis mutandis).
- Let $S_1 \cap S_2 = \emptyset$.
- $F_1 \land F_2$ is $T_1 \cup T_2$ satisfiable
:*if and only if* - There is an equivalence relation $\sim$ over $V_1 \cap V_2$ such that: $F_i \land F[\sim]$ is $T_i$ satisfiable.

- Pick $M_1 = M|_{S_1, V_1 \cap V_2}$ and $M_2 \equiv M|_{S_2, V_1 \cap V_2}$, $x \sim y \iff x = y$.

- Suppose $\sim$ is equivalence relation such that $F_i \land F[~]$ is $T_i$ satisfiable.
- Since $T_1$ is stably infinite, we have infinite model $M_1 \models F_1 cap F[\sim]$.
- By downward lowenheim skolem, we have a countably infinite model $M_1$.
- So choose $M_1, M_2$ countable, thus $|M_1| = |M_2|$.
- Since $M_1 \models F[\sim]$ and $M_2 \models F[\sim]$, this means that $M_1(x) = M_1(x')$ if and only if $M_2(x) = M_2(x')$, because $F[\sim]$ asserts that all elements in the equivalence class are equal, and elements that are not in the equvalence class are
*not*equal. - Thus, we have that $M_1(x) = M_1(x')$ if and only if $x \sim x'$ if and only if $M_2(x) = M_2(x')$.
- TODO: I am not totally convinced here! I need to think :)