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?



You must log in to answer this question.

Browse other questions tagged .