PCF theory

Stream: maths

[Nir Paz]

I'm finally getting started on PCF theory! The project is hosted on this git repository, and will follow article 14 in "Handbook of set theory" - "Cardinal Arithmetic", with the general goal of getting to results about... cardinal arithmetic (a few more details are in the readme). So far I have formalized the existence of club guessing sequences (theorem 2.17), which is basically the only thing we can do before actually defining the basics of PCF.

A little disclaimer, I don't have plans to get this into mathlib at the moment. I would nevertheless love feedback/help.

In PCF/Playground.lean I have the definitions I talk up below, but I'm not really sure about any of them. Keep in mind they are not very organized at the moment. The very beginning of PCF has many definitions which are easy to jump between on paper but have no single obvious way to formalize, so it will likely be a minute before they all settle down. Here are some details, and feel free to comment on only a part of it because this is a lot of stuff:

Let L be a linear order, A any type and I an ideal on A (an ideal here is a family of subsets downwards closed and closed under finite union. Equivalent to Ideal (Set ι)). Then we can define a partial order on (A → L) using the ideal I: for f, g : A → L, define f <I g if {x | g(x) ≤ f(x)} ∈ I. That is, the set of exceptions to f < g is small. ≤I, =I etc are defined similarly. Note that f ≤I g is not equivalent to (f <I g or f =I g), so this is not a Preorder in the mathlib sense.

When h : A → Ordinal, we will look at the collection of functions "below" h, the set of f : A → Ordinal which are bounded by h at every coordinate. PCF theory studies the properties of the orders <I on such sets with different ideals I.

• First I defined set-ideals,SIdeal α := Order.Ideal (Set α), because working directly with Order.Ideal is annoying.

• For a type A, an order L and h : A → L, FunsBelow h is the set of functions from A to L which are smaller than h everywhere.

• The most common case is where A is a set of ordinals and we look at $\prod A$, which in the above implementation means h is the identity. This is Ordinal.Prod A (better name?) for A : Set Ordinal. Since this definition is just FunsBelow with specific inputs, this extra layer shouldn't hurt definitional equality between the two.

These definitions have the effect that when talking about an ideal on A : Set Ordinal, its elements will have type Set A and not Set Ordinal. I don't know if this is good or bad.

A important property is being an "exact upper bound" of a set. The definition is in the book for the interested, but importantly it uses both a < and a ≤ relation, which like I said above don't have to corrospond in the usual way. So the definition must explicitly take them both:

• Set.ExactUpperBound (le lt : α → α → Prop) (A : Set α) (a : α) means that a is an exact upper bound of A with the relations le and lt. We then define

• Set.ExactUpperBound_SIdeal for the case where the orders are ≤I and <I, so it only takes in a set, an element and an ideal.

Some of the results we'll get to soon have the form "if a set of functions from some A to the ordinals has some order-property with respect an ideal I, then it has an exact upper bound with respect to I".

We could also define ExactUpperBound_SIdeal without defining exact upper bounds of general orders not induced by an ideal, but it seems strange not to have it.

Next we want to talk about cofinalities of such orders induced by an ideal, specifically cofinalities of $\prod A$ for a set of ordinals $A$ and with respect to an ideal $I$ on $A$.

First we define the more general case of the cofinality of a set of functions given an ideal:

def Order.SIdeal_cof {L A : Type*} [LinearOrder L] (S : Set (A → L)) (I : SIdeal A) :=
  @Order.cof S (fun f g ↦ f.1 ≤I g.1)

and then the ordinal case as a definition using this case.

The main property we will want an order ≤I to satisfy is for it to have True Cofinality. This means that it has a linearly ordered cofinal set, or equivalently an increasing cofinal sequence. We call the length of the shortest such sequence, if it exists, the true cofinality of the order. The biggest results of this chapter will say that for many sets of ordinals A there are ideals I so that the product of A has true cofinality with respect to ≤I.

If an order has true cofinality then it is simply equal to its cofinality. Therefore we only need the property of having true cofinality, which we define for a general relation:

def Order.hasTCF {α : Type*} (r : α → α → Prop) : Prop :=
  ∃ A : Set α, (∀ a ∈ A, ∀ b ∈ A, r a b ∨ r b a) ∧ (∀ x : α, ∃ y ∈ A, r x y)

Finally this lets us define the pcf (possible cofinalities) of a set of ordinals as the set of true cofinalities that its product can attain, with any proper ideal:

def Ordinal.pcf (A : Set Ordinal) : Set Cardinal :=
  {SIdeal_cof_Prod A I | (I : SIdeal A) (_hI : Set.univ ∉ I) (_hTCF : @hasTCF (Prod A) (· ≤I ·))}

I think the main reason I ended up defining so many things as just plugging in specific inputs to another definition is because we can't use any typeclasses when dealing with orders induced by ideals, both because we work with many orders at the same time and because there isn't a class for the relationship between ≤I and <I.

