Two variable logic with ultimately periodic counting

TL;DR

This paper extends two-variable logic with periodic counting quantifiers, proving decidability of satisfiability and finite satisfiability, and showing spectra are Presburger-definable, with refinements to the biregular graph method.

Contribution

It introduces a new logic with ultimately periodic counting, establishes its decidability, and refines the biregular graph method for analyzing two-variable logics.

Findings

Satisfiability and finite satisfiability are decidable for the extended logic.

Spectra of sentences are definable in Presburger arithmetic.

Refinements to the biregular graph method improve analysis of two-variable logics.

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.