> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/200-set-theory/topics/extensions-by-definitions.md).

# 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.
