Difference between revisions of "Fraïssé characterization of elementary equivalence"
Ulf Rehmann (talk | contribs) m (moved Fraisse characterization of elementary equivalence to Fraïssé characterization of elementary equivalence over redirect: accented title) |
Ulf Rehmann (talk | contribs) m (MR/ZBL numbers added) |
||
Line 71: | Line 71: | ||
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" />. | 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 | + | 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==== | ====References==== | ||
− | <table><TR><TD valign="top">[a1]</TD> <TD valign="top"> | + | <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 {{MR|0140396}} {{ZBL|0118.01501}} </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> |
Revision as of 16:57, 15 April 2012
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 MR0140396 Zbl 0118.01501 |
[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 |
Fraïssé characterization of elementary equivalence. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Fra%C3%AFss%C3%A9_characterization_of_elementary_equivalence&oldid=23276