Łoś–Tarski preservation theorem

Source: Wikipedia, the free encyclopedia.

The Łoś–Tarski theorem is a

Jerzy Łoś and Alfred Tarski
.

Statement

Let be a theory in a first-order logic language and a set of formulas of . (The sequence of variables need not be finite.) Then the following are equivalent:

  1. If and are models of , , is a sequence of elements of . If , then .
    ( is preserved in substructures for models of )
  2. is equivalent modulo to a set of formulas of .

A formula is if and only if it is of the form where 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 , 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 , i.e. logically equivalent to a first-order existential formula. [2]

Note that this property fails for finite models.

Citations

References