How unprovable is Rabin’s decidability theorem?

摘要

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 ACA₀, the complementation theorem for nondeterministic tree automata is equivalent to a statement expressing the determinacy of all Gale-Stewart games given by Bool(Σ₂^{0) sets. It follows that the complementation theorem is provable from II₃1 but not Δ₃1- comprehension. We then use results due to MedSalem-Tanaka, Mollerfeld and Heinatsch-Mollerfeld to prove that · the complementation theorem for non-deterministic tree automata, · the decidability of the Π1 3 fragment of MSO on the infinite binary tree, · the positional determinacy of parity games, and · the determinacy of Bool(Σ₂0) Gale-Stewart games are all equivalent over II₂1-comprehension. It follows in particular that Rabin's decidability theorem is not provable from Δ₃1- comprehension.}