Is this simple reflective separative theory inconsistent?

Question

Working in mono-sorted first order logic with membership:

• Define: $set(x) \equiv_{df} \exists y \, (x \in y)$

• Define: $a \approx b \equiv_{df} \forall x \, (a \in x \leftrightarrow b \in x)$

• Axiomatize:

1. Extensionality: $( set(a) \to[ (a \subseteq b \land b \subseteq a) \leftrightarrow a \approx b])$

2. Separation: $(set(a) \to \exists \ set \ x : \forall y \, (y \in x \leftrightarrow y \in a \land \phi ))$

3. Reflection: $ (\phi \to \exists \ set \ x : \text { trs}(x) \land \phi^x)$

where formula $\phi$ doesn't use $``x"$ in both schemata; $\phi^x$ is the formula obtained from $\phi$ by merely bounding all of its quantifiers by $``\subseteq x"$; and $\text { trs}(x) \iff \forall y \in x (y \subseteq x)$

This theory seems to prove all axioms of $\sf ZF-Reg.$ over the set world of it, and perhaps can even go beyond that? But, my guess is that it is inconsistent!

Is there a clear inconsistency with this theory?

Answer 1

Yes, this theory is inconsistent.

We note that by 1 and 2 that if set(x) and y⊆x, then set(y).

(a) There is a v such that ∀x(set(x)-->x∈v).

Proof:Suppose not. Then ∀v∃s∃t(s∈t∧s∉v). By 3 there is transitive x such that

  set(x) and ∀v(v⊆x-->∃s∃t(s⊆x∧t⊆x∧s∈t∧s∉v). In particular 

  (x⊆x-->∃s∃t(s⊆x∧t⊆x∧s∈t∧s∉x).  But this is impossible.

Suppose that ∀x(set(x)-->x∈V). Then ∃w∀t(t∈V-->t∈w). By 3 there is transitive x

such that set(x) and ∃w(w⊆x∧∀t(t⊆x∧t∈V-->t∈w)). Since t⊆x implies set(t),

t⊆x implies t∈x. By 2, there is a c such that t∈c<-->(t∈x∧t∉t). Since set(c),

c∈c<-->c∉c.