I recently began reading, "The Foundations of Mathematics" by Kenneth Kunen and am having some difficulty understanding the rationale behind one of the very early proofs. The proof is about demonstrating the uniqueness of the empty set using the following 3 Axioms that Kunen establishes early in the book:
A. Set Existence: $\exists x (x=x)$ ...which Kunen will refer to as Axiom $0$
B. Extensionality: $\forall x,y \ \big( \forall z (z \in x \leftrightarrow z \in y) \rightarrow x=y\big )$
C. Comprehension Schema: $\forall z \big ( \exists y \forall x (x \in y \leftrightarrow x\in z \land \varphi(x) \big)$
I've seen the proof referenced many times so I am conceptually familiar with it...but I am having some confusion regarding the formal implementation of it. Kunen's proof is as follows:
(1) $\text{emp}(x):=\forall z (z\notin x)$
(2) By Extensionality, $\text{emp}(x) \land \text{emp}(y) \rightarrow x=y$
(3) To prove that $\exists y [\text{emp}(y)]$, start with any set $z$ (there is one by Axiom $0$) and apply comprehension with $\varphi (x)$ a statement that is always false (for example, $x \neq x$) to get a such that $\forall x (x \in y \leftrightarrow \text{FALSE})$ - i.e. $\forall x (x \notin y)$.
Combining (2) with (3) demonstrates that the empty set $\emptyset$ is unique.
I have several questions:
Firstly, how can we claim that $x \neq x$ is always false. By Set Existence, we claim that there is at least one set with the property that it is equal to itself...i.e. the relation "$=(x,x)$" holds true. In order to claim that $x \neq x$ is always false for any object $x$, shouldn't our Set Existence axiom be of the form $\forall x (x=x)$?
Secondly, given that Set Existence is presumably written correctly, what exactly is its purpose? Kunen's remark in (3), "...there is one by Axiom $0$..." seems to suggest that this axiom asserts that our domain of discourse is non-empty. But what exactly does that mean? My interpretation of a statement like that is, "Ok...so we know that we have at least one object in our domain of discourse, but no comment is made regarding whether we have more than one". Assuming that interpretation is correct, how is it that I can even generate multiple empty sets (say $\emptyset^*$ and $\emptyset '$) in (3) when the claim of the Comprehension Schema is that, "For any given set $z$ I can construct at least one set $y$ such that..."?
Said differently, if I only know for sure that one object $z$ exists (namely the $z$ that would be guaranteed to exist by Set Existence), shouldn't I only be able to generate a single empty set from it...i.e. because the Comprehension Schema states that I can construct at least one subset...but makes no comment about whether or not a can construct more than one ($\emptyset^*$ would be the first instance of an empty set construction but how could I also be guaranteed to construct the other $\emptyset'$?). The only thing I could think to do is use a different $\varphi$ (call it $\psi$) that also always evaluates to FALSE but I am unsure if that is the correct route.
Hopefully this rambling was expressed in a comprehensible manner. Any insight is greatly appreciated!
As said in the comments, since the equality symbol is written as such without being defined, then it's assumed to be a primitive symbol, and mostly when one writes matters in this manner then he's assuming axioms of equality beforehand, that is the system written above is on top of first order logic with equality axioms and those are not shown.
That said, then clearly $x=x$ is always true, since this is an axiom of equality theory.
Now from Existence axiom, we are assured that at least one object exists in the universe of discourse, let that be $K$, then from Separation we can recover the empty object.
Now as regards the proof that no distinct empty objects can exist, that is if $``\emptyset^*"$ and $``\emptyset' "$ are constant symbols defined as:
Define: $x=\emptyset^* \iff \forall y (y \in x \iff y \in K \land y\neq y)$
Define: $x=\emptyset' \iff \forall y(y \in x \iff y \in K \land y \neq y)$
Both of the above definitions can be done in first order logic, since it's already taken to have unlimited number of symbols ready to symbolize definable objects, and we can indeed use as many distinct constant symbols as may we even if all of them are definable in exactly the same manner, i.e. even if all of them turn to symbolize the same object!
Now from Extensionality we can prove that $\emptyset^* =\emptyset'$, that's easy since both have the same membership, that is: $$\forall z (z \in \emptyset^* \leftrightarrow z \in \emptyset')$$.