# Can this reflective class theory interpret ZFC?

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

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

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

• The pure set-theoretic consequences of your theory are precisely the consequences of $ZF-PowerSet$. To convert a proof in your theory to a proof in $ZF-PowerSet$ the constant $V$ could be interlreted by a transitive set that reflects enough first-order formulas – Fedor Pakhomov Dec 19 '18 at 18:45
• @FedorPakhomov would that still be the same if we add $V=L$ to this theory? – Zuhair Al-Johar Dec 20 '18 at 12:05
• I wasn't careful enough yesterday. My claim that $ZF-PowerSet$ axiomatizes pure set-theoretic consequences of your system is wrong, even if we consider the version of ZF with collection. My argument actually just shows that the pure-theoretic part of your system is $(ZF-PowerSet)+TMR$; here $TMR$ is transitive model reflection, e.g. the scheme $\exists M \;(\mathsf{Trans}(M)\land \forall \vec{x}\;(\varphi(\vec{x})\leftrightarrow \varphi^M(\vec{x})))$. But $(ZF-PowerSet)+Coll$ doesn't $TMR$, see Theorem 1.2 from Friedman, Gitman, Kanovei arxiv.org/pdf/1808.04732.pdf – Fedor Pakhomov Dec 21 '18 at 17:37
• Note that nevertheless it still implies that your system couldn't interpret $ZF$. In $ZF$ it is easy to show that $(L\cap H\omega_1)\models (ZF−PowerSet)+TMR$. Thus consistencies of both $(ZF−PowerSet)+TMR$ and your system are provable in $ZF$. And by a standard corollary from Gödel's 2nd incompleteness theorem, no consistent theory $T$ extending Robinson's arithmetic $Q$ could interpret its own consistency. – Fedor Pakhomov Dec 21 '18 at 17:52
• The theory $(ZF−PowerSet)+TMR$ is mutually interpretable with second-order arithmetic $Z_2$. Second order arithmetic could be interpreted in $(ZF−PowerSet)+TMR$ in a standard manner (by natural numbers and sets of naturals). $Z_2$ could formalize notion of constructive set (see Simpson's book) and then it is easy to show in $Z_2$ that $(ZF−PowerSet)+TMR$ holds in $L$. – Fedor Pakhomov Dec 21 '18 at 18:08