Two-variable Logic with Counting and a Linear Order

TL;DR

This paper investigates the finite satisfiability problem for two-variable logic with counting over linearly ordered structures, revealing undecidability with two orders and high complexity with one order, linking it to multicounter automata emptiness.

Contribution

It establishes the decidability and complexity boundaries of C2 logic with linear orders, including undecidability with two orders and a connection to multicounter automata.

Findings

Undecidable for two linear orders with additional binary symbols.

NEXPTIME-complete for one linear order with successor.

Complexity matches multicounter automata emptiness problem.

Abstract

We study the finite satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in the presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in the presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and in the presence of other binary predicate symbols is equivalent, under elementary reductions, to the emptiness problem for multicounter automata.