Why this formulation is not the official exposition of ZF-?

Specification: if $\phi$ is a formula that doesn't use the symbol $x$, with symbols $``y,a,b"$ as its free variables, then : $$\forall a \forall b: \forall k \exists! x \forall y (y \in x \leftrightarrow y \in k \land \phi) $$

Reflection: if $\phi$ is a formula with symbols $``a,b"$ as its free variables, that doesn't use the symbol $\mathsf v$ ; and if $\phi^\mathsf v$ is the formula obtained by bounding all quantifiers in $\phi$ with $\mathsf v$, then: $$\forall a \forall b \ \exists \text{ supertrs } \mathsf v : \phi \implies \phi^\mathsf v$$

Where:

$\mathsf v \text{ is supertrs} \equiv_{df} \forall m \forall n (m \in v \land (n \in m \lor n \subseteq m) \to n \in v)$

That is: a supertransitive set is a set closed under $\in$ and $\subseteq$ relations.

This is a modification of Dana Scott's theory about sets and stages, and I believe this proves all axioms of ZF-Reg., and even without Extensionality it can interpret ZFC.

This exposition of ZF- is actually very simple, neat and elegant. It is much shorter than the usual presentation of ZF- by axioms of Extensionality, Empty, Set union, Power, Separation, Replacement, and Infinity. Moreover, it appears to be pretty much natural and reduces all those diversily looking axioms into just two simple principles "we reflect, then specify!", that's all.

Since this is a well established result decades ago, then given the merits of shortage, elegance, and principled reduction; why it was not adopted as the official exposition of ZF-?

Solution 1:

Leaving aside communal inertia ("why change a perfectly fine presentation?"), which is of course significant, I don't see the benefit of this proposed reaxiomatization.

It is much shorter than the usual presentation of ZF- by axioms of Extensionality, Empty, Set union, Power, Separation, Replacement, and Infinity.

Sure, but length isn't an inherent indicator of quality.

This exposition of ZF- is actually very simple

Is it? Someone new to the field would have substantially more difficulty using it, I suspect, than using the usual $\mathsf{ZF-}$ axioms. Simplicity of presentation and simplicity of use are two different things, and in most situations I think the latter is more important than the former.

it appears to be pretty much natural and reduces all those diversily looking axioms into just two simple principles "we reflect, then specify!", that's all

Again, I don't really buy this: why should "we reflect, then specify" be an accepted bit of set-theoretic intuition? Motivating reflection is nontrivial. By contrast, the $\mathsf{ZF-}$ axioms are graded: consider the various levels of "justifiability" of e.g. Pairing, Infinity, Replacement, and Powerset. Someone who doesn't find all of them intuitive will still (probably) find some of them intuitive, and so a larger portion of the theory is "immediately acceptable." I think this is very useful for the pragmatic side of things: to a strong set theory skeptic we can argue that the "inoffensive part" of $\mathsf{ZF-}$ is still strong enough to do what they need, while it's not clear how to whip up something similar for your approach.

There's also the more technical aspect: if you're interested in fragments of $\mathsf{ZF-}$ (which I personally am very much), a more modular approach is significantly easier to use.

To sum up, I think that while this is of course a neat result, as an axiomatization of $\mathsf{ZF-}$ it is inferior to the standard one(s) in terms of intuitive appeal and immediate usability - and I don't think that its advantages make up for that.