Kurt Gödel Research Center

2016 seminar talk: How unprovable is Rabin's decidability theorem?

Talk held by Leszek Kołodziejczyk (University of Warsaw, Poland) at the KGRC seminar on 2016-01-14.

Abstract

Rabin's decidability theorem states the decidability of the monadic second order (MSO) theory of two successors, i.e. of the infinite binary tree with the left- and right-successor relations. The MSO theory of two successors is able to express some nontrivial determinacy principles, and most proofs of Rabin's theorem make use of such principles, so it is reasonable to ask whether the theorem could be unprovable in relatively strong axiomatic theories.

I will talk about some joint work with Henryk Michalewski in which we attempt to give a reverse-mathematical characterization of the logical strength needed to prove Rabin's theorem. We show that over $ACA_0$, the complementation theorem for nondeterministic tree automata, which is a crucial ingredient of typical proofs of Rabin's theorem, implies a sentence expressing the determinacy of all $Bool({\bf \Sigma^0_2})$ games. Moreover, using results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld, we show that over $\Pi^1_2$-$CA_0$, this sentence is actually equivalent to Rabin's theorem restricted to the $\Pi^1_3$ fragment of MSO.

It follows from our work and from known results on determinacy principles that even a restricted version of Rabin's theorem is unprovable in $\Delta^1_3$-$CA_0$. On the other hand, any version that can be stated in second-order arithmetic is provable in $\Pi^1_3$-$CA_0$ (and, in fact, in $\Pi^1_2$-$CA_0$ plus $\Pi^1_3$ induction).