Open determinacy

Stream: maths

[Patrick Lutz]

Recently, Michael Wolman and I formalized a proof of open determinacy (the proof can be found here) and are thinking about formalizing Borel determinacy. But before we do we would like to figure out a good set of definitions for the concepts involved in determinacy, especially a good definition of "game" and of "strategy." So I thought I'd start this thread to get feedback on our ideas.

The work we've done so far is on github here. Right now it's kind of messy but I think the core definitions are not too hard to parse. Here's a summary of these core definitions:

• A "game" consists of a type $\alpha$ of possible moves, a type $\beta$ of players and a function turn which determines at each position in the game which player should move next. A position in such a game is a finite list of elements of $\alpha$.
• A "quasi-strategy" is a kind of generalization of a strategy. Formally a quasi-strategy for a player $p \in \beta$ consists of a set of positions in the game such that for any position $s$ in this set, if player $p$ should play next then at least one extension of $s$ is in the set and if some other player should play next then every extension of $s$ is in the set.
• A quasi-strategy is a strategy if, when it's player $p$'s turn, exactly one extension of $s$ is in the set.
• A "play" of the game is a function $f \colon \N \to \alpha$. A play obeys a quasi-strategy if every long enough prefix of $f$ is in the set of positions of the quasi-strategy.
• A payoff set for a game is a function $P$ from plays to $\beta$. A quasi-strategy is winning if for all plays $f$ which obey the quasi-strategy, $P(f)$ matches the player of the quasi-strategy.
• A set $A\subseteq \N \to \alpha$ corresponds to a payoff set in a game where the players are "true" and "false."

My first question is whether there is any feedback about these definitions. I will also mention some of our ideas about how to approach Borel determinacy and how we might want to change these definitions.

[Patrick Lutz]

One thing that would be nice is having a better definition for a "strategy at position $s$." Here's one idea for changing the definitions:

• A "rooted game tree" $T$ consists of:
  • A game $G$
  • A root $s$ (a position in the game)
  • A set of positions in the game
  • A proof that $s$ is in the set of positions and that all positions extend $s$
• A predicate "is quasi-strategy" on rooted game trees which takes a game $G$, a rooted game tree $T$ and a player $p$ and asserts that for all $t$ in $T$'s set of positions:
  • If it's player $p$'s turn then there is at least one element of $\alpha$ which can be added to $t$ to get another element of $T$
  • If it's not player $p$'s turn then all elements of $\alpha$ can be added to $t$ to get an element of $T$

[Patrick Lutz]

I've noticed that there have been a few discussions of borel determinacy on here in the past. Some of these discussions involved the borel hierarchy. However, it is not necessary to talk about the borel hierarchy to prove borel determinacy. In particular, one can do the following:

• Define what it means for a payoff set to be "unravellable"
• Prove that all closed sets are unravellable
• Prove that the class of unravellable sets is closed under negations and countable unions

The only tricky point here is that "unravellable" needs to be defined slightly differently from the way it is in the literature on determinacy. In particular, for this proof it is best to define a set $A$ to be unravellable if for all continuous functions $f$, $f^{-1}(A)$ is unravellable in the normal sense

[Pedro Sánchez Terraf]

This is an extremely interesting development. The material on Borel hierarchy is still under PR review, but it is still of an elementary character---no need to depend on that, as you say

[Patrick Lutz]

Another thing that would be nice for defining games and strategies and so on is to be able to define games where the set of possible moves depends on the turn. E.g. suppose we have a function E : ℕ → Type* then it would be nice to be able to define a game where the set of possible moves after $n$ turns is E(n). The problem is that a position in this game should be a finite list $s$ where the type of the nth element of the list is E(n). But I am not aware of such finite lists in mathlib

[Patrick Lutz]

One solution I've thought of for this is to allow "positions" in a game to be a "cylinder" in this sense. However, it would also be nice to be able to use all the lemmas already proved about lists in mathlib, which don't seem to be as abundant for cylinders. Also the set of cylinders is not a type in mathlib, which makes things more complicated

[Patrick Lutz]

Also, once we decide on better definitions, Michael and I would like to add what we've done to mathlib. Does anyone have any suggestions for the best place in mathlib for the basic definitions of games and strategies to go?

[David Wärn]

This sounds very interesting, especially your ideas on proving Borel determinacy.

I've tried to propagate here before the idea of treating infinite games using coinduction. All the concepts you describe have simple coinductive characterisations. I'll explain a bit how. Let me first say that it's not so important what coinductive types "really are", rather what's important is their API, which is centered on destructors and corecursors (this is dual to how an inductive type has constructors and a recursor, or elimination principle). So, regardless of how exactly you choose to define your concepts, I would suggest to build a coinductive API around them. An upshot of this perspective is that you never have to think about positions as lists of moves, or of the natural numbers which index the moves in a play.

