Extension by definitions

In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol ${\displaystyle \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 ${\displaystyle \emptyset }$ and the new axiom ${\displaystyle \forall x(x\notin \emptyset )}$, meaning "for all x, x is not a member of ${\displaystyle \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.