Partial well-orders

Stream: maths

[Violeta Hernández]

I'm currently not very satisfied with the API on docs#PartiallyWellFoundedOn

[Violeta Hernández]

I want to talk about partially well-ordered types, in the context of defining poset games, as these are the posets for which the game is guaranteed to terminate.

[Violeta Hernández]

But currently I can only talk about partially well-founded sets. Of course I could use something like PartiallyWellFoundedOn univ but that seems annoying.

[Violeta Hernández]

I'm also not convinced our definition of partial well-founded orders is the best one. "Any infinite sequence indexed by naturals has an increasing subsequence of length 2" is intuitive and relatively concise. But I feel like there's an easier definition we could be using, which allows us to better make use of existing API:

def PartiallyWellOrdered {α : Type*} (r : α → α → Prop) : Prop :=
  WellFounded r ∧ ∀ t : Set α, IsAntichain r t → t.Finite

[Violeta Hernández]

Of course, we can then prove our current definition as an equivalence

[Violeta Hernández]

So here's my idea:

1. Make an Order/PartiallyWellFounded file containing the (simplified) definition of a partially well-founded type, plus some basic API mimicking the current docs#PartiallyWellFoundedOn API.
2. Redefine PartiallyWellFoundedOn as PartiallyWellFounded on a subtype (just as we defined docs#WellFoundedOn in terms of docs#WellFounded).
3. Profit

[Violeta Hernández]

@Daniel Weber Does any of this make sense?

[Daniel Weber]

I'm not sure this is equivalent — the naturals numbers are a wqo with ≤, but ≤ isn't well founded

[Daniel Weber]

I think the main benefit of using inductive types for well foundedness is that it lets you use well founded induction, but I don't think that's a common use case for wqos

[Violeta Hernández]

Daniel Weber said:

I'm not sure this is equivalent — the naturals numbers are a wqo with ≤, but ≤ isn't well founded

I think there might be some notational issues here. When we say (N, ≤) is a wqo, do we mean that N is a wqo with relation ≤, or that the (total) order corresponding to N is a wqo?

[Violeta Hernández]

These are different statements. The distinction might be clearer if you replace wqo by well-founded.

[Violeta Hernández]

Actually, question. Is a preorder with infinitely many order-equivalent elements a wqo?

[Violeta Hernández]

It has no infinite ≤ antichains but it does have an infinite < antichain

[Daniel Weber]

I think I'm a bit confused - what do you mean by partially well founded? There is no PartiallyWellFoundedOn - there's docs#Set.PartiallyWellOrderedOn, and it means what you said - that every infinite sequence has two elements an increasing subsequence of length 2.

[Daniel Weber]

Violeta Hernández said:

Actually, question. Is a preorder with infinitely many order-equivalent elements a wqo?

If there's some element a such that ¬r a a then r isn't a wqo, as the infinite sequence formed by a constant a doesn't have an increasing subsequence, so it doesn't really make sense to consider wqo with respect to <, only ≤.
The preorder may or may not be wqo with respect to ≤

[Violeta Hernández]

Partially well founded should be partially well ordered which is quasi well ordered. I'm just getting the terms mixed up.

[Violeta Hernández]

Daniel Weber said:

Violeta Hernández said:

Actually, question. Is a preorder with infinitely many order-equivalent elements a wqo?

If there's some element a such that ¬r a a then r isn't a wqo, as the infinite sequence formed by a constant a doesn't have an increasing subsequence, so it doesn't really make sense to consider wqo with respect to <, only ≤.
The preorder may or may not be wqo with respect to ≤

Ah that's interesting, so a well-founded order is measured with respect to <, but a partial well order is measured with respect to ≤