IsSuccLimit

Stream: maths

[Yury G. Kudryashov]

@Violeta Hernández Is it intentional that docs#Order.IsSuccLimit allows bot while docs#Ordinal.IsLimit and docs#Cardinal.IsLimit don't?

[Yury G. Kudryashov]

Should we change IsSuccLimit to assume ¬IsMin a (or ¬IsBot a?)

[Yury G. Kudryashov]

CC @Yaël Dillies

[Yaël Dillies]

This was already discussed at length in !3#15005. Upshot is that is_succ_limit is the useful predicate in general, but the literature is divided on whether 0 is a limit ordinal. Eg my Logic & Set Theory lectures this year claim it is, but Wikipedia claims the opposite.

[Yaël Dillies]

Personally I'm in favour of changing cardinal.is_limit to allow 0, or maybe to rename is_succ_limit to is_succ_prelimit and define a new is_succ_limit that matches cardinal.is_limit.

[Kevin Buzzard]

I wouldn't trust "random lecturer who doesn't really care about the question" any more.

[Kevin Buzzard]

However I think I agree with your random lecturer!

[Violeta Hernández]

I've got nothing new to say here but I might as well say hi

[Violeta Hernández]

Long time no see

[Yury G. Kudryashov]

From topology point of view, {0} is an open set while all other {c}, IsSuccLimit c are.

[Yury G. Kudryashov]

I will think about the IsSuccPrelimit option.

[Pedro Sánchez Terraf]

I'm definitely with the topology camp on this one, and since 0 is isolated, it is not a limit. Nor obviously a successor.

[Kevin Buzzard]

From the order point of view, 0 is the sup of the ordinals strictly less than it, so it's a limit ordinal. But maybe it's like 1 not being a prime despite it satisfying many of the criteria for and properties of primality.

[Pedro Sánchez Terraf]

You just have proved that a sup need not be a limit :wink:

[Pedro Sánchez Terraf]

Yury G. Kudryashov said:

Violeta Hernández Is it intentional that docs#Order.IsSuccLimit allows bot while docs#Ordinal.IsLimit and docs#Cardinal.IsLimit don't?

Wrt cardinals, limit is only used for infinite ones.

[Violeta Hernández]

I was thinking about this again. I think there's reasonable arguments towards both sides of 0 being a limit ordinal or not. Another argument in favor is that ω | 0, and in fact IsSuccLimit o ↔ ω | o. An argument against is that a normal function evaluated at 0 need not be the supremum of itself evaluated at values less than 0, i.e. f 0 ≠ 0 in general.

[Violeta Hernández]

From a strictly practical perspective, I do think it's bad that we have two nearly identical definitions with a lot of shared results. Most of the basic results about Ordinal.IsLimit, like a < o → succ a < o or o ≤ a ↔ ∀ x < o, x ≤ a, are still true for o = 0.

[Violeta Hernández]

It's in our spirit as mathematicians to prove things in their greatest generality, right? With that mindset, I think it makes a lot of sense to prove stuff about IsSuccLimit o, and tack on the o ≠ 0 assumption only when it's needed.

[Violeta Hernández]

I think the name IsSuccLimit is already enough of a compromise. These aren't really limit ordinals, depending on who you're talking to, but it's just more convenient to set things up in terms of a common definition like that one.

[Kevin Buzzard]

We have docs#Prime and docs#Preprime (edit: apparently we don't!)

[Yury G. Kudryashov]

We have docs#IsPreconnected

[Violeta Hernández]

I guess another possibility is to keep both definitions, but define them in the same file. That way the APIs never diverge much.

[Violeta Hernández]

That seems to be what's happening with IsPreconnected

[Violeta Hernández]

@Yaël Dillies Thinking about this again. What do you think about turning IsSuccLimit into IsSuccPrelimit and defining IsSuccLimit x ↔ IsSuccPrelimit x ∧ ¬ IsMin x?

[Yaël Dillies]

I think that's a fine approach

[Violeta Hernández]

Is the name fine? I feel very iffy about outright replacing a definition by a non-equivalent one, but at the same time, I don't think it's proper to just call the new definition something like IsSuccLimit'

[Yury G. Kudryashov]

Please mention the rename in the new docstring.

[Violeta Hernández]

I'm finding this change to be quite destructive. There's a lot of theorem names involving IsSuccLimit that have to be completely removed since they're now just false when stated like that.

[Violeta Hernández]

The diff is 700+ lines and it doesn't even build yet. Admittedly it can be compressed a bit if I wait until a later PR to introduce the new induction principles, but still, a lot of this is just renaming and deprecating.

[Violeta Hernández]

I'm thinking, maybe we could go about this in stages? First introduce the new definition using some temporary alias like IsSuccLimit', with a docstring explaining the future rename. Then redefine Cardinal.IsLimit and Ordinal.IsLimit using it. Finally, perform the switch IsSuccLimit' → IsSuccLimit and IsSuccLimit → IsSuccPrelimit at once.

[Violeta Hernández]

The initial PR that introduces the new definition should really not be touching any other files. That's scope creep in my view.

[Yury G. Kudryashov]

Or you can start with renaming the old definition.

[Violeta Hernández]

Ah, that's much cleaner. I'll make the PR for that soon.

[Violeta Hernández]

Initial renaming PR: #16518

[Violeta Hernández]

Somewhat on a related note, I'm having a lot of trouble doing the succ x → x + 1 replacement on ordinals.

[Violeta Hernández]

The main issue is that docs#Ordinal.IsLimit is stated in terms of succ. So anything tangentially related to limit ordinals uses succ all over the place.

[Violeta Hernández]

I could redefine IsLimit, but that's a wasted effort if we do it before IsSuccLimit drops

[Yury G. Kudryashov]

You can add IsSuccLimit first, if it's more convenient.

[Violeta Hernández]

Yeah, that's the idea. I am sort of expecting it to take a while for IsSuccLimit to be up and running though.

[Violeta Hernández]

Never mind! That was quick

[Violeta Hernández]

Now, here's a question. What's the design principle for IsSuccLimit and IsSuccPrelimit?

[Violeta Hernández]

Do we duplicate all lemmas where either is applicable? Or do we only use the one that yields the strongest conclusion?

[Violeta Hernández]

For instance, do we want both IsSuccPrelimit ℵ₀ and IsSuccLimit ℵ₀?

[Yaël Dillies]

I think the stronger one is enough