Stream: Is there code for X?
Topic: Borel determinacy
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?
Mario Carneiro (May 16 2020 at 09:12):
I expect so, although it's hard to say without details of the proof
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
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."
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.
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
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.
David Wärn (May 16 2020 at 10:36):
borel_rank plays the role of countable ordinals, to index what Martin calls , but is not totally ordered?
Reid Barton (May 16 2020 at 10:36):
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
Reid Barton (May 16 2020 at 10:38):
(I imagine choice is used in the rest of the proof of Borel determinacy, though.)
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 's directly
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.
Reid Barton (May 16 2020 at 10:42):
I'm not sure I follow what you are suggesting, could you elaborate?
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 " either by recursion on (assuming you have a universe) or as an inductive family indexed on .
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).
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)
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 . 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 (May 16 2020 at 10:50):
Reid Barton (May 16 2020 at 10:53):
You don't mean "a countable union of Borel level families", but rather "the family obtained from a countable set of Borel level families defined by is a Borel level family", I think.
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
Reid Barton (May 16 2020 at 10:55):
Or rather, it's both at once
David Wärn (May 16 2020 at 10:58):
Yes, it would be in the successor of the countable union
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
Reid Barton (May 16 2020 at 11:02):
Well the way it's presented there is to prove some statement by strong induction on where has the form "for all and all Borel subsets of of Borel rank , ..."
Reid Barton (May 16 2020 at 11:04):
And you need for example that if is continuous and has Borel rank then so does .
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
Reid Barton (May 16 2020 at 11:12):
I think this also works. It's a bit mind-bending!
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.
David Wärn (May 16 2020 at 11:13):
Oh, I didn't realise there were multiple s involved
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 of finite sequences" and then my brain asks "of what?"
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
Reid Barton (May 16 2020 at 11:16):
And in particular, it is changing in applications of the inductive hypothesis.
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.
Reid Barton (May 16 2020 at 11:21):
I'll try writing down these different approaches to Borel sets and see what happens.
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.
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.
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?
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
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.
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.
David Wärn (May 16 2020 at 13:33):
This looks about right
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 has uncountable cofinality?
Reid Barton (May 16 2020 at 13:40):
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.
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