Is this $\large \in$ $|$ $\large =$ exchange naive set theory consistent?

This question is more of a trick.

Notation: for any formula $$\phi$$, let $$\phi^=$$ mean the formula obtained by merely replacing each occurrence of the membership symbol $$\in$$ in $$\phi$$ by the equality symbol $$=$$, so for example if $$\phi$$ is the formula $$(y \in y)$$, then $$\phi^=$$ is the formula $$(y=y)$$.

We assume full Extensionality throughout this exposition.

Notice this naive like Comprehension axiom scheme:

If $$\phi$$ is a formula in the first order language of set theory (i.e.; $$\sf FOL(=,\in)$$), in which the symbol $$x"$$ doesn't occur free, then: $$[\exists y (\phi^=) \wedge \exists y ((\neg \phi)^=) \to \exists x \forall y (y \in x \iff \phi)]$$; is an axiom.

Axiom of Multiplicity: $$\exists x,y: x \neq y$$

This theory supply the appearance of an inconsistent theory. However, a proof of this inconsistency keeps eluding me?!

Is this theory consistent?

The point is that this theory is very naive. The antecedent of comprehension is an extremely simple syntactical procedure, more of a trick really! In other words its a very naive kind of restriction on the original unrestricted naive comprehension.

The general expectation for such maneuvers is inconsistency!?

This theory [if consistent] has a universal set. So if consistent, it might be interpretable in one of the fragments of $$\sf NF$$? It would be nice to see if that is the case!

• Since for all x, x not in x, the replacement gives for all x, x /= x. – William Elliot May 27 at 9:27
• @WilliamElliot, you mean if $\phi$ is the formula $(\forall x (x \not \in x))$ then $\phi^=$ is the formula $\forall x (x \neq x)$; yes that is correct! Notice that this is just a definition of a syntactical procedure, its NOT to be understood as stipulating axioms, i.e. it does NOT mean that if $\phi$ is an axiom then $\phi^=$ is an axiom. – Zuhair May 27 at 9:33

Here is a model: $$\{1,2\}$$ with $$1\in 1 \qquad 1\notin 2 \qquad 2\in 2 \qquad 2\notin 1$$

That is, two Quine atoms side by side in an otherwise empty world.

In this model $$\in$$ and $$=$$ behave identically, so $$\phi^=\leftrightarrow \phi$$. Thus, the antecedent of your comprehension axiom demands that there is a $$y$$ that satisfies $$\phi$$ and another $$y$$ that doesn't satisfy $$\phi$$, which means that the collection you're looking for is either $$\{1\}$$ or $$\{2\}$$, which are exactly the options you have.

(Note that this model does not have a universal set).

That is the only model, though. If you strengthen your multiplicity axiom such that it promises three distinct sets $$a,b,c$$, then the following loophole will give unrestricted comprehension, and therefore an inconsistent theory:

The restricted comprehension axiom allows you to form $$\{a,b\}$$ -- because there is now a $$c$$ such that $$\neg(c=a\lor c=b)$$ -- and this unordered pair cannot equal both $$a$$ and $$b$$ at the same time, so there are some sets $$p,q$$ such that $$p\in q$$ but $$p\ne q$$.

Now to form unrestricted $$\{y\mid \psi(y)\}$$, use your comprehension axiom with a parameter $$a$$ and $$\phi \equiv (\forall p,q(p\in q\leftrightarrow p=q)\land y=a) \lor (\neg \forall p,q(p\in q\leftrightarrow p=q) \land \psi(y))$$

• @Zuhair: Indeed. Fixed, thanks. – Henning Makholm May 27 at 12:33
• It appears that one can remedy this by requiring that every subformula $\psi(y)$of the formula $\phi$ [having no parameters other than those of $\phi$], must obey the antecedent of comprehension. And of course upgrade the multiplicity axiom to assert existence of 3 distinct sets. – Zuhair May 27 at 12:57
• @Zuhair: That would, among other restrictions, require every atomic formula to be either $a\in y$ or $y\in a$ or $y=a$ for some variable or parameter $a$. That sounds quite limiting, worse than NF. (And how do you deal with variables that are bound by quantifiers inside $\phi$?) – Henning Makholm May 27 at 13:02
• If I put $\phi$ in Prenex normal form, then would the same hold. I tend to think so. If so then this would escape even my recent restrictions on subformulas. – Zuhair May 28 at 8:29