How unprovable is Rabin's decidability theorem?

Leszek Aleksander Kołodziejczyk, Henryk Michalewski

We study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that the complementat…