In mathematical logic, monadic second order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over certain types of graphs.
Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be existential quantifiers, outside of any other part of the formula. The first-order quantifiers are not restricted. By analogy to Fagin's theorem, according to which existential (non-monadic) second-order logic captures precisely the descriptive complexity of the complexity class NP, the class of problems that may be expressed in existential monadic second-order logic has been called monadic NP. The restriction to monadic logic makes it possible to prove separations in this logic that remain unproven for non-monadic second-order logic; for instance, testing the connectivity of graphs belongs to monadic co-NP (the complement of monadic NP) but not to monadic NP itself.