±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 $\Phi ({\bar {x}})$ a set of formulas of $L$. (The set of sequence of variables ${\bar {x}}$ need not be finite.) Then the following are equivalent:

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

A formula is $\forall _{1}$ if and only if it is of the form $\forall {\bar {x}}[\psi ({\bar {x}})]$ where $\psi ({\bar {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