How unprovable is Rabin's decidability theorem?

DOI10.1145/2933575.2934543MaRDI QIDQ4635942zbMATH OpenOpenAlexFDO

Authors Henryk Michalewski, Leszek Aleksander Kołodziejczyk

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1508.06780

zbMATH Keywords

automata on infinite treesdeterminacy of infinite gamesmonadic second order logicRabin's decidability theoremreverse mathematics

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Foundations of classical theories (including reverse mathematics) (03B30) Automata and formal grammars in connection with logical questions (03D05) Determinacy principles (03E60) Second- and higher-order arithmetic and fragments (03F35)

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

Recommendations

• The logical strength of Büchi's decidability theorem
• The logical strength of Büchi's decidability theorem
• scientific article; zbMATH DE number 3983141
• scientific article; zbMATH DE number 2206111
• An algebraic proof of Rabin's tree theorem

Cited in

(10)

• An algebraic proof of Rabin's tree theorem
• When Is Reachability Intrinsically Decidable?
• scientific article; zbMATH DE number 1499098 (Why is no real title available?)
• Monadic Second Order Logic with Measure and Category Quantifiers
• A functional (monadic) second-order theory of infinite trees
• The logical strength of Büchi's decidability theorem
• scientific article; zbMATH DE number 2206111 (Why is no real title available?)
• The logical strength of Büchi's decidability theorem
• The metamathematics of separated determinacy
• Automatic structures and the problem of natural well-orderings

This page was built for publication: How unprovable is Rabin's decidability theorem?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635942)