[This is a question on the FOM mailing list.]
In 1997, Harvey Friedman introduced the following theory: Let $\in$ be a binary predicate and $U$ be a constant. Add the following axioms:
Subworld separation (SS): $(\forall x \in U)(\exists y \in U)(\forall z)(z \in y \leftrightarrow (z \in x \land \varphi))$ where $y$ is not free in $\varphi$.
Reducibility (RED): $(\forall x_1 \ldots x_n \in U)((\exists y) \varphi \to (\exists y \in U) \varphi)$ where $\varphi$ does not mention $U$ and has free variables among $x_1, \dotsc, x_n, y$.
This theory interprets ZFC. With extensionality, it proves ZF − Foundation.
Can this system be simplified further in any way, while retaining the ability to interpret ZFC? For example, paper 2 says:
Under pure predication, the Subworld Separation axiom scheme has to restricted so that $\varphi$ has at most the free variable $x$. However, an additional restriction on SS is warranted — that $x$ be given by an explicit definition without parameters. In addition, some restrictions on RED may also be appropriate, although it is less clear how this is to be determined. We now conjecture that SS and RED alone, even under such restrictions, is sufficiently strong to provide an interpretation of ZFC.
Has this conjecture been proven? If so, what is the resulting axiomatization?
Alternatively, can we upper-bound the number of parameters for $\varphi$ required in these schemas, as in parameter-free ZFC?
References:
Harvey M. Friedman. Axiomatization of set theory by extensionality, separation, and reducibility: seminar notes. 1997 October 5.
Harvey M. Friedman. From Russell's paradox to higher set theory. 1997 October 10.
Harvey M. Friedman. The interpretation of set theory in mathematical predication theory: preliminary report. 1997 October 25.
