von Neumann hierarchy: #26543 , #26518

Stream: PR reviews

[Kenny Lau]

I'm creating a new thread for the discussion of the following two PR's on von Neumann hierarchy:
* #17027 by @Violeta Hernández

• #26543 by @Violeta Hernández
• #26518 by @Knala Solomon

[Kenny Lau]

It's an unfortunate situation that Violeta took a hiatus for a few months, it isn't fair to anyone, I recognise this.

[Kenny Lau]

But unfortunately this is the case so you two might have to decide by rock paper scissors

[Kenny Lau]

As discussed separately, I personally prefer the name vonNeumann and notation V_ from the first PR, but also the definition using limitRecOn from the second PR

[Kenny Lau]

and also please include the API (4 lemmas now) directly after the definition, no matter which definition you two end up choosing.

[Kenny Lau]

I think all of the theorems proved in the two PR's are good, so I would keep all the theorems.

[Violeta Hernández]

As I mentioned in that PR, the exact definition of the hierarchy is pretty much irrelevant once you prove the characterizing result x ∈ V_ o ↔ rank x < o. My PR gets that done in 50-odd lines and everything below that just makes use of it; the other PR doesn't seem to contain that result.

[Violeta Hernández]

(Also hi! I'm back from my break.)

[Aaron Liu]

welcome back, I didn't know you went on break I though you just vanished

[Kenny Lau]

Violeta Hernández said:

As I mentioned in that PR, the exact definition of the hierarchy is pretty much irrelevant once you prove the characterizing result x ∈ V_ o ↔ rank x < o. My PR gets that done in 50-odd lines and everything below that just makes use of it; the other PR doesn't seem to contain that result.

I think I prefer limitRecOn because it is existing structure and you get API for free. Also note that it's equal amount of work to get to the 4 API lemmas I want in any case (and your PR doesn't have all 4 :slight_smile: ).

[Kenny Lau]

I don't think it's irrelevant beyond the point of x ∈ V_ o ↔ rank x < o

[Violeta Hernández]

Every single result in #26518 exists in my PR with the expection of rank_def, which to me seems somewhat superfluous. It's just saying that rank x = o ↔ rank x ≤ o ∧ ∀ a < o, ¬ rank x ≤ a.

[Violeta Hernández]

You get API for free using limitRecOn, sure, but now all your proofs have to have three cases that are broadly very similar. I'm trying to avoid that.

[Kenny Lau]

I'm saying that you can still get that by proving your definitional lemma as the 4th API.

[Violeta Hernández]

Sure, but then why use the limitRecOn definition if the plan is to just immediately move to the more workable one?

[Kenny Lau]

The 4 APIs I want are:

1. V_0 = empty
2. V_(succ o) = (V o).powerset
3. For limit o, V_o = Union { V_o' | o' < o }
4. For any o, V_o = Union { V_o'.powerset | o' < o } (Violeta gets this for free)

[Violeta Hernández]

(Note that I have all 4, I just have to prove the first 3 a bit later down the file)

[Kenny Lau]

hmm, you might have a point here

[Violeta Hernández]

I prove them at the very end in my PR, because I actually don't need them for anything else! But I could very well have placed them right after proving the characterization x ∈ V_ o ↔ rank x < o

[Violeta Hernández]

(In fact, my definition also gets 1 basically for free)

[Kenny Lau]

Would you also mind updating (merging master to) your PR because it seems like you already got the smaller PR's in?

[Kenny Lau]

it helps to decluster the file change page

[Violeta Hernández]

I'll try. I haven't quite figured out the way PRs are supposed to work now.

[Kenny Lau]

@Violeta Hernández
First, fork Mathlib to a local copy
image.png

1. Go to the main folder of mathlib
2. git remote -v
3. git remote add fork git@github.com:vihdzp/mathlib4.git
4. git remote -v
5. git checkout master
6. git pull
7. lake exe cache get
8. git checkout vi.vn_hierarchy
9. git merge master
10. Resolve the merge conflicts manually
11. git commit -am "resolve conflicts"
12. git push -u fork vi.vn_hierarchy (only this time, for the future you just do git push)

[Kenny Lau]

On further thought now I think your definition is better.

[Kenny Lau]

I look forward to seeing it after you merge master

[Violeta Hernández]

I think I'm not able to edit #17027 anymore. Am I doing something wrong, or do I need to create a new PR?

[Etienne Marion]

Probably you need to migrate it to a fork. See Mathlib4 wiki > Migration to PRs from forks.

