Harvey Friedman's axioms for set theory

[wfdc]

In 1997, Harvey Friedman introduced the following system:

Let < be a binary predicate and W be a constant.

Subworld separation (SS):

(A x < W)(E y < W)(A z)(z < y <-> (z < x & P))

where y is not free in P.

Reducibility/witness (RED/WIT):

(A x1 ... xn < W)((E y) P -> (E y < W) P)

where P does not mention W and has free variables among x1, ..., xn, y.

This system 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, the paper says:

"Under pure predication, the Subworld Separation axiom scheme has to restricted so that P 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?

References:

Harvey M. Friedman. From Russell's paradox to higher set theory. 1997 October 10. https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/FromRusselltoSetThy-1rnmfbg.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210908/6dab018d/attachment-0001.html>