Interpretation of $ZFC^-$ in 2nd order Peano arithmetic

Question

Let $Z_2^-$ be the 2nd order Peano arithmetic without the schema of Countable Choice. It has been known, since 1960s at least, that $ZFC^-$ (without the power set) admits an interpretation in $Z_2$ via (some part of) sets in $Z_2$ that code well-founded trees. I wonder is there a published clean self-contained construction of this interpretation.

Answer 1

This started out as a comment, but it ended up too long so here it is as an answer.

The best reference I know for this is Simpson's book Subsystems of Second-Order Arithmetic, who does most—not quite all!—of what you need across Sections 3–6 of Chapter VII. A disadvantage of his presentation for your purpose, however, is that he's concerned with more precise questions, about what you get with weaker axioms to start with. So it's a little bit of work to extract just the one interpretation result you want from his more general work.

With that in mind, let me summarize what Simpson does, how it answers what you want, and what the missing piece is.

1. In Section 3 he gives the construction of coding sets by well-founded trees. Simpson uses $\mathsf{ATR}_0$ (so transfinite recursion for arithmetical properties) as his base theory here. This suffices to prove the basic facts to make the coding work, and so $\mathsf{ATR}_0$ can interpret a fragment of $\mathsf{ZFC}^-$. (As Joel noted in a comment, this construction is also useful in other contexts. That being able to do transfinite recursion is important for the construction is also apparent in the dissertation he linked.)

2. In Section 4 Simpson discusses how to carry out the construction of the constructible universe in this framework. Again, $\mathsf{ATR}_0$ suffices. Briefly, the main idea is that $\mathrm L$ is built up by a recursion of arithmetical operations, because the $\mathrm{Def}$ operator is itself built by a recursion of arithmetical operations.

3. In Section 5 he turns to stronger Comprehension schemata. The main point is that $\Pi^1_{k+1}$-Comprehension in second-order arithmetic interprets $\Pi_1$-Separation in set theory, for $k \ge 1$. Another important fact he proves is that $\Pi^1_{k+1}$-Comprehension remains true if you restrict to only the constructible sets.

4. In Section 6 he turns to the $\mathsf{AC}$ schema (or rather, fragments of this schema). The key result here is Theorem VII.6.16, that if every set is constructible then $\Sigma^1_k\text{-}\mathsf{AC}$ is equivalent (over $\mathsf{ATR}_0$) to $\Delta^1_k$-Comprehension, for $k \ge 3$. (For smaller $k$, $\Sigma^1_k\text{-}\mathsf{AC}$ is outright provable without needing every set to be constructible.)

5. The one thing Simpson doesn't seem to give in his book is an argument that the $\mathsf{AC}$ schema in arithmetic implies the model of set theory coded by well-founded tree satisfies the Collection schema. The way you can prove this is the same as in the dissertation Joel linked. Briefly: Suppose there is a well-founded $T$ so that for every $X \in^* T$ there's a tree $Y$ satisfying some property. (Here I use $\in^*$ to mean the membership relation as defined on the trees.) The quantifying over $\in^*$-elements of $T$ amounts to quantifying over certain nodes in $T$. So we have that for every node there is a tree $Y$ so that blah blah. This is the set-up needed to use $\mathsf{AC}$. We get a listing of all the trees $Y$, and then it's a simple bit of coding to combine together these trees to get a single tree $B$ so that each $Y \in^* B$. Whence we get that the model of set theory coded by the trees satisfies Collection.

Putting this all together: $\mathsf{ZFC}^-$ is interpreted in $Z_2^-$ by coding sets as well-founded trees, where we restrict to only to the constructible sets. Restricting to the constructible sets preserves $Z_2^-$ and also gives the $\mathsf{AC}$ schema. The Comprehension schema implies that the interpreted model satisfies Separation, while the $\mathsf{AC}$ schema implies it satisfies Collection.