On Effective Banach-Mazur Games and an application to the Poincaré Recurrence Theorem for Category

Technical Summary: On Effective Banach-Mazur Games and an Application to the Poincaré Recurrence Theorem for Category

Problem Statement
Classical mathematics often relies on non-constructive existence proofs (e.g., via the Axiom of Choice or Zorn's Lemma) to demonstrate that objects with certain properties exist by showing the set of such objects is "large" in a topological sense (Baire category). Specifically, the Banach-Mazur game provides a game-theoretic characterization of sets of the first category (meager sets): a set is of first category if and only if the second player has a winning strategy.

However, in the realm of computability theory and effective analysis, existential arguments are insufficient. There is a need to extract the "effective content" of classical theorems, requiring explicit, algorithmic constructions. While the effective Baire category theorem and effective measure-theoretic versions of the Poincaré Recurrence Theorem are known, the effective topological version of the Poincaré Recurrence Theorem had not been fully established for all sets of effective first category. The authors aim to bridge this gap by effectivizing the Banach-Mazur game and applying it to dynamical systems.

Methodology
The authors develop a framework for Effective Topological Spaces and Effective Banach-Mazur Games within the context of Computable Analysis.

1. Effective Topological Spaces: The work operates primarily within computable $T_0$ spaces (specifically strongly computable $T_0$ spaces for the first game version and complete computable metric spaces for the second). These spaces are equipped with a countable basis and a representation of basic open sets via partial computable surjections. Key definitions include:

   • c.e. open sets: Unions of basic open sets that are computably enumerable.
   • Effective nowhere dense sets: Sets $A$ where a computable function can map any basic open set to a smaller basic open set disjoint from $A$.
   • Effective first category sets: Countable unions of effective nowhere dense sets.

2. Effective Banach-Mazur Games: The authors define two versions of the game to characterize effective meagerness:

   • Version 1: Player 2 (P2) is restricted to an effective strategy (computable response), while Player 1 (P1) has unbounded resources. The game is played on a strongly computable $T_0$ space.
   • Version 2: P1 has an effective strategy, while P2 has unbounded resources. This version requires the space to be a complete computable metric space to utilize Cantor's Intersection Theorem for convergence.

3. Game-Theoretic Proofs: Instead of using Zorn's Lemma (which is non-constructive), the authors provide explicit, constructive strategies for the players. They demonstrate that if a set is of effective first category, P2 possesses a computable winning strategy. Conversely, if P2 has a computable winning strategy, the target set is of effective first category.

Key Contributions and Results

1. Characterization of Effective First Category Sets:
   The primary theoretical contribution is Theorem 4.3, which establishes that in a strongly computable $T_0$ space, a set $M$ is of effective first category if and only if Player 2 has an effective winning strategy in the Banach-Mazur game $BM(M, M^c)$. This provides a purely game-theoretic, constructive characterization of effective meagerness, avoiding non-constructive existential arguments.

2. Application to Liouville Numbers:
   The authors apply their framework to the set of Liouville numbers ($E$). They prove (Theorem 4.12) that the complement of the set of Liouville numbers ($E^c$) is an effective first category set. Consequently, the set of Liouville numbers is effectively co-meager. This result highlights that while Liouville numbers are "small" in terms of Lebesgue measure and Hausdorff dimension, they are "large" in the effective topological sense.

3. Effective Poincaré Recurrence Theorem for Category:
   The paper's central application is Theorem 5.5, the Effective Poincaré Recurrence Theorem for Category.

   • Context: For a bounded computably enumerable (c.e.) open region $X \subseteq \mathbb{R}^n$ equipped with a computable homeomorphism $T$ that admits no non-empty open wandering sets.
   • Result: The set of non-recurrent points in $X$ is a set of effective first category.
   • Method: The authors define the set of non-recurrent points $N(E)$ and construct an effective winning strategy for Player 2 in the game $BM(N(E), X \setminus N(E))$. By showing that for any open set chosen by P1, P2 can effectively choose a sub-set disjoint from the non-recurrent points (utilizing the non-existence of wandering sets), they prove that the intersection of the game play avoids the non-recurrent set entirely.

Significance
The paper claims significance in providing a game-theoretic proof of the effective topological Poincaré Recurrence Theorem. Unlike previous approaches that might rely on effective ergodic theorems (which are measure-theoretic), this work operates strictly within the topological framework of Baire category.

By effectivizing the Banach-Mazur game, the authors demonstrate that the "size" of the set of non-recurrent points is not just topologically small (meager) but effectively small (effective first category). This means the set of non-recurrent points can be covered by a computably enumerable union of effective nowhere dense sets, and a computable strategy exists to avoid these points. This resolves the issue of establishing the topological Poincaré theorem for all sets of effective first category, offering a constructive perspective on recurrence in computable dynamical systems.