In the paper On Interpretations of Arithmetic and Set Theory of Kaye and Wong they write:
Equipped with $\in$-induction, we obtain an inverse interpretation of PA in ZF−Inf*. The plan is to define a natural bijection $p: V \to \text{On}$ between the whole universe and the ordinals. The required interpretation can then be obtained by composing this map with the map $o$ defined on $\text{On}$. At first, it appears difficult to see how to use $\in$-induction at all, since the required inductive definition of $p$ is $p(x) = \sum_{y\in x} \, 2^{p(y)}$ and this seems to need a separate induction on the cardinality of $x$ —- just the sort of induction we don’t yet have and are trying to justify. However, there is a way round this problem using ordinal summation.
Here ZF−Inf* is ZF plus the negation of Inf in addition to the axiom TC, which says that every set is contained in a transitive closure.
I don't understand the point the authors are trying to make here. Specifically:
Can't we just define $p(x) = \sum_{y\in x} \, 2^{p(y)}$ using $\in$-induction in ZF-Inf*?
What do they mean by "this seems to need a separate induction on the cardinality of x —- just the sort of induction we don’t yet have and are trying to justify." ?
How can you define the summation over $x$? We have not defined the notion of summation over a given set, even when the set is finite. We finally lead to the definition of Kaye and Wong, when we tried to define the summation over $x$ formally.
Kaye and Wong defined their sum by using set induction on $x$. They suggested that it is likely to define their sum ranged over a finite set $x$ by induction on the size of $x$. (They did not follow it, however.) Our usual sum notation $\sum_{i=1}^n a_n$ only cares the number of terms, not the set of range. It could be the reason why they mention this sentence.