Trivial proof in ZFC

Question

Let's take some theorem of ZFC, e.g.: $$(1)\: \exists x \forall y ( y \notin x) $$ We can then choose a constant, denote it by '$\varnothing$' to get the following: $$(2)\:\forall x (x\notin \varnothing) $$ My question is: what's the precise proof of (2) given (1)? Also, let the axioms of FOL be the ones from Geoffrey Hunter's Metalogic (axiom schemata QS1-7), plus the axioms of ZFC (though I think they're irrelevant). The only allowed rule of inference is modus ponens.

P.S. I know that the question is ridiculous, and obviously the "jump" between (1) and (2) makes sense. The only thing that bugs me is that I can't justify this "jump" formally :)

Answer 1

It is a standard theorem about FOL that given a theory which entails a wff $\exists_1x\varphi(x)$, then we can conservatively add a new constant $c$ to the language of the theory, together with the new axiom $\varphi(c)$. This is conservative in this sense that we will still be able to prove nothing in the language of the original theory which we couldn't prove before (even when we use the new constant to instantiate old universal axioms -- see Henning Makholm's important comment below). So there is a good sense in which the new constant just sprinkles onto the original theory some "syntactic sugar" (some nice notation that enables the medicine to go down more easily, by helping us to put things more snappily or more memorably) without at all changing the basic power of the theory.

That is all that is going on in the present case. Adding notation for the empty set is typically just adding syntactic sugar, which we are allowed to do because, once we know there is a set with no members, it is immediate that this is unique, so we have $\exists_1x\forall y(y \notin x)$, and we can apply that mentioned standard theorem.

Answer 2

See the following post.

Form George Tourlakis, Lectures in Logic and Set Theory. Volume 2 : Set Theory, page 122 :

"Let us recall the basics of introducing new function symbols [in first-order logic]. Suppose that we have the following:

$\vdash_T (\exists y) A(y, x)$ --- [call it : "existence condition"]

and

$\vdash_T A(y, x) \land A(z, x) \rightarrow y = z$ --- [call it : "uniqueness condition"]

then we may introduce a new function symbol, say $f_A$, into the language of $T$ by the axiom

$f_ A(x) = y \leftrightarrow A(y, x)$".

Now, in $\mathsf {ZFC}$ we have the Null Set axiom :

$\exists y \lnot \exists x (x \in y)$

i.e.

$\exists y \forall x (x \notin y)$.

Since it is provable from this axiom and the Extensionality axiom that there is a unique such set, we may use the "technique" described above to introduce the notation '$\emptyset$’ to denote it.

In conclusion, it is not enough to prove "the existence" condition; you need also "the uniqueness" condition.

Answer 3

Let's add my rather informal view:

I think the definitions are considered only some kind of meta thing and not actually part of the language.

So you have to choose a way to give a meaning to definitions.

I can think of 2 kinds of definitions:

• A property. Let's say $x$ is not empty means $\exists y(y\in x)$
• An object. You want to denote the $\varnothing$ the $x$ such that $x$ is not empty.

Now let's try to resolve the following formula $$\forall x(x\text{ is not empty}\Longrightarrow x\ne\varnothing)$$

It's quite clear how to resolve a property, it's equivalent to $$\forall x(\exists y(y\in x)\Longrightarrow x\ne\varnothing)$$ but what about $\varnothing$? One way to look at it is to say the formula holds for all $x$ ($z$ in this case) from the definition of $\varnothing$ $$\forall z(\exists y(y\in z)\Longrightarrow\forall x(\exists y(y\in x)\Longrightarrow x\ne z))$$ For this to be actually useful, you need to known such $z$ exists and that it's unique. Both are quaranteed if $\varnothing$ is well defined.