Keywords

1 Introduction

Monadic Second-order (mso) logic is one of the fundamental logics used in the areas of verification and model checking. It is a very expressive formalism, comprising most of the other logics used for specifications, like ltl, ctl*, modal \(\mu \)-calculus, etc. Thus, the decision methods for mso over infinite words [9]; trees [24]; and certain linear orders [26] are commonly used to easily derive more decidability results. Because of its strength, it seems that mso lies at the borderline of decidability, a prominent example is the theorem of Shelah [26] stating that the mso theory of reals is undecidable. Similar undecidability results hold in the case of infinite words, when adding new monadic predicates [25]; or infinite trees when adding a well-order on the nodes [10]. A separate branch of studies asks which asymptotic extensions of mso are decidable [1, 4, 7].

Since variants of mso seem to occur on both sides of the decidability borderline, one can ask the following question: what makes a given theory (un)decidable? The aim of this work is to survey results answering the above question using two notions of complexity of the theory.

2 Descriptive Set Theory

The first notion of complexity that we discuss is the topological complexity of sets available in the given logic. To measure this complexity, one uses Borel and Projective Hierarchies, see [18]. From this perspective, mso theory of infinite words is very simple, as all the languages definable there are Boolean combinations of \(\mathbf {\Pi }^{0}_{2}\)-sets [28]. Similarly, the topological complexity of mso over infinite trees is also under control, the languages definable there occupy exactly the first \(\omega \) levels of the hierarchy of \(\mathcal {R} \)-sets (introduced by Kolmogorov in [19]); all of them belong to \(\mathbf {\Delta }^{1}_{2}\); and all of them are measurable [14].

On the other hand [15, 26], the mso theory of reals \((\mathbb {R},{\le })\) is undecidable, the proofs rely on a construction of a very complexFootnote 1 set \(Q\subseteq \mathbb {R}\). Shelah [26] conjectured, that when we restrict set quantification to Borel subsets of \(\mathbb {R}\) then the theory becomes decidable. This conjecture is still open, the best known result going in that direction follows from Rabin’s theorem [24]: mso of \(\mathbb {R}\) with set quantifiers ranging over \(\mathbf {\Pi }^{0}_{2}\)-sets is decidable.

Bojańczyk in [2] proposed an asymptotic extension of mso (denoted mso+u) by a quantifier \(\mathsf U\) that informally allows to express that the delays between consecutive events are unbounded. Although some fragments of mso+u were proved to be decidable [3,4,5, 8]; the question of decidability of the full logic mso+u was left open. The first witness that the logic might turn out to be undecidable was given by a result [16] showing that mso+u over infinite words defines languages lying arbitrarily high in Projective Hierarchy (i.e. \(\mathbf {\Pi }^{1}_{n}\)-complete). By incorporating the methods of Shelah [26], this led to the following results.

Theorem 1

([6]). Assume a set-theoretic axiom that v = l (called Axiom of Constructibility [13, 17]). Let \(\mathcal {L} \) be an extension of mso logic that defines a \(\mathbf {\Pi }^{1}_{6}\)-complete set of infinite words. Then the \(\mathcal {L} \)-theory of the infinite tree is undecidable.

Corollary 2

([6]). It is consistent with zfc that the mso+u theory of the infinite tree is undecidable.

Although the above corollary does not prove undecidability of mso+u, it implies that there is no concrete algorithm solving that theory which correctness can be proven in zfc. Thus, there was no hope that the theory may be decidable in the standard sense. This line of research was later surmounted by a direct proof of undecidability of mso+u over infinite words [7].

3 Reverse Mathematics

We will now focus on decidable theories, like in the classical theorems of Büchi [9] and Rabin [24]. We would like to understand how logically difficult these theorems are. The standard notion of complexity used for measuring logical difficulty of theorems is given by reverse mathematics [12, 27]. The recipe is as follows:

  1. 1.

    We choose some logical system to work in, usually it is second-order arithmetic.

  2. 2.

    We formalise the given theorem as a sentence \(\varPhi \) in that logical system.

  3. 3.

    We choose some very weak basic theory (usually it is a theory called \(\mathrm {RCA}_0\)).

  4. 4.

    Then we prove that over \(\mathrm {RCA}_0\), the sentence \(\varPhi \) is equivalent to some known axiom \(\chi \).

