For common theories that talk about something more general than firstorder arithmetic (e.g. set theories and subsystems of secondorder 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_1CA$, $ATR_0$, $\Pi^1_1CA$, $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 syntaxchecking instead of anything fancy), instead of using cheap tricks like from the proof of Craig's theorem.

2$\begingroup$ Somewhat related: math.stackexchange.com/questions/1989762/… $\endgroup$– Noah SchweberJul 2 '17 at 1:41

$\begingroup$ Surely this is not known for ZFC... $\endgroup$– Will SawinJul 2 '17 at 4:03

1$\begingroup$ @WillSawin Note that it's trivial to provide an axiomatization of the arithmetical consequences of ZFC; I do doubt that a natural axiomatization exists, but surely "surely" isn't justified there. $\endgroup$– Noah SchweberJul 2 '17 at 18:25

$\begingroup$ @NoahSchweber My confidence in the word "surely" is based not on any mathematical argument but just in the fact that, if a natural axiomatization is known, it would be significant enough that I would have heard of it. $\endgroup$– Will SawinJul 3 '17 at 3:00
A somewhat general method has been explained by Azriel Lévy [Axiomatization of induced theories, Proc. Am. Math. Soc. 12, 251253 (1961); ZBL0178.31603; MR0122702] The method does not give axioms that are very intuitive, but I think they fit your "rudimentary syntaxchecking" 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 Z_{2} also has this property, but finitely axiomatizable theories will not have this property.

1$\begingroup$ This is a beautiful result, +1. However, note that in describing the axiomatization we still make reference to ZF itself, and so I don't think this is completely satisfying. $\endgroup$ Jul 2 '17 at 18:16

$\begingroup$ Why is it necessary that the theory be essentially reflexive? It seems like having an $\omega$model or being sound enough to encode standard proof theory ought to be enough. $\endgroup$ Jun 30 '18 at 16:23

$\begingroup$ Why have $\Phi$ range over finite fragments? Why not simply add all statements of the form "If ZF proves $\hat\sigma$ then $\sigma$"? $\endgroup$ Dec 5 '21 at 1:38

$\begingroup$ On second thought, perhaps that's the arithmetic part of ${\sf ZF}+{\rm Con}({\sf ZF})$, not of $\sf ZFC$. EDIT: Yeah, take $\sigma=F$ $\endgroup$ Dec 5 '21 at 1:42