±1-sequence

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 (Hodges 1997).

Statement

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

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

A formula is ${\mathrm{\forall }}_1$ if and only if it is of the form $\mathrm{\forall }\overline{x}[\psi (\overline{x})]$ where $\psi (\overline{x})$ is quantifier-free.

Note that this property fails for finite models.

References

• Peter G. Hinman (2005), Fundamentals of Mathematical Logic, A K Peters, ISBN 1568812620.
• Hodges (1997), A Shorter Model Theory, Cambridge University Press, ISBN 0521587131.

Template:Mathlogic-stub