> I don't agree it's a different problem, as OP pointed out, ZF with the axiom of infinity replaced by its negation is equal to first order Peano Arithmetic, so

> I don't agree it's a different problem, as OP pointed out, ZF with the axiom of infinity replaced by its negation is equal to first order Peano Arithmetic, sometimes referred to as the theory of hereditarily finite sets. Being unable to talk about the set of natural numbers except through encodings (which is how you do infinitary math without infinity) is different than having a symbol for the set of natural numbers which may or may not have additional properties which cannot be discerned within the theory itself (e.g. Lowenheim-Skolem). > Said theory is also sufficient for all intents and purposes of doing real analysis. Large chunks of real analysis can indeed be carried out, but significant amounts cannot. Many theorems in analysis concerning perfect sets are not provable in that theory (usually stated as ACA0).