On the strictness of the quantifier structure hierarchy in first-order logic

TL;DR

This paper investigates the quantifier structure hierarchy in first-order logic, proving its strictness over finite and ordered finite structures using novel Ehrenfeucht-Fraisse game variants.

Contribution

It introduces a new game-based method to characterize quantifier classes and demonstrates the hierarchy's strictness in finite and ordered structures, advancing understanding in descriptive complexity.

Findings

The quantifier structure hierarchy is strict over finite structures.

The hierarchy remains strict even over ordered finite structures.

A new Ehrenfeucht-Fraisse game variant characterizes quantifier classes.

Abstract

We study a natural hierarchy in first-order logic, namely the quantifier structure hierarchy, which gives a systematic classification of first-order formulas based on structural quantifier resource. We define a variant of Ehrenfeucht-Fraisse games that characterizes quantifier classes and use it to prove that this hierarchy is strict over finite structures, using strategy compositions. Moreover, we prove that this hierarchy is strict even over ordered finite structures, which is interesting in the context of descriptive complexity.