How unprovable is Rabin's decidability theorem?

Original · EN

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 ACA₀ 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 Σ⁰₂ sets. It follows that complementation for tree automata is provable from Π¹₃- but not Δ¹₃-comprehension. We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that over Π¹₂-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 Bool(Σ⁰₂) Gale-Stewart games are all equivalent. Moreover, these statements are equivalent to the Π¹₃-reflection principle for Π¹₂-comprehension. It follows in particular that Rabin's decidability theorem is not provable in Δ¹₃-comprehension.