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)