ZFCfin, ZFC with infinity replaced by its negation is biinterpretable with PA, Peano Arithmetic. This result goes back to Ackermann,
- W. Ackermann. Die Widerspruchsfreiheit der allgemeinen Mengenlehre,
Math. Ann. 114 (1937), 305–315.
You may want to read about the early history of this theory here:
- Ch. Parsons. Developing Arithmetic in Set Theory without Infinity: some
historical remarks, History and Philosophy of Logic 8 (1987), 201–213.
That this is a reasonable setting for finitary mathematics has been argued extensively, see for example:
G. Kreisel. Ordinal logics and the characterization of informal notions of
proof, in Proceedings of the International Congress of Mathematicians. Edinburgh, 14–21 August 1958, J.A. Todd, ed., Cambridge
University Press (1960), 289–299.
G. Kreisel. Principles of proof and ordinals implicit in given concepts, in
Intuitionism and proof theory, A. Kino, J. Myhill, R. E. Veseley, eds.,
North-Holland (1970), 489–516.
That the theories are biinterpretable essentially means that they are the same, only expressed in different ways. More formally, we have a recursive procedure that assigns to each formula $\phi$ in the language of PA a formula $\phi^t$ in the language of ZFCfin and conversely, there is another recursive procedure that to each $\psi$ in the language of ZFCfin assigns a $\psi^{t'}$ in the language of PA. These procedures have the property that $\phi$ is provable in PA iff $\phi^t$ is provable in ZFCfin, and $\psi$ is provable in ZFCfin iff $\psi^{t'}$ is provable in PA, and moreover PA proves for each $\phi$ that it is equivalent to $(\phi^t)^{t'}$ and similarly ZFCfin proves of each $\psi$ that it is equivalent to $(\psi^{t'})^t$.
The translations are actually not too involved. In one direction, we can define in ZFCfin the class of natural numbers (the ordinals) and define its arithmetic operations the usual way, so that the resulting class satisfies PA. In the other direction, there is a nice argument: We can define in PA the relation $nEm$ iff there is a 1 in the $n$th place from the right in the binary representation of $m$. It turns out that the resulting structure consisting of the numbers seeing as the universe, with $E$ being membership is a model of ZFCfin. If we apply these procedures to the standard model $\omega$, we obtain $V_\omega$, and viceversa.
As for your question of whether one can do analysis in this setting, not quite. One can code some infinite sets in PA but not enough for all the arguments one needs in elementary analysis. A bit more formally, the subsystem of second order arithmetic known as $ACA_0$ proves the same arithmetic statements as PA, they are equiconsistent (provably in PA) and it is understood that it captures what we usually call predicativism. In particular, arguments requiring non-predicative definitions cannot be proved here. See:
Feferman, S. Systems of predicative analysis, i. The Journal of Symbolic Logic 29, 1
(1964), 1–30.
Feferman, S. Systems of predicative analysis, ii. The Journal of Symbolic Logic 33
(1968), 193–220.
The standard reference for systems of second order arithmetic is the very nice book:
You will find there many examples of theorems, results, and techniques in basic analysis that go beyond what $ACA_0$ can do. For example, the basic theory of Borel sets cannot be developed in $ACA_0$.
Your use of the word "intuitive" means that we're entering philosophical waters.
In ZFC, as you know, one can prove the formal version of the assertion "there is, up to isomorphism, only one model of the second-order Peano axioms". But as you are also aware, there are non-standard models of ZFC (assuming it's consistent), and these can have non-standard omegas.
Now to someone who adopts a certain kind of formalist attitude, there's no more to be said. For an intuitionist like Brouwer, on the other hand, our intuition of the natural numbers is basic, and not something that one can (or should even try) to formalize.
For most Platonists, it's simply assumed (an "article of faith") that the entities of mathematics exist in some "universe of abstractions". $\mathbb{N}$ is then a denizen of this universe. Our axiom systems, like PA and ZFC, capture some of the "facts" about this universe that we somehow know.
If you're asking for a precise mathematical definition of the natural numbers, I would say either "there isn't any", or "omega, working inside the ZFC axioms, or something along those lines".
Consider why you're sure that Goodstein's theorem holds for "the standard natural numbers". Surely it's because you believe in ZFC, in some sense. Or at least some fragment of ZFC. In other words, the power set of $\omega$ is ascribed some sort of reality.
Now consider ZFI, which is ZFC plus "there is an inaccessible cardinal". The consistency of ZFI does not follow from the consistency of ZFC. The statement Con(ZFI) is, however, a statement in PA (but of course not provable in PA). Are you sure it's true? Likewise for even stronger large cardinal axioms, or other extensions of ZFC that cannot be shown to be relatively consistent.
As it happens, John Baez and I carried on a lengthy discussion of these matters. Baez said:
Roughly, my dream is to show that “the” standard model is a much more nebulous notion than many seem to believe.
Along the way we considered the "ultra-finitists", who consider even such a notion as $2^{100}$ as unclear.
You'll find the conversation here. Post 5 and post 6 especially focus on your question.
One last comment: regardless of one's philosophical stance, if someone says "This is true of the standard natural numbers", the purely mathematical content of this claim usually amounts to "this can be proved for $\omega$ in ZFC" (or some fragment of ZFC). At least that's how I would understand their assertion.
Best Answer
Yes. If $\mathfrak{M}\models\mathsf{ZF}$-$\mathsf{Inf}$, the "natural numbers of $\mathfrak{M}$" are the things which $\mathfrak{M}$ thinks satisfy the following formula:
Informally, this says "$x$ is a finite ordinal." In $\mathsf{ZF}$-$\mathsf{Inf}$ alone, the standard recursive definitions of addition and multiplication of natural numbers behave as we expect. (These are tedious, though, which is why I'm omitting them; the point is that the "recursion data" witnessing any specific instance of $+$ or $\times$ is itself a finite object.)
What we can't do in this weaker framework is argue that the class defined by $\nu$ above is a set. But that doesn't pose an issue here.