Naming objects when existence and uniqueness was proven Let's take ZF and let $e(X)$ be the sentence $\forall Y. Y \notin X$.
From the axioms, we can prove $\exists X. e(X)$ and $\forall X, Y. e(X) \wedge e(Y) \implies X=Y$. So far so good. Now, we assign a meaning to $\emptyset$: it is the only $X$ that satisfies $e(X)$. Why we are allowed to do this? It seems we are changing the signature of the language. Is there a name for a rule that allows to name objects whose existence and uniqueness was proved, like reflexivity is a rule that allows to conclude $x=x$? Or is the symbol $\emptyset$ just a notational shortcut and a formula $\varphi$ containing the symbol $\emptyset$ is formally a shortcut for $\exists X. e(X) \wedge \phi[\emptyset \leftarrow X]$?
 A: Every instance of $\emptyset$ in a sentence of set theory can be translated out.  More commonly (in my opinion) we use the formula $( \forall x ) ( x \in X \rightarrow x \neq x )$ to define $\emptyset$.  So when we see an occurrence of $\emptyset$ in a formula, we can translate it out thusly:


*

*$X = \emptyset$ and $\emptyset = X$ become $( \forall x ) ( x \in X \rightarrow x \neq x )$;

*$x \in \emptyset$ become $x \neq x$;

*$\emptyset \in X$ becomes $( \exists y ) ( y \in X \wedge ( \forall x ) ( x \in y \rightarrow x \neq x ) )$.


(All occurrences of $\emptyset$ will be in the context of an atomic formula.)
If we think of this as formally changing the signature of the language, we also have to include the defining formula for $\emptyset$ as a new axiom.  What we end up doing is construct a conservative extension of ZF.

Some texts in mathematical logic include a theorem to the effect that if $\Sigma \vdash (\exists ! x ) ( \phi ( x ) )$ then the extension of $\Sigma$ obtained by adding $c_\phi$ as a new constant symbol and adding $\phi ( c_\phi )$ as a new axiom is a conservative extension of $\Sigma$.  More generally we can extend by definitions for relation symbols and function symbols.  A couple of references for this are:


*

*Shoenfield, Mathematical Logic, pp.55-56 (Theorem on Functional Extensions)

*Hinman, Fundamentals of Mathematical Logic, p.179 (Corollary 2.6.15)

*Srivastava, A Course on Mathematical Logic, p.74 (Theorem 5.3.6)

