Can a set have a complement in intuitionistic ZF?

Question

Does IZF (ZF formulated in intuitionistic logic) prove that for any set $a$, $\{x: x \notin a \}$ does not exist?

Answer 1

Suppose $b$ is the proposed set such that: $$∀x. x \in b \Leftrightarrow x \notin a$$ Then let $$u = a \cup b \\ d = \{x \in u : x \notin x\}$$

1. Suppose $d \notin u$. Then:

   • $d \notin a$ because $d \in a ⇒ d \in u$
   • Therefore $d \in b$ because $d \notin a ⇒ d \in b$
   • However $d \in b ⇒ d \in u$ which is contradictory

   Therefore $¬\ d \notin u$.

2. Supposing $d \in d$, then $d \notin d$ which is contradictory, so $d \notin d$.

3. Supposing $d \in u$, then:

   • $d \in d$ because $d \in u ∧ d \notin d$
   • But $d \in d$ contradicts the prior $d \notin d$

   So $d \notin u$.

But now we have deduced both $d \notin u$ and $¬\ d \notin u$, which is contradictory. So the assumption of $b$ existing is false.

You may have expected that intuitionistic logic would save you from $u$ being a universal set, because you cannot prove $∀ x. x \in u$ without excluded middle. However, when proving negative statements in intuitionistic logic, uses of excluded middle can be reduced to non-contradiction, which is intuitionistically valid reasoning. So if an assumption is classically contradictory, it is probably also intuitionistically so (for simple cases, at least).

Answer 2

Consider the rank function $\operatorname{rank}$ defined by $$\operatorname{rank} a = \bigcup\{\operatorname{rank}x + 1 \mid x\in a\}.$$

Then every element of $a$ has a rank smaller than $\operatorname{rank} a$, but you can show that any ordinal $\alpha$ has rank $\alpha$, so any ordinal greater than $\operatorname{rank} a$ is not a member of $a$.

Now I claim that the class $C=\{\beta\in\mathrm{Ord}\mid \alpha\in\beta\}$ is a proper class for any $\alpha$. Assume that $C$ is a set, then $\gamma:=\bigcup C$ is also an ordinal since $C$ is a set of ordinals. Then $\gamma\in C$, which is a contradiction since it implies $\gamma\in C\subseteq \gamma$.

---

Here are some remarks on my proof:

1. $\mathsf{CZF}^-$ (Constructive ZF without Subset Collection) suffices for the proof.

2. In fact, we can derive more on $C=\{\beta\in\mathrm{Ord}\mid \alpha\in\beta\}$.

   Define a proper class $A$ is inexhaustible if for every subset $x\subseteq A$ of $A$ there is $y\in A$ such that $y\notin x$. (That is, $A$ is greater than every subset of it.) Classically, every proper class is inexhaustible, but $\mathsf{IZF}$ need not prove it.

   We can see that if every set is subcountable (i.e., every set is an image of a subset of $\omega$), then $\mathcal{P}(1)$ is a proper class, but not an inexhaustible class. (It follows from that $\mathcal{P}(1)$ is a double complement of $2$ and no double complement of a set is inexhaustible.) However, the statement 'every set is subcountable' is not consistent with $\mathsf{IZF}$, although it is compatible with $\mathsf{CZF}$.

   A slight modification of the previous proof shows $C$ is inexhaustible: let $x\subseteq C$, and take $\gamma:=\bigcup x$. Then we have $\gamma\in C$ but $\gamma\notin x$.