Can an acyclic set construction scheme be proved in Ackermann set theory?

If we define Transpassing in the following manner:

$\phi$ is Transpassing $\iff$ $\exists x,z (x=\{y \in V | \phi(y)\} \wedge \phi(z) \wedge x \subset TC(z))$

Where clearly $\phi$ is a predicate symbol, $TC(x)$ stands for "the transitive closure class of x" defined in a customary manner as the minimal transitive superclass of x, and transitive class is defined as a class that has all of its elements being subsets of it.

Now define Reflective as:

$\phi$ is reflective $\iff$ $\forall (x) (\phi(x) \to x \in V)$

Now $V$ is a primitive constant symbol denoting the class of all sets, as in Ackermann set theory.

Now let's work in a first order set theory that has the following axioms:

1. Extensionality: as in Ackermann's set theory.
2. Class comprehension scheme: if $\phi(y)$ is a formula, then all closures of $(\phi$ is reflective$\to \exists x (x=\{y|\phi(y)\}))$ are axioms.

3. Transitivity: $V$ is a transitive class

4. Acyclicity: no class is an element of its transitive closure

5. Acyclic set construction scheme: if $\phi(y)$ is a formula in which $V$ does not occur, and where $y,z_1,..,z_n$ are all of its free variables, then:

$\forall z_1,..,z_n \in V$$( \phi$ is not transpassing $\to \exists x \in V (x=\{y| \phi(y)\} ))$ is an axiom.

Now this theory would clearly prove all axioms of Ackermann's set theory (except the full consequence of Regularity), including the second completeness axiom for $V$. So the above acyclic set construction principle is indeed stronger than the reflection scheme of Ackermann, to write the later, it is:

Ackermann's reflection scheme for set construction: if $\phi(y)$ is a formula in which $V$ does not occur, and where $y,z_1,..,z_n$ are all of its free variables, then:

$\forall z_1,..,z_n \in V$ $( \phi$ is reflective $\to \exists x \in V (x=\{y| \phi(y)\} ))$ is an axiom.

It is easy to prove that in this theory every reflective predicate (given the conditions of not using the symbol $V$ and parameters standing just for sets) is non-transpassing. But does that hold in the opposite direction?

My question is: Does Ackermann's set theory prove all axioms of this theory? In other words, can we prove in Ackermann's set theory that every non-transpassing predicate (with above qualifications) is a reflective predicate?

The idea is that the theory presented here is based intuitively on a separate notion, that of defining classes of acyclically constructed sets, though it overlaps with Ackermann's in it being essentially a class theory with set-hood taken to be primitive, and it shares with it all of its first four axioms. However, the notion of acyclicity is intuitively different from that of reflection; here all axioms pivot around the theme of acyclic construction while in Ackermann's two axioms seem deliberately fixed to suit proving axioms of union and power, even Regularity doesn't seem to be necessary for Ackermann's. However, should the answer to my question be in the positive, then the above theory would only be a rather long reformulation of Ackermann's set theory though reflects a more unified theme of axiomatization?

• It’s not clear to me why a “transitive closure class” exists. Given $z$, we can certainly define a predicate whose extension is the transitive closure of $z$, defined as “every transitive class $C$ with $z \subseteq C$ contains $x$”, but proving that this predicate is represented by a class requires some comprehension axioms. (This isn’t a problem for the rest of your treatment, though — the predicate version is enough for your definition of “transpassing”.) – Peter LeFanu Lumsdaine Sep 6 '17 at 14:56
• Yes, you can define "transpassing" using the predicate approach! However, given all the axioms, it won't make any difference whether you define it using predicates or you define it using transitive closure classes since the existence of the later would be proven from Extensionality, Class comprehension, and Transitivity, and all of those are necessarily needed (together with axiom of acyclicity) for acyclic set construction scheme to kick in! That said, it appears to me that it would be nicer to define 'transpassing' in terms of transitive closure classes. – Zuhair Al-Johar Sep 6 '17 at 19:45