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 adjunction as well as the rules $\vdash\hspace{-2pt}\alpha(a)\Leftrightarrow\hspace{2pt}\vdash\hspace{-2pt} a\notin\{x|\lnot\alpha(x)\}$, is consistent or even omega consistent in some appropriate sense? Does SU still support its own coding to get a Godelian provability predicate for SU?

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