Zulip Chat Archive

Stream: Is there code for X?

Topic: Borel determinacy


view this post on Zulip Kevin Buzzard (May 16 2020 at 08:55):

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?

view this post on Zulip Mario Carneiro (May 16 2020 at 09:12):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 09:13):

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

view this post on Zulip David Wärn (May 16 2020 at 09:27):

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."

view this post on Zulip Reid Barton (May 16 2020 at 10:00):

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.

view this post on Zulip Reid Barton (May 16 2020 at 10:03):

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.

view this post on Zulip Reid Barton (May 16 2020 at 10:31):

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.

view this post on Zulip David Wärn (May 16 2020 at 10:36):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:36):

Exactly

view this post on Zulip Reid Barton (May 16 2020 at 10:37):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:38):

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

view this post on Zulip David Wärn (May 16 2020 at 10:39):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:41):

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.

view this post on Zulip Reid Barton (May 16 2020 at 10:42):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:45):

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.

view this post on Zulip Reid Barton (May 16 2020 at 10:47):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:50):

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)

view this post on Zulip David Wärn (May 16 2020 at 10:50):

I was thinking of something along these lines: say we want to do this strong induction on Borel subsets of XX. 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

view this post on Zulip Reid Barton (May 16 2020 at 10:50):

Interesting

view this post on Zulip Reid Barton (May 16 2020 at 10:53):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:53):

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

view this post on Zulip Reid Barton (May 16 2020 at 10:55):

Or rather, it's both at once

view this post on Zulip David Wärn (May 16 2020 at 10:58):

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

view this post on Zulip David Wärn (May 16 2020 at 10:59):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:02):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:04):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:06):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:12):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:13):

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.

view this post on Zulip David Wärn (May 16 2020 at 11:13):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:14):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:15):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:16):

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

view this post on Zulip Reid Barton (May 16 2020 at 11:20):

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.

view this post on Zulip Reid Barton (May 16 2020 at 11:21):

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

view this post on Zulip Reid Barton (May 16 2020 at 12:05):

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.

view this post on Zulip Reid Barton (May 16 2020 at 12:08):

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.

view this post on Zulip Reid Barton (May 16 2020 at 12:11):

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

view this post on Zulip Reid Barton (May 16 2020 at 12:16):

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.

view this post on Zulip Reid Barton (May 16 2020 at 12:35):

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

view this post on Zulip Reid Barton (May 16 2020 at 12:36):

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

view this post on Zulip David Wärn (May 16 2020 at 13:33):

This looks about right

view this post on Zulip David Wärn (May 16 2020 at 13:34):

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

view this post on Zulip Reid Barton (May 16 2020 at 13:40):

Yes

view this post on Zulip Reid Barton (May 16 2020 at 13:41):

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

view this post on Zulip David Wärn (May 16 2020 at 14:01):

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


Last updated: May 17 2021 at 15:13 UTC