ZF: (Formal) Proof of Empty Set from Separation 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.

 A: A simple approach is inspired by :


*

*George Tourlakis, Lectures in Logic and Set Theory : Volume 2, Set Theory (2003), page 130.



The formula $\exists x (x=x)$ can be derived from axiom :

$\forall x \varphi(x) \to \varphi[x/t]$

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 :

$∀x∃y∀z (z \in y ↔ z \in x \land \varphi(z)) \ - \ \text{Separation}$. 

With $\text{Separation}$ we can easily prove :

$\varphi(z) \to z \in A \vdash_{\mathsf{ZFC}} ∃y∀z (z \in y ↔ \varphi(z))$ --- (*)

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 :


$\vdash_{\mathsf{ZFC}} ∃y∀z (z \in y ↔ z \ne z)$.


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 : 

$\vdash_{\mathsf{ZFC}} ∀z (\lnot z \in \emptyset ↔ z = z)$.

Using once more the equality axiom : $z=z$, by tautological implication again (and the abbreviation $\notin$) we conclude with :


$∀z (z \notin \emptyset)$.




The above derivation can be easily adapted to the proof system of :


*

*Alan Hamilton, Logic for mathematicians (1978) :


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.
A: Question 2 and 4: this is legit. If you prefer to be concrete, first invoke the axiom of infinity (as you say), which states that "there is a successor set", and then use $A_0$ as shorthand for that successor set. (In this proof, it's just assumed that some set exists. To be ultra-formal, you're right: it has to be proved.)
You could look at it like this: all models are non-empty. Indeed, if there were no set in some model $M$, then $$(\forall x) \bot$$ would be true in that model, so by the predicate-calculus axiom $$[(\forall x) P] \Rightarrow P$$
we obtain $\bot$. This is a contradiction.
Therefore some set does exist in any model of ZF. Label that set $A_0$ and proceed, using the adequacy theorem as you say.
A: Question 2: Is the step from (2) to (3) legit?is the sticking point: there is a division in first-order logic over the status of the empty domain of discourse.
It is traditional to reject the empty domain of discourse, and consequently to have the rule of deduction $\forall x: P(x) \vdash P(t)$, as you noted. With $P$ chosen to be a proposition that asserts the existence of the empty set, we get its existence.
On the other side where empty domains of discourse are allowed, we do not have the above rule of deduction. We can still define a set $\varnothing$, but we cannot prove $\exists x: x = \varnothing$ without the help of an existential axiom such as an axiom of infinity. In fact, the empty domain is a model of ZFC-infinity!
Note that both sides of the divide will use the phrase "first-order logic" without comment to refer to their side. The traditional side calls the other side "free logic".
