What's the consistency strength of restricting parameters in axioms of ZFC (other than Extensionality and Foundation schema) to parameter free definable sets?
So for example, the axiom of pairing would be restricted to:
if $\psi,\phi$ are formulas in which only $``y"$ occur free, and $``y"$ never occur bound, then: $$\forall a \forall b \, [a=\{y: \phi\} \land b=\{y: \psi\} \to \\\exists x \forall y (y \in x \Leftrightarrow y=a \lor y=b)]$$
Where: $k=\{y:\phi\} \iff \forall y \, (y \in k \iff \phi)$
Infinity is stipulated as the existence of a set of all finite von Neumann ordinals.
Choice also restricted to parameter free definable sets, that is: "for any parameter free definable family of nonempty pairwise disjoint sets, there is a set that has singleton intersections with each set in that family. Formally, that is:
if $\phi$ is a formula in one free variable $``y"$; then:
$$\forall a [a=\{y:\phi\} \land \forall x,y \in a (x \neq \emptyset \land x \cap y = \emptyset) \to \\\exists b \, \forall x \in a \, \exists y \, (b \cap x = \{y\})$$
The foundation schema is the usual one, that is:
Foundation: if $\phi(x)$ is a formula in which $``x"$ occur free, and only free; and in which $y$ doesn't occur, and if $\phi(x|y)$ is the formula obtained by merely replacing all occurrences of $``x"$ by $``y"$, then: $$\forall \vec{w} \, [\exists x (\phi(x)) \to \exists x (\phi(x) \land \forall y (\phi(x|y) \to y \not \in x))]$$
Extensionality is written as usual.
This theory though proves induction over naturals, yet it cannot prove basic facts about arithemtic. For example, I don't see a clear proof that every natural must have a successor, simply because there is no proof that all naturals are parameter free definable, and the pairing and union axioms are restricted to parameter free definable sets. One can define relations of successor, addition, and multiplication, "<", exponentiation, etc.., but one cannot prove basic facts about those relations.
What is the exact consistency strength of this theory, can it for example be complete?
If we add the axiom of every natural has a successor. Would the resulting theory be capable of interpreting $\sf PA$? If so, would it then be interpretable in a known consistent fragment of second order arithmetic?