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 all of its quantifiers by $``\subseteq x"$; and $``\text { trs}" $ stands for *is transitive*.


This theory can prove: Set existence, Empty, Pairing, set Union, Power, Infinity, over the set world of it, also it proves [Substitution](https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory#The_axioms_in_Kelley%27s_General_Topology). It can also prove class comprehension scheme. So it appears to prove all axioms of [$\sf MK$](https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory#The_axioms_in_Kelley%27s_General_Topology)-$\sf Reg.$-$\sf Choice$.



> 
> Is this theory consistent?
> 
> 
> 



> 
> If so, is it equivalent to [Bernay's reflection](https://en.wikipedia.org/wiki/Reflection_principle#As_new_axioms)?
> 
> 
> 



What's the consistency strength of this form of 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). 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.


