The MSO+U theory of (N, <) is undecidable
Logic in Computer Science
2015-02-18 v2
Abstract
We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.
Keywords
Cite
@article{arxiv.1502.04578,
title = {The MSO+U theory of (N, <) is undecidable},
author = {Mikołaj Bojańczyk and Paweł Parys and Szymon Toruńczyk},
journal= {arXiv preprint arXiv:1502.04578},
year = {2015}
}
Comments
9 pages, with 2 figures