ordinals and induction

Stream: Is there code for X?

[Sebastien Gouezel]

I would like to make an induction over ordinals less than a given ordinal o (say, o = cardinal.ord (aleph 1 : cardinal.{u})). I can do an induction over all ordinals in ordinal.{u}, but this brings me to universe u+1, which is problematic for me. Instead of this, it would be more convenient to have a representative of o as a type in Type u, with a well-order, but I can't find an API around this. @Mario Carneiro , do you have thoughts about a nice way to do this with current mathlib?

[Floris van Doorn]

If o : ordinal, you can use o.out.α for a representative (using docs#quotient_out), and there are a bunch of lemmas about this, like docs#ordinal.type_out.

[Sebastien Gouezel]

Yes, but as far as I can tell there is no order relation instantiated by default on o.out.α. Maybe it's just a matter of registering them, but since they're not there I was wondering if I was missing another way.

[Floris van Doorn]

Oh, I see. Yeah, most of the ordinal library works with an explicitly given order r, instead of <.

[Sebastien Gouezel]

Maybe it's just a matter of registering a few instances such as

instance (o : ordinal.{u}) : has_lt (o.out.α) := ⟨o.out.r⟩
instance (o : ordinal.{u}) : has_well_founded o.out.α := ⟨has_lt.lt, o.out.wo.wf⟩

(probably building a linear order).

[Floris van Doorn]

What do you want to do with it that you cannot use r directly?

[Sebastien Gouezel]

Maybe it's an #xy problem. I want to show that the cardinality of the sigma-algebra generated by something is controlled in terms of the cardinality of the something. The standard proof is to construct the sets in thz sigma-algebra by transfinite induction, show that it stabilizes at omega_1, and obtain inductively the cardinality controls. The inductive construction would be something like

instance (o : ordinal.{u}) : has_lt (o.out.α) := ⟨o.out.r⟩
instance (o : ordinal.{u}) : has_well_founded o.out.α := ⟨has_lt.lt, o.out.wo.wf⟩
theorem wf (o : ordinal.{u}): @well_founded o.out.α (<) := o.out.wo.wf
theorem ordinal.out_induction {o : ordinal.{u}} {p : o.out.α → Prop} (i : o.out.α)
  (h : ∀ j, (∀ k, k < j → p k) → p j) : p i :=
o.out.wo.wf.induction i h

def induction_generate_from (s : set (set α)) :
  (cardinal.ord (aleph 1 : cardinal.{u})).out.α → set (set α)
| i := s ∪ {∅} ∪ (λ (t : set α), tᶜ) '' (⋃ j : {j // j < i}, induction_generate_from j.1)
      ∪ (set.range (λ (f : ℕ → (⋃ j : {j // j < i}, induction_generate_from j.1)), (⋃ n, (f n).1)))
using_well_founded {dec_tac := `[exact j.2]}

This seems to work fine, but maybe there's a more idiomatic way.

[Reid Barton]

What I did for the small object argument is work as long as possible with a well_order_top, defined here as

class well_order_top (α : Type u) extends complete_linear_order α :=
(wf_lt : well_founded ((<) : α → α → Prop))

but then eventually you have to get your hands on one somehow, which I did here in basically the same way you have written above.

[Reid Barton]

For your cardinality argument of course there is no point in having the flexibility to choose a well-ordered type other than o.out in the cardinality estimate.

[Violeta Hernández]

There's a bunch of API that allows you to go back and forth between ordinals and a representative with the order type of a specific ordinal

[Violeta Hernández]

typein and enum will help you here

[Violeta Hernández]

I'm personally opposed to making < a synonym for o.out.r since that would muddle this distinction, I believe.

[Violeta Hernández]

Oh and also, o.out.wo will give you the proof that o.out.r is a well order in o.out.\a

[Gabriel Ebner]

Yeah, having two different names for the same relation is not ideal. But I'd rather avoid the o.out.r then, and use < instead everywhere.

[Sebastien Gouezel]

I have tried to go following your advice of not making < a synonym for o.out.r. I was afraid it would be very heavy to use, but in fact with a few notations it is completely reasonable. You can have a look at #12422 to check that I am using the library in the way it was intended.

[Violeta Hernández]

Actually, I've thought about this for a bit, and particularly after seeing your code, I can definitely see the merit in the < relation being a thing

[Violeta Hernández]

I may have forgotten than < was quite overloaded as is

[Violeta Hernández]

(by design)

[Violeta Hernández]

Since it seems like other people here agree with the usefulness of this, I'll start to work on this in a few hours

[Fabian Glöckle]

In my first transfinite induction in lean I wrote some lemmas like

lemma lt_of_lt_of_le_unbundled {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] {a b c : α} (hab : r a b) (hbc : ¬r c b) :r a c

Is there an easier way? Otherwise I'd also plead for < instead of r

[Yaël Dillies]

I'm not sure what you mean. Are you trying to avoid ≤ and <? If not, then you can use docs#has_le.le.lt_of_not_le.

[Fabian Glöckle]

My point is precisely that: I don't know if it possible to access the lemma you cited without making the < = r synonym

[Yaël Dillies]

And do you actually need to avoid using ≤ and <?

[Yaël Dillies]

is_strict_order is barely ever used.

[Fabian Glöckle]

No, but in the status quo, as discussed above, there is only o.out.r

[Fabian Glöckle]

I was only supporting the proposal of introducing this has_lt

[Violeta Hernández]

Then you're in luck! Check out #12468.

[Pedro Sánchez Terraf]

I'm trying to generalize this definition
Sebastien Gouezel said:

def induction_generate_from (s : set (set α)) :
  (cardinal.ord (aleph 1 : cardinal.{u})).out.α → set (set α)
| i := s ∪ {∅} ∪ (λ (t : set α), tᶜ) '' (⋃ j : {j // j < i}, induction_generate_from j.1)
      ∪ (set.range (λ (f : ℕ → (⋃ j : {j // j < i}, induction_generate_from j.1)), (⋃ n, (f n).1)))
using_well_founded {dec_tac := `[exact j.2]}

in order to define the Borel hierarchy. I have noted that the union now ranges over the interval Iio i (which is exactly the same set as above). But I felt that it looked prettier to write the union above like ⋃ j (hij: j < i), induction_generate_from j. It seems that the proofs go through with this alternative formulation.

Is there any benefit of using the intervals here?

[Pedro Sánchez Terraf]

By the way, my first attempt to formalize the definition of $\Sigma^0_i$ and $\Pi^0_i$ goes by defining the pair of both families, and then obtaining each pointset by using fst and snd. Is this the simplest approach?
At least I couldn't find references to definitions by nested (“double”) recursion over an ordinal (or its .out, as in the previous discussion).

[Kevin Buzzard]

LaTeX: use double dollars $$ not single dollars (don't ask me why). Definitions: yes I would definitely define the pair. An attempt to do some kind of mutual inductive definition will just get translated internally into the pair definition, and mutual inductives are generally avoided in Lean 3.

[Junyan Xu]

@Pedro Sánchez Terraf I'd recommend that you use an inductive definition like how src#measurable_space.generate_measurable is done:

import set_theory.cardinal.ordinal
universe u
variable {α : Type*}
open cardinal

inductive generate_from (s : set (set α)) : ordinal.{u} → set α → Prop
| basic : ∀ o (u ∈ s), generate_from o u
| empty : ∀ o, generate_from o ∅
| compl : ∀ o u (o' < o), generate_from o' u → generate_from o uᶜ
| union : ∀ o (f : ℕ → set α) (o' : ℕ → ordinal.{u}), (∀ n, o' n < o) → (∀ n, generate_from (o' n) (f n)) → generate_from o (⋃ i, f i)
/- The following version doesn't work:
| union : ∀ o (f : ℕ → set α), (∀ n, ∃ o' < o, generate_from o' (f n)) → generate_from o (⋃ i, f i)
inductive type being declared can only be nested inside the parameters of other inductive types -/

[Pedro Sánchez Terraf]

@Junyan Xu Thanks. My particular definition, as generate_measurable_rec, gets stuck at $\omega_1$, but then again I'm curious if there is any particular benefit of the approach taken in card_measurable_space.

[Pedro Sánchez Terraf]

But most importantly, I do not know how to write standard ordinal recursions that use the $0$, successor, and limit cases.

[Junyan Xu]

There is docs#ordinal.limit_rec_on

[Pedro Sánchez Terraf]

I'll experiment a bit and bring some prototype back. Thanks a lot

[Junyan Xu]

I think we should avoid ordinal.out.α when possible. It seems @Sebastien Gouezel uses it because he wants to have something in Type u rather than ordinal.{u} which is in Type (u+1). But I don't quite see why he needs that in the proof. It seems the only crucial fact is that a N-indexed sequence in omega_1 has an upper bound in omega_1, or in other words, omega is not cofinal with omega_1. I don't see how the universe is crucial here. (Update: another crucial fact is that the unions are taken over an initial segment of omega_1, but those also all have cardinality bounded by aleph_0.)

Notice that my definition doesn't use well-foundedness of the ordinals, and I think that will be used when you prove (by induction) that it works as expected (e.g. that generate_from s o consists of exactly those sets obtained from generate_from s o' for o' < o).

[Sebastien Gouezel]

My definition above is just because I could work out the proof with it :-). If you find another more idiomatic way in terms of an inductive definition, this would probably be better. The reason I used (aleph 1 : cardinal.{u})).out.α is because I wanted a well-order of size aleph_1, i.e., I didn't want to do the induction over all ordinals just because we know we can stop at aleph_1 and this will already give all measurable sets. And also for universe reasons: at the end of the day if everything is in universe u you want bounds in terms of cardinals in the same universe, not the next one (although it would probably be possible to downlift things from a higher universe).

[Pedro Sánchez Terraf]

Sebastien Gouezel said:

at the end of the day if everything is in universe u you want bounds in terms of cardinals in the same universe, not the next one (although it would probably be possible to downlift things from a higher universe).

Indeed, the $\aleph_1$ of the very first universe should suffice foundationally speaking (but I took the trouble to try that and check that it fails with the proofs as they stand). Thanks!

[Junyan Xu]

Indeed I think even though you can show countable {o' // o < o} you would still get a cardinal.{u+1} by default; you can do computation in universe u+1 but need to downlift it using docs#cardinal.lift_le in the end. However, we certainly want the Borel hierarchy be indexed by ordinals (≤ omega_1) rather than omega_1.out.α; once we have the Borel hierarchy and prove that it stabilizes, we may go back to refactor and hopefully golf the cardinality proof.

[Violeta Hernández]

Junyan Xu said:

I think we should avoid ordinal.out.α when possible.

You mean in public-facing API? I can see your point if so, but otherwise hard disagree. The fact that each ordinal.{u} corresponds to a well-ordered type in Type u is a crucial fact. Most notably, we can take indexed suprema of ordinal.{u} when the indexing type is in universe u, but not when it's any larger. By bumping up the universes, it means that we have to move back and forth between the Iio x ≅o x.out.α order isomorphism, which is not ideal and really defeats the purpose.

Maybe part of why it seems so unnatural is due to the odd notation. This could be easily fixed by introducing something like

def ordinal.to_type (o : ordinal.{u}) : Type u := o.out.α

We can then add a doc comment explaining how this represents a canonical type with the given order type.

[Violeta Hernández]

Regarding the public API, I'm reminded that we already have a way around this issue. Instead of using the ordinal supremum, one can use docs#ordinal.bsup. If we want to do even more general stuff, like index a family of sets by ordinals, we can use docs#ordinal.family_of_bfamily and docs#ordinal.bfamily_of_family to easily convert between the out.α indexing and the natural indexing.

I'm not a huge fan of this because it introduces a lot of redundancy into the API (where many theorems have to be stated in terms of either supremum), but that's the best we currently got. Besides, we already get by with this sort of redundancy elsewhere (see all the kinds of set unions in mathlib).

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Thinking about it further. Maybe both introducing ordinal.to_type and making better use of the ordinal.bsup API are good ideas.

[Violeta Hernández]

(Sorry to anyone reading in real time for all the edits, I guess I'm only now really solidifying my ideas here)

[Junyan Xu]

I have no objection to using x.out.α in proofs if it makes things shorter; your golf in #17972 looks great to me. However, in this case we want to define a function with all ordinals as its domain; it would be unnatural to define the hierarchy on ω₁.out.α since you would need to transfer by Iio ω₁ ≅o ω₁.out.α if you want to refer to e.g. the 1st level, or the ωth level in the hierarchy. In particular, we want ⋃ j < i in the statement rather than ⋃ j : i.out.α. Even if you can get away with ω₁.out.α here because the Borel hierarchy stabilizes at ω₁, it wouldn't be possible to do so when defining but IMO that's unnatural; what if we want to define derived sets (which stablizes eventually but at arbitrarily large ordinal), docs#cardinal.aleph, or the von Neumann hierarchy (which doesn't stabilize).

[Pedro Sánchez Terraf]

Violeta Hernández said:

Maybe part of why it seems so unnatural is due to the odd notation. This could be easily fixed by introducing something like

def ordinal.to_type (o : ordinal.{u}) : Type u := o.out.α

Thanks for the comments. Actually notation here is not much of a problem, but I believe that conceptually being able to use ordinals as such parallels set-theoretical practice more faithfully.

My first impression was that the universe problems could not be sidestepped, but it was a nice surprise that mathlib had enough resources to make it work.

[Violeta Hernández]

Junyan Xu said:

Even if you can get away with ω₁.out.α here because the Borel hierarchy stabilizes at ω₁, it wouldn't be possible to do so when defining but IMO that's unnatural; what if we want to define derived sets (which stablizes eventually but at arbitrarily large ordinal), docs#cardinal.aleph, or the von Neumann hierarchy (which doesn't stabilize).

Well, in cases where we do want to talk about all ordinals, we wouldn't even have the option of talking about a type in Type u.

[Violeta Hernández]

I think there's a general feeling that universes are some sort of Lean quirk, but they're just as relevant in mainstream mathematics. The difference is that instead of talking about universe u vs. universe u+1, we talk about sets vs. classes.

[Violeta Hernández]

Anyways. I've let this broil in my mind for a while. I am now entirely on board with defining the Borel hierarchy in terms of ordinals, accepting of course that switching between ordinals and ω₁.out.α will probably be required in a few proofs. If any trouble arises out of this, I'm more than happy to review the admittedly small and specific API for family_of_bfamily and bfamily_of_family.

[Pedro Sánchez Terraf]

Violeta Hernández said:

I think there's a general feeling that universes are some sort of Lean quirk, but they're just as relevant in mainstream mathematics. The difference is that instead of talking about universe u vs. universe u+1, we talk about sets vs. classes.

If I understand correctly, and with the focus on ordinals, it is a quirk of their particular construction in mathlib (perhaps the only standard one in type theory). In ZFC foundations, as you probably know, ordinals live in the (only) “base” universe, they are just sets. Indeed they are representatives :face_palm: but much more canonical. They are not defined as a equivalence classes, so you do not need u+1 to have them.

[Violeta Hernández]

Lean ordinals aren't types, so it doesn't make that much sense to talk about the universe they live in. However, both in Lean and in ZFC, the collection of all ordinals is a class / lives in a higher universe. So talking about intervals of this collection is a subtle matter in both cases.

[Pedro Sánchez Terraf]

Violeta Hernández said:

So talking about intervals of this collection is a subtle matter in both cases.

Actually, in ZFC, bounded intervals are just sets, which are the ones that mostly appear in practice.

[Anne Baanen]

Probably not directly relevant to this thread but you might also be interested in this new paper on ordinals in constructive set theory vs ordinals in homotopy type theory: https://arxiv.org/abs/2301.10696

[Pedro Sánchez Terraf]

@Anne Baanen Thanks, I already took a quick look. But I'm usually interested in classical ordinals.

[Anne Baanen]

I definitely suspected that :grinning_face_with_smiling_eyes: