Existence of well-ordering of epsilon_0 in weak theories

Question

In a discussion on a youtube video on the hydra game I jokingly mentioned how everyone was assuming that $\varepsilon_0$ was well-ordered. This lead to a bit of disagreement (in a nice way!) about the existence of the well-ordering of $\varepsilon_0$, assuming that $\varepsilon_0$ exists in whatever weak theory one was working in. The person with whom I was discussing seemed to think it obvious that if $\varepsilon_0$ existed, then it was an ordinal, hence well-ordered. I am very skeptical, to say the least. To clear things up, I said I would ask here:

Is it possible, in some suitably weak theory, to define (by a code, or outright) the object $\varepsilon_0$ whose elements (or 'elements') are the usual countable ordinals given by Cantor normal form using only smaller ordinals, but the well-ordering on $\varepsilon_0$ is not available in the theory? What is a good reference for the answer, in either case?

To me this seems like it should be true, but I can't pin down what the required weak theory is. Some form of second-order arithmetic seems reasonable to try, but I don't want one that implies the consistency of (first-order) PA, since then clearly $\varepsilon_0$ is well-ordered.

Answer 1

The existence of $\epsilon_0$ and its order is not a problem, its well-foundedness is.

Cantor normal forms (recursively expanded) of ordinals below $\epsilon_0$ can be written as strings over a finite alphabet, and in that form can be manipulated in weak fragments of arithmetic, say in $I\Delta_0+\mathrm{EXP}$. (Even much weaker theories would suffice, such as a theory of polynomial-time functions.)

That is, $I\Delta_0+\mathrm{EXP}$ can define $\epsilon_0$ (as a “definable class” of Cantor normal forms) in a natural way by a low-complexity ($\Delta_0(\exp)$) formula, and it can also define the order $\alpha<\beta$ on its elements, and basic operations like $\alpha+\beta$, $\alpha\cdot\beta$, and $\alpha^\beta$. The theory can prove elementary properties of these operations such as associativity, and in particular, it can prove that $<$ is a linear order. When interpreted in the standard model of arithmetic $\mathbb N$, these definitions give a structure isomorphic to the actual $(\epsilon_0,<,+,\cdot,x^y)$ from the outside world.

In a “second-order” theory of arithmetic like $\mathrm{RCA}_0^*$, we can even turn the above definition of $\epsilon_0$ into an actual object of the theory, rather than just a definable class.

However, what these relatively weak theories cannot prove is that $<$ is a well order, i.e., that it is well founded. More precisely, well foundedness is a second-order property, and thus can be properly stated only in second-order theories: $\forall X\,[\forall\alpha\in\epsilon_0\,((\forall\beta<\alpha\,\beta\in X)\to\alpha\in X)\to\forall\alpha\in\epsilon_0\,\alpha\in X]$. In first-order theories of arithmetic, it is approximated by a transfinite induction schema; $I\Delta_0+\mathrm{EXP}$, or even $\mathrm{PA}$, cannot prove the $\epsilon_0$-induction schema even for formulas of low complexity ($\Delta_0$).