In this paper, author Nik Weaver warns that there could be questions of $\Sigma_1$-validity of ${\mathrm{ZFC}}$ set theory. As I understand it, he suggests that the axioms of a set theory might be strong enough to decide PA-undecidable statements about Turing machines, and moreover decide them wrongly. Wrongly in the sense that e.g. ${\mathrm{ZFC}}$ might prove for a particular machine $t$ there to "exist" a $n\in {\mathbb N}$ such that $t$ halts at step $n$ (i.e. ${\mathrm{ZFC}}$ proves $\exists n.T(n)$ for some statement $T$ about a particular coding up of a machine $t$), but "in reality" the machine actually can't do that. This wouldn't be a problem w.r.t. consistency, since it affects a statement where Peano arithmetic (${\mathrm{PA}}$) axioms were too weak to make a call on it.

See here for some relevant definitions and this related SE question. The relation between ${\mathrm{PA}}$ and ${\mathrm{ZFC}}$ is subtle but e.g. from reading the answer on the mentioned questions, one would think ${\mathrm{PA}}$ got us covered for any given Turing machine w.r.t. $\sigma_1$. So I'm trying to understand where a loophole is that Weaver points out. To clarify, I'm not interested in an inconsistent ${\mathrm{PA}}$ situation or an inconsistent ${\mathrm{ZFC}}$ situation, but I won't presume any soundness properties of the systems. And for the question, I'm also only interested in machines that could (edit: assuming we could wait arbitrary long and provide the memory capacity) be put on the quest to search for a natural and fail to ever halt - despite ${\mathrm{ZFC}}$ claims.

I know that there are conservativity results of ${\mathrm{PA}}$ over ${\mathrm{HA}}$ on, I think, that level of the hierarchy, and similarly with second order-${\mathrm{PA}}$ v. second order-${\mathrm{HA}}$, as well as ${\mathrm{ZF}}$ over ${\mathrm{IZF}}$. I.e. we know that for $\exists n.(f(n)=0)$-statements of ${\mathrm{HA}}$, won't see anything new in ${\mathrm{PA}}$ (${\mathrm{PA}}$ can't fail the world of HA on that level, so to speak). But do we know anything more about ${\mathrm{ZFC}}$ speaking about PA statements? I'm not sure if results I just listed do in fact clarify the $\Sigma_1$-validity issue on their own. Further (since I read someone bring it up in this context) I wonder whether or how ${\mathrm{ZF}}$ models of itself or of ${\mathrm{PA}}$ could clarify what's possible and what's inconsistent. Is this issue discussed somewhere on that level of the hierarchy, where validity issues in connection with "the real world" would still be "hands on" in this sense (i.e. not stuff about Turing jumps somewhere removed from recursive machines)? Assuming ${\mathrm{PA}}$ is right about the world, can ${\mathrm{ZFC}}$ be wrong about the world in this "wrong promise/wait forever" kind of way? I do understand that "wrong promise" might be orthogonal to a hard "wrong" notion in proof theory.

  • $\begingroup$ I've heard that iteration of a process which at step $n$ writes an integer in "recursive base $2n$" (where the exponents also get translated into recursive base $2n$), change all bases to $2n+1$, and then subtracts one, always terminating is sufficient to show consistency of PA, and therefore can't be proved by PA. But ZFC does prove termination of this calculation with any starting input, essentially as a result of the fact that $\varepsilon_0 = \omega^{\omega^{\cdots}}$ is well-ordered. Though I guess that's probably $\Pi_2$ not $\Sigma_1$. $\endgroup$ Commented Sep 19, 2020 at 0:03
  • $\begingroup$ @DanielSchepler Sounds interesting. It's not a bad apple case, though, is it? Weaver, in chapter 2 starting at around page 6, 7 in the above text, speaks about (quote) "if ZFC gives us bad information about which Turing machines halt", where, for this to be persuasive, I suppose there needs to be a means of judging "bad". If your ordinal-type consistency statement can't be dismissed by other means (the machine would indeed just halt), then this would just give another fair theorem and not a false promise of sorts. Or is a real-world-halting that PA doesn't predict automatically bad? $\endgroup$
    – Nikolaj-K
    Commented Sep 19, 2020 at 0:14
  • $\begingroup$ @Nikolaj-K "is a real-world-halting that PA doesn't predict automatically bad?" You have to distinguish between single halting instances and universally halting programs. The former are pretty boring here: $\mathsf{PA}$ is $\Sigma^0_1$-complete (indeed this is gigantic overill; see e.g. the discussion here), so there are no individual instances of halting computations which $\mathsf{PA}$ or $\mathsf{ZFC}$ miss. However, the statement that such-and-such program halts on all inputs is significantly more complicated - it is $\Pi^0_2$ in general. $\endgroup$ Commented Sep 19, 2020 at 2:04
  • 1
    $\begingroup$ (As Daniel said above.) By Godel, no "reasonable" theory (namely: no consistent computably axiomatizable theory interpreting $\mathsf{Q}$) is $\Pi^0_1$-complete, so a fortiori there will be true $\Pi^0_2$ statements which (say) $\mathsf{ZFC}$ misses. As to the question you ask, it is indeed possible that $\mathsf{PA}$ is fully sound but $\mathsf{ZFC}$ is inconsistent, or that $\mathsf{PA}$ is fully sound and $\mathsf{ZFC}$ is consistent but that $\mathsf{ZFC}$ is not $\Sigma_1$-sound, or so on. $\endgroup$ Commented Sep 19, 2020 at 2:06
  • $\begingroup$ @Nikolaj-K I find your question as written a bit unclear, hence my comments as opposed to an answer. If my comments addressed your question I'll be happy to turn them into an answer, let me know - if not, in what way do they not? $\endgroup$ Commented Sep 19, 2020 at 2:10