NB: To define f <I g,... I first defined ≤(g, f) as the set of indices where g ≤ f. Then f <I g := ≤(g, f) ∈ I. I'm not sure if this is useful at all or if it only increases spaghettiness.

@Violeta Hernández so you won't be mad at me for not pinging you.

[Violeta Hernández]

I don't know anything about PCF theory, but I'm willing to learn. Count me in!

I think the decision of working within a separate repo is the correct one. The current ordinal library is a bit tumultuous at the moment (entirely through my fault), and if we want to formalize new mathematics we should focus on moving fast, and then fixing things when we have the time.

[Violeta Hernández]

Question: isn't ≤I in fact a preorder? It's reflexive (because every ideal contains univ) and transitive (because of the totality of the order in L).

[Violeta Hernández]

x < y ↔ x ≤ y ∨ x = y isn't a necessary condition on a preorder, only on partial orders

[Violeta Hernández]

(Does this same comment apply for ExactUpperBound? If we can avoid unbundled relations, it will make things a lot nicer if not simpler.)

[Nir Paz]

Violeta Hernández said:

x < y ↔ x ≤ y ∨ x = y isn't a necessary condition on a preorder, only on partial orders

In mathlib's Preorder the condition is a < b ↔ a ≤ b ∧ ¬b ≤ a, which doesn't necessarily hold. For example if f is always ≤ to g, but equal to it on a positive set and strictly less than it on a positive set, then f ≤ g and ¬ g ≤ f, but f < g doesn't hold.

[Violeta Hernández]

Oh, so the situation is a bit different then. It's not that ≤I isn't a preorder, but rather that said preorder doesn't have the correct <I and =I relations.

[Nir Paz]

Yes, it is a preorder, just not a Preorder by mathlib's standards.

[Violeta Hernández]

Does the resulting order structure have another name? Can it be characterized somehow?

[Nir Paz]

I think the only properties < and ≤ satisfy with each other are
a < b → a ≤ b and a < b ≤ c → a < c (and the symmetric case)
and I don't know of a name for this.

[Nir Paz]

By the way a lot of PCF theory is done on the quotient of the function space with =I, and then they are a partial order and a strict order (still not equivalent in the usual sense though), but I think it might be okay to avoid doing that for a while.

[Violeta Hernández]

Thing is, I was working on redefining Order.cof in terms of a preorder, rather than an unbundled relation. I was expecting that this would make things simpler, but that might not be the case here.

[Violeta Hernández]

Nir Paz said:

I think the only properties < and ≤ satisfy with each other are
a < b → a ≤ b and a < b ≤ c → a < c (and the symmetric case)
and I don't know of a name for this.

All this really says is "≤ is transitive and it's a subrelation of <"

[Nir Paz]

Violeta Hernández said:

Thing is, I was working on redefining Order.cof in terms of a preorder, rather than an unbundled relation. I was expecting that this would make things simpler, but that might not be the case here.

Hmm... with that definition I guess we would need to define the Preorder whose ≤ is ≤I and whose < is ²I, and use that for the cofinality, which indeed is less simple. Basically we want it to be easy to take the cofinality of a single preorder.

[Violeta Hernández]

We could define a type alias on A → L which registers a preorder structure such that ≤ is ≤I, but otherwise use ≤I and <I everywhere else.

[Violeta Hernández]

Thing is, having an unbundled relation takes out a lot of useful functionality, e.g. you can't as easily talk about bounded sets, or suprema/infima, or even docs#Order.Cofinal sets with the way I implemented them.

[Violeta Hernández]

Skimming through the reference you give, it acknowledges that ≤I is a quasi-order (a synonym of preorder) and that <I is irreflexive, but doesn't give any explicit structure that relates both of them

[Violeta Hernández]

So maybe it's better to treat them as separate relations

[Nir Paz]

Violeta Hernández said:

Thing is, having an unbundled relation takes out a lot of useful functionality, e.g. you can't as easily talk about bounded sets, or suprema/infima, or even docs#Order.Cofinal sets with the way I implemented them.

Yea that's a bit of a problem, I ended up defining unbundles versions of Order.Unbounded as Set.Unbounded. I expect if we go down this route there will be some work on this kind of API.

Thing is, there really isn't a natural Preorder that uses <I, so it would always be awkward to use bundled versions of things.

[Violeta Hernández]

We already have an unbundled version of Order.Unbounded, it's docs#Set.Unbounded. Except, we've argued in the past that it should be removed...

[Violeta Hernández]

It's a somewhat counterintuitive definition, Unbounded (· ≤ ·) s means ¬ BddAbove s, while Unbounded (· < ·) s means Cofinal s... at least if ≤ and < come from a linear order.

[Nir Paz]

