How can we know the well-foundedness of $\epsilon_0$?

Question

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}$?

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$.