Extensions by definitions

extensions-by-definitions.md

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 $\varnothing$ for the set which has no member i.e. empty set.

In the formal setting of first-order theories, this can be done by adding to the theory a new constant $\varnothing$ and the new axiom $\forall x(x\notin \varnothing)$, meaning "for all x, x is not a member of $\varnothing$". Doing this 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.