Does separation + reflection prove ZF - extensionality - foundation?

Assume a first-order context. Let $$\mathrm{tran}(x)$$ denote that $$x$$ is transitive:

$$\mathrm{tran}(x) \leftrightarrow (\forall y \in x) (\forall z \in y) (z \in x)$$

Let $$\mathrm{suptran}(x)$$ denote that $$x$$ is supertransitive:

$$\mathrm{suptran}(x) \leftrightarrow (\forall y \in x) (\forall z \subseteq y) (z \in x)$$

Consider the following axiom schemas of reflection:

\begin{align} & \phi \to \exists x (\phi^x \land \mathrm{tran}(x)) & \text{R1} \\ & \phi \to \exists x (\phi^x \land \mathrm{tran}(x) \land \mathrm{suptran}(x)) & \text{R2} \end{align}

where $$\phi$$ is any formula in which $$x$$ is not free and $$\phi^x$$ is the relativization of $$\phi$$ to $$x$$ (changing all quantifiers in $$\phi$$ to range over $$x$$). Ref. 1 says extensionality, separation, and R1 prove pairs, union, powerset, infinity, and replacement. Ref. 2 says

Extensionality, Separation, and Foundation, together with the Reflection Principle, formulated as the axiom schema asserting that each formula is reflected by some set that contains all elements and all subsets of its elements (note that the Vα are like this), is equivalent to ZF.

My questions are the following:

1. Is the supertransitivity condition, as opposed to just transitivity, necessary?
2. Does separation + R# (without extensionality) prove ZF - extensionality - foundation?

References:

1. Stewart Shapiro, Gabriel Uzquiano. Frege meets zermelo: A perspective on ineffability and reflection: A perspective on ineffability and reflection. Cambridge University Press: 2008-08-01. http://people.ucalgary.ca/~rzach/static/banff/rsl-specialissue/shapiro-uzquiano/shapiro-uzquiano.pdf. Page 6.

2. Joan Bagaria. Set Theory. Stanford Encyclopedia of Philosophy: 2019-02-12. https://plato.stanford.edu/entries/set-theory/#UniVAllSet. Section 4, last paragraph.

1. Supertransitivity (in other words, $$V_\alpha$$ for some limit $$\alpha$$) is necessary.

Assume that $$V=L$$ and consider $$L_{\omega_1}$$. It is known that $$L_{\omega_1}$$ satisfies $$\mathsf{ZFC}^-$$, that is, $$\mathsf{ZFC}$$ without Power Set. Furthermore, $$L_{\omega_1}$$ also satisfies Reflection in a sense that for every formula $$\phi(x)$$ with a parameter $$a$$, we can find $$\alpha<\omega_1$$ such that $$a\in L_\alpha$$ and $$L_{\omega_1}\models \phi(a)\leftrightarrow \phi^{L_\alpha}(a).$$

Especially, $$L_{\omega_1}$$ satisfies Extensionality, Separation, Foundation, and R1. However, it does not satisfy the full $$\mathsf{ZF}$$.

2. Everything becomes tricky if we do not have extensionality. However, the above result also shows that R1 + Separation does not prove $$\mathsf{ZF}$$ without Separation and Foundation. (If were, $$L_{\omega_1}$$ must satisfy Powerset.)

I have no idea what happens if we assume R2. However, the following variant of R2 proves other axioms of ZF (except for Extensionality and Foundation):

$$\forall a_1\cdots \forall a_n[ \exists x (a_1,\cdots,a_n\in x\land \text{x is transitive and supertransitive}\land \forall t\in x \ [\phi_0(t)\leftrightarrow \phi^x_0(t)] \land\cdots\land [\phi_n(t)\leftrightarrow \phi^x_n(t)] )].$$

The most tricky axiom would be Replacement: assume that $$\forall x\in a\exists!y \phi(x,y)$$. Find a supertransitive $$M\ni a$$ that reflects $$\forall x\in a\exists!y \phi(x,y)$$ and $$\phi(x,y)$$. Then consider the set $$R$$ given by

$$y\in R \leftrightarrow y\in M \land \exists x\in a\ \phi(x,y).$$

• According to Shapiro and Uzquiano, Extensionality, Separation, and R1 prove Pairing, Union, Powerset, Infinity, and Replacement. Since $L_{\omega_1}$ satisfies Foundation in addition, what axiom of $\mathsf{ZF}$ is missed? Nov 28 '21 at 19:58
• @CameronBuie No! Shapiro in Ref. 1 is using higher order logic. Careful attention must be paied to how he defines $\phi^x$ the bounding is not merely $\in x$ but also $\subseteq x$, the first for set variables, the second for class variables. In addition he doesn't need supertransitivity because he already proved subclasses of sets to be sets from separation axiom, so this acts somehow to mask this issue, I'll write a posting about it and make sure if I got it right. Nov 28 '21 at 21:57
• Nov 28 '21 at 22:56
• Thank you for your answer. I'll leave this open for now in case anyone can address R2. Nov 29 '21 at 5:11
• @Zuhair, thank you for clarifying! Nov 30 '21 at 0:32