Inmathematical logic,monadic second-order logic (MSO) is the fragment ofsecond-order logic where the second-order quantification is limited to quantification over sets.^[1] It is particularly important in thelogic of graphs, because ofCourcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of boundedtreewidth. It is also of fundamental importance inautomata theory, where theBüchi–Elgot–Trakhtenbrot theorem gives a logical characterization of theregular languages.

Second-order logic allows quantification overpredicates. However, MSO is thefragment in which second-order quantification is limited to monadic predicates (predicates having a single argument). This is often described as quantification over "sets" because monadic predicates are equivalent in expressive power to sets (the set of elements for which the predicate is true).

Monadic second-order logic comes in two variants. In the variant considered over structures such as graphs and in Courcelle's theorem, the formula may involve non-monadic predicates (in this case the binary edge predicate${\displaystyle E(x,y)}$), but quantification is restricted to be over monadic predicates only. In the variant considered in automata theory and the Büchi–Elgot–Trakhtenbrot theorem, all predicates, including those in the formula itself, must be monadic, with the exceptions of equality (${\displaystyle =}$) and ordering () relations.

Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must beexistential quantifiers, outside of any other part of the formula. The first-order quantifiers are not restricted. By analogy toFagin's theorem, according to which existential (non-monadic) second-order logic captures precisely thedescriptive 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 thelogic of graphs, testing whether a graph isdisconnected belongs 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.^[2][3] The existence of an analogous pair of complementary problems, only one of which has an existential second-order formula (without the restriction to monadic formulas) is equivalent to the inequality of NP andcoNP, an open question in computational complexity.

By contrast, when we wish to check whether a Boolean MSO formula is satisfied by an input finitetree, this problem can be solved in linear time in the tree, by translating the Boolean MSO formula to atree automaton^[4] and evaluating the automaton on the tree. In terms of the query, however, the complexity of this process is generallynonelementary.^[5] Thanks toCourcelle's theorem, we can also evaluate a Boolean MSO formula in linear time on an input graph if thetreewidth of the graph is bounded by a constant.

For MSO formulas that havefree variables, when the input data is a tree or has bounded treewidth, there are efficientenumeration algorithms to produce the set of all solutions,^[6] 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 (i.e., they do not represent sets). There are also efficient algorithms for counting the number of solutions of the MSO formula in that case.^[7]

The satisfiability problem for monadic second-order logic is undecidable in general because this logic subsumesfirst-order logic.

The monadic second-order theory of the infinite completebinary tree, calledS2S, isdecidable.^[8] As a consequence of this result, the following theories are decidable:

• The monadic second-order theory of trees.
• The monadic second-order theory of${\displaystyle \mathbb{N}}$ under successor (S1S).
• WS2S and WS1S, which restrict quantification to finite subsets (weak monadic second-order logic). Note that for binary numbers (represented by subsets), addition is definable even in WS1S.

For each of these theories (S2S, S1S, WS2S, WS1S), the complexity of the decision problem isnonelementary.^[5][9]

Monadic second-order logic of trees has applications informal verification. Decision procedures for MSO satisfiability^[10][11][12] have been used to prove properties of programs manipulating linkeddata structures,^[13] as a form ofshape analysis, and forsymbolic reasoning inhardware verification.^[14]

• Descriptive complexity theory
• Monadic predicate calculus
• Second-order logic

• Mathematical logic

• Articles with short description
• Short description is different from Wikidata