This note defines Ehrenfeucht-Fraïssé games where identity is not present in the basic language. The formulation is applied to show that there is no elementary theory in the language of one binary relation that exactly characterizes models in which the relation is the identity relation.

In this paper we develop an Ehrenfeucht‐Fraïssé game for. Unlike the standard Ehrenfeucht‐Fraïssé games which are modeled solely after the behavior of quantifiers, this new game also takes into account the behavior of connectives in logic. We prove the adequacy theorem for this game. We also apply the new game to prove complexity results about infinite binary strings.

Two structures A and B are n-equivalent if Player II has a winning strategy in the n-move Ehrenfeucht-Fraïssé game on A and B. In earlier articles we studied n-equivalence classes of ordinals and coloured ordinals. In this article we similarly treat a class of scattered order-types, focussing on monomials and sums of monomials in ω and its reverse ω*.

In this paper we prove under some set theoretical assumptions that if T is a countable unstable theory then there is a pair of models of T such that Ehrenfeucht-Fraïssé games between these models of large variety of lengths are non-determined.

In this paper, we initiate the study of Ehrenfeucht–Fraïssé games for some standard finite structures. Examples of such standard structures are equivalence relations, trees, unary relation structures, Boolean algebras, and some of their natural expansions. The paper concerns the following question that we call the Ehrenfeucht–Fraïssé problem. Given nω as a parameter, and two relational structures and from one of the classes of structures mentioned above, how efficient is it to decide if Duplicator wins the (...) n-round EF game ? We provide algorithms for solving the Ehrenfeucht–Fraïssé problem for the mentioned classes of structures. The running times of all the algorithms are bounded by constants. We obtain the values of these constants as functions of n. (shrink)

This paper introduces a new Ehrenfeucht-Fraïssé type game that is played on two classes of models rather than just two models. This game extends and generalizes the known Ajtai-Fagin game to the case when there are several alternating moves played in different models. The game allows Duplicator to delay her choices of the models till the very end of the game, making it easier for her to win. This adds on the toolkit of winning strategies for Duplicator in (...) Ehrenfeucht-Fraïssé type games and opens up new methods for tackling some open problems in descriptive complexity theory. As an application of the class game, it is shown that, if m is a power of a prime, then first order logic augmented with function quantifiers F1n of arity 1 and height n < m can not express that the size of the model is divisible by m. This, together with some new expressibility results for Henkin quantifiers H1n gives some new separation results on the class of finite models among various F1n on one hand and between F1n and H1n on the other. Since function quantifiers involve a bounded type of second order existential quantifiers, the class game solves an open problem raised by Fagin, which asks for some inexpressibility result using a winning strategy by Duplicator in a game that involves more than one coloring round. (shrink)

C. Karp has shown that if α is an ordinal with ω α = α and A is a linear ordering with a smallest element, then α and $\alpha \bigotimes A$ are equivalent in L ∞ω up to quantifer rank α. This result can be expressed in terms of Ehrenfeucht-Fraïssé games where player ∀ has to make additional moves by choosing elements of a descending sequence in α. Our aim in this paper is to prove a similar (...) result for Ehrenfeucht-Fraïssé games of length ω 1 . One implication of such a result will be that a certain infinite quantifier language cannot say that a linear ordering has no descending ω 1 -sequences (when the alphabet contains only one binary relation symbol). Connected work is done by Hyttinen and Oikkonen in [H] and [O]. (shrink)

Inquisitive first-order logic, InqBQ, is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper makes two contributions to the study of this logic. First, we describe an Ehrenfeucht–Fraïssé game for InqBQ and show that it characterizes the distinguishing power of the logic. Second, we use the game to study cardinality quantifiers in the inquisitive setting. That is, we (...) study what statements and questions can be expressed in InqBQ about the number of individuals satisfying a given predicate. As special cases, we show that several variants of the question how many individuals satisfy α(x) are not expressible in InqBQ, both in the general case and in restriction to finite models. (shrink)

The Ehrenfeucht–Fraïsse game for a logic usually provides an intuitive characterizarion of its expressive power while in abstract model theory, logics are compared by their expressive powers. In this paper, I explore this connection in details by proving a general Lindström theorem for logics which have certain types of Ehrenfeucht–Fraïsse games. The results generalize and uniform some known results and may be applied to get new Lindström theorems for logics.

