For common theories that talk about something more general than first-order arithmetic (e.g. set theories and subsystems of second-order arithmetic), are there nice axiomatizations of their arithmetic parts? I know that the arithmetic part of $ACA\_0$ is $PA$ and the arithmetic parts of $RCA\_0$ and $WKL\_0$ are both $I\Sigma^0\_1$, and I'm mostly interested in stronger theories (like $\Delta^1\_1-CA$, $ATR\_0$, $\Pi^1\_1-CA$, $Z\_2$, $KP$, $ZFC$). I'm also aware that Craig's theorem provides a recursive axiomatization of the arithmetical part of any recursively enumerable theory, but I'm interested in "nice" axiomatizations (basically meaning finite lists of axioms and schemas, where you should be able to tell whether a sentence satisfies a schema by doing some rudimentary syntax-checking instead of anything fancy), instead of using cheap tricks like from the proof of Craig's theorem.



Axiomatizations of arithmetical parts of theories
A somewhat general method has been explained by Azriel Lévy
[[*Axiomatization of induced theories*](https://doi.org/10.1090/S0002-9939-1961-0122702-2), Proc. Am. Math. Soc. 12, 251-253 (1961); [ZBL0178.31603](https://zbmath.org/?q=an:0178.31603); [MR0122702](http://www.ams.org/mathscinet-getitem?mr=122702)] The method does not give axioms that are very intuitive, but I think they fit your "rudimentary syntax-checking" criterion as I understand it.


In short, the arithmetical part of ZF is axiomatized by the Peano axioms and all arithmetical sentences which say "if $\Phi \vdash \widehat{\sigma}$ then $\sigma$" where $\Phi$ ranges over finite subsets of ZF, $\sigma$ ranges over arithmetical sentences, $\widehat{\sigma}$ is the sentence in the language of set theory that says that $(\omega;0,1,{+},{\cdot}) \vDash \sigma$. Lévy proves that the same is true for any essentially reflexive theory (a theory that proves the consistency of any finite fragment of itself). Any recursive extension of ZF has this property and I think Z2 also has this property, but finitely axiomatizable theories will not have this property.


