An Ehrenfeucht‐Fraïssé class game

Abstract

Abstract 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 (coloring) moves played in different models. The game allows Duplicator to delay her choices of the models till (practically) 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 F 1 n 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 H 1 n gives some new separation results on the class of finite models among various F 1 n on one hand and between F 1 n and H 1 n on the other. Since function quantifiers involve a bounded type of second order existential quantifiers, the class game (in a sense) 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. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)