I have preoccupied myself some with very weak set theories that suffice to interpret Robinson Arithmetic, as in this question 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?