Tarski-Vaught Test

== Theorem ==
Let $\MM, \NN$ be $\LL$-structures such that $\MM$ is a substructure of $\NN$.
Then $\MM$ is an elementary substructure of $\NN$ :
:for every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$:
::if there exists an $n$ in $\nN$ such that $\NN \models \map \phi {n, \bar a}$
::then there exists an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$.
The condition on the right side of the statement above can be rephrased as:
:Every existential statement with parameters from $\MM$ which is satisfied in $\NN$ can be witnessed by an element from the substructure $\MM$.
=== Generalization ===
Let $\NN$ be an $\LL$-structure, and $\MM \subseteq \NN$.
Then $\MM$ is the universe of an elementary substructure of $\NN$ :
:for every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$
::if there exists an $n$ in $\NN$ such that $\NN \models \map \phi {n, \bar a}$
::then there exists an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$.
The condition on the right side of the statement above can be rephrased as::
:Every existential statement with parameters from $\MM$ which is satisfied in $\NN$ can be witnessed by an element from the subset $\MM$.
== Proof ==
=== Sufficient Condition ===
Let $\MM$ be an elementary substructure of $\NN$.
Then $\NN \models \exists x: \map \phi {x, \bar a}$ implies that $\MM \models \exists x: \map \phi {x, \bar a}$.
Hence there exists some $m$ in $\MM$ such that:
:$\MM \models \map \phi {m, \bar a}$.
Passing back up to $\NN$ yields the result.
=== Necessary Condition ===
Let $\MM$ be such that:
:For every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$:
::if there exists an $n$ in $\NN$ such that $\NN \models \map \phi {n, \bar a}$
::then there exists an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$.
It is to be shown that $\MM$ is an elementary substructure of $\NN$.
That is:
:for every $\LL$-formula $\map \psi {\bar v}$
and:
:for every $\bar a$ in $\MM$:
::$\paren {\MM \models \map \phi {\bar a} } \iff \paren {\NN \models \map \phi {\bar a} }$
The proof proceeds by induction on complexity of formulas.
Let $\psi$ be quantifier free.
From Quantifier Free Formula is Preserved by Superstructure, quantifier free formulas with parameters from $\MM$ are preserved when passing to and from superstructures.
Hence the result holds.
Let the result holds for $\psi$.
Consider $\neg \psi$:
We have that:
:$\paren {\MM \models \neg \map \psi {\bar a} } \iff \paren {\MM \not \models \map \psi ({\bar a} }$
By the inductive hypothesis:
:$\paren {\MM \not \models \map \psi {\bar a} } \iff \paren {\NN \not \models \map \psi {\bar a} }$
Thus the result follows for $\neg \psi$.
Let the result hold for $\psi_0$ and $\psi_1$.
Consider $\psi_0 \wedge \psi_1$:
We have:
:$\MM \models \map {\psi_0} {\bar a} \wedge \map {\psi_1} {\bar a}$
:
:$\MM \models \map {\psi_0} {\bar a}$
and:
:$\MM \models \map {\psi_1} {\bar a}$
By the inductive hypothesis:
:$\MM \models \map {\psi_0} {\bar a}$ and $\MM \models \map {\psi_1} {\bar a}$
:
:$\NN \models \map {\psi_0} {\bar a}$ and $\NN \models \map {\psi_1} {\bar a}$
Thus the result follows for $\psi_0 \wedge \psi_1$.
Let the result holds for $\psi$.
Consider:
:$\exists x: \map \psi x$
We prove the two directions of this case separately.
First let:
:$\MM \models \exists x: \map \psi {x, \bar a}$
Then there exists $m \in \MM$ such that:
:$\MM \models \map \psi {m, \bar a}$
By the inductive hypothesis:
:$\NN \models \map \psi {m, \bar a}$
and so:
:$\NN \models \exists x: \map \psi {x, \bar a}$
Conversely, let:
:$\NN \models \exists x: \map \psi {x, \bar a}$
By assumption, there exists $m \in \MM$ such that:
:$\NN \models \map \psi {m, \bar a}$
By the inductive hypothesis:
:$\MM \models \map \psi {m, \bar a}$
and hence:
:$\MM \models \exists x: \psi {x, \bar a}$
completing the proof.
== Proof of Generalization ==
=== Sufficient Condition ===
Let $\MM$ be an elementary substructure of $\NN$.
Then:
:$\paren {\NN \models \exists x: \map \phi {x, \bar a} } \implies \paren {\MM \models \exists x: \map \phi {x, \bar a} }$
Hence there exists $m \in \MM$ such that:
:$\MM \models \map \phi {m, \bar a}$
Passing back up to $\NN$ yields the result.
=== Necessary Condition ===
Let $\MM$ be such that:
:for every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$:
::if there exists an $n$ in $\NN$ such that $\NN \models \map \phi {n, \bar a}$
::then there exists an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$.
It is easily shown, using formulae of the form $\map \phi {x, \bar v} = \map f {\bar v} = x$, that $\MM$ is closed under functions, and hence the universe of a substructure.
It remains to be shown that $\MM$ is an elementary substructure of $\NN$.
That is:
:for every $\LL$-formula $\map \psi {\bar v}$ and for every $\bar a$ in $\MM$:
::$\paren {\MM \models \map \phi {\bar a} } \iff \paren {\NN \models \map \phi {\bar a} }$
The proof proceeds by induction on complexity of formulas.
Let $\psi$ is quantifier free.
From Quantifier Free Formula is Preserved by Superstructure, quantifier free formulas with parameters from $\MM$ are preserved when passing to and from superstructures.
Hence the result holds.
Let the result hold for $\psi$.
Consider $\neg \psi$:
We have:
:$\paren {\MM \models \neg \map \psi {\bar a} } \iff \paren {\MM \not \models \map \psi {\bar a} }$
By the inductive hypothesis:
:$\paren {\MM \not \models \map \psi {\bar a} } \iff \paren {\NN \not \models \map \psi {\bar a} }$
Hence the result follows for $\neg \psi$.
Suppose the result holds for $\psi_0$ and $\psi_1$.
Consider $\psi_0 \wedge \psi_1$:
We have that:
:$\MM \models \map {\psi_0} {\bar a} \wedge \map {\psi_1} {\bar a}$
:
:$\MM \models \map {\psi_0} {\bar a}$ and $\MM \models \map {\psi_1} {\bar a}$
By the inductive hypothesis:
:$\MM \models \map {\psi_0} {\bar a}$ and $\MM \models \map {\psi_1} {\bar a}$
:
:$\NN \models \map {\psi_0} {\bar a}$ and $\NN \models \map {\psi_1} {\bar a}$
The result then follows for $\psi_0 \wedge \psi_1$.
Let the result hold for $\psi$.
Consider $\exists x: \map \psi x$:
We prove the two directions of this case separately.
First let:
:$\MM \models \exists x: \map \psi {x, \bar a}$
Then there exists $m \in \MM$ such that:
:$\MM \models \map \psi {m, \bar a}$
By the inductive hypothesis:
:$\NN \models \map \psi {m, \bar a}$
and so:
:$\NN \models \exists x: \map \psi {x, \bar a}$
Conversely, let:
:$\NN \models \exists x: \map \psi {x, \bar a}$
Then by assumption, there exists $m \in \MM$ such that:
:$\NN \models \map \psi {m, \bar a}$
By the inductive hypothesis:
:$\MM \models \map \psi {m, \bar a}$
and hence:
:$\MM \models \exists x: \map \psi {x, \bar a}$
completing the proof.
== Generalization ==
Another common statement of the theorem does not require $\MM$ to be a substructure of $\NN$, it is enough for it to be a subset of $\NN$.
The ($\implies$) is shown just the same as above, while the other direction easily follows, since $\MM$ satisfying the condition that for every $\LL$-formula $\map \phi {x, \bar v}$ and for every $\bar a$ in $\MM$, if there is an $n$ in $\NN$ such that $\NN \models \map \phi {n, \bar a}$, then there is an $m$ in $\MM$ such that $\NN \models \map \phi {m, \bar a}$, is closed under functions (by directly applying the condition to formulae of the form $\map \phi {x, \bar y} = \paren {x = \map f {\bar y} }$), and hence the universe of a substructure, which reduces it to the statement above.
Category:Model Theory for Predicate Logic