I am wondering what the difference between a definition and an axiom.

Isn’t an axiom something what we define to be true?

For example, one of the axioms of Peano Arithmetic states that ∀n:0≠S(n), or in English, that zero isn’t the successor of any natural number. Why can’t we define 0 to be the natural number such that it isn’t the successor of any natural number?

In general, why is an axiom not a definition?

Are there cases where we can formulate definitions as axioms or vice versa?

**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⊂y” is going to be an abbreviation for “∀z(z∈x→z∈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 ⊂ is not a part) you have simply put exactly the same formula on both sides; it is a logical truth of the form ϕ⟺ϕ.

**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 ∀n(x≠S(n)). What this is saying is that we can state a uniqueness condition, namely “∀y(y=x⇔∀n(y≠S(n))),” and, moreover, ∀y(y=0⇔∀n(y≠S(n))). This latter, however, is a substantial statement entailing the existence of a certain kind of object, and if we don’t have ∀n(0≠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 ∀n(0≠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 PA, and take as our new axiom Z(v)⇔∀n(v≠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 ∃x∀n(x≠S(n)), much less ∀n(0≠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 PA.

In either case, we see that definitions simply don’t do the work of axioms.

**Attribution***Source : Link , Question Author : wythagoras , Answer Author : Malice Vidrine*