What is the consistency strength of definable axiomatization of ZFC?

Question

Let $x^\phi$ be the set $x$ that is definable after the parameter free formula $\phi$, i.e. formally we have: $$\forall y (y \in x^{\phi} \leftrightarrow \phi(y))$$

Now by $\text{definable ZFC}$ it is meant the theory having axioms of $\text{ZFC}$ from definable parameters, so every axiom of ZFC becomes a schema, for example axiom of pairing becomes:

Definable Pairing schema: if $\phi, \psi$ are parameter free formulas, then: $$\forall a^\phi, b^\psi \exists x \ \forall y \ (y \in x \leftrightarrow y=a \lor y=b)$$, is an axiom.

Definable Separation schema would be written as: if $\phi_1,...,\phi_n$ are parameter free formulas, and if $ \psi(y,x_1 ^{\phi_1},..,x_n^{\phi_n}) $ is a formula in which only symbols $``y,x_1^{\phi_1},..,x_n^{\phi_n}" $ can occur free, and only occurring free, then:

$$\forall x_1^{\phi_1},..,x_n^{\phi_n} \exists x \forall y \ [y \in x \leftrightarrow y \in x_n^{\phi_n} \wedge \psi(y,x_1^{\phi_1},..,x_n^{\phi_n})]$$, is an axiom.

The same to be applied over all other axioms of $\text{ZFC}$, and infinity is axiomatized in a definable manner like there exists a set of all finite von Neumann ordinals. The only two axioms that are not presented in a definable manner are Extensionality and Foundation.

The formulation of axiom of infinity is the following:

Definable infinity: $\exists x \forall y (y \in x \leftrightarrow y \text{ is a finite von Neumann ordinal})$, where "$y$ is a finite von Neumann ordinal" is definable after the parameter free formula "$y$ is a transitive set of transitive sets that when $y$ is non empty then $y$ is a successor and every non-empty element of $y$ is a successor", where "transitive" means a set whose elements are subsets of it, and "a successor" means a set that is a union of a set and its singleton.

Questions:

1. is $\text{definable ZFC}$ equi-interpretable with $\text{ZFC}$?

2. if Yes to 1, then is $\text{definable ZFC}$ bi-interpretable with $\text{ZFC}$?

3. if No to 1, then what would be the consistency strength of $\text{definable ZFC}$?

Answer 1

The idea of definable separation and definable replacement may be much weaker than one expects, because they can hold vacuously. For example, consider the integers with their successor relation: $$\langle \mathbb{Z},\varepsilon\rangle,$$ where $n\mathrel{\varepsilon} (n+1)$ and these are the only instances of the relation. In this model, every set has exactly one element, its predecessor.

Since this structure has nontrivial automorphisms by translation, which move every point, it has no definable elements. It consequently satisfies vacuously all the definable axioms of set theory: definable pairing, definable power set, definable separation, definable replacement, definable union. It also satisfies full extensionality and full foundation.

This structure also satisfies what I find to be a natural version of the infinity axiom, which asserts, "there is a set containing all the finite von Neumann ordinals." The reason is that this structure has no transitive sets and therefore no objects that would be finite von Neumann ordinals; so every object contains them all vacuously as elements. So this structure satisfies a version of the infinity axiom.

But you stated your infinity axiom to require a set whose elements are exactly the finite von Neumann ordinals, and this assertion is not true in the structure.

Indeed, since your infinity axiom implies explicitly that there is at least one definable set, you will get the empty set from it by an instance of separation and therefore also $\{\emptyset\}$ and so on. And you will get $P(\omega)$ and iterations of this, and so ultimately there will be some actual set theory going on in your theory after all.