Are definitions axioms? I just want to ask a very elementary question.
When we introduce a "definition" in a first order logical system. For example when we say 
Define: $Empty(x) \iff \not \exists y (y \in x) $ 
Isn't that definition itself an "axiom", call it a definitional axiom.
I'm asking this because the one place predicate symbol Empty() is actually new, it is not among the listed primitives of say Zermelo, which has only identity and membership as primitive symbols. 
So when we are stating definitions are we in effect stating axioms? but instead of being about characterizing a primitive, they are definitional axioms giving a complete reference to a specified set of symbols in the system.
Is that correct?
Now if that is the case, then why we don't call it axiom when we state it, I mean why we don't say for example:
Definitional axiom 1) $Empty(x) \iff \not \exists y (y \in x)$
Zuhair
 A: A definition can indeed not be proven nor disproven and can be considered an axiom.
A: I've already asked myself this question, and comparing my knowledge with other people opinions, I found that the answer is no.
Definitions are not axioms; definitions are simply shorthands of a bigger and longer string of symbols.
For example, in set theory we always see that the espression "$x \subseteq y$" is defined as:
$$x \subseteq y \Longleftrightarrow \forall z(z \in x \Rightarrow z \in y ). $$
Note that between "$x \subseteq y$" and "$\forall z(z \in x \Rightarrow z \in y)$" there is the "$\Longleftrightarrow$" (I used the longer version to emphasise that the statement is a definition).
But this statement is written in our imaginary "computer" or "piece of paper" where it's written all the mathematics (at least, I like to think about it like that), where everything is either an axiom or something proved using the axioms or the theorems proved before, this statement should be a theorem or an axiom too.
So, formally thinking about it, it should be a theorem or an axiom. It isn't a theorem, because it hasn't been proved, so it should be an axiom. So giving this statement, it looks like we are adding a new axiom to our theory, and this would mean that all the definitions that have been given in mathematics history are axioms! This wouldn't make sense.
What is really going on here, is that the statement is actually an abbreviation for a longer string of symbols, namely "$\forall z(z \in x \Rightarrow z \in y)$". Abbreviations are required to talk in an easier way of mathematical relations. Formally speaking, shorthands of symbols are a "new" informal version of the formal language symbols. 
Usually, mathematics is done in an informal level, or at least not as formally as when we give the axioms of mathematics. The axioms are stated in a formal language, but then nothing stop us to use abbreviations of them  and still do mathematics correctly. Somethimes, in proofs or definitions, we even use our informal natural language. 
So definitions -at least in high level mathematics- are not given in a formal level. We could consider them some "meta"-statements that makes the formal language of the theory more comfortable to us. Even if you don't like to see it like that, at least we know for sure that definitions tend to make the the mathematical language more and more informal. But remember that hidden behing those shorthands, there are a lot of mathematical formal strings! Take for example the definition of limit,
$$\lim_{x \to c} f(x) = L \Longleftrightarrow_{def}
 \forall \epsilon \in \mathbb{R^+} \exists \delta \in \mathbb{R^+} \forall x \in D: \big(0 < \mid x-c \mid < \delta \Rightarrow \mid f(x) - L \mid < \epsilon \big)$$
it is an abbreviation of a very complicated string of symbols -that are shorthand themselves-! So, when you are proving that $$\lim_{x \to 2}x^2 = 4$$ you are really proving all that complicated stuff with the $\epsilon$-$\delta$ definition of limit with $f(x)=x^2, c= 2$ and $L=4$. 
We could consider also the definition of definite integral, that is a new term that we introduce to abbreviate a much more complicated one (a limit). In that case, what is being defined is a term, so we use the equality simbol $=$, but it's the same idea that we use with $ \Longleftrightarrow.$ It's just a shorthand.
In conclusion, if you want to be clear in a formal point of view, I personally would mark that the statement is a definition using $\Longleftrightarrow_{def}$ and $=_{def}$ (as I used before for the limit definition), so that you can clearly see that the expression is not a strictly formal string of symbols anymore and it's rather an abbreviation. 
I hope this helps :D
