Monadic second order finite satisfiability and unbounded tree-width

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result [Seese, D. (1991). The structure of the models of decidable monadic theories of graphs. Annals of pure and applied logic, 53(2), 169-195]. We prove the following problem is decidable: Input: (i) A monadic second order logic sentence \alpha, and (ii) a sentence \beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of \alpha and \beta may intersect. Output: Is there a finite structure which satisfies both \alpha and \beta such that the restriction of the structure to the vocabulary of \alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form |X_1|+. .. +|X_r|<|Y_1|+. .. +|Y_s|, where the X_i and Y_j are monadic second order variables. We prove the decidability of a similar extension of WS1S.

Authors

• Tomer Kotek

Keywords

No keywords are indexed for this paper.