First-order logic is known to have a severely limited expressive power on finite structures. As a result, several different extensions have been investigated, including fragments of second-order logic, fixpoint logic, and the infinitary logic L∞ωω in which every formula has only a finite number of variables. In this paper, we study generalized quantifiers in the realm of finite structures and combine them with the infinitary logic L∞ωω to obtain the logics L∞ωω, where Q = {Qi: iε I} is a family (...) of generalized quantifiers on finite structures. Using the logics L∞ωω, we can express polynomial-time properties that are not definable in L∞ωω, such as “there is an even number of x” and “there exists at least n/2 x” , without going to second-order logic. We show that equivalence of finite structures relative to L∞ωω can be characterized in terms of certain pebble games that are a variant of the Ehrenfeucht—Fraïssé games. We combine this game-theoretic characterization with sophisticated combinatorial tools from Ramsey theory, such as van der Waerden's Theorem and Folkman's Theorem, in order to investigate the scope and limits of generalized quantifiers in finite model theory. We obtain sharp lower bounds for expressibility in the logics L∞ωω and discover an intrinsic difference between adding finitely many simple unary generalized quantifiers to L∞ωω adding infinitely many. In particular, we show that if Qis a finite sequence of simple unary generalized quantifiers, then the equicardinality, or Härtig, quantifier is not definable in L∞ωω. We also show that the query “does the equivalence relation E have an even number of equivalence classes” is not definable in the extension L∞ωω of L∞ωω by the Härtig quantifier I and any finite sequence Q of simple unary generalized quantifiers. (shrink)

The aim of this paper is to introduce the notion of a game for intuitionistic first-order Kripke models. We also establish links between notions presented here and the notions of logical equivalence and bounded bisimulation for intuitionistic first-order Kripke models, and the Ehrenfeucht–Fraïssé game for classical first-order structures.

We show in the paper that for any non-classifiable countable theory T there are non-isomorphic models and that can be forced to be isomorphic without adding subsets of small cardinality. By making suitable cardinal arithmetic assumptions we can often preserve stationary sets as well. We also study non-structure theorems relative to the Ehrenfeucht-Fraïssé game.

The descriptive complexity of a problem is the complexity of describing the problem in some logical formalism. One of the few techniques for proving separation results in descriptive complexity is to make use of games on graphs played between two players, called the spoiler and the duplicator. There are two types of these games, which differ in the order in which the spoiler and duplicator make various moves. In one of these games, the rules seem to be (...) tilted towards favoring the duplicator. These seemingly more favorable rules make it easier to prove separation results, since separation results are proven by showing that the duplicator has a winning strategy. In this paper, the relationship between these games is investigated. It is shown that in one sense, the two games are equivalent. Specifically, each family of graphs used in one game to prove a separation result can in principle be used in the other game to prove the same result. This answers an open question of Ajtai and the author from 1989. It is also shown that in another sense, the games are not equivalent, in that there are situations where the spoiler requires strictly more resources to win one game than the other game. This makes formal the informal statement that one game is easier for the duplicator to win. (shrink)

Truth, consistency and elementary equivalence can all be characterised in terms of games, namely the so-called evaluation game, the model-existence game, and the Ehrenfeucht–Fraisse game. We point out the great affinity of these games to each other and call this phenomenon the strategic balance in logic. In particular, we give explicit translations of strategies from one game to another.

Gaifman's normal form theorem showed that every first-order sentence of quantifier rank n is equivalent to a Boolean combination of “scattered local sentences”, where the local neighborhoods have radius at most 7n−1. This bound was improved by Lifsches and Shelah to 3×4n−1. We use Ehrenfeucht–Fraïssé type games with a “shrinking horizon” to get a spectrum of normal form theorems of the Gaifman type, depending on the rate of shrinking. This spectrum includes the result of Lifsches and Shelah, (...) with a more easily understood proof and with the bound on the radius improved to 4n−1. We also obtain bounds for a normal form theorem of Schwentick and Barthelmann. (shrink)

