On Expansions of Monadic Second-Order Logic with Dynamical Predicates

TL;DR

This paper proves the decidability of monadic second-order logic over natural numbers extended with certain dynamic predicates derived from integer recurrence sequences, introducing a new technical concept called prodisjunctivity.

Contribution

It establishes decidability results for MSO logic with a broad class of dynamical predicates and introduces the novel concept of effective prodisjunctivity.

Findings

Decidability of MSO theory with dynamical predicates.

Introduction of the concept of effective prodisjunctivity.

Potential applications of prodisjunctivity in logic and computer science.

Abstract

Expansions of the monadic second-order (MSO) theory of the structure $\langle \mathbb{N} ; < \rangle$ have been a fertile and active area of research ever since the publication of the seminal papers of B\"uchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of $\langle \mathbb{N} ; <,P \rangle$, where $P$ ranges over a large class of unary ''dynamical'' predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.