Is the definability axiom schema consistent with ZF?

Let us construct an axiom schema that declares that every set is definable from previous sets. For any formulas $\phi$, $\pi$, $\tau$, the following is instance of this axiom schema:

$$\forall x\forall y.\left( \begin{array} {rl} & \phi(\emptyset) \\ \land & \phi(\mathbb N) \\ \land & (\phi(x) \land \phi(y) \implies \phi(\{x,y\}) \\ \land & (\phi(x) \implies \phi (\bigcup x)) \\ \land & (\phi(x) \implies \phi (P(x))) \\ \land & (\phi(x) \implies \phi(\{z \in x: \pi(z)\})) \\ \land & (\text{\tau is a function formula} \land \phi(x) \implies \phi(\tau[x]))\end{array} \right) \implies \forall x. \phi(x)$$

It essentially goes through each of the ZF axioms, constructing a statement saying that $\phi$ satisfies the set is defines. For example, $(\text{$\tau$is a function} \land \phi(x) \implies \phi(pi[x]))$ represents the axiom schema of replacement. The axiom then states that this statement implies that all sets satisfy $\phi$.

Note in particular that this is more restrictive than $V = L$, since it asserts that ordinals need to be definable as well.

In particular, it implies there are no inaccessible cardinals.

Is this axiom schema consistient with ZF? (Also does it have a name?)

EDIT: The motivation for this axiom is to be comparable to the induction scheme on peano arithmetic. Essentially, its asking if we make ZF more like peano arithmetic, is it still consistient? We could even replace this with a second order axiom, and then ask if like peano arithmetic, it becomes categorical! Of course, this would be a different set theory then the normally envisioned one, but it is still of interest.

• Con(ZFC) does not imply there are inaccessible cardinals – Carl Mummert Jun 12 '18 at 15:55
• Rather than just posting a problem, you could improve the post by adding more context. What is the motivation for the problem? What question does it address? What attempts have you made to solve it? Posts that merely state a problem are generally discouraged, but this might appear to be a pattern; here is a a similarly unmotivated post from just a few minutes ago math.stackexchange.com/questions/2817100/… – Carl Mummert Jun 12 '18 at 15:58
• @CarlMummert Okay, I tried to add more motivation. – PyRulez Jun 12 '18 at 16:05
• There is already an induction schema for ZF, and it is equivalent to Replacement (over ZF-Replacement, of course). Or $\in$-induction, which is equivalent to Regularity (over ZF-Regularity, of course). – Asaf Karagila Jun 12 '18 at 16:05
• I don't see why this implies "only definable sets exist". How do you even define "definable set" internally? – Asaf Karagila Jun 12 '18 at 16:08

Your proposed axiom schema is not consistent with ZF:

ZF proves that $V_{\omega+\omega}$ exists, and if we instantiate your axiom schema with

• $\phi(x)$ meaning $x\in V_{\omega+\omega}$
• $\pi(x)$ meaning some tautology
• $\tau(x,y)$ meaning $x=y$

then it is easy to establish the premises of your schema. (The two last conjuncts on the LHS become trivial with this $\pi$ and $\tau$). It then concludes $\forall x: x\in V_{\omega+\omega}$, or in other words $V_{\omega+\omega}$ is a universal set, which is known to be inconsistent with Selection.

The fact that there are instances with more complex $\pi$ and $\tau$ that are not as obviously inconsistent with ZF doesn't prevent this instance from being inconsistent.

You might be able to say something closer to what you intend if you work in something like NBG instead of ZF, so you can quantify directly over your $\pi$ and $\tau$.