Cardinality of `ZFSet`

Stream: maths

[Daniel Weber]

What is Lean capable of proving regarding the cardinality of docs#ZFSet, compared to the cardinality of e.g. Type?

[Daniel Weber]

As an extreme example, is this axiom inconsistent?

import Mathlib

axiom ZF_small.{u} : Small.{0} ZFSet.{u}

[Floris van Doorn]

No. There should be a well-defined cardinality function ZFSet.{u} -> Cardinal.{u}, and this function should be surjective.

[Floris van Doorn]

There are some other threads on Zulip about the cardinality of Type. IIRC we have #Cardinal.{u} \le #Type u < Cardinal.{u+1}, but whether the \le is equality is independent of Lean.

[Daniel Weber]

Floris van Doorn said:

No. There should be a well-defined cardinality function ZFSet.{u} -> Cardinal.{u}, and this function should be surjective.

That's what I thought, but I didn't manage to prove it — how does the proof work?

[Floris van Doorn]

I think the following works:
construct the ordinals O = { s : ZFSet.{u} | s.IsOrdinal } in ZFSet and the canonical map f : O -> Ordinal.{u} (I think this is doable, right?). Suppose that c : Ordinal.{u} is the least ordinal not in the range of f, take a well-order C : Type u with order type c. Then define a new ZFSet indexed by C which sends x : C to the corresponding ordinal in ZFSet (something like invFun f (typein _ x)). This can be done with PSet.mk + choice, but maybe there is some better API for that (i.e. a "comprehension" function (α : Type u) → (α → ZFSet.{u}) → ZFSet.{u}).

[Floris van Doorn]

Oh, the last step is docs#ZFSet.range.

[Mario Carneiro]

You should be able to prove that the cardinality of ZFSet.{u} is the same as the cardinality of Cardinal.{u} and Ordinal.{u}, which I think has a name like docs#Cardinal.univ

[Mario Carneiro]

(This is unlike the situation for Type u, which you cannot prove is the same cardinality as those three types because Type u is not a quotient, e.g. there could be a very large number of empty types in it and the axioms don't rule this possibility out.)

[Mario Carneiro]

The way I would go about proving this is by setting up a bijection between the levels $V_\alpha$ of the cumulative hierarchy and the beth function, and then proving that $\aleph_\kappa=\beth_\kappa=\kappa$ when $\kappa$ is an inaccessible cardinal

[Junyan Xu]

von Neumann hierarchy is #17027 but apparently nothing about cardinality yet ...

[Nir Paz]

Basically the same proof as Mario's but might be easier to implement (for the ZFSet.{u} ≤ Ordinal.{u} direction):

Define a well order on ZFSet.{u} by extending a well order on V_k to V_(k+1) at every step. Then every prefix is a well order on a ZFSet.{u} and is then Small.{u}, so the supremum of the sizes of the prefixes, which is the size of ZFSet.{u}, is univ.{u}.

[Nir Paz]

This only uses that the Von Neumann hierarchy covers all sets.

[Junyan Xu]

I can't believe I just finished a proof! I got the idea of using WType early, but it took me a few hours to convince myself Cardinal.IsInaccessible.pow_le_of_lt is true and to formalize the proof. This is only the upper bound though, I guess I'll leave the lower bound to you :)

import Mathlib

universe u

def wType := WType fun c : Cardinal.{u} ↦ c.out

def wTypeToPSet : wType.{u} → PSet.{u}
  | WType.mk c f => PSet.mk c.out fun i ↦ wTypeToPSet (f i)

def wTypeToZFSet (x : wType.{u}) : ZFSet.{u} := .mk (wTypeToPSet x)

theorem mem_wTypeToZFSet_mk (s : ZFSet.{u}) (c f) :
    s ∈ wTypeToZFSet (WType.mk c f) ↔ ∃ i : c.out, s = wTypeToZFSet (f i) := by
  obtain ⟨s, rfl : ZFSet.mk _ = _⟩ := Quotient.mk_surjective s
  simp_rw [wTypeToZFSet, wTypeToPSet, ZFSet.mk_mem_iff, (· ∈ ·), PSet.Mem, ZFSet.eq]
  rfl

