By "formal analogies" between the metamathematics of $\mathsf{ZFC}$/set theory and $\mathsf{PA}$(=Peano Arithmetic)/first order arithmetic, I mean facts such as the following:

We are considering a first-order theory ($\mathsf{ZFC}$ or $\mathsf{PA}$) motivated as a first-order approximation to a second-order theory (second-order $\mathsf{ZFC}^2$ or $\mathsf{PA}^2$) which is "more or less" categorical; because of this, some axioms (the separation and replacement axioms on the one hand, the induction axiom on the other) have to be stated as axiom schemes in the first-order theory.

There is an interesting hierarchy of formulæ, $\Sigma_n$ or $\Pi_n$, based on alternations of quantifiers (viz.: the arithmetic hierarchy vs. the Lévy hierarchy); at the lowest ($\Delta_0$) level of this hierarchy are formulæ with only "bounded" quantifiers.

There is a uniform truth predicate for any (concrete) given level of the hierarchy, which is built upon some kind of absoluteness of $\Delta_0$ formulæ. As a related fact, the infinite axiom schemes are naturally stratified along the hierarchy (they can be cut off at the $\Sigma_n$ level and stated as a single formula for each concrete $n$).

There is a reflection theorem which ensures that any finite set of true statements (or one bounded in the hierarchy of formulæ) is consistent. In particular, the full theory proves the consistency of the subtheory with the axiom schemes cut off at the $\Sigma_n$ level: that is, the theory ($\mathsf{ZFC}$ or $\mathsf{PA}$) is reflexive. In fact, it is even

*essentially*reflexive (every consistent extension is reflexive).There is a conservative two-kinded extension (Gödel-Bernays on the set theoretical side, $\mathsf{ACA}_0$ on the arithmetical side) which is obtained by allowing formation of classes but only with a comprehension scheme for such classes that does not involve quantifying over classes; remarkably, this conservative two-kinded extension is finitely axiomatizable. There is also a standard strictly stronger two-kinded extension (Morse-Kelley on the set-theoretical side, second-order arithmetic $\mathsf{Z}_2$ seen as a first-order theory on the arithmetical side).

(I hope I didn't mess things up too much, but all of these facts are standard and can be found in standard textbooks such as Jech's *Set Theory* for the set-theoretical side and Hájek and Pudlák's *Metamathematics of First-Order Arithmetic* plus Simpson's *Subsystems of Second-Order Arithmetic* for the arithmetical side.)

I'm sure many more examples can be found. Maybe I should also nod to the similarity between proof theory of extensions of $\mathsf{PA}$ by analysing ordinal notations made by collapsing recursively large ordinals, and large cardinal extensions of $\mathsf{ZFC}$ — or maybe not.

Yet as striking as this analogy seems, nobody seems to comment upon it as far as I know. (At the very least, this seems pedagogically regrettable: I'm sure all of the above statements would be more memorable to students if the analogous statements were made explicit.)

So: is there some deeper truth to be found behind this parallelism? (Or are all my sample facts just aspects of a single phenomenon? Or is this just a red herring?) Might it make sense to bring $\mathsf{ZFC}$ and $\mathsf{PA}$ under an umbrella metatheory so that the above facts can be proved in a common formalism? At the very least, is there a textbook I missed where the analogy is played out in some detail?

And perhaps more thought provokingly: can one give an example of a completely different kind of theory that is just as similar to $\mathsf{ZFC}$ and $\mathsf{PA}$ as they are to each other?

(I'm of course aware that are also huge differences between $\mathsf{ZFC}$ and $\mathsf{PA}$; but I would tend to say that they make the similarities all the more striking.)