Łoś–Tarski preservation theorem

The Łoś–Tarski theorem is a theorem in model theory, a branch of mathematics, that states that the set of formulas preserved under taking substructures is exactly the set of universal formulas. The theorem was discovered by Jerzy Łoś and Alfred Tarski.

Statement

Let [math]\displaystyle{ T }[/math] be a theory in a first-order logic language [math]\displaystyle{ L }[/math] and [math]\displaystyle{ \Phi(\bar{x}) }[/math] a set of formulas of [math]\displaystyle{ L }[/math]. (The sequence of variables [math]\displaystyle{ \bar{x} }[/math] need not be finite.) Then the following are equivalent:

1. If [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] are models of [math]\displaystyle{ T }[/math], [math]\displaystyle{ A \subseteq B }[/math], [math]\displaystyle{ \bar{a} }[/math] is a sequence of elements of [math]\displaystyle{ A }[/math]. If [math]\displaystyle{ B \models \bigwedge \Phi(\bar{a}) }[/math], then [math]\displaystyle{ A \models \bigwedge \Phi(\bar{a}) }[/math].
   ([math]\displaystyle{ \Phi }[/math] is preserved in substructures for models of [math]\displaystyle{ T }[/math])
2. [math]\displaystyle{ \Phi }[/math] is equivalent modulo [math]\displaystyle{ T }[/math] to a set [math]\displaystyle{ \Psi(\bar{x}) }[/math] of [math]\displaystyle{ \forall_1 }[/math] formulas of [math]\displaystyle{ L }[/math].

A formula is [math]\displaystyle{ \forall_1 }[/math] if and only if it is of the form [math]\displaystyle{ \forall \bar{x} [\psi(\bar{x})] }[/math] where [math]\displaystyle{ \psi(\bar{x}) }[/math] is quantifier-free.

In more common terms, this states that every first-order formula is preserved under induced substructures if and only if it is [math]\displaystyle{ \forall_1 }[/math], i.e. logically equivalent to a first-order universal formula. As substructures and embeddings are dual notions, this theorem is sometimes stated in its dual form: every first-order formula is preserved under embeddings on all structures if and only if it is [math]\displaystyle{ \exists_1 }[/math], i.e. logically equivalent to a first-order existential formula.

Note that this property fails for finite models.

References

• Hinman, Peter G. (2005). Fundamentals of Mathematical Logic. A K Peters. p. 255. ISBN 1568812620.