Ł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.^[1] The theorem was discovered by Jerzy Łoś and Alfred Tarski.

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

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

A formula is ${\displaystyle \forall _{1}}$ if and only if it is of the form ${\displaystyle \forall {\bar {x}}[\psi ({\bar {x}})]}$ where ${\displaystyle \psi ({\bar {x}})}$ 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 ${\displaystyle \forall _{1}}$, 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 ${\displaystyle \exists _{1}}$, i.e. logically equivalent to a first-order existential formula. ^[2]

Note that this property fails for finite models.

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

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

• v
• t
• e