The last step consists of two implications: one of them boils down to proving that the theorem follows from \(\mathrm {RCA}_0 +\chi \) (i.e. one can prove it using only \(\chi \)). The second implication is more tricky, it says that \(\chi \) is necessary for the theorem to hold, i.e. over \(\mathrm {RCA}_0\) the pure fact that \(\varPhi \) holds implies \(\chi \).

Over the years, many standard mathematical results were characterised in terms of their axiomatic strength. As it turned out, the set of additional axioms \(\chi \) that typically appear in this context is very limited. Actually most of the every-day mathematics turns out to be equivalent to one of five standard logical systems, called Big Five [27, page 42]. Among them is Weak König’s Lemma (denoted \(\mathsf {WKL}_0\)), used in many arguments using compactness. An example of a commonly used axiom outside Big Five is Ramsey’s Theorem for Pairs and arbitrarily many colours (\(\mathsf {RT}^2_{<\infty }\)), known to be incomparable to \(\mathsf {WKL}_0\)  [22].

The famous theorem of Büchi states that mso is decidable over infinite words. From the modern perspective, there are at least two different ways of proving that result: either by determinisation à la McNaughton [23]; or by direct complementation as done by Büchi [9]. The combinatorial core of the former approach is based on applications of König’s Lemma, while the latter relies on Ramsey’s Theorem. Thus, from the reverse mathematical point of view these seem to be two orthogonal proofs. However, in both cases the respective principles are used in a very limited way: König’s Lemma is applied to trees generated by automata; while Ramsey’s Theorem is applied to colourings that bear additional algebraic structure.

As it turned out [21], Büchi’s decidability theorem is equivalent over \(\mathrm {RCA}_0\) to the principle of induction for \(\varSigma ^0_2\)-formulae (denoted \(\varSigma ^0_2\) \(\text {-}\mathsf {IND}\)). Also, \(\varSigma ^0_2\text {-}\mathsf {IND} \) was shown [21] to be equivalent to an additive version of Ramsey’s Theorem and to imply the automata-related version of König’s Lemma. These results provide a rather complete picture of the logical strengths of principles involved in Büchi’s decidability result.

Rabin’s Theorem [24] proving decidability of mso over infinite trees was always believed to be more demanding than Büchi’s result. In particular, to the author’s best knowledge there is no known proof of Rabin’s result that would avoid using automata and determinacy of related games. This observation has been formalised in [20], where the authors proved that (in a strong sense) Rabin’s complementation result is equivalent to the statement of determinacy of games with winning conditions being Boolean combinations of \(\mathbf {\Pi }^{0}_{2}\)-sets.

In both above cases, the respective theorem about mso turned out to be equivalent to other standard mathematical statements. This suggests that the decidability results about a logic that is robust enough must convey certain knowledge about the whole mathematical universe. Following this idea it seems interesting and promising to study other decidability theorems for robust logics, for instance the result of decidability of mso over countable linear orders [11, 26]. From the point of view of direct implications, this result is somewhere in-between the theorems of Büchi and Rabin.

4 Conclusions

The aim of this survey was to present certain perspectives in which decidability of a given variant of mso is related to a certain measure of complexity for that logic. The presented examples advocate that, when one faces the question whether a given logic is decidable, it may be useful to analyse the complexity of the logic itself (instead of looking directly for an algorithm or a reduction).

For instance, high topological complexity of languages definable in the logic may indicate (or even prove, see Corollary 2) that the logic cannot be decidable. Similarly, if decidability of the logic has very strong axiomatic consequences, there is no hope to prove it without any strong tools.

On the other hand, if the logic seems to have very limited access to the mathematical universe, one may expect a direct proof of decidability, for instance by a reduction to an appropriately chosen logic that is stronger but still decidable.