Extension by definition

Summary

In mathematical logic, more specifically in the proof theory of first-order theories, an extension by definition formalizes the introduction of a new symbol by means of a definition. For example, it is common in naive set theory to introduce a symbol $\emptyset$ for the set that has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant $\emptyset$ and the new axiom $\forall x(x\notin\emptyset)$, meaning "for all x, x is not a member of $\emptyset$". It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one.