I think they are redundant after all! Here's a proof that axiom 1 is redundant. Let $a,b\in V$, and consider $(1+1)\cdot (a+b)$. By axiom 7 and 8, this is equal to $(a+b)+(a+b)$; on the other hand by axiom 6 it is $(1+1)\cdot a + (1+1)\cdot b$, or $(a+a)+(b+b)$ by axiom 7 and 8. We can then use axioms 2, 3, 4 to show that
\begin{align*}
a^{-1} + (a+b) + (a+b) + b^{-1} &= a^{-1} + (a+a) + (b+b) + b^{-1}\\
b + a &= a + b
\end{align*}
and $V$ is Abelian.
Necessity of some of the other axioms:
4: Take $V=[0,\infty)$ under multiplication, and $K=\mathbb{R}$, with $z\cdot x \mapsto \begin{cases} x^z, & x\neq 0\\0, &x=0.\end{cases}$
5: Consider $K=\mathbb{C}$, $V=\mathbb{R}$ with $z\cdot x = \Re(z)x$.
6: Necessary once you toss out commutativity. Take $K=F_3$, and $V$ the Heisenberg group over $F_3$, with $z\cdot x = x^z$. Since all elements of $V$ have order dividing 3, axiom 7 is satisfied, but
$$\left(\left[\begin{array}{ccc}1 & 0 &0\\0 & 1 & 1\\0 & 0& 1\end{array}\right]\left[\begin{array}{ccc}1 & 1 & 0\\0 & 1 & 0\\0 & 0 &1\end{array}\right]\right)^2 \neq \left[\begin{array}{ccc}1 & 0 &0\\0 & 1 & 1\\0 & 0& 1\end{array}\right]^2\left[\begin{array}{ccc}1 & 1 & 0\\0 & 1 & 0\\0 & 0 &1\end{array}\right]^2.$$
7: Take $K=\mathbb{C}$, $V=\mathbb{R}$, and $z\cdot x = |z|x$.
8: See comment by Jyrki below.
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.
Best Answer
In my opinion, it is a matter of perspective.
If we work with fields as objects within mathematics (say, within the theory of ZFC), then the field axioms are basically definitions that decide which objects in our universe are fields, and which ones aren't.
On the other hand, if we view fields as models for a certain theory, then the field axioms describe the properties such a model has to satisfy. In this case I would argue that calling those properties axioms is more appropriate.
If I construct some object in a more powerful theory, and show that it satisfies the axioms, I could argue that the object is something that satisfies some definitions. On the other hand, from the viewpoint of the object itself, it is some structure that satisfies the axioms, it does not "know" that it is constructed as part of a larger, more powerful theory.
Similarly, the Peano Axioms could be taken as axioms that tell us which properties arithmetics has, but on the other side, we could see it as a collection of properties that together define a class of objects that behave arithmetical. For example, we could show that the natural numbers are such an object, and thus satisfy the definition of a "Peano object"
It is even quite natural within set theory to switch between these viewpoints. For example, you commonly encounter countable models of ZFC, which are just sets inside the universe and thus an object defined by the axioms of ZFC (although we could not prove its existence within ZFC, but that's another story).
On the other hand, such sets are models of ZFC, so from the perspective of the model itself, it looks as if you have a complete universe. Then the axioms of ZFC are actual axioms, telling you which statements are true, constructions are allowed to be made, etc.