How unprovable is Rabin's decidability theorem?
Leszek Aleksander Kołodziejczyk, Henryk Michalewski · 2016
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 over the second-order arithmetic theory ACA0, the complementation theorem for nondeterministic tree automata is equivalent to a statement expressing the determinacy of all Gale-Stewart games given by Bool(∑02) sets. It follows that the complementation theorem is provable from Π13- but not Δ13-comprehension.