Does adding a "hereditarization" operator to ZFC result in an equiconsistent theory? Corrections:
I made a number of mistakes when formulating this question. These include but are not limited to: saying hereditary set when I meant transitive set.

A hereditary set is the empty set or a set whose elements are all hereditary sets. Equivalently, the following holds if and only if a set $A$ is hereditary.
$$ \forall x \mathop. (x \,(\in^2)\, A \to x \in A) $$
Naively, it seems to me like adding a hereditarization operator $h(X)$ where $X$ is a set is possible and makes intuitive sense. However, I'm wary of the $(\in^n)$ operation, which is quantifying over syntax in an odd way.
$$ z \in h(X) \;\; \text{if and only if} \;\; \exists n \ge 1 \mathop. z\;(\in^n)\;X $$
Temporarily setting aside the question of whether the hereditarization operator is useful for anything, how do I show that adding it results in a theory that's equiconsistent with ZFC? (ZFC is a reduct of ZFC+$h$, so that direction is trivial).
Is adding $h$ to ZFC merely an extension by a definition? I'm pretty sure that it isn't because the definition does too much but am not certain.
 A: It sounds (your symbolic definition doesn't actually work, as Asaf observed) like you're talking about the transitive closure operation, where $tc(x)$ is the set of elements of $x$, or elements of elements of $x$, or etc. If so, the situation is quite the opposite of your expectation: $\mathsf{ZF}$ can already do that!
While on the face of things the definition of the transitive closure looks like an infinitely long definition, we can in fact collapse it to a single first-order formula - so that in fact it already exists (as a definable class operation) in $\mathsf{ZF}$. Specifically, say that $x\in^?y$ iff there is some finite sequence of sets whose first term is $x$, whose last term is $y$, and whose $n$th term is $\in$ its $(n+1)$th term. We can talk about finite sequences by talking about functions with domain a finite ordinal.
$\mathsf{ZF}$ then proves that for each set $y$ the class $\{x: x\in^?y\}$ is a set. The key axiom (scheme) here is replacement, which more generally justifies all sorts of seemingly-infinitary constructions in a purely first-order way.

As a first step, try to prove the following: that for each $x$, the class of "finite iterated powersets" of $x$ is a set, that is, the class $\{y: \exists n\in\omega(y=\mathcal{P}^n(x))\}$ is a set (part of this exercise is to precisely formulate this claim!).

If we drop replacement then things become quite hairy: $\mathsf{Z}$ (= $\mathsf{ZF}$ without replacement) cannot prove that all sets have transitive closures, and more generally all sorts of "obvious" recursive constructions break down. I'm not an expert on set theories without replacement in general, but Mathias has several papers on them (see e.g. here).

Now granted, there is a subtlety here. Suppose $M$ is a non-$\omega$-model of $\mathsf{ZFC}$, that is, $M\models\mathsf{ZFC}$ but $\omega^M\not\cong\omega$ ($M$'s natural numbers are nonstandard). Then when we consider the above-indicated definition inside $M$ of "transitive closure," we'll see some spillage:

Suppose $M$ is a non-$\omega$-model of $\mathsf{ZFC}$. Then there are $x,y\in M$ such that:

*

*$M\models x\in tc(y)$, but


*there is no finite sequence $a_0,a_1,...,a_k$ of elements of $M$ such that $x=a_0\in^Ma_1\in^M...\in^Ma_k=y$, and indeed


*the set of elements of $M$ which are "(truly-)finite-depth-elements" of $y$ is not definable in $M$.

This is a good exercise, and points to the limitations of "internal definition by recursion." The point is that a non-$\omega$-model $M$, by virtue of "being wrong about $\mathbb{N}$," will also be wrong - in specific ways! - about recursive constructions. But this isn't news: this same sort of issue happens whenever we consider "internalizations" of non-first-order notions, and is just something you generally have to be wary of throughout model theory and set theory.
