Arithmetic, First-Order Logic, and Counting Quantifiers

TL;DR

This paper explores the expressive power of first-order logic with counting quantifiers and arithmetic, proving Presburger arithmetic's closure under unary counting and implications for graph reachability and the Crane Beach conjecture.

Contribution

It establishes that Presburger arithmetic remains closed under unary counting quantifiers, providing new insights into logical expressibility and limitations.

Findings

Presburger arithmetic is closed under unary counting quantifiers.

Reachability in finite graphs is not expressible with unary counting and addition.

A specific version of the Crane Beach conjecture fails.

Abstract

This paper gives a thorough overview of what is known about first-order logic with counting quantifiers and with arithmetic predicates. As a main theorem we show that Presburger arithmetic is closed under unary counting quantifiers. Precisely, this means that for every first-order formula phi(y,z_1,...,z_k) over the signature {<,+} there is a first-order formula psi(x,z_1,...,z_k) which expresses over the structure <Nat,<,+> (respectively, over initial segments of this structure) that the variable x is interpreted exactly by the number of possible interpretations of the variable y for which the formula phi(y,z_1,...,z_k) is satisfied. Applying this theorem, we obtain an easy proof of Ruhl's result that reachability (and similarly, connectivity) in finite graphs is not expressible in first-order logic with unary counting quantifiers and addition. Furthermore, the above result on Presburger arithmetic helps to show the failure of a particular version of the Crane Beach conjecture.