Let's first consider the type of games from a coinductive perspective. Let's say $\beta$ is the type of players. For a player $b : \beta$, we will have a type $G(b)$ of games where $b$ is the starting player. Given a game $g : G(b)$, there should be some type $\alpha(g)$ of available starting moves, and for any $a : \alpha(g)$, there should be a next player $np(a) : \beta$, together with a next game $ng(a) : G(np(a))$, in which $np(a)$ is the starting player. Here, $\alpha$, $np$, and $ng$ are all destructors for the (indexed) type $G$ of games. The corresponding corecursor explains how to define games (essentially, it says that for any other type family $G'$ over $\beta$ which has the same destructors as $G$, there is a map $G'(b) \to G(b)$, i.e. a way to define games from terms of $G'$).

Now let's describe the type of plays in a game $g : G(b)$. A play $f : pl(g)$ should determine an first move $mv(p) : \alpha(g)$ (this is one destructor) together with a play $tail(p) : pl(ng(mv(p)))$ (this is another destructor). The corecursor explains how to define plays.

Now let's describe quasi-strategies for player $p : \beta$. For any $b : \beta$ and $g : G(b)$, we have a type $qs_p(g)$ of quasi-strategies for $p$ starting at $g$. If $p = b$, a quasi-strategy should produce a non-empty subset of $\alpha(g)$ (this is one destructor), and for any element of this subset, a quasi-strategy for the resulting next game (this is another destructor). If $p \ne b$, the quasi-strategy determines for any possible next game, a quasi-strategy. The corecursor for quasi-strategies explains how to define a quasi-strategy.

In a similar way, you can define strategies (either directly, or by defining coinductively what it means for a quasi-strategy to be a strategy). You can also define coinductively what it means for a play to be consistent with a quasi-strategy. There is a fundamental theorem that given a quasi-strategy for each player, there is a play consistent with each of the quasi-strategies. In the coinductive framework, this play can be defined directly by corecursion.

All the examples above are maybe simple, and can be understood directly without coinduction. My expectation is that when you go further and formalise more complicated concepts (e.g. related to Borel determinacy), the coinductive perspective becomes more useful.

Lean does not support coinductive types as primitive type formers, but non-indexed coinductive types have been defined in docs#pfunctor.M. It should also be feasible to define indexed M-types, which should be sufficient for all the definitions above. But again, even if you don't want to take this route, I would suggest to think about the coinductive API for the definitions you gave above. That is, to define destructors and corecursors for all your types, and to use them in place of inspecting the actual definition of a game / play etc.

[Pedro Sánchez Terraf]

Patrick Lutz said:

• A "game" consists of a type $\alpha$ of possible moves, a type $\beta$ of players and a function turn which determines at each position in the game which player should move next. A position in such a game is a finite list of elements of $\alpha$.

I've seen at most one example of game with more than two players in descriptive set theory. If you have pointers to more uses of this general setting, I'd be thankful. Are you thinking about more general game-theoretic issues here?

[Patrick Lutz]

Pedro Sánchez Terraf said:

I've seen at most one example of game with more than two players in descriptive set theory. If you have pointers to more uses of this general setting, I'd be thankful. Are you thinking about more general game-theoretic issues here?

I don't know many examples in descriptive set theory of games with multiple players. But allowing multiple players did not seem to make anything harder so I decided to include it. The statement of open determinacy that I linked to only allows games where the set of players is Prop

[Pedro Sánchez Terraf]

By the way,
Patrick Lutz said:

The statement of open determinacy that I linked to only allows games where the set of players is Prop

I couldn't check your code yet (perhaps the reasons are there) but I think it is an interesting point in deciding whether Prop or bool is the appropriate choice of a 2-element set.

[Patrick Lutz]

Pedro Sánchez Terraf said:

I couldn't check your code yet (perhaps the reasons are there) but I think it is an interesting point in deciding whether Prop or bool is the appropriate choice of a 2-element set.

The nice thing about using Prop is that subsets (which are maps from the set to Prop) are literally payoff sets according to my definition

[Patrick Lutz]

David Wärn said:

I've tried to propagate here before the idea of treating infinite games using coinduction. All the concepts you describe have simple coinductive characterisations.

I'll need more time to think about this, but it's an interesting idea. One thing I am concerned about is that in the proof of borel determinacy, some of the definitions and proofs really seem to rely on knowing the number of turns. In particular, in this proof the definition of "k-covering" (bottom of page 451) and the inverse limit construction (lemma 4) seem hard to understand using only the "coinductive api" for games.

[Pedro Sánchez Terraf]

Patrick Lutz said:

Pedro Sánchez Terraf said:

I couldn't check your code yet (perhaps the reasons are there) but I think it is an interesting point in deciding whether Prop or bool is the appropriate choice of a 2-element set.

The nice thing about using Prop is that subsets (which are maps from the set to Prop) are literally payoff sets according to my definition

Yes, that's nice. Also, there's the obvious asymmetry between the two players (both bool and Prop are ordered in the expected way). But (to make my suggestion more precise) if you need to topologize the type of payoff sets, please take into account that Prop is not canonically discrete.

[Felix Weilacher]

I'm really glad someone is working on this! One very small thing is that I have an open PR #18248 that, to facilitate building what Kechris calls "schemes", defines a function res which is identical to your function stream_prefix and proves similar things about it. In general I wish there was more in mathlib about the interplay between finite and infinite sequences in terms of topology/DST.

[Felix Weilacher]

Patrick Lutz said:

One solution I've thought of for this is to allow "positions" in a game to be a "cylinder" in this sense. However, it would also be nice to be able to use all the lemmas already proved about lists in mathlib, which don't seem to be as abundant for cylinders. Also the set of cylinders is not a type in mathlib, which makes things more complicated

I don't like the current state of cylinder x n. It feels very weird that I need to provide all of x when I'm only using its first n entries. Maybe you could use \Sigma n, E(n) as your \alpha and somehow restrict to plays f where f(n).1 = n for all n? Maybe thats too messy though.

[Patrick Lutz]

Felix Weilacher said:

I don't like the current state of cylinder x n. It feels very weird that I need to provide all of x when I'm only using its first n entries. Maybe you could use \Sigma n, E(n) as your \alpha and somehow restrict to plays f where f(n).1 = n for all n? Maybe thats too messy though.

That's an interesting idea. What would be really nice to have imo is a type of "finite dependent lists" (i.e. lists where the type of each element depends on the position in the list) with a good api.

[Patrick Lutz]

Then "cylinder" could also be defined in a more natural way

[Yaël Dillies]

Finite dependent lists already exist. See for example docs#quiver.path

[Patrick Lutz]

Yaël Dillies said:

Finite dependent lists already exist. See for example docs#quiver.path

If I'm understanding correctly, you mean "mathlib already contains things that are essentially finite dependent lists, e.g. quiver.path." What's not clear to me (but I would be happy to learn about) is whether there is some sort of standard "finite dependent list" in mathlib the way listis the standard type of finite lists. I agree that quiver.path is a finite dependent list, but (if I understand correctly) a fairly specialized one that is not appropriate for defining games in determinacy

[Felix Weilacher]

Maybe this warrants a new topic, but I was talking with Michael today (we happen to be at the same conference right now) and there was strong agreement that using list.concat as the standard way to inductively build our finite sequences is pretty terrible and results in a lot of rw's for things that really ought to be defeq. I think we're both in favor of just using list.cons and accepting that, in DST, we're going to think of sequences as being built from right to left. Or, maybe its more correct to say that when doing DST we're going to ignore the usual meaning of a few things like list.nth or the way lists display when doing an #eval etc. The downsides seem minor. Any thoughts on setting this as the standard for DST in mathlib moving forwards?

[Pedro Sánchez Terraf]

I'm not quite sure if I understand the phrase “ignore the usual meaning of ... list.nth”. I think this means that it won't reflect the meaning of application (as in Kechris' book), since the ordering is reversed.

I actually agree chaging order is immaterial, and this might be the right way to go. But perhaps this also means that there's some “list API for DST” that needs to be developed.

[Felix Weilacher]

list.nth s n is meant to be the "nth element of a list s", but if we're thinking of our lists as going from right to left, then we would think of this as the s.length - n - 1-th element

[Felix Weilacher]

So yes, if you're thinking about lists as functions with some natural number as their domain, this is saying list.nth is not giving us function application (which is what it is intended to represent).

[Patrick Lutz]

Another option would be to define a new type of list which naturally grows at the end instead of the beginning and allows for different types at different positions. Such an object could be defined very similar to quiver.path that was mentioned above. This would solve multiple problems at once for doing DST in Lean

[Patrick Lutz]

This is all assuming that such a thing has not already been defined in mathlib of course

[Felix Weilacher]

Patrick Lutz said:

Another option would be to define a new type of list which naturally grows at the end instead of the beginning and allows for different types at different positions. Such an object could be defined very similar to quiver.path that was mentioned above. This would solve multiple problems at once for doing DST in Lean

I think this would be great but I'm not personally interested in redoing all the stuff that is already nicely set up for lists

[Patrick Lutz]

Felix Weilacher said:

I think this would be great but I'm not personally interested in redoing all the stuff that is already nicely set up for lists

Fair enough, though I feel some of that has already happened with cylinders.

[Felix Weilacher]

Yes agreed. At some point it is probably worth reworking parts of the pi_nat file