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?

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