Monadic second-order logic

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.

Syntax

Concretely, the basic syntax of MSO is as follows:

• There is an infinity of second-order variables, denoted X, Y, \ldots.
• If t is a first-order term and X is a second-order variable, then x \in X is a formula of MSO.
• If \varphi is a first-order formula - perhaps using the aforementioned atomic predicate - then it is also an MSO formula.
• If \varphi(X) is an MSO formula then so are \forall X. \varphi(X) and \exists X. \varphi(X).

Successors

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 s(-), then we speak of one successor. The MSO theory of \mathbb{N} with one successor, also known as S1S, is decidable.

• If the syntax consists of two function symbols, say s0(-) and s1(-), then we speak of two successors. The MSO theory of finite binary strings \mathbb{B}^\ast two successors, also known as S2S, is also decidable.

References

• Wikipedia page.