The MSO+U theory of (N, <) is undecidable

TL;DR

This paper proves that the MSO+U logic, which extends monadic second-order logic with an unbounding quantifier, is undecidable over infinite words, resolving an open problem and improving prior results.

Contribution

It establishes the undecidability of MSO+U on infinite words, settling an open question and removing the need for additional axioms used in earlier proofs.

Findings

MSO+U logic is undecidable on infinite words

The result improves previous undecidability proofs

Settles an open problem in logic theory

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.