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

TL;DR

The paper introduces a counting-logic formula-size game (CS) that blends elements of the HV first-order size game and the Immerman–Lander counting-game to analyze succinctness in $\mathcal{C}^t_m$. It proves a lower bound of $|\phi| \ge \sqrt{n}/t$ for any 3-variable counting-logic formula distinguishing two linear orders of sizes $n$ and $m>n$, and provides a matching upper bound of $|\phi| = O(n/t)$ for the $\mathcal{C}^t_2$ fragment, thereby extending Grohe–Schweikardt’s FO lower bounds to counting logic. The framework relies on extended syntax trees, separators, and a counting-aware weighting scheme, including the novel concept of gap variables to handle counting quantifiers. The results advance our understanding of succinctness in counting logics and have potential implications for characterizing the expressive power of graph neural networks via counting-logical formalisms.

Abstract

Ehrenfeucht-Fraïssé (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äänänen. 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.

Figures (10)

• Figure 1: Two families, $A = \{(\mathcal{A}, \alpha)\}$ and $B = \{(\mathcal{B}, \beta)\}$, for the $\exists z$ move in the HV-game.
• Figure 2: The $\exists^{\geq k}$-move in the CS game. On the left the $k$-Change operation: $k$ different elements are chosen by Spoiler. On the right the two steps of the $k$-Multiplication. The first step is to form all $k$-choice functions (each symbolized by a box). In the second step Spoiler picks one interpretation in each box to compose the new family.
• Figure 3: Structures $\mathcal{A}$ and $\mathcal{B}$ with relations $red$ and $blue$, and a possible $\exists^{\geq 2}x$ move.
• Figure 4: The structure of the proof.
• Figure 5: Case 2 of the proof of Lemma \ref{['key:Lemma']}. We associate a ball with center $\alpha(u)$ of radius $\delta_1({u,v})$ for every $u \in \{x,y,min,max\}$ on $\mathcal{A}$ (resp. $\beta(u)$ on $\mathcal{B}$). Each ball associated to variable $u$ accounts for the ability of the pair $\{u,z\}$ to separate. The crossed dot on $\mathcal{A}$ represents a choice on the linear order from $F^k$, the crossed dot on $\mathcal{B}$ represents "a best attempt" at a response for indistinguishability. In Case 2, the choice on $\mathcal{A}$ is in a nearness relationship (for $\delta_1(\{x,z\})$ on the figure), and there is no element of $\mathcal{B}$ that matches the separating conditions for indistinguishability (in the figure, d$(a_1, \alpha(x)) =$ d$(b_1, \beta(x))$ but $<$-type$(a_1) \neq$$<$-type$(b_1)$).

Theorems & Definitions (41)

• Definition 3.1: $r$-round EF $m$-pebbling game
• Theorem 3.2
• Definition 3.3: HV game for formula size on first-order logic
• Theorem 3.4
• Definition 4.1
• Definition 4.2: CS game for formula size on counting logic
• Example 4.3
• Theorem 5.1: Characterization Theorem
• Corollary 5.2
• Corollary 5.3