Can a set have a complement in intuitionistic ZF? Does IZF (ZF formulated in intuitionistic logic) prove that for any set $a$, $\{x: x \notin a \}$ does not exist?
 A: 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:

*

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


*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$.
A: 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\}$$

*

*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$.


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


*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).
