Reflective Set Theory $\mathsf{RfST}$ is formulated in first order predicate logic with extra-logical primitives of equality $``="$, membership $``\in"$, and a single primitive constant symbol $V$ denoting the class of all sets.

The axioms are those of first order identity theory +

**Extensionality:**$\forall x (x \in a \leftrightarrow x \in b) \to a=b$**Class comprehension:**if $\varphi(y)$ is a formula in which the symbol $``y"$ occurs free, then all closures of: $\exists x \forall y (y \in x \leftrightarrow y \in V \wedge \varphi(y))$ are axioms.**Reflection:**if $\varphi(y, x_1,..,x_n)$ is a formula in $FOL(=,\in)$, in which only $y,x_1,..,x_n$ occur free, then:

$$\forall x_1,..,x_n \in V \\ [\exists y (\varphi(y,x_1,..,x_n)) \to \exists y \in V (\varphi(y,x_1,..,x_n))]$$

is an axiom

**Transitive:**$ y \in x \in V \to y \in V$**Foundation:**$\exists m\in x \to \exists y \in x \forall z \in x (z \not \in y)$

/Theory definition finished.

Personally I see this axiomtization to be the most elegant of set\class theories that I ever knew of!

Can this theory interpret $ZFC$ over $L$?

I mean clearly axioms of pairing, union, separation and replacement over $V$ from pure set formulas, infinity, are all provable here, however power is not easily provable here, but any set in $V$ that is an element of a stage $L_{\kappa}$, would have all of its subsets in $L_{\kappa}$ be in $V$, because all of them are definable by pure set formulas; so we must be able to reflect the existence of a set of all those subsets inside $V$, thus interpreting $ZFC + V=L$.