Is this reflection schema equivalent to second order Bernays reflection?

Question

This posting comes as a possible salvage to this earlier presented reflective theory which was proved inconsistent. Attesting the particulars of the underlying language in reflection axioms.

Working in mono-sorted first order logic with equality $``="$ and membership $``\in"$:

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

• Axiomatize:

1. Extensionality: $( a \subseteq b \land b \subseteq a \to a=b)$

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

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

where formulas $\phi, \varphi$ do not use $``x"$; $\varphi$ do not use $``="$; $\varphi^x$ is obtained from $\varphi$ by merely bounding its quantifiers by $``\subseteq x"$ if the quantified variable appears only on the right of symbol $\in$, and by $``\in x"$ whenever it appears on the left. $``\text { trs}" $ stands for is transitive.

Can this syntactic restriction on $\varphi^x$ manage to escape inconsistency?

I conjecture that this reflection scheme would be equivalent to second order Bernays reflection schema (page 21) over the rest of axioms of this theory.

Answer 1

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

(b)V∉V

Proof:Suppose V∈V. By 2, there is an x such that set(x) and ∀y(y∈x<-->y∈V∧y∉y).

  Then x∈x<-->x∉x.

Then ∃w(w∉w∧∀t(t∈V-->t∈w)). By 3, there is a transitive x such that

∃w(w∈x∧(w∉w∧∀t(t∈x∧t∈V-->t∈w))). But then x=w, and thus w∈w.