I have preoccupied myself some with very weak set theories that suffice to interpret Robinson Arithmetic, as in this question http://mathoverflow.net/questions/222125/is-extensionality-needed-for-the-incompleteness-of-very-weak-set-theories. May we have confidence that the theory SU, which has the axioms for empty set and for universal set and for adjunction as well as the rules $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\notin\{x|\lnot\alpha(x)\}$ and $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\in\{x|\alpha(x)\}$ is consistent or even omega consistent in an appropriate sense? Does SU still support its own coding to get a Godelian provability predicate for SU?

SU has all set terms and we presuppose an underlying theory of identity by having the Leibnizian-Russellian definition of $a=b$ as $\forall u(a\in u\rightarrow b\in u)$ and the axiom schema $\vdash\forall x, y(x=y\rightarrow(\alpha(x)\rightarrow\alpha(y)))$.

P.S. The appropriate omega consistency I want is that if $\vdash\alpha(t)$ for all terms $t$ then $\nvdash\exists x\lnot\alpha(x)$.