# 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]$?

-

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:

1. $X = \emptyset$ and $\emptyset = X$ become $( \forall x ) ( x \in X \rightarrow x \neq x )$;
2. $x \in \emptyset$ become $x \neq x$;
3. $\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)
-
Adding a new constant without any new axiom will also give a conservative extension. The reason this sort of extension is especially nice is model-theoretic: since every model contains a unique empty set, a model of the expanded theory is essentially the same thing as a model of the original theory. – Chris Eagle Feb 26 '13 at 17:16
Thanks. I found an article on this: en.wikipedia.org/wiki/Extension_by_definitions – sdcvvc Feb 26 '13 at 17:21
@sdcvvc: I must have searched for the wrong thing on Google; I didn't come across that article. – arjafi Feb 26 '13 at 17:27