Connecting Decidability and Complexity for MSO Logic
This work is about studying reasons for (un)decidability of variants of Monadic Second-order (mso) logic over infinite structures. Thus, it focuses on connecting the fact that a given theory is (un)decidable with certain measures of complexity of that theory.
The first of the measures is the topological complexity. In that case, it turns out that there are strong connections between high topological complexity of languages available in a given logic, and its undecidability. One of the milestone results in this context is the Shelah’s proof of undecidability of mso over reals.
The second complexity measure focuses on the axiomatic strength needed to actually prove decidability of the given theory. The idea is to apply techniques of reverse mathematics to the classical decidability results from automata theory. Recently, both crucial theorems of the area (the results of Büchi and Rabin) have been characterised in these terms. In both cases the proof gives strong relations between decidability of the mso theory with concepts of classical mathematics: determinacy, Ramsey theorems, weak Konig’s lemma, etc.
KeywordsMonadic second-order logic Decidability Descriptive set theory Reverse mathematics
- 1.Blumensath, A., Colcombet, T., Parys, P.: On a fragment of AMSO and tiling systems. In: STACS, pp. 19:1–19:14 (2016)Google Scholar
- 5.Bojańczyk, M., Colcombet, T.: Bounds in \(\omega \)-regularity. In: LICS, pp. 285–296 (2006)Google Scholar
- 7.Bojańczyk, M., Parys, P., Toruńczyk, S.: The MSO+U theory of (n, \(<\)) is undecidable. In: STACS, pp. 1–8 (2016)Google Scholar
- 8.Bojańczyk, M., Toruńczyk, S.: Deterministic automata and extensions of weak MSO. In: FSTTCS, pp. 73–84 (2009)Google Scholar
- 9.Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Lane, S.M., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi, pp. 1–11. Springer, New York (1962)Google Scholar
- 12.Friedman, H.: Some systems of second order arithmetic and their use. pp. 235–242 (1975)Google Scholar
- 19.Kolmogorov, A.N.: Operations sur des ensembles. Mat. Sb. 35, 415–422 (1928). (in Russian, summary in French)Google Scholar
- 20.Kołodziejczyk, L.A., Michalewski, H.: How unprovable is Rabin’s decidability theorem? In: LICS, pp. 788–797 (2016)Google Scholar
- 21.Kołodziejczyk, L.A., Michalewski, H., Pradic, P., Skrzypczak, M.: The logical strength of Büchi’s decidability theorem. In: CSL, pp. 36:1–36:16 (2016)Google Scholar