I think the question can be quite philosophical, but I see that $WF(\epsilon_0)$ is widely accepted as one of the attributes of the natural numbers.

  • Gentzen proved $Con(PA)$ with $PRA+WF(\epsilon_0)$.
  • The proofs of some theorems of arithmetic, such as Goodstein's theorem or the termination of Hydra Game, essentially rely on $WF(\epsilon_0)$.

However, I'm curious if there ever is an justification about this. I'm aware of that ZFC provides such justification, but also I couldn't convict myself whether the set $\omega$ in ZFC (one of the interpretation of it) really gives us the natural number $\mathbb{N}$.

(Just to be clear: the statement of $WF(\epsilon_0)$ itself doesn't require any set theory - it can be coded into arithmetic statement.)

On the other hand, highly unlikely, but if ever $WF(\epsilon_0)$ turns out to be equivalent with $Con(PA)$ or $Con(PA+Con(PA))$, all of which have $\mathbb{N}$ as a model, we know that it is true. If I understand formalism correctly, even the strictest formalists wouldn't deny these consistency statements because they can't make any deduction without having actual natural numbers or strings, which is equivalent to having PA.

I am relatively new on metamathematics field, and I learned logic from a formalist. ZFC seems just another random formal theory to me, except that I can't do second-order logic without some decent set theory.

So my question is this: is there any non set-theoretical justification for $WF(\epsilon_0)$, which involves the natural number $\mathbb{N}$?

  • 1
    $\begingroup$ Second-order arithmetic can prove $WF(\varepsilon_0)$ too. $\endgroup$
    – Wojowu
    Apr 23, 2020 at 10:19
  • 1
    $\begingroup$ Timothy Chow has written an expository article on the consistency of arithmetic and the induction up to $\epsilon_0$. It appeared in the Mathematical Intelligencer (timothychow.net/consistent.pdf). Maybe he can say something about this. $\endgroup$
    – godelian
    Apr 23, 2020 at 10:30
  • $\begingroup$ @Wojowu Actually I mentioned in OP about second-order scheme and I'm not satisfied with it. I believe that proving something with second-order arithmetic is technically equivalent to proving it with a set theory, which must be backed up with a first-order characterization such as ZFC. $\endgroup$
    – Paul Sohn
    Apr 23, 2020 at 11:01
  • $\begingroup$ @godelian Not exactly. I've read the article a month ago. Perhaps I skimmed a lot, but I couldn't get any information further than "$PRA+WF(\epsilon_0)$ is neither stronger nor weaker than $PA$, and it proves $Con(PA)$." No claim that $WF(\epsilon_0)$ actually holds for the natural numbers. $\endgroup$
    – Paul Sohn
    Apr 23, 2020 at 11:18

1 Answer 1


Let me use the notation $\omega_n$ for an exponential tower of $\omega$'s of height $n$, so $\omega_{n+1}=\omega^{\omega_n}$. Then $\epsilon_0$ is the supremum of $\{\omega_n:n\in\omega\}$. PA proves well-foundedness of $\omega_n$ for each individual $n$, but it needs a separate proof for each $n$. If you believe PA (which you apparently do) and you believe in the natural numbers (which, unlike your formalist teacher, you also apparently do), then you should accept that "for all $n$, $\omega_n$ is well-founded." The well-foundedness of $\epsilon_0$ then follows, because, if there were an infinite decreasing sequence in $\epsilon_0$, its first term and therefore all its terms would be below $\omega_n$ for some $n$.

  • 3
    $\begingroup$ The funny thing is that you can even prove in PA that PA separately proves well-foundedness of $\omega_n$ for each n. You just can't go from this to "$\omega_n$ is well-founded for all $n$" in PA (by Lob). But if PA is sound then this conclusion does follow and therefore $\epsilon_0$ is well-founded. $\endgroup$
    – Nik Weaver
    Apr 23, 2020 at 14:32
  • $\begingroup$ @NikWeaver Can you give a source for the claim in your first sentence or a brief sketch of how one would show that? $\endgroup$
    – JoshuaZ
    Apr 23, 2020 at 14:34
  • $\begingroup$ Might take a while to fully understand the scheme, but I think this is the answer I was looking for. Thanks! $\endgroup$
    – Paul Sohn
    Apr 23, 2020 at 14:52
  • $\begingroup$ @JoshuaZ I don't have a source ... it's "clear" because you can give a uniform description of the $n$th proof $P_n$, and seeing that each of them is a proof in PA is easy. So I guess it would be pretty easy to write down a proof of this in PA, just very tedious. $\endgroup$
    – Nik Weaver
    Apr 23, 2020 at 15:59
  • 2
    $\begingroup$ @NikWeaver I just mean that psychologically it's hard to imagine accepting PA without accepting PA + "PA is sound" which also implies $WF(\epsilon_0)$. $\endgroup$
    – cody
    Apr 24, 2020 at 17:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.