Sorry I meant I defined Set.UpperBound

[Violeta Hernández]

Nir Paz said:

Thing is, there really isn't a natural Preorder that uses <I, so it would always be awkward to use bundled versions of things.

The book says <I is a "strict partial ordering". Does that mean that the relation <I or = is a partial order in the Mathlib sense? Sorry, misread

[Nir Paz]

Even though upperBounds exists. Although only uses a LE instance so in this case it would be a bit better to use it. But I don't see a a way to do that without explicitly providing the order anyways, since we can't have a LE instance for every ideal...

I settled on possibly not using any classes for the orders because of thses kinds of stuff.

[Violeta Hernández]

Oh of course, I forgot that you could freely choose an ideal

[Nir Paz]

About cof, would it be catastrophical to have 2 definitions? loogle bring up 11 theorems that involve it, we probably need just a few for this project. So maybe you can refactor like you wanted but we can also have a version like the current one?

[Violeta Hernández]

It would not be catastrophical, though it would certainly be annoying

[Nir Paz]

I would be fine defining unbundled cofinality in the project (copying what exists right now into some file) and using that without it being in mathlib. It would be easy, quick and dirty, but taking this approach might make the project unfit for mathlib.

[Violeta Hernández]

I think there's two possibilities here. Either
a) We do not do the refactor, and we instead keep Order.cof defined as is. If any theorems are easier to state using @Order.cof α (· ≤ ·) then we just do that.
b) We do the refactor. We can still define the cofinality in the way that is required for PCF, we can do something like

def Order.SIdeal_cof {L A : Type*} [LinearOrder L] (S : Set (A → L)) (I : SIdeal A) :=
  have : Preorder (A → L) := sorry -- temporarily register `≤I` as a preorder
  Order.cof (A → L)

and then port whatever API is useful so that we don't have to keep explicitly defining the Preorder (A → L) instance

[Nir Paz]

Violeta Hernández said:

I think there's two possibilities here. Either
a) We do not do the refactor, and we instead keep Order.cof defined as is. If any theorems are easier to state using @Order.cof α (· ≤ ·) then we just do that.
b) We do the refactor. We can still define the cofinality in the way that is required for PCF, we can do something like

def Order.SIdeal_cof {L A : Type*} [LinearOrder L] (S : Set (A → L)) (I : SIdeal A) :=
  have : Preorder (A → L) := sorry -- temporarily register `≤I` as a preorder
  Order.cof (A → L)

and then port whatever API is useful so that we don't have to keep explicitly defining the Preorder (A → L) instance

I'll make a quick test of (b)

[Violeta Hernández]

In fact, there might even be a "best of two worlds" approach here. We can define something like

def idealPreorder (I : SIdeal A) : Preorder (A → L) where
  le := (· ≤I ·)
  le_refl := sorry
  le_trans := sorry

Then, if it ever becomes useful to use the Preorder structure within a proof, we can simply use have : Preorder (A → L) := idealPreorder I.

[Violeta Hernández]

...although there is a problem with my plan: there is already a preorder structure on A → L! Specifically the one given by docs#Pi.preorder

[Violeta Hernández]

There are ways around this, of course. We could instead register a type alias on A → L, something like WithIdeal A L I = A → L with the order ≤I. Or, maybe we can just lower the priority of the Pi.preorder instance?

[Nir Paz]

Violeta Hernández said:

In fact, there might even be a "best of two worlds" approach here. We can define something like

def idealPreorder (I : SIdeal A) : Preorder (A → L) where
  le := (· ≤I ·)
  le_refl := sorry
  le_trans := sorry

Then, if it ever becomes useful to use the Preorder structure within a proof, we can simply use have : Preorder (A → L) := idealPreorder I.

Honestly I tend to think the Preorder structure won't be useful very often. From the little experimenting I did I always ran into weird defeq and rewrite problems when I had both a bundled and an unbundled version of the relations. And things involving both <I and ≤I have to be unbundled, so probably almost all definitions later on will be unbundled.

[Violeta Hernández]

Yeah, that makes sense.

Does solution (b) seem like it could work? If it does then I think it's by far the cleanest approach.

[Violeta Hernández]

I have my Order.cof refactor in some Mathlib branch, I think it's called something like vi.cofinal. It's basically ready, except I haven't finished porting some currently unused and soon to be deprecated theorems. That might be useful in testing things out.

[Nir Paz]

Thanks I was about to quickly write my own definition, I'll copy yours

[Violeta Hernández]

My main motivation for the refactor was that I thought it would make things simpler, and in my opinion, at least the cofinality file itself does become cleaner after the changes I made. But of course, if this refactor makes downstream projects (like this one!) more difficult, then I'm willing to change course.

[Violeta Hernández]

...sorry if i'm getting you dragged down into details that aren't ultimately mathematical

[Violeta Hernández]

