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)

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 establish a general hierarchy theorem for quantifier classes in the infinitary logic L∞ωωon finite structures. In particular, it is shown that no infinitary formula with bounded number of universal quantifiers can express the negation of a transitive closure.This implies the solution of several open problems in finite model theory: On finite structures, positive transitive closure logic is not closed under negation. More generally the hierarchy defined by interleaving negation and transitive closure operators is strict. This proves a conjecture of (...) Immerman.We also separate the expressive power of several extensions of Datalog, giving new insight in the fine structure of stratified Datalog. (shrink)