Numerical expressive power of logical languages with cardinality comparison.

This article investigates the numerical expressive power of several logical languages—fragments of Presburger Arithmetic (PbA), monadic second-order logic with counting over finite domains (MSO|$^{\phi}(\#)$|), and shallow second-order graded modal logic with counting over image-finite frames (SOGML|$^{\textsf{s},\phi}(\#)$|). It establishes that their respective existential fragments without certain key symbols (|$1$| in PbA, equality in MSO|$^{\phi}(\#)$|, and graded modalities in SOGML|$^{\textsf{s},\phi}(\#)$|) define exactly the strongly semilinear sets, while adding these symbols or universal quantifiers extends definability to all semilinear sets. The paper further provides a simpler characterization of definable subsets of natural numbers in the one-dimensional case as those semilinear sets closed under taking multiples, and explores applications of these results in frame correspondence theory, illustrating how modal-like languages with counting can define various numerical frame properties.