Partial elementary map (source code)

= Partial elementary map

An injective map between subsets of structures is partial elementary when it preserves every first-order formula on tuples from its domain. This is stronger than a <partial embedding>, which only preserves quantifier-free formulas. In countable models, successive one-point extensions in both directions produce an elementary isomorphism by the <back-and-forth method>.