hereditarily

Stream: maths

[Violeta Hernández]

Thinking about the newly added docs#Set.hereditarily, it occurred to me that it should also have applications in game theory as well. Most notably, short games are hereditarily finite, and impartial games are hereditarily equal to their negatives.

[Violeta Hernández]

I was going to suggest this

def hereditarily' {α} (r : α → α → Prop) [is_well_founded α r] (p : α → Prop) : α → Prop
| x := p x ∧ (∀ y, r y x → hereditarily' y)
using_well_founded {
  rel_tac := λ _ _, `[exact is_well_founded.to_has_well_founded r],
  dec_tac := `[assumption] }

but for some reason I get an app_builder exception.

[Violeta Hernández]

Unfortunate that this typeclass doesn't seem to interact well with the equation compiler.

[Violeta Hernández]

Oops forgot to ping @Junyan Xu

[Junyan Xu]

Actually I'm not sure hereditarily is necessary, given that it could be defined nonrecursively as a forall using docs#relation.refl_trans_gen. For pgames we already have docs#pgame.subsequent defined in terms of trans_gen, so there's even less need to use hereditarily.

[Yuyang Zhao]

We can change the definition of docs#Set.hereditarily if that's better.

[Violeta Hernández]

Junyan Xu said:

Actually I'm not sure hereditarily is necessary, given that it could be defined nonrecursively as a forall using docs#relation.refl_trans_gen.

I think having both the inductive definition and the equivalence with the transitive closure is good.

[Violeta Hernández]

Same applies with pgames

[Violeta Hernández]

Really, if there's enough of a need for it, we can also create a named relation for the reflexive transitive closure of ∈. I wouldn't ditch hereditarily even then though. If there's more than one canonical way to write something down, that often is good justification for making a definition.

[Eric Wieser]

That argument only works if we add the lemma connecting the refl_trans_gen spelling to the new definition :)

[Violeta Hernández]

Oh of course, that's part of the plan

[Violeta Hernández]

Wait, I think I have a better idea.

[Violeta Hernández]

We could add an inductive lemma on refl_trans_gen itself

[Violeta Hernández]

Since after all, refl_trans_gen applies more generally than for just well-founded relations

[Violeta Hernández]

...oh wait, the inductive lemma in question would just be the induction principle for refl_trans_gen

[Violeta Hernández]

Yeah... Maybe we don't need hereditarily at all

[Violeta Hernández]

I just realized

[Violeta Hernández]

"Hereditarily transitive" is too strong of a condition

[Violeta Hernández]

A transitive set of transitive sets is already an ordinal

[Violeta Hernández]

Since "hereditarily p" for a transitive set is exactly the same as "p for all members"

[Yuyang Zhao]

I proved it in #18329 as Set.is_ordinal_iff_mem_is_transitive

[Violeta Hernández]

I see

[Violeta Hernández]

Surely that should be the definition instead, then? It should be strictly easier to prove

[Violeta Hernández]

But then, notice the definition from my PR is quite simple to prove for a transitive set of transitive sets

[Violeta Hernández]

theorem is_ordinal_of_transitive_of_mem_transitive (hx : x.is_transitive)
  (H : ∀ y : Set, y ∈ x → y.is_transitive) : x.is_ordinal :=
⟨hx, λ y z w hyz hzw hwx, (H w hwx).subset_of_mem hzw hyz⟩

[Violeta Hernández]

Not to be confrontational, but I'd rather we go with my definition for two reasons:
a. It seems like the simplest statement to prove among all the equivalences - a transitive set transitive under ∈, a transitive set of transitive sets, and a hereditarily transitive set, are all easily proven to satisfy this; the converses aren't immediate
b. I've already gotten a lot done with it

[Violeta Hernández]

For reference, here's the equivalent statements (I know of):

1. A transitive set x where y ∈ z ∈ w ∈ x implies y ∈ w (my definition)
2. A transitive set, transitive under ∈
3. A transitive set, trichotomous under ∈
4. A transitive set, strictly totally ordered under ∈
5. A transitive set, well-ordered under ∈
6. A transitive set of transitive sets
7. A hereditarily transitive set

[Violeta Hernández]

5 is the Wikipedia definition, but is far too strong (as seen by all the other statements). Listing all the immediate (one-line) implications:

• 1 ↔ 2
• 5 → 4 → 2 or 3
• 7 → 6 → 2

[Violeta Hernández]

Takeuti & Zaring use 3, but I imagine proving ∀ (y ∈ x) (z ∈ x), y ∈ z ∨ y = z ∨ z ∈ y would be somewhat cumbersome, which only leaves 1 and 2

[Yuyang Zhao]

That's ok, I don't strongly request using my definition.

[Violeta Hernández]

And notice that 1 is just 2 without redundant conditions, since the transitivity condition gives you y ∈ x, z ∈ x, w ∈ x from y ∈ z ∈ w ∈ x

[Violeta Hernández]

Oh alright

[Violeta Hernández]

Again, hope I'm not coming off in a negative way, I've just been thinking about this for a while now

[Violeta Hernández]

On this topic, I just opened a new PR just containing the definition and easiest lemmas from my other larger PR

[Violeta Hernández]

#18513

[Violeta Hernández]

Should have done this much earlier, I apologize

[Violeta Hernández]

This doesn't depend on the sym2.game_add stuff or anything like that

[Mario Carneiro]

Violeta Hernández said:

Surely that should be the definition instead, then? It should be strictly easier to prove

It is extremely rare to have to prove that a random set is an ordinal. Most of the time you get ordinals out of very general constructions which are always ordinal-producing by construction. So I don't see this as a strong argument - the definition of ordinal should be almost completely irrelevant because it is so heavily dependent on its robust API

[Mario Carneiro]

In such a situation, I usually bias toward short definitions

[Violeta Hernández]

I think our definition should still make the least amount of assumptions possible.

[Violeta Hernández]

And I think the definition I've went with also meets this criterion