Would this salvage the $\in|=$ exchange naive set theory?

This is a possible salvage for the failed attempt in this posting.

Informally this theory asserts the existence of a set $$\{x|\phi\}$$ for any formula $$\phi$$ such that when all membership symbols in it are replaced by equality symbols then every subformula of the resulting formula would hold of at least one object, and also the negation of that subformula must hold of at least one object.

The idea of this tricky kind of comprehension, is to take any formula $$\phi$$ having all and only $$x_1,..,x_n$$ occurring free, then replace all $$\in$$ symbols in it by the equality symbol $$=$$, call it $$\phi^=$$, then take each subformula $$\psi^=$$ of $$\phi^=$$, and let $$\vec{p_\psi}$$ be the string of all variables free in $$\psi$$ other than $$x_1,..,x_{n-1}$$, ordered after their quantificational order in $$\phi$$; now add to $$\psi^=$$ the existential prefix $$\exists \vec{p_\psi}$$, as to have the formula $$\exists \vec{p_\psi} (\psi^=)$$.

Now we come to state our Modified naive Comprehension axiom:

Comprehension: If $$\phi$$ is a formula in the first order language of set theory in which all and only symbols $$x_1,..,x_n$$ occur free, and if $$\psi_1,..,\psi_m$$ are all subformulas of $$\phi$$; then: $$\forall x_1,..,x_{n-1}\big{(}\bigwedge_{i=1}^m[\exists \vec{p_{\psi_i}} (\psi_i^=) \land \exists \vec{p_{\psi_i}}(\neg \psi_i^=)] \\ \to \exists x \forall x_n (x_n \in x \leftrightarrow \phi)\big{)}$$; is an axiom.

Axiom of Multiplicity: $$\forall x,y \ \exists z (z \neq x \land z \neq y)$$

/

I personally think this is complex a little bit, I highly doubt its consistency though. Yet if there is a chance that this is consistent, then it would actually prove $$\mathcal All$$ of the axioms of a short axiomatization of $$\sf NF$$, [although axioms of Frege $$1^*$$ and of unordered intersection relation set must be written in another equivalent way], since full Extensionality is assumed here.

The idea here is to block the loophole argument presented in the answer to the prior attempt. We add the requirement of making the preconditional check for every subformula of $$\phi^=$$, and not just for $$\phi^=$$ as it was the case in the prior attempt. I hope this manage to block that argument.

Although the procedure looks a little bit complex here, but it's not really that complicated, since it's easy to check for truth of equality sentences.

I need to comment that I think this method most likely fails, i.e. it is inconsistent, and further restrictions must be added, for instance prenex normal forms might escape the above restrictions, so we might need the restriction that every subformula of $$\phi$$ must not be a prenex normal form of a formula that is not in prenex normal form. However a proof of inconsistency of this theory still eludes me.

• So with $\phi\equiv y\ne a$, we construct $\{a\}^\complement$? -- And with $\phi\equiv a\in y$, we construct $\{\,x\mid a\in x\,\}$? – Hagen von Eitzen May 27 at 21:41
• @HagenvonEitzen, yes – Zuhair May 28 at 4:52
• OK, and finite union is also readily obtained, so as $u:=\{a\}^\complement\cup\{b\}^\complement$, or as $u:=\{\,x\mid a\in x\,\}\cup\{\,x\mid a\notin x\,\}$, we get the all-set $u$ with $u\in u$ – Hagen von Eitzen May 28 at 5:06
• @HagenvonEitzen, Yes this is expected, since this method prove all axioms of NF! – Zuhair May 30 at 20:11