Is there a 'nice' axiomatization in the language of arithmetic of the statements ZF proves about the natural numbers?

Solution 1:

I'm hesitant to answer negatively - as soon as I do, someone's going to post some neat fact I didn't know about! - but I strongly suspect that the answer to your question is no, there is no such nice axiomatization known currently.

Why? You mention $ACA_0$. Well, that the arithmetic consequences of ZF are much much much much more than those of $ACA_0$: for example, ZF proves the consistency of $ACA_0$, not to mention $ATR_0$, $\Pi^1_1-CA_0$, $Z_2$, $Z_3$, . . . , $Z_\omega$, . . . , $KP$, . . . , $Z$ (= Zermelo set theory), . . . More generally, suppose $\alpha$ is a "reasonably definable" ordinal (e.g. $\omega_1, \omega_2, \omega_\omega, ...$). Then $ZF$ proves that $V_\alpha$ exists, and hence that $Th(V_\alpha)$ is consistent.

Now, $ZF$ can't decide what $Th(V_\alpha)$ is, in general (is the continuum hypothesis true? that's a question about $Th(V_{\omega+3})$!), but $ZF$ will be able to prove that certain things are in $Th(V_\alpha)$ (e.g. $ZF$ proves that $V_{\omega+\omega}$ is a model of $Z$). So we can take "large" definable $\alpha$s, and isolate "known subtheories" of $Th(V_\alpha)$, and $ZF$ proves the consistency of these theories - and this gives us a truly daunting class of arithmetic consequences of $ZF$. Before we even begin to do anything interesting, we've already left the realm of known theories of arithmetic far behind.

There's another twist on this question that occurs to me. Suppose I want to describe the arithmetic consequences of some stronger theory ZFC+X (knowing me, X is probably a large cardinal property :P). Well, that's going to be even harder than describing the arithmetic consequences of ZFC. But, maybe I can "reduce" to the ZFC problem: what if I just want a "nicely" axiomatized set $\Gamma$ of arithmetic sentences such that maybe $\Gamma$ doesn't exhaust the arithmetic consequences of ZFC+X, but the arithmetic consequences of ZFC+$\Gamma$ are exactly the arithmetic consequences of ZFC+X!

Let's say that such a $\Gamma$ "captures ZFC+X arithmetically over ZFC." Then: for "natural" such X (large cardinals, forcing notions, statements about cardinal arithmetic, etc.), can we find "natural" $\Gamma$ which capture ZFC+X arithmetically over ZFC?

To the best of my knowledge no such example exists. Note that even ZFC+"Con(ZFC+X)" doesn't in general capture the arithmetic consequences of ZFC+X: ZFC+X will have some high-complexity arithmetic consequences (in the sense of the arithmetic hierarchy, while consistency statements are merely $\Pi^0_1$, and we can find e.g. true $\Pi^0_2$ sentences which are not provable from ZFC + all true $\Pi^0_1$ sentences! (If I recall correctly, "ZFC is $\Sigma^0_1$ correct" is such a statement.)

And the same situation appears to hold with regard to describing the arithmetic consequences of ZFC "modulo" smaller theories, like KP or Z.

Again, however, this is not my area of expertise, so I will be happy to be corrected if something is known along these lines!