ZF ordinal formalization

Stream: maths

[RustyYato]

I'm trying to formalize ordinals as transitive sets based on ZF axioms (no choice, I'm polyfilling Classical logic via axiom of excluded middle directly without going through Classical.choice).

I'm having trouble formalizing a ⊂ b -> a ∈ b given two ordinals a and b. I think this is required or very helpful to prove membership trichotomy, which I haven't done yet. I've linked this below.

The strategy I'm using is based off of this document: https://www.ucl.ac.uk/~ucahcjm/ast/ast_notes_2.pdf, and ProokWiki. But I just realized both proofs seem to be using properties of ordinals that haven't been established yet. And ProofWiki seems to be using circular proofs.

So I'm stuck. My strategy so far is to show that since b \ a is nonempty (since a is a proper subset of b), there exists a minimal element (let's call it s). Then prove s = a, and since s ∈ b \ a, it follows that a ∈ b. This is taken from ast_notes_2.pdf. I can prove that s ⊆ a, but the converse a ⊆ s is proving challenging. This step in ProofWiki appeals to membership trichotomy (which in turn appeals back to this very proof no matter what path is taken through ProofWiki), and in ast_notes_2.pdf it appeals to the well ordering of set membership.

Also, because ∈ is a l.o. of β, γ ∈ α implies that γ ∈ s, thus α ⊆ s

Where l.o. is linear order, but this also seems to depend on trichotomy which is only established later. So I'm not sure how to translate this proof to Lean.

https://github.com/RustyYato/zfc/blob/5900e67043afda4b4ab51611885fa0dd6d451fff/Zfc/Ordinal.lean#L121-L154

I've defined Ordinals as def Zf.IsOrdinal (a: α): Prop := ∀x ∈ a, x ∩ a = x. Which I think is correct, since it is equivalent to Definition 3 in Proof Wiki, if we take set membership to be the relation. https://proofwiki.org/wiki/Definition:Ordinal. However I'm not sure if this enforces that set membership well orders a. It was able to prove that ω and all Nat are ordinals, so it not obviously wrong, but that isn't proof that this definition is correct.

I have also proven that this definition is equivalent to def Zf.IsTransitive (a: α): Prop := ∀x ∈ a, x ⊆ a, so that seems like strong proof that it is correct.

tldr: I'm having trouble formalizing a ⊂ b -> a ∈ b given two ordinals a and b, and any pointers would be very helpful.

[Sky Wilshaw]

Your definition of ordinal has a bug: an ordinal is a transitive set of transitive sets, not a transitive set. For instance, {0, {0}, {{0}}} is considered an ordinal by your program.

[RustyYato]

Oh wow that would do it. Thanks! I'll see how I can fix that

[RustyYato]

I guess using Definition two from ProofWiki would be easiest

https://proofwiki.org/wiki/Definition:Ordinal/Definition_2

Looks like that is a promising direction, thanks!

[Violeta Hernández]

I've been able to find a very minimal definition of ordinals in the past:

/-- A transitive set is one where every element is a subset. -/
def IsTransitive (x : ZFSet) : Prop :=
  ∀ y ∈ x, y ⊆ x

/-- A set `x` is a von Neumann ordinal when it's a transitive set, that's transitive under `∈`. We
prove that this further implies that `x` is well-ordered under `∈`.

The transitivity condition is written in an even weaker form, where `a ∈ b` and `b ∈ c` imply
`a ∈ c` when only `c ∈ x` and not `a ∈ x` or `b ∈ x` are known a priori. -/
def IsOrdinal (x : ZFSet) : Prop :=
  x.IsTransitive ∧ ∀ a b c : ZFSet, a ∈ b → b ∈ c → c ∈ x → a ∈ c

[Violeta Hernández]

See my PR #15793

[Violeta Hernández]

This is a much weaker definition than any of the ones in ProofWiki. I've proven that it's equivalent to being a transitive well-ordered set in a Lean 3 branch I'm currently working on porting.

[RustyYato]

Cool, actually your PR was why I started this! Since this seems like a step up from my last adventure in Lean (proving things about the Naturals, and defining the Reals). I'm still wrapping my head around that definition.

I'm curious, what's the benefit of a weaker definition if it is equivalent to the standard definition?

Currently I'm using this definition

def Zf.IsTransitive (a: α): Prop := ∀x ∈ a, x ⊆ a

def Zf.IsTotalOrder (a: α): Prop := ∀x y, x ∈ a -> y ∈ a -> (x ∈ y ∨ x = y ∨ y ∈ x)

structure Zf.IsOrdinal (a: α): Prop where
  IsTransitive: IsTransitive a
  IsTotalOrder: Zf.IsTotalOrder a

and am currently working on addition, and am having some trouble there, but I think I can figure it out.

[Antoine Chambert-Loir]

@Violeta Hernández I presume that your definition makes use of the axiom of regularity/foundation. Set theorists usually find it interesting to have a definition of ordinals that avoids this axiom because if you don't add it, and take the class of sets which are “regular” (there is no chain of element containing an element containing…), then it gives you a model of Set theory that satisfies the regularity axiom, hence indicates some independence of that axiom with respect to the other ones.

[Violeta Hernández]

I hadn't noticed that, but yes. A quine atom would be an ordinal under this definition.

[Violeta Hernández]

"A well-ordered set under ∈" is probably the correct definition under such generality