# 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:

1. 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?

2. 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?

3. 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$?

4. 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.

• As for (4), it is standard to assume in FOL that models are non-empty. – Martti Karvonen Sep 24 '15 at 18:33
• You can prove directly in first-order logic that some set exists; $(\exists x)[x \in x \lor \lnot x \in x]$ is a logical validity. – Carl Mummert Sep 27 '15 at 8:18
• In the book Set Theory:An Introduction to Independence Proofs , by Kunen,the first axiom of ZFC is $\exists x (x=x)$ because all the other axioms except Infinity begin with "$\forall$" .His development is to initially derive as much as possible without Infinity and without Choice (and even without Foundation) but if all your axioms begin with "$\forall$" you cannot deduce that anything exists. – DanielWainfleet Oct 3 '15 at 6:27

A simple approach is inspired by :

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 :

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.

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.

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".