theorem wTypeToZFSet_surjective : Function.Surjective wTypeToZFSet :=
  fun s ↦ s.inductionOn fun s ih ↦ by
    choose x hx using ih
    let T := Shrink s.toSet
    use WType.mk _ fun y ↦ x _ ((Cardinal.outMkEquiv.trans (equivShrink s.toSet).symm) y).2
    ext z; rw [mem_wTypeToZFSet_mk]
    simp_rw [hx, eq_comm (a := z), ← Set.mem_range, ← Subtype.val.comp_apply, Set.range_comp,
      Equiv.range_eq_univ, Set.image_univ, Subtype.range_val, z.mem_toSet]

lemma Cardinal.ne_zero_of_aleph0_le {c} (h : Cardinal.aleph0 ≤ c) : c ≠ 0 := by
  rintro rfl; exact Cardinal.aleph0_ne_zero (le_zero_iff.mp h)

lemma Cardinal.pow_mono_left (c : Cardinal) : Monotone fun x : Cardinal ↦ x ^ c := by
  rintro ⟨x⟩ ⟨y⟩ le; rcases c with ⟨c⟩
  exact ⟨_, le.some.injective.comp_left (α := c)⟩

theorem Cardinal.IsInaccessible.pow_le_of_lt {c κ : Cardinal} (h : κ.IsInaccessible)
    (lt : c < κ) : κ ^ c ≤ κ := by
  obtain ⟨c, rfl : Cardinal.mk _ = _⟩ := Quotient.mk_surjective c
  rw [← κ.mk_ord_toType, power_def, ← mk_univ]
  have : @Set.univ (c → κ.ord.toType) =
      ⋃ i : κ.ord.toType, Set.range fun f : c → Set.Iio i ↦ (↑) ∘ f := by
    rw [eq_comm, Set.eq_univ_iff_forall]
    intro f
    rw [← h.2.1.cof_eq, ← κ.ord.type_toType] at lt
    have ⟨i, hi⟩ := Ordinal.lt_cof_type (Cardinal.mk_range_le (f := f).trans_lt lt)
    exact Set.mem_iUnion.mpr ⟨i, fun j ↦ ⟨f j, hi _ ⟨j, rfl⟩⟩, rfl⟩
  rw [this]
  refine (mk_iUnion_le _).trans ((mul_le_max _ _).trans ?_)
  have := ne_zero_of_aleph0_le h.1.le
  rw [← κ.mk_ord_toType] at this
  have := mk_ne_zero_iff.mp this
  simp_rw [sup_le_iff, ciSup_le_iff (bddAbove_range _), mk_ord_toType]
  refine ⟨⟨le_rfl, fun i ↦ mk_range_le.trans ?_⟩, h.1.le⟩
  rw [← power_def]
  refine (pow_mono_left _ (cantor _).le).trans ?_
  simp_rw [← power_mul]
  refine (h.2.2.2 _ <| mul_lt_of_lt h.1.le (mk_Iio_ord_toType _) lt).le

theorem ZFSet.cardinalMk : Cardinal.mk ZFSet.{u} ≤ Cardinal.univ.{u, u+1} :=
  (Cardinal.mk_le_of_surjective wTypeToZFSet_surjective).trans <| WType.cardinalMk_le_of_le' <| by
    refine (Cardinal.sum_le_sum _ (fun _ ↦ Cardinal.univ.{u,u+1})
      fun _ ↦ Cardinal.univ_inaccessible.pow_le_of_lt (Cardinal.lift_lt_univ _)).trans ?_
    rw [Cardinal.sum_const', Cardinal.mul_eq_right Cardinal.univ_inaccessible.1.le
      Cardinal.mk_cardinal.le]
    rw [Cardinal.mk_cardinal]
    exact Cardinal.ne_zero_of_aleph0_le Cardinal.univ_inaccessible.1.le

[Junyan Xu]

Have people thought about redefining docs#PSet and docs#SetTheory.PGame as WTypes?

[Mario Carneiro]

We generally prefer to make inductive definitions over using generic combinators where possible

[Mario Carneiro]

Instead, I think it would be better to have a deriving handler for proving that inductive types are equivalent to W types along the lines of haskell's deriving Generic

[Junyan Xu]

It would also be nice to automate this file by automatically constructing the surjection from a WType to the algebraic substructure generated by a set. Situations like DivisionRings that don't have a universal object is not very common, but even when a univeral object exists (like MvPolynomial for Algebra), WType could be used to determine the cardinality of the universal object. In fact the cardinality of MvPolynomial was previously determined using WType, but later refactored through the cardinality of Finsupp.

