Notation guide (adapted from Metamath):

• 𝜑, a metavariable standing for any logical formula, abbreviates the conjunction of all hypotheses listed for a given proposition; writing each line as ⊢ (𝜑 → …) puts the theorem in "deduction form," which can be easier to apply in #Metamath.

• ⊢ 𝜑 asserts that 𝜑 is true; the turnstile is descended from #Frege's own Urteilsstrich (judgment stroke).

• 𝐴𝑅𝐵 means the ordered pair ⟨𝐴, 𝐵⟩ is an element of 𝑅, or we could say 𝐵 immediately follows 𝐴

• 𝐵 = (𝑅‘𝐴) means 𝐵 is the unique set such that 𝐴𝑅𝐵 is true (when such a 𝐵 exists) which means 𝑅 is function-like when restricted to operating on the singleton {𝐴}

• (𝑅”𝐴) is the image of 𝐴

• dom 𝑅 is the domain of 𝑅, the class of all sets 𝑥 such that there is a set 𝑦 that would make 𝑥𝑅𝑦 true.

• Fun 𝑅 is true when 𝑅 is function-like for all sets in its domain.

• ◡𝑅 is the converse of 𝑅 so 𝐴◡𝑅𝐵 iff 𝐵𝑅𝐴

• (tc‘𝑅) is the #TransitiveClosure of 𝑅 (Metamath uses (t+‘𝑅) which can be awkward.) Whitehead and Russell use the term ancestral to describe how 𝐴(tc‘𝑅)𝐵 means 𝐴 is some “ancestor” of 𝐵. Alternately, we can say 𝐵 eventually follows 𝐴.

• V is the universal class, every set is a member, and only sets may be members of any class. After Frege’s later work ran into Russell’s Paradox, it was discovered that not every class {𝑥 | 𝜑} makes sense as a set and so we need the hypothesis ⊢ (𝜑 → 𝐴 ∈ V) before we can talk about the function value of 𝐴 or the ordered pair ⟨𝐴, 𝐵⟩ being an element of 𝑅. V is not italic because it is a constant symbol, like tc, dom, and Fun.

@FishFace Update:

What I refer to as EScbO is usually called #LO the #LinearOrdering principle.

⊢ ∃y ∀a ∈ x ∀b ∈ x ∀c ∈ x (¬ aya ∧ ((ayb ∧ byc) → ayc) ∧ (ayb ∨ a = b ∨ bya))
or using abbreviations in #Metamath
⊢ ∃y y Or x

I think AC implies LO, but LO is independent of DC and CC.

So we have { 1, 2 } ∈ Fin₁ ⊆ Fin₁ₐ ⊆ Fin₂ ⊆ Fin₃ ⊆ Fin₄ ⊆ Fin₅ ⊆ Fin₆ ⊆ Fin₇

If a set is in Fin₁ then it is considered finite by all the other definitions.

But since the axiom of choice is equivalent to saying every set can be well-ordered, if we accept it VII-finite sets are equinumerous with a finite ordinal and so Fin₇ ⊆ Fin₁ and so the differences between these definitions collapse and ZF becomes ZFC, which is a widely accepted basis for Set Theory.

My consultation with math resources was inspired by a blog post:

https://www.infinitelymore.xyz/p/what-is-the-infinite

#Metamath #ZFC #SetTheory #AxiomOfChoice #FiniteSet #Infinity

Also from #Metamath I learned #infinity is hard to think about.

A . Lévy in "The independence of various definitions of finiteness" Fundamenta Mathematicae, 46:1-13 (1958) established 8 distinct set-theoretic definitions of a #finiteSet which in ZF cannot be equated without the #AxiomOfChoice

I-finite -- equinumerous with a finite ordinal. // i.e. admits a finite well-order (Numerically Finite) ⟺ the powerset of its powerset is Dedekind finite ⟺ every collection of its subsets has a maximum element ⟺ every collection of subsets has a minimal element

Ia-finite -- not the union of two sets which are not I-finite

II-finite -- every possible way of finding within the set a chain of nested subsets always contains a maximum element (Tarski finite) ⟺ equivalently every such chain contains its intersection ⟺ (Linearly Finite) ⟺ (Stäckel Finite)

|||-finite -- It's powerset is |V-finite finite, (weakly Dedekind finite) ⟺ cannot be mapped onto ordinal ω ⟺ doesn't contain a chain of subsets which can be placed in order with ω

|V-finite -- doesn't have a proper subset which is equinumerous to itself. (Dedekind finite) ⟺ there is no 1-1 map from ordinal ω to it ⟺ it is strictly dominated by the disjoint sum of it and a singleton (acts finite under successor)

V-finite -- it is either empty or strictly dominated by the disjoint sum of it with itself (acts finite under addition)

VI-finite -- it is either empty, a singleton or strictly dominated by the Cartesian product of it with itself (acts finite under multiplication)

VII-finite -- it cannot be infinitely well-ordered (not equiinumerous with the ordinal ω or any larger ordinal)