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 +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$

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

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

4. Transitive: $\forall x \in V \forall y \in x ( y \in V)$

5. 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$.

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 +

1. Extensionality: $\forall x (x \in a \leftrightarrow x \in b) \to a=b$

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

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

4. Transitive: $ y \in x \in V \to y \in V$

5. 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$.