[Violeta Hernández]

I'm annoyed by the lack of a ping in this thread :stuck_out_tongue:

[Violeta Hernández]

I think this more general result should be true: if α is a well-founded codirected order such that ¬ Small.{u} α but Small.{u} (Iio x) for every x, then α is equinumerous with Cardinal.{u} (and Ordinal.{u}).

[Floris van Doorn]

Violeta Hernández said:

I'm annoyed by the lack of a ping in this thread :P

A trick I just learned today: in the Zulip webpage, you can go to [Gear] > Personal Settings > Alert Words and add something like ZFSet if you want to be notified about any message about ZFSet (or any other word).

[Violeta Hernández]

I have ordinal and cardinal as alert words, and I can see them marked in orange, but it didn't notify me :frown:

[Violeta Hernández]

Junyan Xu said:

von Neumann hierarchy is #17027 but apparently nothing about cardinality yet ...

It's not too difficult to show V_ o is a small set through well-founded induction, it should be a similar proof to docs#SetTheory.Game.small_setOf_birthday_lt. Once you have that, it's immediate that #ZFSet ≤ univ * univ = univ.

[Violeta Hernández]

No need to get into inaccessibles or beth cardinals

[Mario Carneiro]

well, I suggested that proof in part because those are also theorems I want to have for independent reasons

[Violeta Hernández]

(Though, that lemma on inaccessibles seems useful, as well as ℵ_ x = ℶ_ x = x for x an inaccessible)

[Mario Carneiro]

wow, monospace beth looks terrible

[Violeta Hernández]

On a related note, it'd be nice to get #18239 merged since it's currently blocking the von Neumann PR

[Junyan Xu]

The lemma on inaccessibles should be broken into two: c < κ.ord.cof → κ ^ c = κ ^< c and κ.IsStrongLimit → c < κ → κ ^< c ≤ κ where ^< is docs#Cardinal.powerlt.

[Mario Carneiro]

I think you also have κ ^< κ ≤ κ?

[Violeta Hernández]

Here's how to prove ℶ_ x = x for inaccessibles. Since beth is a strictly monotonic function on well-orders, x ≤ ℶ_ x. For the other direction, it suffices to prove ℶ_ y < x for y < x. Use ordinal induction. The case y = 0 as well as the successor case are trivial. For the limit case, use that the supremum of less than x cardinals less than x is also less than x.

[Violeta Hernández]

Then ℵ_ x = x follows from x ≤ ℵ_ x and ℵ_ x ≤ ℶ_ x = x

[Violeta Hernández]

(this proof sketch does some conflation of ordinals and cardinals but the point stands)

[Mario Carneiro]

the property ℶ_ x = x is also true in more generality than inaccessibles

[Mario Carneiro]

although the most precise precondition is being a beth fixed point, which is...

[Violeta Hernández]

Yeah of course, beth is a normal function and every normal function has a proper class of fixed points

[Violeta Hernández]

docs#Ordinal.not_bddAbove_fp

[Mario Carneiro]

yeah but what I mean is that you don't need to assume the full strength of inaccessible cardinal-ness to prove that a cardinal is a beth fixed point

[Junyan Xu]

Junyan Xu said:

The lemma on inaccessibles should be broken into two: c < κ.ord.cof → κ ^ c = κ ^< c and κ.IsStrongLimit → c < κ → κ ^< c ≤ κ where ^< is docs#Cardinal.powerlt.

Sorry, it seems powerlt is not the right concept here. I want the base to be less than something, not the exponent.

[Mario Carneiro]

Are you sure?

[Mario Carneiro]

note that things switch around when you use arrow notation vs exponent notation

[Junyan Xu]

Yeah, the base is the codomain. If the domain (exponent) has cardinality less than the cofinality of the base, then the image lies in some initial segment. That's how my proof works.

[Mario Carneiro]

right, which suggests you should be using powerlt

[Mario Carneiro]

the theorem Cardinal.IsInaccessible.pow_le_of_lt you gave is equivalent to showing that if kappa is inaccessible then κ ^< κ ≤ κ

[Mario Carneiro]

because κ ^< κ is the supremum of κ ^ c for c < κ

[Junyan Xu]

That's true, but in my intended refactoring of the lemma, I think c < κ.ord.cof → κ ^ c = κ ^< c is only true if ^< is interpreted as power_baselt.

[Violeta Hernández]

Can you hold off on refactoring anything relating to cofinality for a month or two

