Two variable logic with ultimately periodic counting

TL;DR

This work extends two-variable logic with counting by introducing ultimately periodic counting quantifiers and proves the decidability of both satisfiability and finite satisfiability, while also showing that the spectrum of any sentence is definable in Presburger arithmetic. The authors reduce logical satisfiability to the analysis of constrained biregular graphs, establishing Presburger-definable characterizations of graph-size vectors via existential Presburger formulas. They develop a multi-layered framework, starting from a 1-color core and progressively handling multi-color and non-simple matrices, including completeness constraints and digraphs, with a detailed complexity analysis culminating in a 2-$ exp$ upper bound for satisfiability. The results yield precise information about the model sizes (spectrum) and position the work relative to existing decidability results for related logics. Overall, this paper demonstrates how Presburger-definable size constraints in biregular graphs can powerfully decide expressive extensions of FO2 with counting, with broad implications for description logic tools and finite-model theory.

Abstract

We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the ``biregular graph method''. In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

Figures (13)

• Figure 1: Illustration of a graph representation of a structure with $1$-types $\pi_1,\pi_2,\pi_3$. The $2$-types are $E_1,E_2,E_3,E_4$ represented by edges with color black, red, blue and green, respectively. The vertices $u_1,u_2,u_3$ are in $A_{\pi_1}$, $v_1,v_2$ are in $A_{\pi_2}$ and $w$ is in $A_{\pi_3}$.
• Figure 2: Edge swapping used in the proof of Lemma \ref{['lem:1type-s1']}. After swapping there is one less parallel edge between $u$ and $v$, and the degrees of all vertices stay the same.
• Figure 3: Illustration of the choice of the vertices $z_0\in Z$ and $u\in U_1$. The set $V'$ is the set of the neighbors of $z_0$. The set $U'$ is the set of the neighbors of the vertices in $V'$ in set $U_1$, i.e., the set of vertices reachable from $z_0$ in distance $2$. Since $|U_1|\geq \delta(\va,\vb)^2+1$ and $|U'|\leq \delta(\va,\vb)^2$, there is a vertex $u \in U_1 - U'$. We merge $z_0$ and $u$ into one vertex.
• Figure 4: Illustration of why the formula for the "not big enough" case is a necessary condition.
• Figure 5: Splitting a vertex $w$ in a digraph $G$ into two vertices $u$ and $v$ in $G'$. One is adjacent to all the outgoing edges and the other to all the incoming edges.

Theorems & Definitions (117)

• theorem 1
• proposition 1
• theorem 2
• theorem 3
• corollary 1
• proof
• remark 1
• theorem 4
• corollary 2
• definition 1