Mastodawn

@FishFace
Here's the paper from 1958:

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