# Axiomatizations of arithmetical parts of theories

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.

• Somewhat related: math.stackexchange.com/questions/1989762/… – Noah Schweber Jul 2 '17 at 1:41
• Surely this is not known for ZFC... – Will Sawin Jul 2 '17 at 4:03
• @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. – Noah Schweber Jul 2 '17 at 18:25
• @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. – Will Sawin Jul 3 '17 at 3:00

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.
• 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. – James Hanson Jun 30 '18 at 16:23