How unprovable is Rabin's theorem?

Second-order arithmetic is an axiomatic theory in a language with two sorts of variables, one for representing natural numbers and the other for representing sets of natural numbers. The theory is roughly as strong as set theory without the power set axiom. Fragments of second-order arithmetic provide a natural way of measuring the logical strength needed to prove theorems of "ordinary" (i.e., not set-theoretic) mathematics.

In my talk, I will first give an overview of the basics of second-order arithmetic, and then explain what axioms are needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. The work on Rabin's theorem is joint with Henryk Michalewski.