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

  • $\begingroup$ 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 $\endgroup$ – Fedor Pakhomov Dec 19 '18 at 18:45
  • $\begingroup$ @FedorPakhomov would that still be the same if we add $V=L$ to this theory? $\endgroup$ – Zuhair Al-Johar Dec 20 '18 at 12:05
  • 1
    $\begingroup$ 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 $\endgroup$ – Fedor Pakhomov Dec 21 '18 at 17:37
  • 1
    $\begingroup$ 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. $\endgroup$ – Fedor Pakhomov Dec 21 '18 at 17:52
  • 1
    $\begingroup$ 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$. $\endgroup$ – Fedor Pakhomov Dec 21 '18 at 18:08

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.