How unprovable is Rabin's decidability theorem?

Abstract

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 complementation theorem for tree automata, which forms the technical core of typical proofs of Rabin's theorem, is equivalent over the moderately strong second-order arithmetic theory $\mathsf{ACA}_0$ to a determinacy principle implied by the positional determinacy of all parity games and implying the determinacy of all Gale-Stewart games given by boolean combinations of ${\bf Σ^0_2}$ sets. It follows that complementation for tree automata is provable from $Π^1_3$- but not $Δ^1_3$-comprehension. We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that over $Π^1_2$-comprehension, the complementation theorem for tree automata, decidability of the MSO theory of the infinite binary tree, positional determinacy of parity games and determinacy of $\mathrm{Bool}({\bf Σ^0_2})$ Gale-Stewart games are all equivalent. Moreover, these statements are equivalent to the $Π^1_3$-reflection principle for $Π^1_2$-comprehension. It follows in particular that Rabin's decidability theorem is not provable in $Δ^1_3$-comprehension.