The reverse mathematics of decidability results for monadic second order logic

I will talk about the results of a reverse mathematics-style study of the axiomatic strength needed to prove two classical results on the decidability of monadic second order theories: Büchi's Theorem, which concerns the monadic theory of the natural numbers with successor, and Rabin's Theorem, which concerns the monadic theory of the full infinite binary tree with the left- and right-successor relations.
Unlike most typical decidability theorems for first order theories, the proofs of Büchi's and Rabin's Theorems seem to require the use of some nontrivial set-theoretic principles: either Ramsey's Theorem or Kőnig's Lemma in the case of Büchi, and a restricted version of Borel determinacy in the case of Rabin. We show that in fact, the Ramsey-theoretic principle needed to prove Büchi's Theorem is quite tame, and the decidability theorem itself holds in the recursive reals, though it is not provable in RCA_0. On the other hand, the determinacy principle used in the proof of Rabin's Theorem turns out to be equivalent to a crucial automata-theoretic fact used in the inductive proof of the theorem, and in some contexts to the decidability theorem itself. It follows that Rabin's Theorem is unprovable in relatively strong fragments of second order arithmetic.
The talk will be based on joint work with Henryk Michalewski, Pierre Pradic and Michał Skrzypczak.