I have been studying a 1969 article by Rabin that proofs his apparently very influential Tree Theorem (that says the monadic second-order theory of 2 successors, S2S, is decidable).

To give a bit of context: the proof is focused around automata on infinite trees, and his basic idea is to construct an automaton $\mathcal A_\phi$ for each sentence $\phi$ of S2S representing it. This is done inductively on the structure of a formula, and thus to do this, we need to see that we can construct automata that represent the union or intersection of two automata (for $\vee$ and $\wedge$), and the complement and projection of an automaton (for $\neg$ and $\exists$). Then it is shown that a sentence $\phi$ is true iff $\mathcal A_\phi$ accepts at least one tree (that is, $T(\mathcal A_\phi)$, the set of tree accepted by $\mathcal A_\phi$ is non-empty).

To prove the negation and emptiness parts of this proof, I have read an article of Thomas (Languages, Automata, and Logic, ch.6, 1997). In his paper, he views runs of an automaton as games, and negation and emptiness follow from a certain determinacy theorem. This approach follows (Gurevich and Harrington, 1982). The determinacy theorem stated by Thomas is the following:

Theorem. (Determinacy of Rabin chain tree automata games)

In the game $\Gamma_{\mathcal A,t}$ based on a Rabin chain tree automaton $\mathcal A$ and a tree $t$, from any game position, either player 0 (Automaton) or player 1 (Pathfinder), has a memoryless winning strategy.

This theorem seems to come from Gurevich and Harrington, who in their paper prove a Forgetful Determinacy Theorem.

Now my question is about this determinacy result. It reminds something of Gale-Stewart games and their theorem. Now I am not yet very familiar with Gale-Stewart games and descriptive set theory, but I am wondering:

Question. Is there a link between the Determinacy Theorem by Thomas or Gurevich and Harrington and the Gale-Stewart Theorem? Can one be proven using the other, can we alter circumstances to see some equivalence, etc. So basically:

(How) are the results related?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.