if you want to go the quick and dirty route of just copying the current cofinality file then that's also fine

[Nir Paz]

Violeta Hernández said:

...sorry if i'm getting you dragged down into details that aren't ultimately mathematical

That's what I was hoping for haha. I'm a bit scared of rushing things and ending up having to redo 3000 lines of code because I didn't think things through.

[Nir Paz]

So this is good!

[Nir Paz]

Here's the definition with your new cofinality:

def Order.cof' (α : Type*) [Preorder α] : Cardinal :=
  ⨅ s : { s : Set α // IsCofinal s }, #s.1

instance instPreorderSIdeal {A L : Type*} [LinearOrder L] (I : SIdeal A) : Preorder (A → L) where
    le := (· ≤I ·)
    le_refl := by
      intro f
      dsimp [LE.le, le_SIdeal, ltSet]
      simp_all only [lt_self_iff_false, setOf_false, I.empty_mem]
    le_trans := sorry
    lt_iff_le_not_le := sorry

def Order.SIdeal_cof' {L A : Type*} [LinearOrder L] (S : Set (A → L)) (I : SIdeal A) : Cardinal :=
  @cof' S (@Subtype.preorder (A → L) (instPreorderSIdeal I) S)

I'm seeing if I can prove things about it now. btw I couldn't figure out how to define the preorder instance inside the definition so I did it outside with instPreorderSIdeal. It's probably because I'm doing something stupid with the syntax.

[Violeta Hernández]

Syntax looks fine to me, or at least, as fine as is possible given what we're trying to do

[Nir Paz]

I mean when I try to put it inside the definition it doesn't work, but it should be able to.

[Violeta Hernández]

Do note that instPreorderSIdeal should be a def rather than an instance, otherwise you're going to get some nasty diamonds

[Nir Paz]

Wait if the instance takes an explicit argument (the ideal) does it still get automatically synthed?

[Violeta Hernández]

No, but both instances will be found if you ever need to use either one of them on A → I later on, and that might cause problems

[Nir Paz]

Well I'm having a little trouble testing the new definition because there isn't a definition for cofinal sets yet. IsCofinal is bundled. The options are to define an SIdeal_cofinal predicate by using IsCofinal, going down the full bundled route, or define a more general unbundled cofinal predicate, and the test of the new def will be to show all the necessary api for it in the case of SIdeals.

I'll try the second one tomorrow. Thankfully we have unbundledSet.Bounded and Set.Unbounded already, so the chain stops here for now.

[Violeta Hernández]

Idea, can we perhaps use the same solution of Order.SIdeal_cof for other notions? That is, instead of using Set.Bounded (· ≤I ·) s or whatnot, we define something like Order.SIdeal_bddAbove s I as BddAbove with the ≤ relation given by ≤I. This should hopefully simplify notation, and it also means that if we ever have to port a theorem that exists on BddAbove to our new definition, we can do it more directly.

[Violeta Hernández]

This idea is compatible with both the idea that order relations should be bundled within Mathlib, and that they should be unbundled within the context of PCF, since we can always use the instPreorderSIdeal trick to use a definition expecting a bundled relation with our unbundled ≤I.

[Nir Paz]

There are really 2 ideas here. First is to have SIdeal_bounded S I, which we could define with either Set.Bounded or BddAbove. The second is to use BddAbove for it.

I like the first idea in either case, but it's less clear to me which option is better. With cof there is no unbundled version (I'm from the future) so using a preorder makes a lot of sense. But in this case both versions exist. Set.Bounded feels more natural, but BddAbove seems to have significally more API.

[Violeta Hernández]

Yeah, I would avoid Set.Bounded. It will almost surely get deprecated / removed in the near-ish future.

It's currently only used for a few theorems about ordinals (most of which I've already switched over to BddAbove), and within a single file with API that I wrote back in 2022, before I found out that BddAbove was a thing.

[Violeta Hernández]

(pinging @Yaël Dillies as someone who also had strong opinions on Set.Bounded and Set.Unbounded)

[Violeta Hernández]

@Nir Paz how are things going? Sorry I haven't been involved with this, I've been much busier this past month than expected.

I'm still trying to get my cofinality refactor into Mathlib, though this has led to other auxiliary refactors I'm still sorting out. Would it be ok if I temporarily copy over my code into your repo? That could also help us gauge if my plans really do work out as well as I expect.

[Nir Paz]

@Violeta Hernández same here, life got in the way hard and I didn't work on this for a while. I'll be back home in a few days and then make some progress.

So since there isn't much code yet I don't know if it would tell us much to use the new cofinality stuff, and there is actually a lot to do before we have to talk about cofinalities/true cofinalities for pcf, so the definitions we talked about that might get tricky with the refactor will probably just sit there for a while.

I'm planning on keeping the current old-cofinality defs for now and change them when the refactor happens