Is it possible to prove the existence of the empty set in MK without the axiom schema of class comprehension (ASoCC)? My conjecture is: No. Either one postulates the existence or proves it via the ASoCC.
Furthermore, the proof I came up with (using AsoCC) does only guarantee $\emptyset$ to be a class but not necessarliy a set. How could I prove that $\emptyset$ is infact no proper class?
Thank you in advance!
Proposition (Existence of $\eta$)
There exists a class $\eta$ that does not contain any elements.
$$ \exists \eta ~ (\forall a ~ \neg (a \in \eta)) ~~.$$
Let $a$ be a set and assume the predicate $\psi(a) :\Leftrightarrow \neg (a = a)$, and $\eta$ such that
$$ \forall (a \in \eta \Leftrightarrow \psi (a)) ~~. $$
The existence of $\eta$ is guaranteed by the Axiom Schema of Class Comprehension and, by proposition ($\forall a (a=a)$), it has in fact the desired property that $(\forall a ~ \neg (a \in \eta))$.