Definability in the monadic second-order theory of successor

Abstract

Let be a relational system whereby D is a nonempty set and P₁ is an m₁-ary relation on D. With we associate the (weak) monadic second-order theory consisting of the first-order predicate calculus with individual variables ranging over D; monadic predicate variables ranging over (finite) subsets of D; monadic predicate quantifiers; and constants corresponding to P₁, P₂, …. We will often use ambiguously to mean also the set of true sentences of .