Is intuitionistic naive set theory consistent?

Question

I'm asking because the usual argument that a set either belongs in itself or not doesn't apply. I did a quick search and it appears that the logic is also required to be contraction free. If it's inconsistent, in very broad terms, what is the proof?

Answer 1

Full comprehension is intuitionistically inconsistent. Suppose $R$ is a set such that $$x \in R \leftrightarrow x \notin x$$ for all sets $x$. Then, $$R \in R \leftrightarrow R \notin R$$ so we have an instance of a closed formula $\phi$ such that $\phi \leftrightarrow \lnot \phi$. This is the problem.

Indeed, given $\phi \to \lnot \phi$, it is easy to deduce that $\phi \to \bot$, i.e. $\lnot \phi$. But if we assume $\lnot \phi \to \phi$ as well, then we get $\phi$ by modus ponens. Thus, we have both $\lnot \phi$ and $\phi$ – a contradiction.