Borel Determinacy

[David Roberts]

Hi all,

I was wondering what constructive perspectives, if any, there are on the theorem that Gale–Stewart games with Borel payoff sets (“Borel games”) are determined. Famously, not even the axioms of ZFC without Replacement (so, something like Bounded Zermelo with Choice, or ETCS) can show this, an axiom like “all beths exist” or at minimum “all beths with countable ordinal index exist” is required. 

I was wondering if the question about the determinacy of a Borel game even makes sense from a constructive point of view, regardless of whether it can be proved or not. For other special cases one can examine the setup and think about what constructive, or at least neutral, thinking has to say. From Wikipedia:

Real-world games of perfect information, such as tic-tac-toe, chess, or infinite chess, are always finished in a finite number of moves (in infinite chess-games this assumes the 50-move rule is applied). If such a game is modified so that a particular player wins under any condition where the game would have been called a draw, then it is always determined.[4] The condition that the game G_A is always over (i.e. all possible extensions of the finite position result in a win for the same player) in a finite number of moves corresponds to the topological condition that the set A giving the winning condition for G_A is clopen in the topology of Baire space.

Here the set A is a subset of Baire space, which is certainly an object one can discuss/examine from a constructive pov. The Gale–Stewart theorem says that closed (and open) A give determined games. I’ve seen the G–S theorem described as being constructive, for instance in The extent of constructive game labellings  by Benedikt Löwe and Brian Semmes (https://eprints.illc.uva.nl/id/eprint/654/1/X-2005-02.text.pdf). They also have a footnote:

The fact that Büchi conjectures that there is a constructive proof of Borel determinacy [Bü83, Problem 1] suggests that his notion of “constructive” is extremely liberal, at least more liberal than our notion of a combinatorial labelling.

[Bü83] is published in the Journal of Symbolic Logic (https://www.jstor.org/stable/2273681).

I suspect that Büchi’s idea that the proof of open determinacy “actually presents” the winner might well only be constructive in the sense of not using choice, but perhaps it really is constructive.

From the point of view of looking at Baire space as a locale, and what it would be mean to talk about payoff sublocales, I don’t know what is meaningful here.

I asked a while ago on MathOverflow about whether mathematics “really needs Replacement”, and while people keep pointing to Borel Determinacy, it was a shock at the time to find out that it only needs the instance of replacement which is essentially induction along omega_1 to get the function \alpha |—> P^\alpha(|N) for countable ordinals \alpha. (See https://golem.ph.utexas.edu/category/2021/07/borel_determinacy_does_not_require_replacement.html for discussion). I do not doubt that derminacy of G–S games is mathematics, but I’m wondering if there is any content that avoids non-constructive commitments, and how strong results can be, and if this is provable say in the internal language of a topos.

I’m interested to hear thoughts or receive pointers to literature.

David