Monadic second-order logic (often abbreviated MSO) is a fragment of second-order logic in which we may only quantify over sets (and not arbitrary predicates of arbitrary arity).
It is often studied in Computer Science because of its good decidability, definability, and complexity properties.
Concretely, the basic syntax of MSO is as follows:
Decidability and definability results often refer to MSO with one, two, or more successors. This refers to the function symbols available in terms.
If the syntax supports only one unary function symbol , then we speak of one successor. The MSO theory of with one successor, also known as S1S, is decidable.
If the syntax consists of two function symbols, say and , then we speak of two successors. The MSO theory of finite binary strings two successors, also known as S2S, is also decidable.