[Kenny Lau]

@Violeta Hernández yes, you need to create a new PR, per above

[Violeta Hernández]

I've moved my old PR here: #26543

[Violeta Hernández]

Relating to the rank_def theorem. I could add it to my PR, but it'd just be this:

theorem rank_def {x : ZFSet} {o : Ordinal} : rank x = o ↔ x ⊆ V_ o ∧ ∀ o' < o, ¬ x ⊆ V_ o' := by
  simp_rw [subset_vonNeumann, not_le, forall_lt_iff_le, le_antisymm_iff]

I feel like we can probably do without this.

[Violeta Hernández]

You know, if I had a nickel for every time someone tried to do the von Neumann hierarchy while I already had a PR for it open, I'd have two nickels.

[Kenny Lau]

Violeta Hernández said:

You know, if I had a nickel for every time someone tried to do the von Neumann hierarchy while I already had a PR for it open, I'd have two nickels.

well that's what happens if you go hiatus :slight_smile:

[Kenny Lau]

Violeta Hernández said:

Relating to the rank_def theorem. I could add it to my PR, but it'd just be this:

theorem rank_def {x : ZFSet} {o : Ordinal} : rank x = o ↔ x ⊆ V_ o ∧ ∀ o' < o, ¬ x ⊆ V_ o' := by
  simp_rw [subset_vonNeumann, not_le, forall_lt_iff_le, le_antisymm_iff]

I feel like we can probably do without this.

I agree that might not be necessary.

[Kenny Lau]

@Violeta Hernández i've left some comments on your PR

[Notification Bot]

This topic was moved here from #PR reviews > #17027 , #26518 von Neumann hierarchy by Kenny Lau.

[Violeta Hernández]

I think I've addressed all your suggestions. If there's further golfing to be done I'm not finding it.

[Kenny Lau]

@Violeta Hernández :golf:

[Violeta Hernández]

Nice! Some of these are a bit more aggressive than what I'd usually do, but I'll take it

[Kenny Lau]

lol, you don't have to take anything i say, i'm not an official reviewer

[Violeta Hernández]

few lines equals more good

[Kenny Lau]

@Violeta Hernández variable stuff; you can accept multiple suggestions at once in the files changed page

[Violeta Hernández]

I'm of the opinion that if you have to constantly switch the explicitness of your variables then it sort of defeats the purpose of having the variables block to begin with

[Kenny Lau]

ok

[Kenny Lau]

but do you think it's good to specify .{u} for those variables?

[Violeta Hernández]

It future-proofs the file, so I'm fine with it

[Knala Solomon]

Violeta Hernández said:

You know, if I had a nickel for every time someone tried to do the von Neumann hierarchy while I already had a PR for it open, I'd have two nickels.

that's unfortunate. I just saw the todo and got excited because it felt like something i could take a stab at. I'm new here and didn't think to search existing PR's.

[Kenny Lau]

Knala Solomon said:

Violeta Hernández said:

You know, if I had a nickel for every time someone tried to do the von Neumann hierarchy while I already had a PR for it open, I'd have two nickels.

that's unfortunate. I just saw the todo and got excited because it felt like something i could take a stab at. I'm new here and didn't think to search existing PR's.

it happens, it’s unfortunate

[Kenny Lau]

but I hope you still had fun and learnt something in the process

[Kenny Lau]

and you can still pick other stuffs to pr!

[Knala Solomon]

Kenny Lau said:

but I hope you still had fun and learnt something in the process

yeah definitely

[Knala Solomon]

how do i close/cancel my pr?

[Knala Solomon]

nvm i see it

[Violeta Hernández]

If you want to PR something related to ZFC: Grothendieck universes! Now that we have the von Neumann hierarchy, we can state (and perhaps prove) that the Grothendieck universes are exactly the sets V_ x for x inaccessible.

[Dexin Zhang]

For Grothendieck universes I wrote a proof before that might be helpful, though the definition of ZFSet.card there is a bit complicated

[Violeta Hernández]

Isn't (V x).card just docs#Cardinal.preBeth ?

[Violeta Hernández]

(in fact, I added this definition precisely for this reason!)

[Violeta Hernández]

Relating to this, we're currently missing the fact that aleph x = beth x = x for x inaccessible. I'm pretty sure I sketched a proof of this not too long ago, search in Zulip and you should find it.

[Junyan Xu]

#maths > Cardinality of `ZFSet` @ 💬