In mathematical logic, monadic second-order logic 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 graphs of bounded treewidth. Second-order logic allows quantification over predicates. However, MSO is the fragment in which second-order quantification is limited to monadic predicates. This is often described as quantification over "sets" because monadic predicates are equivalent in expressive power to sets.
Existential monadic second-order logic 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 second-order logiccaptures precisely the descriptive complexity of the complexity classNP, 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, in the logic of graphs, testing whether a graph is disconnectedbelongs to monadic NP, as the test can be represented by a formula that describes the existence of a proper subset of vertices with no edges connecting them to the rest of the graph; however, the complementary problem, testing whether a graph is connected, does not belong to monadic NP. The existence of an analogous pair of complementary problems, only one of which has an existential second-order formula is equivalent to the inequality of NP and coNP, an open question in computational complexity. By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finite tree, this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to a tree automaton and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generally nonelementary. Thanks to Courcelle's theorem, we can also evaluate a Boolean MSO formula in linear time on an input graph if the treewidth of the graph is bounded by a constant. For MSO formulas that have free variables, when the input data is a tree or has bounded treewidth, there are efficient enumeration algorithms to produce the set of all solutions, ensuring that the input data is preprocessed in linear time and that each solution is then produced in a delay linear in the size of each solution, i.e., constant-delay in the common case where all free variables of the query are first-order variables. There are also efficient algorithms for counting the number of solutions of the MSO formula in that case.
