$\begingroup$

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

Answers