For a fixed first order language $L$, one of the rules of inference of the formal deductive system $K_L$ of predicate calculus is:
$$
\forall x_i:A(x_i)\to A(t)\tag{1}
$$
where $A$ is a well-formed formula of $L$ and $t$ is a term in $L$ which is free for $x_i$ in $A(x_i)$.
Since ZF is an extension of $K_L$ for a suitable language $L$, from the instance
$$
\forall A\,\exists B\,\forall C:C\in B\leftrightarrow C\in A\wedge C\neq C\tag{2}
$$
of the Axiom Schema of Separation, we infer, by $(1)$,
$$
\exists B\,\forall C:C\in B\leftrightarrow C\in A_0\wedge C\neq C\tag{3}
$$
where $A_0$ is just a set in the universe of a model of ZF. So,
$$
\exists B\,\forall C:C\not\in B\tag{4}
$$
and we proved the existence of an empty set.
Questions:
When getting rid of the $\forall A$ according to $(1)$, it seems to me that if $t$ is not a constant or a previously defined symbol then it's useless to get rid of the universal quantifier, no?
Is the step from $(2)$ to $(3)$ legit? I mean, in order to take a specific set $A_0$, do we need to have a previous proof that a $A_0$ exists? Also, if $A_0$ was just another variable name, could we infer $(4)$ from $(3)$ to get the existence of the empty set?
Formally, what justifies infering $(4)$ from $(3)$? This inference seems intuitively clear, but formally a proof would have to be given. Would it be correct to say that the Adequacy Theorem for $K_L$ gives the existence of such a formal proof because $(3)\to(4)$ is a logically valid well-formed formula of $L$?
All in all, in order to prove the Empty Set Axiom from the Axiom Schema of Separation, do we need to have a previous proof that some set, denote it by $A_0$, exists in order to use $A_0$ in $(3)$? I know that the Axiom of Infinity gives the existence of a set, so this question is basically of a logical nature more than anything else.
Best Answer
A simple approach is inspired by :
The formula $\exists x (x=x)$ can be derived from axiom :
with $\varphi(x) := \lnot x = x$ and $x$ as $t$, by tautological implication [$\vDash_{TAUT} (\mathcal A \to \lnot \mathcal B) \to (\mathcal B \to \lnot \mathcal A)$], the equality axiom $x=x$ and Modus ponens [$\exists x$ is an abbreviation for $\lnot \forall \lnot$].
Note that it is a theorem of "pure" logic (i.e. the formula is valid) and formalize the "standard" assumption for the semantics of first-order languages that requires interpretations with non empty domains.
Thus, there are sets.
Consider now :
With $\text{Separation}$ we can easily prove :
using $\mathcal A \to \mathcal B \vDash_{TAUT} \mathcal A \leftrightarrow \mathcal A \land \mathcal B$.
Thus $\varphi(z) \to z \in A \vDash _{TAUT} \varphi(z) \leftrightarrow \varphi(z) \land z \in A$ and replacing the equivalentes into $\text{Separation}$ we get the result.
Consider now $\varphi(z) := z \ne z$
1) $\vdash (z=z)$ --- equality axiom
2) $\vdash z = z \to (z \ne z \to z \in A)$ --- from $\vDash_{TAUT} \mathcal A \to (\lnot \mathcal A \to \mathcal B))$
3) $\vdash z \ne z \to z \in A$ --- from 1) and 2) by Specialization and Modus ponens.
Thus, from 3) and (*) above we get :
Having proved the existence of a new set, we can intriduce a name for it : $\emptyset$ [with $\text{Extensionality}$ we can prove that it is unique].
Thus, we have $\vdash_{\mathsf{ZFC}} ∀z (z \in \emptyset ↔ z \ne z)$ and, by tautological implication :
Using once more the equality axiom : $z=z$, by tautological implication again (and the abbreviation $\notin$) we conclude with :
The above derivation can be easily adapted to the proof system of :
By Prop.4.3 all tautologies are theorems of $K_{\mathcal L}$ and the system has the Generalisation rule as primitive. Specialization is (K5) and (E7) is the equality axiom.