Borel determinacy

Stream: Is there code for X?

[Kevin Buzzard]

Consider the type of maps from nat to bool. Given a subset S of this type, you get a two-player game. Two players, Odd and Even, alternately choose booleans and build a function, and player one (Even, choosing f(0)) wins iff the resulting function is in S. For some subsets S, one player has a winning strategy: these games are called determined. For a random S there will be no winning strategy for either player, assuming the axiom of choice (the axiom of determinacy is the statement that all games are determined and I believe it is consistent with ZF but contradicts choice).

Now X := nat -> bool is an infinite product of bools and if we regard these bools as having the discrete topology, X gets product topology. Open determinacy is the theorem that if S is an open set then some player has a winning strategy. The proof is that a basic open set contains Y -> bool for a cofinite set Y and moves numbered in Y have no effect on the outcome, so the game is essentially finite and so someone has a winning strategy by brute force.

Borel determinacy is a cool result in this area. It says that if S is a Borel set in the sense of topology then some player has a winning strategy. I remember going through the proof when I was a grad student.

We don't have any of this kind of logic stuff as far as I know. I gave a talk "about mathlib" yesterday (I posted the slides on Twitter) and during the discussion afterwards a logician asked if we had a proof of this and said it was an interesting result because of some theorem saying that you can't prove it without some kind of induction up to omega_1. It reminded me of Sebastien's talk in Pittsburgh which also contained such an induction which he did with clever use of an inductive type. Can a similar trick be used here?

[Mario Carneiro]

I expect so, although it's hard to say without details of the proof

[Mario Carneiro]

from a purely logical point of view, lean has the power to do transfinite induction to omega_1 and far beyond

[David Wärn]

Isn't this the proof of open determinacy? "assume player one cannot guarantee a win in any finite number of moves. Then player two has a strategy that preserves this. After using this strategy, player one did not win after finitely many moves. Since S is open, player one did not win."

[Reid Barton]

The main argument of https://www.math.ucla.edu/~dam/booketc/purely_inductive.pdf (page 6) is a strong induction on the Borel rank. That is, the inductive hypothesis is applied not to the "components" of the set under consideration, but different Borel sets (in fact, Borel sets in different ambient spaces) of equal Borel rank. However, there is still a trick to avoid working directly with ordinals which applies here.

[Reid Barton]

It's the method I used in https://gist.github.com/rwbarton/201fa67f590e2932808032343bfab9cc
Basically, create a new inductive type borel_rank which has the same structure as the inductive prop which defines Borel-ness, but without any of its data fields, and then prove a theorem of the form "for all r : borel_rank, for all Borel sets which can be constructed using a proof whose shape agrees with r, ..." by induction on r.

[Reid Barton]

A theme is that these transfinite induction arguments need to induct on something well-founded (of course) and of sufficiently high cofinality (in the case of Borel sets, we can build a new Borel set out of countably many old Borel sets so every countable set of stages in our induction must have an upper bound). However, inducting on a total order is frequently not necessary. If you also require that the order is total, then you have an ordinal (of sufficiently high cofinality). Classically there is no shortage of these (and so it is also possible to emulate this argument in Lean) but even in ZF there might not be any ordinal of uncountable cofinality, and in any case the argument with ordinals might be annoying to formalize. Without the total condition, you can just write down an auxiliary inductive type with the required properties.

[David Wärn]

So borel_rank plays the role of countable ordinals, to index what Martin calls $\Sigma_\alpha$, but is not totally ordered?

[Reid Barton]

Exactly

[Reid Barton]

A corollary is that this sort of argument does not need choice, since you can also build the required W-type in ZF

[Reid Barton]

(I imagine choice is used in the rest of the proof of Borel determinacy, though.)

[David Wärn]

I guess you can also skip the indexing and the define the inductive type borel_level_family of $\Sigma_\alpha$ 's directly

[Reid Barton]

I guess I should be a little careful about saying you don't need choice because you might need it to get back to the exact definition of Borel set you started with.

[Reid Barton]

I'm not sure I follow what you are suggesting, could you elaborate?

[Reid Barton]

The way I think I know to do this is to define borel_rank first, and then define the proposition "has Borel rank $\alpha$" either by recursion on $\alpha$ (assuming you have a universe) or as an inductive family indexed on $\alpha$.

[Reid Barton]

Er, of course you don't need a universe to define a proposition, sorry (was thinking about a different context).

[Reid Barton]

