Fraïssé characterization of elementary equivalence

Interpretations for a 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é [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 [a5] and H.J. Keisler [a4], Fraïssé's characterization applies only to those first-order languages whose non-logical vocabulary is finite and contains no functional constants.

Let be such a first-order language (with equality). Each predicate constant in the non-logical vocabulary of is associated with an unique positive integer called its degree. Let be an infinite set of individual constants not in the non-logical vocabulary of . The family of first-order languages is defined as follows:

1) is ;

2) is the language obtained from by adding to the non-logical vocabulary of .

Interpretations for are ordered pairs , where is a non-empty set (the domain of ) and is a function defined on the non-logical vocabulary of as follows:

1) if is an individual constant, (the denotation of on ) is a member of ;

2) if is a predicate constant of degree , (the extension of on ) is a subset of .

When is an interpretation of and are members of , denotes the interpretation of with domain that agrees with on the non-logical vocabulary of and in which is the denotation of for all , .

Given interpretations and for , is a sub-interpretation, or subsystem, of provided that:

1) ;

2) and give the same denotations to individual constants of ;

3) if is a predicate constant of degree , .

Let be a subset of . denotes the subsystem of generated by (i.e., the smallest subsystem of whose domain contains ). When is non-empty, exists and its domain is finite if is finite. Let denote the null set. exists when or when and contains individual constants.

For each , is defined on pairs of interpretations for as follows:

1) if and only if and are isomorphic;

2) if and only if

2a) for all there is a such that ;

2b) for all there is an such that .

Fraïssé proved that and are elementarily equivalent if and only if for all .

For a sentence in , is the number of distinct variables occurring in ; is called the quantifier rank of . One writes when and give the same truth values to all sentences in of quantifier rank less than or equal to . and are elementarily equivalent if and only if for all .

Let be an enumeration (without repeats) of the individual variables in . Fix an enumeration (without repeats) of the formulas in . Let be a non-empty finite set of formulas. There is an such that and occurs before in the enumeration when . Let denote , and let denote .

Given , , , and a sequence of members of of length , the formula is defined as follows. is the conjunction of the set consisting of all atomic formulas in in the variables which are satisfied by in , and of the negations of all such formulas which are not satisfied by in . is the conjunction of

and

Let denote the null sequence. When , is written . For fixed and there are only finitely many formulas of the form . is a formula in free variables and bound variables. Hence is of quantifier rank .

Assume that and are interpretations for , and are natural numbers such that , is a sequence of members of of length , and is a sequence of members of of length . is satisfied by in if and only if . This result implies that for all the following assertions are equivalent:

1) ;

2) ;

3) is a model of . Fraïssé's characterization is immediate.

It also follows that any sentence of quantifier rank less than or equal to which is true on is a logical consequence of (i.e., true on all models of ). Hence every such sentence of its negation is a logical consequence of . Since for fixed there are only finitely many sentences of the form , there are only finitely many non-equivalent sentences of quantifier rank less than or equal to . Let be a sentence of quantifier rank . Assume that has models. Let be the sentence

is a distributive normal form in the sense of J. Hintikka [a3]. Furthermore, and are logically equivalent (i.e., have exactly the same models).

Let be a set of sentences. Call a theory when every logical consequence of is a member of . Assume that has models. Let

Let . and have exactly the same models; is decidable if and only if is recursive and is finitely axiomatizable if and only if there is an such that the models of are closed under .

Alternative definitions of can be found in [a6] and [a7]. A. Ehrenfeucht [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 [a6], [a7], and [a8].

References

[a1]	A. Ehrenfeucht, "An application of games to the completeness problem for formalised theories" Fundam. Math. , 49 (1956) pp. 129–141
[a2]	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
[a3]	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
[a4]	H.J. Keisler, "Ultraproducts and elementary classes" Indagationes Mathematicae , 23 (1961) pp. 277–295
[a5]	S. Kochen, "Ultraproducts in the theory of models" Ann. of Math. , 74 (1961) pp. 231–261
[a6]	A. Mostowski, "Thirty years of foundational studies" , Barnes and Noble (1966)
[a7]	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
[a8]	G. Weaver, J. Welaish, "Back and forth arguments in modal logic" J. Symb. Logic , 51 (1987) pp. 969–980