View source for Fraïssé characterization of elementary equivalence

Interpretations for a [[Formal language|formal language]] are equivalent provided that they give the same truth values to sentences in the language. Equivalent interpretations for first-order languages are said to be elementarily equivalent. R. Fraïssé [[#References|[a2]]] established a characterization for elementary equivalence that is purely mathematical, in the sense that it does not mention sentences. Unlike the characterizations of S. Kochen [[#References|[a5]]] and H.J. Keisler [[#References|[a4]]], Fraïssé's characterization applies only to those first-order languages whose non-logical vocabulary is finite and contains no functional constants.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101601.png" /> be such a first-order language (with equality). Each predicate constant in the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101602.png" /> is associated with an unique positive integer called its degree. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101603.png" /> be an infinite set of individual constants not in the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101604.png" />. The family of first-order languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101605.png" /> is defined as follows:

1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101606.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101607.png" />;

2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101608.png" /> is the language obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f1101609.png" /> by adding <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016010.png" /> to the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016011.png" />.

Interpretations for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016012.png" /> are ordered pairs <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016013.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016014.png" /> is a non-empty set (the domain of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016015.png" />) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016016.png" /> is a function defined on the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016017.png" /> as follows:

1) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016018.png" /> is an individual constant, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016019.png" /> (the denotation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016020.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016021.png" />) is a member of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016022.png" />;

2) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016023.png" /> is a predicate constant of degree <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016024.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016025.png" /> (the extension of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016026.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016027.png" />) is a subset of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016028.png" />.

When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016029.png" /> is an interpretation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016030.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016031.png" /> are members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016032.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016033.png" /> denotes the interpretation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016034.png" /> with domain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016035.png" /> that agrees with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016036.png" /> on the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016037.png" /> and in which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016038.png" /> is the denotation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016039.png" /> for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016040.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016041.png" />.

Given interpretations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016042.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016043.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016044.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016045.png" /> is a sub-interpretation, or subsystem, of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016046.png" /> provided that:

1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016047.png" />;

2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016048.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016049.png" /> give the same denotations to individual constants of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016050.png" />;

3) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016051.png" /> is a predicate constant of degree <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016052.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016053.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016054.png" /> be a subset of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016055.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016056.png" /> denotes the subsystem of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016057.png" /> generated by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016058.png" /> (i.e., the smallest subsystem of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016059.png" /> whose domain contains <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016060.png" />). When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016061.png" /> is non-empty, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016062.png" /> exists and its domain is finite if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016063.png" /> is finite. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016064.png" /> denote the null set. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016065.png" /> exists when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016066.png" /> or when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016067.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016068.png" /> contains individual constants.

For each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016069.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016070.png" /> is defined on pairs of interpretations for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016071.png" /> as follows:

1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016072.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016073.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016074.png" /> are isomorphic;

2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016075.png" /> if and only if

2a) for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016076.png" /> there is a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016077.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016078.png" />;

2b) for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016079.png" /> there is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016080.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016081.png" />.

Fraïssé proved that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016082.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016083.png" /> are elementarily equivalent if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016084.png" /> for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016085.png" />.

For <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016086.png" /> a sentence in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016087.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016088.png" /> is the number of distinct variables occurring in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016089.png" />; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016090.png" /> is called the quantifier rank of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016091.png" />. One writes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016092.png" /> when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016093.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016094.png" /> give the same truth values to all sentences in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016095.png" /> of quantifier rank less than or equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016096.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016097.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016098.png" /> are elementarily equivalent if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f11016099.png" /> for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160100.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160101.png" /> be an [[Enumeration|enumeration]] (without repeats) of the individual variables in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160102.png" />. Fix an enumeration (without repeats) of the formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160103.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160104.png" /> be a non-empty finite set of formulas. There is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160105.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160106.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160107.png" /> occurs before <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160108.png" /> in the enumeration when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160109.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160110.png" /> denote <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160111.png" />, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160112.png" /> denote <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160113.png" />.

Given <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160114.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160115.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160116.png" />, and a sequence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160117.png" /> of members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160118.png" /> of length <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160119.png" />, the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160120.png" /> is defined as follows. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160121.png" /> is the conjunction of the set consisting of all atomic formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160122.png" /> in the variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160123.png" /> which are satisfied by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160124.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160125.png" />, and of the negations of all such formulas which are not satisfied by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160126.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160127.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160128.png" /> is the conjunction of

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160129.png" /></td> </tr></table>

