English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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. We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that • the complementation theorem for non-deterministic tree automata, • the decidability of the Π13 fragment of MSO on the infinite binary tree, • the positional determinacy of parity games, and • the determinacy of Bool(∑02) Gale-Stewart games are all equivalent over Π12-comprehension. It follows in particular that Rabin's decidability theorem is not provable from Δ13-comprehension.

How unprovable is Rabin's decidability theorem?