How unprovable is Rabin's decidability theorem?

TL;DR

This paper investigates the logical strength required to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree, revealing it exceeds certain weak comprehension axioms.

Contribution

It establishes the exact logical strength needed for Rabin's theorem, connecting it to determinacy principles and reflection principles in second-order arithmetic.

Findings

Rabin's theorem is equivalent to a determinacy principle over ACA_0.

Complementation for tree automata is provable from Pi^1_3 but not Delta^1_3 comprehension.

Rabin's decidability theorem is not provable in Delta^1_3 comprehension.

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 \Sigma^0_2}$ sets. It follows that complementation for tree automata is provable from $\Pi^1_3$- but not $\Delta^1_3$-comprehension. We then use results due to MedSalem-Tanaka, M\"ollerfeld and Heinatsch-M\"ollerfeld to prove that over $\Pi^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 \Sigma^0_2})$ Gale-Stewart games are all equivalent. Moreover, these statements are equivalent to the $\Pi^1_3$-reflection principle for $\Pi^1_2$-comprehension. It follows in particular that Rabin's decidability theorem is not provable in $\Delta^1_3$-comprehension.