Monadic second-order logic: Difference between revisions

Revision as of 17:29, 3 November 2017

Revision as of 12:58, 31 July 2018

Line 1:

In [[mathematical logic]], '''monadic second order logic (MSO)''' is the fragment of [[HigherSecond-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 allows quantification over [[Predicate (mathematical logic)|predicates]]. However, MSO is the [[Fragment (logic)|fragment]] 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).