The first-order logical theory Th $({\mathbb{N}},x + 1,F(x))$ is proved to be complete for the class ATIME-ALT $(2^{O(n)},O(n))$ when $F(x) = 2^{x}$ , and the same result holds for $F(x) = c^{x}, x^{c} (c \in {\mathbb{N}}, c \ge 2)$ , and F(x) = tower of x powers of two. The difficult part is the upper bound, which is obtained by using a bounded Ehrenfeucht–Fraïssé game.

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

In a relational language consisting of a single relation R, we investigate pseudofiniteness of certain Hrushovski constructions obtained via predimension functions. It is notable that the arity of the relation R plays a crucial role in this context. When R is ternary, by extending the methods recently developed by Brody and Laskowski, we interpret 〈Q+,<〉 in the 〈K+,≤∗〉-generic and prove that this structure is not pseudofinite. This provides a negative answer to the question posed in an earlier work by Evans (...) and Wong. This result, in fact, unfolds another aspect of complexity of this structure, along with undecidability and the strict order property proved in the mentioned earlier works. On the other hand, when R is binary, it can be shown that the 〈K+,≤∗〉-generic is decidable and pseudofinite. (shrink)

We give a sufficient condition for the inexpressibility of the k-th extended vectorization of a generalized quantifier $\sf Q$ in ${\rm FO}({\vec Q}_k)$ , the extension of first-order logic by all k-ary quantifiers. The condition is based on a model construction which, given two ${\rm FO}({\vec Q}_1)$ -equivalent models with certain additional structure, yields a pair of ${\rm FO}({\vec Q}_k)$ -equivalent models. We also consider some applications of this condition to quantifiers that correspond to graph properties, such as connectivity and (...) planarity. (shrink)

Although it is known that reachability in undirected finite graphs can be expressed by an existential monadic second-order sentence, our main result is that this is not the case for directed finite graphs (even in the presence of certain "built-in" relations, such as the successor relation). The proof makes use of Ehrenfeucht-Fraisse games, along with probabilistic arguments. However, we show that for directed finite graphs with degree at most k, reachability is expressible by an existential monadic second-order sentence.

We explore the finite model theory of the characterisation theorems for modal and guarded fragments of first-order logic over transition systems and relational structures of width two. A new construction of locally acyclic bisimilar covers provides a useful analogue of the well known tree-like unravellings that can be used for the purposes of finite model theory. Together with various other finitary bisimulation respecting model transformations, and Ehrenfeucht–Fraïssé game arguments, these covers allow us to upgrade finite approximations for full (...) bisimulation equivalence towards approximations for elementary equivalence. These techniques are used to prove several ramifications of the van Benthem–Rosen characterisation theorem of basic modal logic for refinements of ordinary bisimulation equivalence, both in the sense of classical and of finite model theory. (shrink)

The semantics of the independence friendly logic of Hintikka and Sandu is usually defined via a game of imperfect information. We give a definition in terms of a game of perfect information. We also give an Ehrenfeucht-Fraïssé game adequate for this logic and use it to define a Distributive Normal Form for independence friendly logic.

We investigate the definability in monadic ∑11 and monadic Π11 of the problems REGk, of whether there is a regular subgraph of degree k in some given graph, and XREGk, of whether, for a given rooted graph, there is a regular subgraph of degree k in which the root has degree k, and their restrictions to graphs in which every vertex has degree at most k, namely REGkk and XREGkk, respectively, for k ≥ 2 . Our motivation partly stems from (...) the fact that REGkk and XREGkk are logspace equivalent to CONN and REACH, respectively, for k ≥ 3, where CONN is the problem of whether a given graph is connected and REACH is the problem of whether a given graph has a path joining two given vertices. We use monadic first - order reductions, monadic ∑11 games and a recent technique due to Fagin, Stockmeyer and Vardi to almost completely classify whether these problems are definable in monadic ∑11 and monadic Π11, and we compare the definability of these problems. (shrink)

We study how equivalent nonisomorphic models an unsuperstable theory can have. We measure the equivalence by Ehrenfeucht-Fraisse games. This paper continues the work started in $[HT]$.

