What is exactly the difference between a definition and an axiom?

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 $\forall n:0\neq 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?


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.


A definition is a conservative extension of the language by a new symbol and some axioms involving this symbol. The key word here is conservative; in general axioms strengthen the system in question, while definitions are not allowed to do so.


In this instance, I'm taking Peano arithmetic to be defined in the first-order theory over functions $0, s, +, \times$ of arity 0, 1, 2, 2 respectively. The symbol $0$ is just that - a symbol. It needs no definition in this language. It already exists. We need the axioms to tell us what we're allowed to do with these symbols. You want to "define" how $0$ behaves, and you do this by setting up some axioms.

Completely alternative point of view: the reason we haven't defined $0$ to be the thing such that no successor is $0$, is because such a thing doesn't a priori exist. There's nothing in the other axioms to tell us that $0$ behaves in this special way: we can't prove it exists, but nor can we prove that it doesn't. For instance, I could define an eggly function $\mathbb{C} \to \mathbb{C}$ to be entire and bounded but non-constant. It takes a bit of work to show that no eggly functions exist, but it is a fact. Therefore, this is very much a definition and not an axiom: we have shown that no eggly functions can exist. On the other hand, the Peano axiom that "induction holds" is something we simply know to be true, but it's so basic that it's just not possible to prove it or its converse. Therefore, we just say "the induction axiom is true", and call it an axiom. Axioms are true by fiat; definitions must be proved to be valid.

Additionally, consider the following. There's an axiom of the set theory ZF that an empty set exists. However, this can be derived from the axiom of infinity (which asserts that a set exists) and the axiom of comprehension (which lets us select a subset for which "false" holds). Therefore, you could quite reasonably remove the empty-set axiom and instead supply a definition of "empty set". In this instance, we supply the axiom because it really seems like overkill not to - it's a matter of aesthetic. We like to have an axiom which says "there is an empty set", even if it's really a theorem that can be derived from the other axioms, because it's just a bit neater.

To summarise, the line is not always very clear-cut, and it's not always clear whether something should be an axiom or a definition. Both can be appropriate, and it may be down to what is most aesthetically pleasing.


From a proof theory perspective, there is no difference. They are both effectively announce the truthhood of something without providing a proof thereof.

The difference arises when one applies model theory, which is required to apply the mathematical results (whether applied explicitly or implicitly). A definition is wholly contained within the mathematical system. One cannot disagree with it because it is simply an artifact of the way the system is written. One can also sometimes rewrite the system to exclude a definition which is "offensive."

An axiom, on the other hand, reaches outside towards the system that is being modeled. These axioms define the range of problems for which the mathematical systems are applicable. If one disagrees with an axiom, it simply states that the mathematical system is not applicable to a particular class of problems because you are not willing to accept the axioms.

From a practical perspective, there is some difference between writing a definition from writing an axiom. You have a little more freedom when naming and defining definitions, because you wholly control their meaning. When it comes to axioms, you tend to have to interact with what others define things to mean. As an example, within a mathematical system, I may elect to redefine "+" to have a meaning not usually associated with addition. This may be effective for visually depicting a concept and making sure the reader remembers it (so long as it is close enough to addition to not give the cognitive dissonance). However, if I provide an axiom which requires something be "continuous," and my use of "continuous" is actually not the same as the more agreed upon definition, now I can cause great confusion. The axioms are something which are typically addressed up front, before your own style has leaked into the notation and verbiage. If one uses a standard terminology in the axioms, it is more likely to confuse someone who is scanning across a bunch of papers looking for a solution to their problem.

A great example of an axiom shows up in physics: "a closed system." A closed system is one where no energy crosses the border of the system (derivative of energy flux is zero). This could be a definition in some abstract scenarios, but in almost all cases it is an axiom. Not all systems satisfy the "closed system" axiom (in fact, technically speaking, no system 100% satisfies it except perhaps the universe as a whole). The applicability of any mathematical modeling under the axiomatic assumption of a closed system is limited by how well "closed system" describes the system someone is exploring.

On the other hand, there could be cases where one would elect to use it in the sense of a definition. For example, if you were working with an abstract mathematical construct and you found a subset of this construct which has behaviors similar to a closed system in thermodynamics, you may elect to define a closed system to match that subset of your construct. One might be exploring a class of ring generators, and notice that some of them demonstrate a behavior like entropic decay. One may choose to identify these behaviors with thermodynamics terms like "closed system" because it does a good job of capturing the relationships you are focused on. However, since it is purely encapsulated within your mathematics, it's okay if it's not "the official definition." That definition does not have to interact with the thousands of papers on thermodynamically closed systems quite as much as you would if your construct was only applicable to closed systems. In that case, you would want to treat it as an axiom.

In all, it's effective to think of a "definition" as something internal to your work, while an "axiom" tends to connect to the greater body of work, defining which classes of problems allow the application of your work.