Discussions "Borel determinacy"

Stream: general

[Sven Manthe]

This is the discussion thread for my formalization of Borel determinacy (https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean, announcement see https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Borel.20determinacy). In particular, at some point I will probably ask some questions here about whether/how to put this into mathlib. Apart from the definition of Gale-Stewart games and the main proof (which does not seem to be too reusable), the project also contains some API on "trees" in the sense of descriptive set theory, subsets of List A that are stable under taking prefixes, and a bit of category theory (for example, the computation of filtered colimits along isomorphisms).

[Michael Rothgang]

Do you think any of the tactics you wrote would be useful more broadly? (I haven't carefully looked at what they do.)

[Sven Manthe]

Michael Rothgang said:

Do you think any of the tactics you wrote would be useful more broadly? (I haven't carefully looked at what they do.)

Let's distinguish cases. casesPlayers, which just does cases on all variables of a fixed type in context, is easy, but maybe also convenient to have in mathlib. synthIsPosition and synthIsFixing are domain-specific.
simpAtStar just works around a missing configuration option for simp: simp at * won't simplify hypotheses that are dependencies of other hypothesis, which is annoying for tactic sequences like simp at *; omega. This is discussed at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/simp.20at.20*.20with.20hypotheses.20occurring.20in.20the.20goal, https://github.com/leanprover/lean4/issues/5593 and I would argue that my simpAtStar should be added as an option to simp.
The last remaining metaprogram is abstract, which moves a proof into an auxilary lemma. This is for performance reasons: Many tactics, like simp, rw or even sorry, will consider large proof terms generated by tactics that are called ad hoc (e.g., f x (by omega)). There is a current workaround that after a def is finished, abstractNestedProofs is called to do something similar to my abstract on propositional subterms. However, this is only done with the value, not with type of the definition, and it is also only done after the definition is evaluated completely, possibly slowing down later parts of this evaluation. I would argue that such a procedure should be applied eagerly as soon as a propositional subterm appears either in the type or the value of a definition (this should also fix https://github.com/leanprover/lean4/issues/5108, and there is discussion in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/count_heartbeats.20CPU.20usage). My current abstract, however, only suffices to avoid the worst performance impacts and is not even able to handle universe metavariables, so that doing this would be some work that I probably won't do. Also note that the performance impact in my project is much larger because I didn't follow the mathlib convention to use junk values instead of propositional arguments (i.e., replace f x (h : p) for p : Prop by if h : p then f x h else default), and mathlib uses propositional arguments only at a few spots (e.g., List.getElem), where the performance impact due to unnecessary unfolding of proof terms isn't that significant yet.

[Bjørn Kjos-Hanssen]

API on "trees" in the sense of descriptive set theory would be nice to have in Mathlib.

[Felix Weilacher]

Tagging @Patrick Lutz who was interested in this

[Sven Manthe]

Bjørn Kjos-Hanssen ☀️ said:

API on "trees" in the sense of descriptive set theory would be nice to have in Mathlib.

There currently is something in the file "PiNat", but it codes basic opens by pairs of sequences and natural numbers, while I'm using lists. My choice seemed more convenient (one does not have to choose extensions of lists to sequences, thus needs no separate handling of the empty set, and there is already a good API on lists), but does only work for powers, not arbitrary products. Maybe both approaches could coexist in Mathlib.

[Yaël Dillies]

Does this have anything to do with docs#CantorScheme ?

[Sven Manthe]

Yaël Dillies said:

Does this have anything to do with docs#CantorScheme ?

Yes, this is one of the files that currently use PiNat. (And the result on embedding Cantor sets into Borel subsets of Polish spaces can also be deduced from determinacy.)

[Felix Weilacher]

There is docs#PiNat.res which allows one to use Lists in a very limited way. Having a more well-developed API would be great.

[Felix Weilacher]

In #maths > borel sigma-algebra & quotient topology , we have discussed formalizing the result that Analytic sets are Lebesgue measurable, Baire measurable, etc.

These can also be deduced from Borel (just closed) determinacy. I wonder if it would be better to formalize these deductions than to give the direct proofs.

[Sven Manthe]

Let's consider Baire category (measure should be analogous). I'm indeed inclined to think that it would be best to formalize the (unraveled) Banach-Mazur game to deduce the Baire property. On the one hand, this is also the proof Kechris uses if I remember correctly, and on the other hand this gives the corresponding results under, e.g., projective determinacy. However, currently mathlib does not even seem to know what analytic or projective sets are unless I missed something (these words have too many definitions in different areas...)

[Felix Weilacher]

Kechris gives several proofs of analytic Lebesgue/Baire measurability, but I agree that it would be good to have a proof method which goes up through the projective hierarchy fairly seamlessly

[Felix Weilacher]

MeasureTheory.AnalyticSet

[Felix Weilacher]

^Analytic is defined but nothing further.

[Violeta Hernández]

Maybe not a huge deal, but the repo currently doesn't build in Reservoir: https://reservoir.lean-lang.org/@sven-manthe/borel_det

[Sven Manthe]

Thanks for the hint, hopefully fixed (lake build failed also locally since the main file was in the wrong place; I didn't realize this before using only VS Code)

[Sven Manthe]

For those interested into getting (parts of) this into mathlib: It would be helpful if some of my PRs get reviewed (e.g., https://github.com/leanprover-community/mathlib4/pull/18458 is open for more than a week and required for my definition of trees and thus of games)

[Yaël Dillies]

I am handicapped from a crisis of RSI, so I won't suggest you ask for my review, but in usual times please ask for my review

[Ruben Van de Velde]

Anyone can do that, by the way. It's a lot easier for reviewers and maintainers if anyone (especially someone familiar with the mathematics or working on related things) has given the PR a first review pass

[Sven Manthe]

I wanted to ask whether there are people with a strong interest of getting Borel determinacy into mathlib (lately, reviewing times are rather long, see https://github.com/leanprover-community/mathlib4/pull/18763, https://github.com/leanprover-community/mathlib4/pull/19546). To be fair, I don't think that there are many interesting intermediate results in my project, but the main result should definitely be appropriate. I'm not sure at the moment whether I'll continue trying to get it into mathlib.

[David Michael Roberts]

Paper is out: https://arxiv.org/abs/2502.03432 ^_^

[David Michael Roberts]

@Sven Manthe I was curious to know what you meant by the sentence:

It also demonstrates that using consistency-wise strong fragments of ZFC does not pose an obstruction to formalizing in itself.

Is this because of the usual claim that (instances of) Replacement are needed for Borel Determinacy? I do know that having the existence of P^alpha(|N)—for alpha a countable ordinal—is enough on top of (roughly) Zermelo set theory as a base theory.

From skimming the paper, I was wondering if your statement

Furthermore, we replace the use of transfinite induction to show unravelability by a direct induction on the construction of Borel sets. This requires a strengthening of unravelability, which we term “universal unravelability”

amounts to the use of induction along countable ordinals as mentioned, in Martin's proof.

[David Michael Roberts]

Oh, I see you said more or less what I asked, at the end of section 3.2. I was searching for the wrong terms so didn't see that.

Also, I would gently push back on the claim

Thus, Borel determinacy, which is famous for requiring a much larger fragment of ZFC than most usual theorems [citing Friedman 1971] ... [emphasis added]

It's not a much larger fragment, the single axiom that "all beths exist" is very mild and more than suffices (one might instead ask that arbitrarily-iterated power sets exist). And asking that merely countable-ordinal-iterated powersets exist is likewise weaker again.

It took me years to understand that experts know, but don't really say, that what BD needs to a lot weaker than what is usually said in print (including when citing Friedman's famous result), and eventually we get this: https://golem.ph.utexas.edu/category/2021/07/borel_determinacy_does_not_require_replacement.html

[Sven Manthe]

David Michael Roberts said:

amounts to the use of induction along countable ordinals as mentioned, in Martin's proof.

Exactly - I replace this by showing that the universally unravelable sets form a σ-algebra, which I called "direct induction" here

[Sven Manthe]

David Michael Roberts said:

It's not a much larger fragment, the single axiom that "all beths exist" is very mild and more than suffices (one might instead ask that arbitrarily-iterated power sets exist). And asking that merely countable-ordinal-iterated powersets exist is likewise weaker again.

I agree that the word "much" here is very dependent on the perspective. My intention was more along the lines of: "most usual theorems" are even provable in fragments of higher order arithmetic, which do not suffice to even talk about infinite beth numbers literally. (I'm aware of Leinster's article.)

[David Michael Roberts]

OK, thanks for clarifying the baseline: HOA, not, eg ETCS. I was making an assumption about that.

[David Michael Roberts]

BTW, I'm very happy this has been done (I didn't see the announcement of the formalisation earlier, just learned it from the arXiv posting).