von Neumann hierarchy

Stream: mathlib4

[Violeta Hernández]

Is there anyone currently interested in implementing the von Neumann hierarchy and ordinals for ZFSet?

[Violeta Hernández]

I remember there was someone back in 2022 who ended up treading over a lot of my own theorems... but none of this ever made its way to Mathlib 3, let alone Mathlib 4

[Violeta Hernández]

I'm currently trying to port it and further develop it

[Violeta Hernández]

I've opened #15793 as a small, initial port of the 2022 file

[Antoine Chambert-Loir]

That's interesting! Do you know what people did in Agda/HoTT?

https://www.cs.bham.ac.uk/~mhe/TypeTopology/Iterative.Ordinals.html

[Antoine Chambert-Loir]

https://doi.org/10.1017/jsl.2017.84

[Violeta Hernández]

That looks interesting, but I'm not really familiar with other theorem provers

[Dexin Zhang]

Hi! I've been working on formalizing von Neumann universes recent days in my personal project. My hope is to prove Vκ (where κ is an inaccessible cardinal) are exactly the models of second order ZF, and I've proved one direction (here is what I have done).

Although I'd never contributed to lean community before, I'm definitely interested in implementing them in Mathlib.

[Violeta Hernández]

That looks pretty interesting. A lot of the theorems in there should probably exist in Mathlib in some form

[Violeta Hernández]

btw @Dexin Zhang your definition of rank is wrong

[Violeta Hernández]

it should be the supremum of the successors of the ranks of previous elements, instead of the other way around

[Violeta Hernández]

We have docs#WellFounded.rank, though the API is quite underdeveloped

[Joachim Breitner]

That’s a generalization of the order-theoretic height, is it? I have a PR extending that definition’s API in https://github.com/leanprover-community/mathlib4/pull/15524, JFTR. Probably worth at least to cross-link the definitions in the docstrings.

[Violeta Hernández]

I'm not sure if I'd call it a generalization, since it's only defined in the case of a well-founded order. But yes, it's a similar idea

[Yaël Dillies]

Joachim Breitner said:

That’s a generalization of the order-theoretic height, is it?

It feels a bit orthogonal rather than a generalisation since it does have a bigger return type, but it also requires a well-founded order to make sense

[Joachim Breitner]

Fair enough. I guess it’s only a generalization in the sense that “where both exist, one can obtain the height from the rank”.

[Dexin Zhang]

Violeta Hernández said:

btw Dexin Zhang your definition of rank is wrong

Thank you for telling me! I haven't realized my definition is wrong :exhausted:

[Dexin Zhang]

Violeta Hernández said:

We have docs#WellFounded.rank, though the API is quite underdeveloped

The universe level makes it quite subtle. The existing docs#WellFounded.rank produces Ordinal.{u} for α: Type u, but ZFSet.{u} lives in Type (u+1)

ZFSet.mem_wf.rank will produce ZFSet.{u} → Ordinal.{u+1}, but I prefer ZFSet.{u} → Ordinal.{u} so that universe levels coincide

[Violeta Hernández]

We actually have this situation elsewhere in the library. The docs#SetTheory.PGame.birthday of a game is the direct analog of the rank of a set. Instead of defining it as the least ordinal larger than the ranks of member sets, you define it as the least ordinal larger than the birthdays of option games for either player. The recursive definition ensures the correct universe.

[Violeta Hernández]

PGame is to Game like PSet is to ZFSet.

[Violeta Hernández]

I have an open PR defining birthdays in Game, as the least birthday of any PGame that quotients to it.

[Violeta Hernández]

All of this design could be copied nearly verbatim into a SetTheory/ZFC/Rank.lean file

[Violeta Hernández]

In both cases, we could show the equality rank x = lift (Ordinal.rank x)

[Violeta Hernández]

The theorem x ∈ neummann o ↔ rank x < o could be a separate thing we then do to link both files togeteher

[Dexin Zhang]

Got it! I think the case in ZFSet is much simpler than Game, since we can prove PSet.rank respects PSet.Equiv and use Quotient.lift

[Dexin Zhang]

Shall I open a PR for that Rank.lean?

[Violeta Hernández]

Sure thing! I'll be glad to review it

[Violeta Hernández]

Any progress on this?

[Dexin Zhang]

Violeta Hernández said:

Any progress on this?

No, I'm still waiting for github permission

Maybe I should make a fork and work on it first

[Violeta Hernández]

That would be nice. I guess I could always PR it myself

[Dexin Zhang]

@Violeta Hernández I opened #15977 for the Rank.lean