Ordinal notations

Stream: maths

[Violeta Hernández]

I've always been a bit conflicted about the SetTheory.Ordinal.Notation file. I find what it does really cool: it's essentially a formally-verified calculator for ordinal arithmetic below ε₀. But on the other hand, the chances this gets used elsewhere in Mathlib are basically zero. Not to mention that the proofs in the file are quite finicky and have the annoying habit of breaking as refactors come along...

I guess my question is: is this a one-off file? The fact that the file is named Notation, and the main type defined in it is just Note, sort of imply this to be the one ordinal notation we have in Mathlib. But like, this is the most basic ordinal notation out there!

I'm currently working on getting the Veblen hierarchy into Mathlib, and that would allow us to define an ordinal notation (also with computable arithmetic) all the way up to the Feferman-Schütte ordinal Γ₀. There's dozens more ordinal notations - admittedly most of these aren't very relevant or interesting, but the more well-known ones like Bachmann's psi and maybe Kleene's O might be fun to formalize.

[Violeta Hernández]

Still, I can't shake the feeling that there's little of mathematical value here.

[Nir Paz]

Kleene's O sounds really cool to formalize! Connecting this to computability by showing that Kleene's O is the supremum of definable well orders on N (I think? This isn't my specialty) is also an interesting goal.

In general I think we should be very careful applying any subjective reasoning to what counts as "interesting". This subject is well known in the literature, maybe that's enough.

[Nir Paz]

Although I know this is easy for me to say as someone who doesn't often need to maintain the file

[Violeta Hernández]

Well, in that case. I'll work to clean up the notation file and I'll try to at least PR the Veblen notation once I have all the tools for it :smile:

[Mario Carneiro]

@Violeta Hernández said:

I guess my question is: is this a one-off file? The fact that the file is named Notation, and the main type defined in it is just Note, sort of imply this to be the one ordinal notation we have in Mathlib. But like, this is the most basic ordinal notation out there!

If you want to add more complicated computable ordinal notations, I think it would be fine to rename this one to be more specific.

[Mario Carneiro]

You are correct that this is mainly intended as a leaf file. I think it is good for demonstrations, and also for just getting your head around how ordinal operations work, to be able to work with concrete objects and compute with them. I wish we had more of this kind of thing in mathlib (polynomials are another area that can benefit from this, for multiple reasons)

[Mario Carneiro]

have the annoying habit of breaking as refactors come along...

I think this is literally the case with any code that uses the stuff you are refactoring. I think it's good to remember that mathlib is a library and intended for uses beyond just its own borders, and refactors do have costs

[Violeta Hernández]

Since getting ordinal stuff into Mathlib is pretty slow, I'll start a separate Lean repo as a dump of sorts for ordinal notation things. I'll start by refactoring/expanding on the existing Notation file and I'll build up from there.

[Violeta Hernández]

https://github.com/vihdzp/ordinal-notation

[Violeta Hernández]

Just revamped the Cantor Normal Form notation file in my own branch! There were a few issues with the file in its Mathlib state which I believe I've nicely addressed.

• Comparison on docs#ONote is non-computable, since it relies on docs#ONote.repr. I redefined this to simply be the lexicographic ordering (which of course coincides with the standard ordering for normal forms). This has the advantage of being a linear order, which means we can mostly dispose of docs#ONote.cmp in favor of docs#cmp.
• The definitions of the operations docs#ONote.add and docs#ONote.sub are tweaked and simplified slightly. The definition of docs#ONote.opow is simplified quite substantially, now only requiring one auxiliary function instead of six.
• Golfing! I got rid of all the non-terminal simps from the original file, and separated the more complicated parts of the arithmetical arguments into new lemmas I plan on PRing to Mathlib soon. The file is overall about 100 lines shorter, and the proofs should now be much more maintainable.

[Violeta Hernández]

There's just one part of the file I haven't touched, which is the stuff on docs#ONote.fundamentalSequence. The issue is, if we plan on having more than one ordinal notation on Mathlib, it doesn't make sense to make a new definition of fundamental sequences for each. But on the other hand, we already have a "general" non-computable version of this in docs#Ordinal.IsFundamentalSequence

[Violeta Hernández]

I think it could be useful to separate both notions. Since fundamental sequences are almost always assumed to be countable (and computable), we could rename the version in the cofinality file to something like CofinalSequence

[Violeta Hernández]

We could then define the fast-growing hierarchy for any given system of fundamental sequences.

[Violeta Hernández]

I think this could be a general definition for the countable notion of a fundamental sequence:

def Sequence.{u} (α : Type u) : Type u :=
  Option α ⊕ (ℕ → α)

def Sequence.StrictMono {α : Type*} [LinearOrder α] : Sequence α → Prop
  | Sum.inl _ => true
  | Sum.inr f => _root_.StrictMono f

def Sequence.IsLimit {α : Type*} [LinearOrder α] : Sequence α → α → Prop
  | Sum.inl none, x => IsMin x
  | Sum.inl (some x), y => x ⋖ y
  | Sum.inr f, y => ∀ x, x < y ↔ ∃ n, x < f n

structure FundamentalSequence.{u} {α : Type u} [LinearOrder α] (top : α) : Type u where
  sequence : Sequence α
  strictMono : sequence.StrictMono
  limit_eq : sequence.IsLimit top

def FundamentalSequenceSystem.{u} (α : Type u) [LinearOrder α] : Type u :=
  ∀ top : α, FundamentalSequence top

[Violeta Hernández]

I'm inclined to use FS instead of the FundamentalSequence mouthful, but even though I've seen that abbreviation a lot I don't know if a) it's standard and b) if it'll be understandable at first glance