The authors show, by means of a finitary version □finλ, D of the combinatorial principle □b*λ of [7], the consistency of the failure, relative to the consistency of supercompact cardinals, of the following: for all regular filters D on a cardinal λ, if Mi and Ni are elementarily equivalent models of a language of size ≤ λ, then the second player has a winning strategy in the Ehrenfeucht-Fraïssé game of length λ+ on ∏i Mi/D and ∏i Ni/D. If (...) in addition 2λ=λ+ and i <λ implies |Mi|+|Ni|≤ λ+ this means that the ultrapowers are isomorphic. This settles negatively conjecture 18 in [2]. (shrink)

The present article, which is a revised version of part of [Hu1], deals with various relations between models which might serve as exact formulations for the vague concept "similar" or "almost isomorphic". One natural class of such formulations is equivalence in a given logic. Another way to express similarity is by potential isomorphism, i.e., isomorphism in some extension of the set-theoretic universe. The class of extensions may be restricted to give different notions of potential isomorphism. A third method is to (...) study the winning strategies for an Ehrenfeucht-Fraisse-game played between the two models, and the properties of the resulting equivalence and nonequivalence trees. The basic question studied here is whether one such notion of similarity implies another. Some implications and counterexamples listed in this part are previously known or trivial, but all are mentioned for completeness' sake. Only models of cardinality ℵ 1 are considered. Some results are therefore connected with the Continuum Hypothesis. (shrink)

We study how equivalent nonisomorphic models of unsuperstable theories can be. We measure the equivalence by Ehrenfeucht-Fraisse games. This paper continues [HS].

The properties of the ${\forall^{1}}$ quantifier defined by Kontinen and Väänänen in [13] are studied, and its definition is generalized to that of a family of quantifiers ${\forall^{n}}$ . Furthermore, some epistemic operators δ n for Dependence Logic are also introduced, and the relationship between these ${\forall^{n}}$ quantifiers and the δ n operators are investigated.The Game Theoretic Semantics for Dependence Logic and the corresponding Ehrenfeucht- Fraissé game are then adapted to these new connectives.Finally, it is proved that the ${\forall^{1}}$ (...) quantifier is not uniformly definable in Dependence Logic, thus answering a question posed by Kontinen and Väänänen in the above mentioned paper. (shrink)

We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.

We show in this paper that the theory of ordinal addition of any fixed ordinal ωα, with α less than ωω, admits a quantifier elimination. This in particular gives a new proof for the decidability result first established in 1965 by R. Büchi using transfinite automata. Our proof is based on the Ehrenfeucht games, and we show that quantifier elimination go through generalized power.RésuméOn montre ici que, pour tout ordinal α inférieur à ωω, la théorie additive de ωα (...) admet une élimination des quantificateurs. On obtient ainsi une nouvelle preuve de la décidabilité de ces théories . On utilise ici les jeux d'Ehrenfeucht, avec un formalisme à la Ferrante et Rackoff, et on montre que le fait d'admettre une élimination des quantificateurs se transmet par produit généralisé. (shrink)

We prove a local normal form theorem of the Gaifman type for the infinitary logic L∞ωω whose formulas involve arbitrary unary quantifiers but finite quantifier rank. We use a local Ehrenfeucht-Fraïssé type game similar to the one in [9]. A consequence is that every sentence of L∞ωω of quantifier rank n is equivalent to an infinite Boolean combination of sentences of the form ψ, where ψ has counting quantifiers restricted to the -neighborhood of y.

This book gives a comprehensive overview of central themes of finite model theory – expressive power, descriptive complexity, and zero-one laws – together with selected applications relating to database theory and artificial intelligence, especially constraint databases and constraint satisfaction problems. The final chapter provides a concise modern introduction to modal logic, emphasizing the continuity in spirit and technique with finite model theory. This underlying spirit involves the use of various fragments of and hierarchies within first-order, second-order, fixed-point, and infinitary logics (...) to gain insight into phenomena in complexity theory and combinatorics. The book emphasizes the use of combinatorial games, such as extensions and refinements of the Ehrenfeucht-Fraissé pebble game, as a powerful way to analyze the expressive power of such logics, and illustrates how deep notions from model theory and combinatorics, such as o-minimality and treewidth, arise naturally in the application of finite model theory to database theory and AI. Students of logic and computer science will find here the tools necessary to embark on research into finite model theory, and all readers will experience the excitement of a vibrant area of the application of logic to computer science. (shrink)

