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.

  • 3
    $\begingroup$ I'm not sure I understand the question. The order on $\epsilon_0$ as such can be constructed in very weak fragments of PA, but those theories cannot prove it is a well order (i.e., satisfies appropriate forms of induction). $\endgroup$ – Emil Jeřábek Mar 6 '17 at 9:19
  • 1
    $\begingroup$ @Emil this is exactly the sort of answer I'm after. Details would be good, to settle the argument conclusively. I don't even care about the ordering, merely the existence of $\varepsilon_0$, but the actual definition is perhaps important for my purposes. $\endgroup$ – David Roberts Mar 6 '17 at 9:39
  • $\begingroup$ @EmilJeřábek or, perhaps you mean the order type of $\varepsilon_0$ can be defined in a weak fragment of PA, so we can consider $\varepsilon_0$ to be 'defined' in this way... $\endgroup$ – David Roberts Mar 6 '17 at 10:50
  • 2
    $\begingroup$ The comment from @EmilJeřábek answers the question, but it might be worthwhile to amplify it to say "but those theories and even PA itself cannot prove it is a well order." $\endgroup$ – Andreas Blass Mar 6 '17 at 16:05

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

| cite | improve this answer | |
  • 2
    $\begingroup$ +1. And for the OP, although (an order of type) $\epsilon_0$ is definable as a class in PA in an appropriate sense, we can improve this - working in ACA$_0$, a conservative extension of PA, there actually is an object which is a linear order of type $\epsilon_0$ (again, in an appropriate sense). The "appropriate sense" is that the class/object needs to be interpreted in the standard model. $\endgroup$ – Noah Schweber Mar 6 '17 at 16:41
  • $\begingroup$ @NoahSchweber thanks, that extra detail helps. $\endgroup$ – David Roberts Mar 6 '17 at 22:51
  • $\begingroup$ Emil, while the weak theories and even PA do not prove that the $\epsilon_0$ order on representations is a well order, could you tell me whether they nevertheless prove of every particular computable sequence (or other complexity-limited sequence), that it is a not a descending sequence in the order? In other words, in the models where $\epsilon_0$ is not well-ordered, what is the complexity of the simplest counterexample to well-foundedness? I guess this is closely related to the failure of induction that you mention in your final remark. $\endgroup$ – Joel David Hamkins Mar 7 '17 at 0:03
  • 2
    $\begingroup$ @JoelDavidHamkins I don't think that's the case. I suspect that via the equivalence WF($\epsilon_0$) iff Con(PA), any model in which $\epsilon_0$ is illfounded will have a computable (with standard index, even!) descending chain, corresonding to a putative proof of inconsistency in PA (although that proof will be nonstandard, a standard index can say "look for the lex. least proof of $0=1$," and I think that will be the only parameter needed). But I'm not sure. $\endgroup$ – Noah Schweber Mar 7 '17 at 1:18
  • 1
    $\begingroup$ Yes, there may be a computable descending chain. $\endgroup$ – Emil Jeřábek Mar 7 '17 at 10:00

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.