This posting comes as a possible salvage to [this](https://mathoverflow.net/questions/409916/whats-the-consistency-strength-of-this-form-of-reflection) earlier presented reflective theory which was [proved inconsistent](https://mathoverflow.net/questions/409916/whats-the-consistency-strength-of-this-form-of-reflection/410575#410575). 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](https://www.researchgate.net/publication/220366286_Bernays_and_Set_Theory) schema (page 21) over the rest of axioms of this theory.



Is this reflection schema equivalent to second order Bernays reflection?
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.


