Definition: The class of first-order logic formulas in the language that contains only unary predicates.

Decidability: special case of first-order theory of Boolean Algebras, or WS1S, so it can be decided using techniques we have seen:

• Deciding Boolean Algebra with Presburger Arithmetic
• Deciding MSOL over Strings and Trees in Lecture 15

If we take a formula in monadic class and

• flatten
• skolemize
• look at Herbrand universe

Then we obtain set constraints.

Converse is also true: for every set constraint there exists a corresponding formula in monadic class.

• Bachmair, Ganzinger, Waldmann: Set constraints are the monadic class