Monadic second-order logic: Difference between revisions

Revision as of 00:09, 25 August 2022

Revision as of 18:38, 14 November 2022

Line 32:

== Decidability and complexity of satisfiability ==

The satisfiability problem for monadic second-order logic is undecidable in general because this logic subsumes [[Firstfirst-order logic]].

The monadic second order theory of the infinite complete [[binary tree]], called [[S2S (mathematics) | S2S]], is [[decidability (logic)|decidable]].<ref>{{Cite journal|last=Rabin|first=Michael O.|date=1969|title=Decidability of Second-Order Theories and Automata on Infinite Trees|url=https://www.jstor.org/stable/1995086|journal=Transactions of the American Mathematical Society|volume=141|pages=1–35|doi=10.2307/1995086|jstor=1995086|issn=0002-9947}}</ref> As a consequence of this result, the following theories are decidable:

* The monadic second-order theory of trees.

* The monadic second order theory of <math>\mathbb{N}</math> under successor (S1S).

* wS2SWS2S and wS1SWS1S, which restrict quantification to finite subsets (weak monadic second order logic). Note that for binary numbers (represented by subsets), addition is definable even in wS1SWS1S.

For each of these theories (S2S, S1S, wS2SWS2S, wS1SWS1S), the complexity of the decision problem is [[nonelementary problem|nonelementary]].<ref name=":0" /><ref>{{Cite journal|last1=Stockmeyer|first1=Larry|last2=Meyer|first2=Albert R.|date=2002-11-01|title=Cosmological lower bound on the circuit complexity of a small problem in logic|url=https://doi.org/10.1145/602220.602223|journal=Journal of the ACM|volume=49|issue=6|pages=753–784|doi=10.1145/602220.602223|s2cid=15515064|issn=0004-5411}}</ref>

=== Use of satisfiability of MSO on trees in verification ===