Extending the WMSO+U Logic With Quantification Over Tuples
Abstract
We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier U, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a generalized quantifier U, expressing the fact that there exist tuples of arbitrarily large finite sets satisfying a given property. First, we prove that the new logic WMSO+U_tup is strictly more expressive than WMSO+U. In particular, WMSO+U_tup is able to express the so-called simultaneous unboundedness property, for which we prove that it is not expressible in WMSO+U. Second, we prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+K_tup.
Cite
@article{arxiv.2311.16607,
title = {Extending the WMSO+U Logic With Quantification Over Tuples},
author = {Anita Badyl and Paweł Parys},
journal= {arXiv preprint arXiv:2311.16607},
year = {2023}
}
Comments
This is an extended version of a paper published at the CSL 2024 conference