Monadic second-order logic: Difference between revisions

Revision as of 22:06, 25 March 2017

Revision as of 15:10, 26 March 2017

Line 1:

In [[mathematical logic]], '''monadic second order logic (MSO)''' is the fragment of [[Higher-order logic|second-order logic]] where the second-order quantification is limited to quantification over sets.<ref>{{cite book|first1=Bruno|last1=Courcelle|author1-link=Bruno Courcelle|first2=Joost|last2=Engelfriet| title=Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach| publisher=Cambridge University Press|date=2012-01-01|isbn=978-0521898331|url=http://dl.acm.org/citation.cfm?id=2414243|accessdate=2016-09-15}}</ref> 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.

Second-order logic more generally allows quantification over [[Predicate (mathematical logic)|predicates]],. and monadicHowever, second-order logicMSO is the [[Fragment (logic)|fragment]] of MSO in which onlysecond-order quantification is limited to monadic predicates (predicates having a single argument). This is often described as quantification over "sets" because monadic predicates are allowedequivalent in expressive power to sets (the set of elements for which the predicate is true).

However, a monadic predicate is equivalent in its expressive power to a set (the set of elements for which the predicate is true), so monadic second-order logic is often more simply described in terms of sets rather than predicates.

Existential monadic second-order logic (EMSO) is the fragment of MSO in which all quantifiers over sets must be [[existential quantifier]]s, 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 (complexity)|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 (graph theory)|connectivity of graphs]] belongs to monadic co-NP (the [[Complement (set theory)|complement]] of monadic NP) but not to monadic NP itself.<ref>{{citation