[dilippkumar]

Thanks for the pointer.

I went down the rabbithole, and as far as I can tell, you have to axiomatically assume infinities are real in order to prove Goodstein’s theorem.

I challenge the existence of ordinal numbers in the first place. I’m calling into question the axioms that conjure up these ordinal numbers out of (what I consider sketchy) logic.

But it was a really fun rabbithole to get into, and I do appreciate the elegance of the Goodstein’s theorem proof. It was a little mind bending.

[skulk]

yes, if you want ordinal numbers in ZFC you need to take the axiom of infinity. Other than that it's a pretty straightforward construction. If you reject the axiom of infinity you also essentially reject all of standard analysis (using limits to study reals often implicitly invokes the axiom of infinity).