1 Answer 1


The question and comment thread seem a bit all over the place; let me collect the various facts which I think together summarize the situation appropriately.

Any "appropriate" theory $T$ - like $\mathsf{PA}$ or $\mathsf{ZFC}$ - is strong enough to verify all true halting facts. That is, such theories are $\Sigma_1$-complete. Conversely, per Godel no such theory is $\Pi_1$-complete. In particular, if $T$ is "appropriate" in the relevant sense then so is $T+\neg\mathsf{Con}(T)$; since this latter theory is $\Sigma_1$-complete, consistent, and proves a false $\Sigma_1$-sentence, it (and a fortiori $T$ itself) must not be $\Pi_1$-complete.

So a consistent theory of the type we're looking at cannot afford to make any false $\Pi_1$ assertions, but it could conceivably make a false $\Sigma_1$ assertion. This distinction between $\Pi_1$ and $\Sigma_1$ explains why there is no tension between Weaver's observation and the "sufficiency" of $\mathsf{PA}$ (and indeed much less) for $\Sigma_1$ propositions.

Finally, $\mathsf{ZFC}$ could indeed be consistent but $\Sigma_1$-unsound even if $\mathsf{PA}$ is fully sound - at least, working within a reasonably weak background theory. Specifically, assuming $\mathsf{ZFC+Con(ZFC)}$ is consistent in the first place then so is $\mathsf{ZFC+Con(ZFC)+\neg Sound_{\Sigma_1}(ZFC)+Sound(PA)}$. (The "$+\mathsf{Sound(PA)}$"-bit is redundant since $\mathsf{ZFC}$ already proves that $\mathsf{PA}$ is fully sound, I'm just including it for explicitness.) So basically we cannot use the correctness of $\mathsf{PA}$ to justify even the $\Sigma_1$-correctness of $\mathsf{ZFC}$ without baking the latter assumption into our base theory at the outset. However, this happens long before we hit $\mathsf{ZFC}$: the same holds for $\Pi^1_1$-$\mathsf{CA_0}$, if memory serves, which is a tiny fragment of $\mathsf{Z_2}$ which is itself a tiny tiny tiny fragment of $\mathsf{ZFC}$. So leaping all the way to $\mathsf{ZFC}$ here is massive overkill, and I think makes this phenomenon appear more mysterious than it actually is.

  • $\begingroup$ On the other hand, all this talk of ZFC not being sound is... peculiar, let's say. $\endgroup$ Commented Sep 21, 2020 at 19:05
  • 1
    $\begingroup$ @AndrésE.Caicedo Not the most peculiar thing I've considered today, though! :P $\endgroup$ Commented Sep 21, 2020 at 19:09
  • 1
    $\begingroup$ @AndrésE.Caicedo: I'm curious now, what is your strongest argument for the (arithmetical) soundness of ZFC? $\endgroup$
    – user21820
    Commented Feb 12, 2021 at 14:41

You must log in to answer this question.

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