@FishFace
Here's the paper from 1958:

http://matwbn.icm.edu.pl/ksiazki/fm/fm46/fm4611.pdf

Where reference [7] is
https://eudml.org/doc/213059 where 𝔖 is defined to have ur-Elements

Prior work:
(𝔖 or ZF) + AC ⊢ Fin₁ = Fin₁ₐ = Fin₂ = Fin₃ = Fin₄ = Fin₅ = Fin₆ = Fin₇

EScbO = the axiom "Every set can be (linearly, strictly) ordered"

Theorem 1 is
(𝔖 or ZF) ⊢ Fin₁ ⊆ Fin₁ₐ ⊆ Fin₂ ⊆ Fin₃ ⊆ Fin₄ ⊆ Fin₅ ⊆ Fin₆ ⊆ Fin₇

Theorem 2 is
(𝔖 or ZF) ⊢ ( R Orders A ∧ A ∈ Fin₂ ) → A ∈ Fin₁

Theorem 3 is
(𝔖 or ZF) + EScbO ⊢ Fin₁ = Fin₁ₐ = Fin₂

Theorem 4 is
𝔖 + EScbO ⊢ Fin₁ ≠ Fin₃

Theorem 5 is
𝔖 + EScbO ⊢ Fin₃ ≠ Fin₄

Theorem 6 is
𝔖 + EScbO ⊢ Fin₄ ≠ Fin₅

Theorem 7 is
𝔖 + EScbO ⊢ Fin₅ ≠ Fin₆

Theorem 8 is
𝔖 + EScbO ⊢ Fin₆ ≠ Fin₇

Theorem 9 is
𝔖 ⊢ Fin₁ ≠ Fin₁ₐ

Theorem 10 is
(𝔖 or ZF) ⊢ ( Fin₁ₐ = Fin₂ → Fin₁ = Fin₁ₐ )

Theorem 11 is
𝔖 ⊢ Fin₁ₐ ≠ Fin₂

As it so happens, I know of a proof:
ZF + CC ⊢ Fin₁ = Fin₄

Where the axiom of Countable Choice, CC, can be expressed as ⊢ (𝑥 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))

See https://us.metamath.org/mpeuni/fin41.html where CC is used only for the line ⊢ (ω ≼ 𝑥 ↔ ¬ 𝑥 ≺ ω)

So good guess!

And JDH on Substack isn't requiring payments which disadvantages him with respect to SEO, so please share the links. #AxiomOfCountableChoice #AxiomOfChoice #SetTheory #CountableChoice

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)