Extensions of MSO and the monadic counting hierarchy
The paper studies the expressive power of first-order logic extended with the unary second-order qualifier Most\(^1\). The authors first consider monadic second-order logic with first-order Rescher quantifier over unary vocabularies, and show that it corresponds to Presburger arithmetic. Then they extend this result to monadic second-order logic with the vectorization of the Rescher quantifier by proving its correspondence to the \(\Delta_0\)-fragment of arithmetic. The paper next shows that every vectorization of the first-order Rescher quantifier is definable in the logic FO(Most\(^1\)) and that FO(Most\(^1\)) collapses to uniform-TC\(^0\) on unary vocabularies. The collapse follows a separation result for first-order logic with the binary second-order majority quantifier and FO(Most\(^1\)) over the empty vocabulary. On strings, however, the logic FO(Most\(^1\)) captures the linear fragment of the counting hierarchy, and over a non-unary vocabulary, it can define complete problems for every level of the counting hierarchy.
scientific article; zbMATH DE number 5835734
scientific article