The quantifier rank measures maximum nesting depth:Two first-order structures are rank-n equivalent if they agree on all first-order sentences of quantifier rank at most . For tuples one similarly compares all such formulas evaluated at the tuples.
In the -round Ehrenfeucht-Fraïssé game, player I, the Spoiler, chooses an element from either structure each round; player II, the Duplicator, chooses an element in the other. After rounds the corresponding chosen tuples must define a partial isomorphism of structures: all atomic formulas, including equality and the interpretations of constants, have matching truth values. Repetitions must be respected. Failure of this condition is a loss for II.
The precise finite-vocabulary Ehrenfeucht-Fraïssé theorem is: for a finite relational language, allowing finitely many constants,The tuple version has the same conclusion when the corresponding tuples are fixed before play. The implication from a winning strategy to rank equivalence holds for arbitrary languages, by induction on formulas. For the converse, finite relational vocabulary ensures only finitely many rank-bounded types in a fixed tuple of variables; their defining formulas let one transfer the type of the next move. Without a finiteness hypothesis, the converse for the full atomic-diagram game need not hold. This qualification matters in the next part.
Under the finite relational vocabulary hypothesis of the Ehrenfeucht-Fraïssé theorem, II wins the timed game exactly when the structures are elementarily equivalent. If II wins, then for every choice of by I, its strategy restricts to a winning strategy in . Hence the models agree on every sentence of quantifier rank at most . Every first-order sentence has finite quantifier rank, so they agree on all sentences.
Conversely, elementary equivalence gives for every . Choose a winning strategy for each , and use that strategy once I announces . Unlike the infinite game, the timed game permits the strategy to depend on the announced horizon.
The PDF does not explicitly impose finite vocabulary. If an arbitrary language and the full partial isomorphism of structures winning condition are intended, the reverse assertion is false. Here is a failure of finite-round game equivalence in infinite languages. Let be unary relational. Letand obtain by adjoining one point satisfying every .
For any finite sublanguage, every Boolean cell of predicates has infinitely many elements in both structures. Every finite partial isomorphism of structures of these reducts can therefore be extended in either direction. Induction on formulas, or a back-and-forth method, shows their reducts are elementarily equivalent. Since every sentence uses finitely many symbols, in the whole language.
Nevertheless I wins by choosing : every point of fails some , so no response preserves all atomic formulas. Thus the printed unrestricted equivalence requires the finite-vocabulary convention, or a game which additionally restricts each play to a finite vocabulary fragment.
Use the one-relation language and the total orderswhere the second is the order sum: every point in its natural-number block lies below every point in its integer block.
To show II wins every finite Ehrenfeucht-Fraïssé game, use the interval threshold strategy for discrete linear orders. With rounds left, corresponding open intervals and end rays between already matched points have either the same size below , or both have at least elements. Their sizes may be infinite. The chosen-point correspondence is order preserving. Initially the unique interval is infinite in both orders, so the invariant holds.
If I chooses a repeated point, II repeats its counterpart. If I chooses in a short interval, II chooses the point with the same finite rank in the matching interval. In a long interval, let . If one side of the chosen point has fewer than elements, reproduce that size in the other interval; the opposite sides then both have at least elements. Otherwise choose a response having at least elements on each side. Such a response exists because the interval has at least elements. The endpoint and successor/predecessor properties of these two discrete orders allow the finite small-side counts to be reproduced. This establishes the invariant with rounds left and gives a finite-game winning strategy. Therefore II wins the timed game.
In the infinite Ehrenfeucht-Fraïssé game, I first chooses a point in the integer block of . It has infinitely many predecessors. II must respond with some , which has exactly predecessors. I then chooses distinct predecessors of . To preserve order and equality, II would need distinct points below , which is impossible. ThusI chooses the required finite length only after seeing II's first response, which explains why this does not contradict the timed-game result.
Take a rooted directed graph with one root and one terminal vertex , with its sole edge . Let have a root and two terminal vertices , with edges and . The relationis a bisimulation. Each root move can be matched by a root move ending in a related terminal vertex. At all related terminal pairs there are no further edges, so both matching conditions are vacuous. Yet the directed graphs have two and three vertices and cannot be isomorphic. Bisimilarity need not preserve the number of successors.
Here and in the next part, the second graph's edge relation is , and its response vertices belong to . These are the corrections to the printed relation and vertex slips in the bisimulation clauses.
Suppose first that is a bisimulation containing the root pair. II maintains the invariant that the current pair lies in . If I moves in the first rooted directed graph, the forth clause supplies a matching successor in the second; if I moves in the second, the back clause supplies a matching successor in the first. II can choose such a response every time I can move. Therefore II never loses after finitely many steps and wins the bisimulation game.
Conversely, let be a winning strategy for II. Define to consist of all endpoint pairs of finite legal plays starting at the roots and consistent with , including the initial root pair. This definition keeps every possible history; it does not assume that depends only on the current position.
Take and a finite history realizing it. For any successor of , extend that history by having I choose the edge . Since is winning, it supplies a successor of . The new endpoint pair belongs to , proving forth. Letting I choose any successor of proves back in the same way. Hence is a bisimulation andConnectedness ensures that both projections of cover all vertices: I can walk any finite directed path from either root and II's strategy supplies the matching path. The equivalence itself only concerns the rooted reachable behaviour and remains valid without connectedness.
Articles by others on the same topic
There are currently no matching articles.