[FOM] Query on arithmetic and fragments of ZFC

[Colin McLarty]

A widely mentioned "folk theorem" says Peano Arithmetic is proof
theoretically equivalent to Zermelo Fraenkel with choice but without
infinity.  It is not entirely "folk" though, and is well discussed in
"On interpretations of arithmetic and set theory ", Richard Kaye and
Tin Lok Wong (Notre Dame Journal 48(2007), 497-510).  Aki Kanamori
gave me that reference.

A related result says ZFC (with infinity) but with powerset restricted
to positing just n successive powersets of N is equivalent to (n+1)st
order arithmetic.  I thank Harvey Friedman for showing me the value of
this for my work on arithmetic foundations for the Grothendieck
apparatus and Aki for good pointers on how to work in this framework.
A preprint "What is the theory ZFC minus powerset?" by Victoria
Gitman, Joel David Hamkins, and Thomas A. Johnstone shows there are
delicate axiomatic issues here -- but they address independence issues
in set theory rather than proof theoretic strength.

Is there a good reference for the proof theory of ZFC with restricted powerset?

I do not yet know the precise theorems on this, let alone proofs.  And
I would also like good references to cite in an article.

best, Colin