If you define the proposition by recursion then I think you will need choice to prove that for any original Borel set, there exists a rank such that the set has that rank (compare https://gist.github.com/rwbarton/201fa67f590e2932808032343bfab9cc#file-colimit_closure-lean-L167)

[David Wärn]

I was thinking of something along these lines: say we want to do this strong induction on Borel subsets of $X$. Define an inductive prop is_borel_level_family : set X -> Prop, with introduction rules "the family of open subsets is a Borel level family", "a countable union of Borel level families is a Borel level family", and "the 'successor' of a Borel level family is a Borel level family", where the successor is obtained by countable unions and complements from the previous stage. Then the default induction principle for this Prop is hopefully what we need? And afterwards you should be able to prove that any Borel set is in some Borel level family

[Reid Barton]

Interesting

[Reid Barton]

You don't mean "a countable union of Borel level families", but rather "the family $B$ obtained from a countable set $B_i$ of Borel level families defined by $B = \{\bigcup V_i \mid V_1 \in B_1, V_2 \in B_2, ...\}$ is a Borel level family", I think.

[Reid Barton]

Oh whoops I should have read to the end of the sentence first--that's the successor case

[Reid Barton]

Or rather, it's both at once

[David Wärn]

Yes, it would be in the successor of the countable union

[David Wärn]

To be clear I haven't read Martin's proof so I'm not sure exactly what kind of induction it uses

[Reid Barton]

Well the way it's presented there is to prove some statement $P(\alpha)$ by strong induction on $\alpha < \omega_1$ where $P(\alpha)$ has the form "for all $X$ and all Borel subsets $Y$ of $X$ of Borel rank $\alpha$, ..."

[Reid Barton]

And you need for example that if $p : X' \to X$ is continuous and $Y \subset X$ has Borel rank $\alpha$ then so does $p^{-1}(Y) \subset X'$.

[Reid Barton]

But maybe that means you just need to adapt is_borel_level_family to have a type like is_borel_level_family : (\Pi X, set (set X)) -> Prop

[Reid Barton]

I think this also works. It's a bit mind-bending!

[Reid Barton]

First you do induction on the is_borel_level_family hypothesis to find out what your actual hypothesis is, and then you do induction on the proof of that hypothesis.

[David Wärn]

Oh, I didn't realise there were multiple $X$ s involved

[Reid Barton]

Yes, it's slightly frustrating to read the paper because it just says things like "a set $T$ of finite sequences" and then my brain asks "of what?"

[Reid Barton]

Of course the answer is "of sets", but in type theory I think it would be of a type that is different at different points of the argument

[Reid Barton]

And in particular, it is changing in applications of the inductive hypothesis.

[Reid Barton]

Now I am wondering whether it is possible to prove the fact about the closure under colimits from the gist I linked earlier without using choice.

[Reid Barton]

I'll try writing down these different approaches to Borel sets and see what happens.

[Reid Barton]

So far I have https://gist.github.com/rwbarton/f5846712370a0064b03dc9c2b44372bb
If I didn't mess anything up, all of these descriptions should be equivalent assuming choice; I'm not sure which ones are equivalent in the absence of choice. Actually, it now seems to me that many of them could be inequivalent. I somewhat arbitrarily wrote lemma statements saying that each is equivalent to the previous but that might not be the best organization.

[Reid Barton]

I tried to make all the descriptions as parallel as possible, to make the general form obvious. So the definition of level families is a bit different than the description you gave.

[Reid Barton]

Ah, maybe I should try to define being a level family and membership in the family simultaneously somehow... is that possible?

[Reid Barton]

My problem is: suppose I want to prove borel_ind s → ∃ r, borel_ranked_ind r s. Obviously I'm going to have to induct, and use the inductive hypothesis, but then I only get a statement like ∀ i, ∃ r, ... and I need choice to turn this into the r : ℕ → borel_rank to pass to borel_rank.union.

[Reid Barton]

The more I think about it, the more I think this implication is actually false without choice.

[Reid Barton]

That's okay as a practical matter (it's a lot easier to use choice this way than to encode things using ordinals), though.

[David Wärn]

This looks about right

[David Wärn]

Even if you used ordinals for indexing, wouldn't you still need choice to prove that $\omega_1$ has uncountable cofinality?

[Reid Barton]

Yes

[Reid Barton]

So in this approach the role of choice is more transparent, I think: to show that every Borel set has a rank.

[David Wärn]

The more I think about it the more I like this borel_rank approach! It's nice that it avoids universes and also that it just mirrors the definition of Borelness