Tarski-Vaught Test

This article needs to be linked to other articles. In particular: throughout You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

This page has been identified as a candidate for refactoring of medium complexity. In particular: Merge the various sections and appropriately modularise the various logical steps so as to reduce the repetition as far as possible. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Theorem

Let $\MM, \NN$ be $\LL$-structures such that $\MM$ is a substructure of $\NN$.

Work In Progress In particular: The page Definition:Structure is a disambiguation page, in which the form in which it is used here may not be included. The level of clarity in this page generally needs improving. Hence the invocation of the Disambiguate template. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.

The term Definition:Structure as used here has been identified as being ambiguous. If you are familiar with this area of mathematics, you may be able to help improve $\mathsf{Pr} \infty \mathsf{fWiki}$ by determining the precise term which is to be used. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Disambiguate}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Then $\MM$ is an elementary substructure of $\NN$ if and only if:

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

Work In Progress In particular: Before sense can be made of this page, Definition:Substructure and Definition:Elementary Substructure need to be written. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.

The term Definition:Logical Formula as used here has been identified as being ambiguous. If you are familiar with this area of mathematics, you may be able to help improve $\mathsf{Pr} \infty \mathsf{fWiki}$ by determining the precise term which is to be used. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Disambiguate}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

The condition on the right side of the if and only if 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$ if and only if:

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 if and only if 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.

This article, or a section of it, needs explaining. In particular: Worth making it explicit exactly what that result is, so as to clarify what is being sought here. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Explain}} from the code.

$\Box$

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

if and only if:

$\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}$

if and only if:

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

$\blacksquare$

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.

$\Box$

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.

This article contains statements that are justified by handwavery. In particular: "It is easily shown" is not used on this site. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding precise reasons why such statements hold. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Handwaving}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

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

if and only if:

$\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}$

if and only if:

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

$\blacksquare$

This page has been identified as a candidate for refactoring of medium complexity. In particular: These two proofs need to be merged and rationalised. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Generalization

This page has been identified as a candidate for refactoring of medium complexity. In particular: Merge this in with the above. No attempt at tidying has been made on the below, except to correct spelloes and bring $\LaTeX$ style up to house style. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

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.

$\blacksquare$

Source of Name

This entry was named for Alfred Tarski and Robert Lawson Vaught.