[Violeta Hernández]

Something nice about this approach is that we wouldn't need to separate docs#ONote.fastGrowing and docs#ONote.fastGrowingε₀. Every FundamentalSequenceSystem can be used to create its own fast-growing hierarchy, and fastGrowingε₀ just uses the fundamental sequence system for WithTop (NONote).

[Violeta Hernández]

Here's how the definition of the FGH looks like, btw:

def fastGrowing (s : FundamentalSequenceSystem α) [WellFoundedLT α] (x : α) (n : ℕ) : ℕ :=
  match s x with
  | ⟨Sum.inl none, _, _⟩ => n + 1
  | ⟨Sum.inl (some y), _, h⟩ => have := h.lt; (fastGrowing s y)^[n] n
  | ⟨Sum.inr f, hs, hl⟩ => have := lt_of_strictMono_of_isLimit hs hl n; fastGrowing s (f n) n
termination_by wellFounded_lt.wrap x

[Violeta Hernández]

https://github.com/vihdzp/ordinal-notation/blob/master/OrdinalNotation/FundamentalSequence.lean

[Violeta Hernández]

This is much more Mathilb-ready than my huge ONote refactor, all that's really missing is an answer to "what do we do about docs#IsFundamentalSequence"

[Violeta Hernández]

which note: is also an important concept in its own right

[Yaël Dillies]

Violeta Hernández said:

I'm inclined to use FS instead of the FundamentalSequence mouthful

What about FundamentalSeq?

[Violeta Hernández]

I like that middle ground

[Violeta Hernández]

What about FundamentalSequenceSystem? Does FundamentalSystem work as a shortening?

[Violeta Hernández]

Well, my refactor/enhancement of the Cantor Normal Form ordinal notation is pretty much done.

[Violeta Hernández]

There's still two sorries left in the proof that docs#NONote.repr is a principal segment embedding - this is because the top of said embedding is ε₀, whose (most natural) definition depends on the Veblen hierarchy.

[Violeta Hernández]

The thing is, I legitimately have no idea if it's even feasible for this to make it into Mathlib.

[Violeta Hernández]

I stand by all the changes I made, but they required basically everything to be reproven from scratch. If I did a PR, it'd be 1200 lines long with no way to split it.

[Violeta Hernández]

This is on top of 400 lines or so of API for fundamental sequences. That could more easily make it into Mathlib, but without tweaking the Notation and Cofinality files first it'd put us in the awkward position of having three unconnected notions of fundamental sequences.

[Violeta Hernández]

I also accumulated about 100 lines of auxiliary lemmas that should be in Mathlib, so for now I'll just work on getting those in

[Yaël Dillies]

Violeta Hernández said:

I stand by all the changes I made, but they required basically everything to be reproven from scratch. If I did a PR, it'd be 1200 lines long with no way to split it.

Big unsplittable PRs are sometimes the way of life. We can still review them

[Violeta Hernández]

Alright then!

[Violeta Hernández]

I'll PR the fundamental sequence stuff first, which can fortunately be neatly split into two or even three small PRs. Then I'll PR the big CNF refactor.

[Violeta Hernández]

#18463 (+189 -1) defines the type of fundamental sequences and establishes its basic API.

[Violeta Hernández]

I'd like to start work on Veblen's ordinal notation, but that depends on #17751

[Violeta Hernández]

Once that goes through I can provisionally copy the veblen PR to my repo and start working on that

[Violeta Hernández]

Something perhaps obvious but quite nice I just realized: being able to construct a fundamental sequence system for a type immediately implies decidability of IsSuccLimit and IsSuccPrelimit

[Violeta Hernández]

Since you can just check the length of the corresponding fundamental sequence