A question on the consistency of a (seemingly) very weak set theory

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

• I don't quite understand the additional axiom in SU - is "$\{x: \neg \alpha(x)\}$" actually a term in your language? If not, what exactly is it shorthand for? (For example, are you saying that there is a set of all $x$ such that $\neg\alpha(x)$?) Also, what assumptions are you willing to make - e.g. if SU is consistent relative to ZFC, are you happy? – Noah Schweber Mar 11 '16 at 23:58
• The addition you are alluding to comprise inference rules and not axioms. Yes, $\{x|\lnot\alpha(x)\}$ is a term. In fact, all terms $\{x|\alpha(x)\}$ are terms of SU. I would believe that SU is consistent relative to much weaker theories than $ZFC$, but any result is of interest. – Frode Bjørdal Mar 12 '16 at 0:10
• OK, then I am worried your theory is inconsistent: you have a term $\{x: \neg (x\in x)\}$! Now, you don't have an axiom scheme saying $\forall x[\alpha(x)\iff x\in \{x: \alpha(x)\}]$, so we don't immediately hit a contradiction - but at this point I wouldn't be surprised if there is a contradiction. – Noah Schweber Mar 12 '16 at 0:14
• May terms $\lbrace x \mid \alpha(x) \rbrace$ contain parameters? – Andrej Bauer Mar 12 '16 at 7:53
• I think the worry about inconsistency comes from the fact that changing your inference rule to the axiom $\forall a . (\alpha(a) \Leftrightarrow a \not\in \lbrace x \mid \lnot \alpha(x) \rbrace)$ opens the road to Russell's paradox. – Andrej Bauer Mar 12 '16 at 8:01