Inexpressibility results in Finite Model Theory are often proved by showing that Duplicator, one of the two players of an Ehrenfeucht game, has a winning strategy on certain structures.In this article a new method is introduced that allows, under certain conditions, the extension of a winning strategy of Duplicator on some small parts of two finite structures to a global winning strategy.As applications of this technique it is shown that • — Graph Connectivity is not expressible in existential monadic (...) second-order logic , even in the presence of a built-in linear order,• — Graph Connectivity is not expressible in MonNP even in the presence of arbitrary built-in relations of degree n0, and• — the presence of a built-in linear order gives MonNP more expressive power than the presence of a built-in successor relation. (shrink)

We strengthen nonstructure theorems for almost free Abelian groups by studying long Ehrenfeucht–Fraı̈ssé games between a fixed group of cardinality λ and a free Abelian group. A group is called ε -game-free if the isomorphism player has a winning strategy in the game of length ε ∈ λ . We prove for a large set of successor cardinals λ = μ + the existence of nonfree -game-free groups of cardinality λ . We concentrate on successors of singular cardinals.

Trees are natural generalizations of ordinals and this is especially apparent when one tries to find an uncountable analogue of the concept of the Scott-rank of a countable structure. The purpose of this paper is to introduce new methods in the study of an ordering between trees whose analogue is the usual ordering between ordinals. For example, one of the methods is the tree-analogue of the successor operation on the ordinals.

Trees are natural generalizations of ordinals and this is especially apparent when one tries to find an uncountable analogue of the concept of the Scott-rank of a countable structure. The purpose of this paper is to introduce new methods in the study of an ordering between trees whose analogue is the usual ordering between ordinals. For example, one of the methods is the tree-analogue of the successor operation on the ordinals.

An Abelian group G is strongly λ -free iff G is L ∞, λ -equivalent to a free Abelian group iff the isomorphism player has a winning strategy in an Ehrenfeucht–Fraı̈ssé game of length ω between G and a free Abelian group. We study possible longer Ehrenfeucht–Fraı̈ssé games between a nonfree group and a free Abelian group. A group G is called ε -game-free if the isomorphism player has a winning strategy in an Ehrenfeucht–Fraı̈ssé game of (...) length ε between G and a free Abelian group. We prove in ZFC existence of nonfree ε -game-free groups for many successors of regular cardinals. We also show that the length of the game obtained is very close to the optimal length provable in ZFC alone. On the other hand, assuming existence of a Mahlo cardinal, we sketch a proof that it is consistent to have a very highly game-free still nonfree group. First we present an introduction to basic constructions and then we introduce some results concerning the standard tools for building more complicated groups, namely transversals and λ -systems. It follows that all the constructions generalize to algebras in a fixed variety satisfying the strong construction principle. (shrink)

For countable structures U and B, let $\mathfrak{U}\overset{\alpha}{\rightarrow}\mathfrak{B}$ abbreviate the statement that every Σ0 α (Lω1,ω) sentence true in U also holds in B. One can define a back and forth game between the structures U and B that determines whether $\mathfrak{U}\overset{\alpha}{\rightarrow}\mathfrak{B}$ . We verify that if θ is an Lω,ω sentence that is not equivalent to any Lω,ω Σ0 n sentence, then there are countably infinite models U and B such that $\mathfrak{U} \vDash \theta, \mathfrak{B} \vDash \neg \theta$ , (...) and $\mathfrak{U}\overset{n}{\rightarrow}\mathfrak{B}$ . For countable languages L there is a natural way to view L structures with universe ω as a topological space, XL. Let [U] = {B ∈ XL∣B ≅ U} denote the isomorphism class of U. Let U and B be countably infinite nonisomorphic L structures, and let $C \subseteq \omega^\omega$ be any Π0 α subset. Our main result states that if $\mathfrak{U}\overset{\alpha}{\rightarrow}\mathfrak{B}$ , then there is a continuous function f: ωω → XL with the property that $x \in C \Rightarrow f(x) \in \lbrack\mathfrak{U}\rbrack$ and $x \notin C \Rightarrow f(x) \in \lbrack\mathfrak{B}\rbrack$ . In fact, for α ≤ 3, the continuous function f can be defined from the $\overset{\alpha}{\rightarrow}$ relation. (shrink)