and

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160130.png" /></td> </tr></table>

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160131.png" /> denote the null sequence. When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160132.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160133.png" /> is written <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160134.png" />. For fixed <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160135.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160136.png" /> there are only finitely many formulas of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160137.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160138.png" /> is a formula in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160139.png" /> free variables and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160140.png" /> bound variables. Hence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160141.png" /> is of quantifier rank <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160142.png" />.

Assume that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160143.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160144.png" /> are interpretations for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160145.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160146.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160147.png" /> are natural numbers such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160148.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160149.png" /> is a sequence of members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160150.png" /> of length <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160151.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160152.png" /> is a sequence of members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160153.png" /> of length <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160154.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160155.png" /> is satisfied by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160156.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160157.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160158.png" />. This result implies that for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160159.png" /> the following assertions are equivalent:

1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160160.png" />;

2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160161.png" />;

3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160162.png" /> is a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160163.png" />. Fraïssé's characterization is immediate.

It also follows that any sentence of quantifier rank less than or equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160164.png" /> which is true on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160165.png" /> is a logical consequence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160166.png" /> (i.e., true on all models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160167.png" />). Hence every such sentence of its negation is a logical consequence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160168.png" />. Since for fixed <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160169.png" /> there are only finitely many sentences of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160170.png" />, there are only finitely many non-equivalent sentences of quantifier rank less than or equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160171.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160172.png" /> be a sentence of quantifier rank <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160173.png" />. Assume that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160174.png" /> has models. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160175.png" /> be the sentence

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160176.png" /></td> </tr></table>

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160177.png" /> is a distributive normal form in the sense of J. Hintikka [[#References|[a3]]]. Furthermore, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160178.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160179.png" /> are logically equivalent (i.e., have exactly the same models).

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160180.png" /> be a set of sentences. Call <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160181.png" /> a theory when every logical consequence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160182.png" /> is a member of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160183.png" />. Assume that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160184.png" /> has models. Let

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160185.png" /></td> </tr></table>

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160186.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160187.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160188.png" /> have exactly the same models; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160189.png" /> is decidable if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160190.png" /> is recursive and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160191.png" /> is finitely axiomatizable if and only if there is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160192.png" /> such that the models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160193.png" /> are closed under <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160194.png" />.

Alternative definitions of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f110/f110160/f110160195.png" /> can be found in [[#References|[a6]]] and [[#References|[a7]]]. A. Ehrenfeucht [[#References|[a1]]] independently obtained Fraïssé's characterization formulated in terms of two-person games. Fraïssé's characterization has been extended to provide characterizations of equivalence for a variety of  "non-elementary"  languages. For example, see [[#References|[a6]]], [[#References|[a7]]], and [[#References|[a8]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Ehrenfeucht,   "An application of games to the completeness problem for formalised theories"  ''Fundam. Math.'' , '''49'''  (1956)  pp. 129–141</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  R. Fraïssé,   "Sur quelques classifications des relations basés sur des isomorphismes restraintes"  ''Publ. Sci. Univ. Alger. Ser. A'' , '''2'''  (1955)  pp. 11–60, 273–295</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  J. Hintikka,   "Distributive normal forms in first order logic"  J.N. Crossley (ed.)  M.A.E. Dummet (ed.) , ''Formal Systems and Recursive Functions'' , North-Holland  (1965)  pp. 48–91</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  H.J. Keisler,   "Ultraproducts and elementary classes"  ''Indagationes Mathematicae'' , '''23'''  (1961)  pp. 277–295</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  S. Kochen,   "Ultraproducts in the theory of models"  ''Ann. of Math.'' , '''74'''  (1961)  pp. 231–261</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  A. Mostowski,   "Thirty years of foundational studies" , Barnes and Noble  (1966)</TD></TR><TR><TD valign="top">[a7]</TD> <TD valign="top">  D. Scott,   "Logic with denumerably long formulas and finite strings of quantifiers"  J.W. Addison (ed.)  L. Henkin (ed.)  A. Tarski (ed.) , ''The Theory of Models'' , North-Holland  (1966)  pp. 329–341</TD></TR><TR><TD valign="top">[a8]</TD> <TD valign="top">  G. Weaver,   J. Welaish,   "Back and forth arguments in modal logic"  ''J. Symb. Logic'' , '''51'''  (1987)  pp. 969–980</TD></TR></table>