It's well known that ZF (equivalently ZFC by this question) proves more about the natural numbers than PA. The set of such statements is recursively enumerable so it is recursively axiomatizable. Is it difficult to explicitly axiomatize these statements in the language of arithmetic?

Obviously 'nice' is somewhat subjective but I think one thing that would qualify is if the set of such statements had an axiomatization that is some finite set of axioms together with some finite set of axiom schemata that are 'quantified over formulas' like the axiom schema of induction, or (I'm not sure if this is equivalent or not) having a conservative extension in the language of $ACA_0$ that is finitely axiomatizable.

  • 3
    $\begingroup$ Why the votes to close? I think this is a nice question. $\endgroup$ Oct 29, 2016 at 22:11

1 Answer 1


While not part of the question itself, I think it's worth noting that there is a huge gap between "model satisfying the arithmetic consequences of $\mathsf{ZFC}$" and "some model of $\mathsf{ZFC}$'s version of the naturals" even when we restrict to the countable setting - see here.

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!

  • 1
    $\begingroup$ I think the situation described in your first paragraph happened anyway on MO: mathoverflow.net/questions/273463/… $\endgroup$ Jul 2, 2017 at 5:52
  • 1
    $\begingroup$ @FrançoisG.Dorais That's a very interesting result, but I personally wouldn't call it natural rather than technical. I think the sticking point is that a natural axiomatization shouldn't refer to ZF itself at any point in its definition. So while it's very interesting, I don't think it falls into the same category as e.g. $I\Sigma_{17}$. Of course this is subjective, but that's my personal opinion. $\endgroup$ Jul 2, 2017 at 18:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .