Arithmetic, first-order logic, and counting quantifiers
Nicole Schweikardt · ACM Transactions on Computational Logic · 2005
This article 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 φ( y , z ) over the signature {<,+} there is a first-order formula ψ( x , z ) which expresses over the structure 〈ℕ,<,+〉 (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 φ( y , z ) 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.