A Game for Counting Logic Formula Size and an Application to Linear Orders

TL;DR

This paper introduces a new Ehrenfeucht-Fra"issé game tailored for counting logic with limited variables, enabling the first known lower bounds on formula size for distinguishing linear orders.

Contribution

It extends existing formula size lower bounds from first-order logic to counting logic, using a novel game combining previous approaches.

Findings

Established the first formula size lower bound for counting logic.

Extended lower bounds for distinguishing linear orders to counting logic.

Demonstrated the applicability of the new game to finite model theory.

Abstract

Ehrenfeucht-Fra\"iss\'e (EF) games are a basic tool in finite model theory for proving definability lower bounds, with many applications in complexity theory and related areas. They have been applied to study various logics, giving insights on quantifier rank and other logical complexity measures. In this paper, we present an EF game to capture formula size in counting logic with a bounded number of variables. The game combines games introduced previously for counting logic quantifier rank due to Immerman and Lander, and for first-order formula size due to Adler and Immerman, and Hella and V\"a\"an\"anen. The game is used to prove the main result of the paper, an extension of a formula size lower bound of Grohe and Schweikardt for distinguishing linear orders, from 3-variable first-order logic to 3-variable counting logic. As far as we know, this is the first formula size lower bound for counting logic.