4
$\begingroup$

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

Improve this question
$\endgroup$
9
  • $\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
    Commented Dec 19, 2018 at 18:45
  • $\begingroup$ @FedorPakhomov would that still be the same if we add $V=L$ to this theory? $\endgroup$
    – Zuhair Al-Johar
    Commented Dec 20, 2018 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
    Commented Dec 21, 2018 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
    Commented Dec 21, 2018 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
    Commented Dec 21, 2018 at 18:08

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .