
Summary: This paper presents a relatively compact yet complete proof of the Forgetful Determinacy Theorem (FDT) of Yuri Gurevich and Leo Harrington. The original motivation for this theorem was to provide a simpler proof of a powerful decidability result by Michael Rabin. Rabin's result and related techniques have found considerable application in computer science in dealing with the satisfiability problem for modal logics of programs. The FDT asserts the existence of a special kind of winning strategy in a particular class of infinite games. Although it first appeared as part of an alternative proof of Rabin's theorem, the FDT is a game-theoretic result that applies to more general situations than those in which it was originally used. Both the FDT and an earlier result by Richard Büchi and Lawrence Landweber address the issue of what kind of information is necessary to execute the winning strategy. Recently infinite games have been used to model non-terminating computations, and common methods of specification for such computations produce games to which the FDT applies. The original proof of the FDT was sketchy. Other proofs have been given, including one by Alexander and Vladimir Yakhnis that strengthened the result by providing more explicit strategies for the players. Nevertheless, there was still need for a more compact proof. To produce such a proof, we apply a modified version of the one by Yakhnis and Yakhnis to the slightly more general setting of graph-games. We use the notion of graph-games to emphasize the relationship between the FDT and the earlier result by Büchi and Landweber.
Logic in computer science, infinite games, decidability, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), winning strategy, monadic second-order theories, Decidability of theories and sets of sentences, graph-games, forgetful determinacy theorem, restricted-memory strategies, Games involving graphs, Higher-order logic; type theory
Logic in computer science, infinite games, decidability, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), winning strategy, monadic second-order theories, Decidability of theories and sets of sentences, graph-games, forgetful determinacy theorem, restricted-memory strategies, Games involving graphs, Higher-order logic; type theory
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 11 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
