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 Buchi 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.