[Mario Carneiro]

I don't think any such thing was proposed?

[Mario Carneiro]

Junyan Xu is talking about refactoring the proof written just above

[Violeta Hernández]

Oh sorry we're still talking about the not-in-Mathlib pow_le_of_lt lemma

[Mario Carneiro]

Junyan Xu said:

That's true, but in my intended refactoring of the lemma, I think c < κ.ord.cof → κ ^ c = κ ^< c is only true if ^< is interpreted as power_baselt.

yeah I find this theorem suspicious

[Mario Carneiro]

I don't think you need it, as I pointed out you can just talk about κ ^< κ and then κ ^ c for c < κ

[Mario Carneiro]

and κ ^ κ and κ ^< c for c < κ don't really come up

[Junyan Xu]

Okay. I'm in a lecture so I'll think about it later.
Has Violeta defined def Ordinal.vonNeumann : Ordinal.{u} ↪ ZFSet.{u} somewhere? That would give the lower bound. I almost finished proving it's injective.

[Violeta Hernández]

Yep, in the PR you linked above

[Violeta Hernández]

I didn't prove it's an injection, but that should follow easily from a < b → V_ a ∈ V_ b which I did prove

[Violeta Hernández]

#17027

[Junyan Xu]

I think it also follows from docs#ZFSet.mem_irrefl

[Junyan Xu]

This is my definition:

