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$.
You are trying to deduce something about the importance of 5th axiom only from the axioms itself, which is impossible.
The axioms by itself do not carry any significance. What is important is that the set defined by the axioms is (a) unique and (b) isomorphic to some real-world object (real-world natural numbers, as in "two apples" and "three oranges").
Giving away the fifth axiom means that:
a) Peano axioms no longer define a set of natural numbers, as there could be two non-isomorphic (and even not of the same cardinality) sets, both compatible with Peano axioms; rather they define a class of sets, each containing a subset, isomorphic to $\{0, 1, 2, 3, \ldots\}$. For example, let us consider the set $\mathbb N$ in its usual sense, and the set $\mathbb C \setminus {\mathbb N}^+$. Both sets fulfill the Peano axioms (except for the fifth one), but they are quite different in itself.
b) Of course, the second set from the previous paragraph has nothing in common with a real=world object called "the natural numbers".
Best Answer
Axioms are not "defined to be true"; I'm not even sure what that would mean. What they are is evaluated as true. Practically speaking all this means is that in the mathematical context at hand, you're allowed to jot them down at any time as the next line in your proof.
Definitions have virtually nothing to do with truth, but are instead shorthand for formulae or terms of the language. Using the language of set theory as my example, "$x\subset y$" is going to be an abbreviation for "$\forall z(z\in x\to z\in y)$". If you were to put these two expressions on either side of a biconditional symbol, it would of course be true, but not because we have assumed it to be true, but rather because when you have unpacked everything into the actual formal language of set theory (of which $\subset$ is not a part) you have simply put exactly the same formula on both sides; it is a logical truth of the form $\phi\iff\phi$.
Update: I realized this answer would be more complete if I addressed the example you show above with $0$, and addressed comments made below by @MauroALLEGRANZA.
Let's say I want to define $0$ as a shorthand for the unique $x$ such that $\forall n(x\neq S(n))$. What this is saying is that we can state a uniqueness condition, namely "$\forall y(y=x\Leftrightarrow \forall n(y\neq S(n)))$," and, moreover, $\forall y(y=0\Leftrightarrow \forall n(y\neq S(n)))$. This latter, however, is a substantial statement entailing the existence of a certain kind of object, and if we don't have $\forall n(0\neq S(n))$ as an axiom, how will we derive it? It should be obvious that merely having a way to say "predecessor-less object" does nothing to guarantee the existence of a predecessor-less object; at best, you've shifted the burden of the axiom $\forall n(0\neq S(n))$ onto another axiom that circumlocutes the constant symbol $0$. Having two ways to say "predecessor-less object", one in the original language and one in a metalanguage, doesn't do any more work than only having one way to say it.
Sig. Allegranza brought up a variant where the defined symbol becomes a genuine formal symbol of an expanded formal language, and we only look at extensions of the theory axiomatizing the equivalence of the new predicate with a formula of the old language. In this case the axiom stating the equivalence is not even utterable in our old language, much less will it have any consequences for the models of said language. With our above example, we might have the new one-place predicate $Z(v)$ added to the language of $\mathsf{PA}$, and take as our new axiom $Z(v)\Leftrightarrow \forall n(v\neq S(n))$. That is, we have a predicate, now part of the formal language, that is equivalent to the statement that $v$ is predecessor-less. But now that there's a formal axiom about $Z$, just try to derive $\exists x\forall n(x\neq S(n))$, much less $\forall n(0\neq S(n))$, from just this axiom alone. It should be easy to see that you're not going to be able to derive any non-trivial sentences in the language of $\mathsf{PA}$.
In either case, we see that definitions simply don't do the work of axioms.