An Ehrenfeucht-Fraisse class game

摘要

This paper introduces a new Ehrenfeucht-Fraisse 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-Fraisse 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 (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.