def Ordinal.vonNeumann : Ordinal.{u} ↪ ZFSet.{u} where
  toFun := WellFoundedLT.fix fun o ih ↦
    ZFSet.range fun x ↦ ih _ ((equivShrink <| Set.Iio o).symm x).2
  inj' o' o eq := by
    contrapose! eq
    wlog lt : o' < o
    · exact (this _ _ eq.symm <| (le_of_not_lt lt).lt_of_ne' eq).symm
    conv_rhs => rw [WellFoundedLT.fix_eq]
    intro h
    sorry

[Junyan Xu]

Oh, I'm defining the vN ordinal while you're defining one level of the vN hierarchy ... but I think mem_irrefl still yields a proof?

[Violeta Hernández]

Oh oops wrong von Neumann

[Violeta Hernández]

I'm pretty sure I had that in a Lean 3 branch

[Violeta Hernández]

In any case it's my planned next PR after #17001 goes through

[Violeta Hernández]

(which reminds me, there really should be a bot notifying about merge conflicts)

[Junyan Xu]

I've been using the Arc browser lately; it has a "live folder" for pull requests and in my experience if a PR gains a merge conflict it will pop out of the folder (probably due to added label) so you sees it immediately, even when the folder is collapsed.
image.png
https://techcrunch.com/2024/04/11/arc-browsers-live-folders-will-auto-update-tabs-for-you/

[Junyan Xu]

Finished the equality:

import Mathlib

universe u

def wType := WType fun c : Cardinal.{u} ↦ c.out

def wTypeToPSet : wType.{u} → PSet.{u}
  | WType.mk c f => PSet.mk c.out fun i ↦ wTypeToPSet (f i)

def wTypeToZFSet (x : wType.{u}) : ZFSet.{u} := .mk (wTypeToPSet x)

-- extract a statement about ∈ ZFSet.mk (PSet.mk _ _)
theorem mem_wTypeToZFSet_mk (s : ZFSet.{u}) (c f) :
    s ∈ wTypeToZFSet (WType.mk c f) ↔ ∃ i : c.out, s = wTypeToZFSet (f i) := by
  rcases s; congrm (∃ _, ?_); exact ZFSet.eq.symm

theorem wTypeToZFSet_surjective : Function.Surjective wTypeToZFSet :=
  fun s ↦ s.inductionOn fun s ih ↦ by
    choose ih ih_spec using ih
    use WType.mk _ fun x ↦ ih _ ((Cardinal.outMkEquiv.trans (equivShrink s.toSet).symm) x).2
    ext z
    simp_rw [mem_wTypeToZFSet_mk, ih_spec, eq_comm (a := z), ← Set.mem_range, ← Subtype.val.comp_apply,
      Set.range_comp, Equiv.range_eq_univ, Set.image_univ, Subtype.range_val, z.mem_toSet]

lemma Cardinal.ne_zero_of_aleph0_le {c} (h : Cardinal.aleph0 ≤ c) : c ≠ 0 := by
  rintro rfl; exact Cardinal.aleph0_ne_zero (le_zero_iff.mp h)

lemma Cardinal.pow_mono_left (c : Cardinal) : Monotone fun x : Cardinal ↦ x ^ c := by
  rintro ⟨x⟩ ⟨y⟩ ⟨_, inj⟩; rcases c; exact ⟨_, inj.comp_left⟩

-- break into c < κ.ord.cof → κ ^ c = κ <^ c. and κ.StrongLimit → c < κ → κ <^ c ≤ κ.
theorem Cardinal.IsInaccessible.pow_le_of_lt {c κ : Cardinal} (h : κ.IsInaccessible)
    (lt : c < κ) : κ ^ c ≤ κ := by
  obtain ⟨c, rfl : Cardinal.mk _ = _⟩ := Quotient.mk_surjective c
  rw [← κ.mk_ord_toType, power_def, ← mk_univ]
  have : @Set.univ (c → κ.ord.toType) =
      ⋃ i : κ.ord.toType, Set.range fun f : c → Set.Iio i ↦ (↑) ∘ f := by
    rw [eq_comm, Set.eq_univ_iff_forall]
    intro f
    rw [← h.2.1.cof_eq, ← κ.ord.type_toType] at lt
    have ⟨i, hi⟩ := Ordinal.lt_cof_type (Cardinal.mk_range_le (f := f).trans_lt lt)
    exact Set.mem_iUnion.mpr ⟨i, fun j ↦ ⟨f j, hi _ ⟨j, rfl⟩⟩, rfl⟩
  rw [this]
  refine (mk_iUnion_le _).trans ((mul_le_max _ _).trans ?_)
  have := ne_zero_of_aleph0_le h.1.le
  rw [← κ.mk_ord_toType] at this
  have := mk_ne_zero_iff.mp this
  simp_rw [sup_le_iff, ciSup_le_iff (bddAbove_range _), mk_ord_toType]
  refine ⟨⟨le_rfl, fun i ↦ mk_range_le.trans ?_⟩, h.1.le⟩
  rw [← power_def]
  refine (pow_mono_left _ (cantor _).le).trans ?_
  simp_rw [← power_mul]
  refine (h.2.2.2 _ <| mul_lt_of_lt h.1.le (mk_Iio_ord_toType _) lt).le

theorem ZFSet.cardinalMk_le_univ : Cardinal.mk ZFSet.{u} ≤ Cardinal.univ.{u, u+1} :=
  (Cardinal.mk_le_of_surjective wTypeToZFSet_surjective).trans <| WType.cardinalMk_le_of_le' <| by
    refine (Cardinal.sum_le_sum _ (fun _ ↦ Cardinal.univ.{u,u+1})
      fun _ ↦ Cardinal.univ_inaccessible.pow_le_of_lt (Cardinal.lift_lt_univ _)).trans ?_
    rw [Cardinal.sum_const', Cardinal.mul_eq_right Cardinal.univ_inaccessible.1.le
      Cardinal.mk_cardinal.le]
    rw [Cardinal.mk_cardinal]
    exact Cardinal.ne_zero_of_aleph0_le Cardinal.univ_inaccessible.1.le

noncomputable def Ordinal.vonNeumann : Ordinal.{u} ↪ ZFSet.{u} where
  toFun := WellFoundedLT.fix fun o ih ↦
    ZFSet.range fun x ↦ ih _ ((equivShrink <| Set.Iio o).symm x).2
  inj' o' o eq := by
    contrapose! eq
    wlog lt : o' < o
    · exact (this _ _ eq.symm <| (le_of_not_lt lt).lt_of_ne' eq).symm
    conv_rhs => rw [WellFoundedLT.fix_eq]
    refine fun h ↦ ne_of_mem_of_not_mem' (ZFSet.mem_range.mpr ⟨equivShrink _ ⟨o', lt⟩, ?_⟩)
      (ZFSet.mem_irrefl _) h.symm
    dsimp only
    rw [Equiv.symm_apply_apply]

theorem ZFSet.cardinalUniv_le_mk : Cardinal.univ.{u, u+1} ≤ Cardinal.mk ZFSet.{u} := by
  rw [Cardinal.univ_id]
  exact ⟨Ordinal.vonNeumann⟩

theorem ZFSet.cardinalMk : Cardinal.mk ZFSet.{u} = Cardinal.univ.{u, u+1} :=
  cardinalMk_le_univ.antisymm cardinalUniv_le_mk

[Junyan Xu]

Regarding IsInaccessible.pow_le_of_lt, I still think it should be broken into a lemma about IsRegular/cofinality and another about IsStrongLimit, and that seems to necessitate the introduction of a powerBaseLT operation. (or I guess I'll just write it as a supremum)

[Violeta Hernández]

Please don't introduce a powerBaseLT operation

[Violeta Hernández]

I think powerlt is already questionable enough as is

[Violeta Hernández]

Otherwise yeah I think splitting up the lemma would be an improvement

[Junyan Xu]

Violeta Hernández said:

It's not too difficult to show V_ o is a small set through well-founded induction, it should be a similar proof to docs#SetTheory.Game.small_setOf_birthday_lt. Once you have that, it's immediate that #ZFSet ≤ univ * univ = univ.

Well we already know every ZFSet is small: docs#ZFSet.small_toSet.

Mario Carneiro said:

the property ℶ_ x = x is also true in more generality than inaccessibles

Is there a more general and easy-to-state condition that the proof of Inaccessible -> beth fixed point should factor through? (the same for aleph?)

[Violeta Hernández]

1. Oh of course, I'm being silly. Being able to define V_ o as a ZFSet already makes it small.
2. I don't know any other nicer condition to factor through. There might be some random large cardinal condition that's weaker than inaccessibles but still implies it, but even if that were true it would probably just make the argument more complicated.

[Violeta Hernández]

Aleph/beth fixed points are not really notable once you're past the initial surprise of their existence

[Mario Carneiro]

Junyan Xu said:

Is there a more general and easy-to-state condition that the proof of Inaccessible -> beth fixed point should factor through? (the same for aleph?)

Possibly κ ^< κ = κ

[Junyan Xu]

If $\kappa=2^\lambda$ is infinite and GCH holds, then $c<\kappa$ implies $c\le\lambda$, so $\kappa^c=2^{\lambda c}=2^\lambda=\kappa$, so $\kappa^{<\kappa}=\kappa$ but $\kappa$ doesn't have to be an alpha/beta fixed point.

[Junyan Xu]

Assume $\kappa^{<\kappa}$ and $\kappa$ is not of the form $2^c$, then for all $1\le c<\kappa$, we have $2^c\le \kappa^c=\kappa$, so $2^c < \kappa$, showing that $\kappa$ is a strong limit. Using this result, we then know that $2^\kappa=\kappa^{\mathrm{cof}(\kappa)}$; since we assume $\kappa^c\le\kappa$ for $c <\kappa$, we conclude that $\mathrm{cof}(\kappa)\ge\kappa$, i.e. $\kappa$ is regular. So the condition $\kappa^{<\kappa}$ is not more general than inaccessibility.
(I found the SE question when I was trying to prove $\kappa^{<\kappa}$ for inaccessible $\kappa$.)

[Nir Paz]

I don't think there is a better condition but a simple proof is that if k is a strong limit than it has the form ב_λ for a limit λ, and then if k is regular then cof(k)=cof(λ)=k.

[Dexin Zhang]

There is a more general result, $|V_\kappa|=\kappa$ when $\kappa$ is inaccessible. Then the cardinality of ZFSet comes from (V_ Cardinal.univ.{u}.ord).toSet ≃ ZFSet.{u}.

[Violeta Hernández]

It's not much more general of a result, since $|V_{\kappa}| = \beth_\kappa$ for infinite $\kappa$

[Junyan Xu]

A much shorter proof built on top of #17027 is formalized here.

[Junyan Xu]

Floris van Doorn said:

A trick I just learned today: in the Zulip webpage, you can go to [Gear] > Personal Settings > Alert Words and add something like ZFSet if you want to be notified about any message about ZFSet (or any other word).

Is there a way to subscribe to certain accounts?

[Jason Rute]

Violeta Hernández said:

I have ordinal and cardinal as alert words, and I can see them marked in orange, but it didn't notify me :(

I get better notifications in the new beta zulip app. https://blog.zulip.com/2024/12/12/new-flutter-mobile-app-beta/

[Violeta Hernández]

I opened #20749 introducing the "pre-beth" function, i.e. beth starting from zero. I don't think this is a standard mathematical object, but it slightly simplifies some proofs about beth; more importantly, this satisfies #(V_ o) = preBeth o for every ordinal o, and I plan to prove this in a follow-up.