3
$\begingroup$

I am looking for a second order proof that ordinals are well-ordered up to $\epsilon_0$.

So, starting with encoding those ordinals in numbers, defining the < relation on those encoded ordinals and then prove the well-ordering and as consequence, that transfinite induction is allowed.

Preferably the proof is such that it is close to a formal proof.

I have been searching with Google, but I can't find anything useful. I can construct the proof by myself, it isn't that difficult, but is there some kind of standard work that contains these proofs?

Thanks in advance.

$\endgroup$
3
  • 4
    $\begingroup$ There is no canonical notion of "second order proof". Which notion do you have in mind? $\endgroup$
    – Goldstern
    Mar 20, 2016 at 23:48
  • $\begingroup$ A system where you can quantify over predicates. $\endgroup$
    – Lucas K.
    Mar 21, 2016 at 20:03
  • 1
    $\begingroup$ "A system where you can quantify over predicates" describes the language of second order logic. This description does not tell you which proofs you allow. One way (the cheap way, but still good enough for most of mathematics) is to translate second order statements into first order statements in the language of ZFC, and then use your favorite first order proof system (plus ZFC axioms, or more) to analyse these statements. $\endgroup$
    – Goldstern
    Mar 22, 2016 at 0:29

1 Answer 1

10
$\begingroup$

The usual proof that the ordinal notations for ordinals below $\varepsilon_0$ is well-ordered takes place in set theory and uses the fact that actual ordinals (i.e., not notations) are well-ordered.

The proof relies on Cantor Normal Form: that every ordinal $\alpha$ can be written in a unique way in the form $$\alpha = \omega^{\beta_1}n_1 + \omega^{\beta_2}n_2 + \cdots + \omega^{\beta_k}n_k$$ where $\beta_1 \gt \beta_2 \gt \cdots \gt \beta_k$ and $1 \leq n_1,n_2,\ldots, n_k \lt \omega$.

By induction on $\alpha \lt \varepsilon_0$, show that $\alpha$ has a unique ordinal notation. To do this, note that f $\alpha \lt \varepsilon_0$ then we must have $\alpha \gt \beta_1 \gt \beta_2 \gt \cdots \gt \beta_k$ and so each exponent $\beta_i$ has been shown to have a unique notation.

The result of this process is an order-preserving function from the ordinal $\varepsilon_0$ to your set of notations which is the inverse of the evaluation map that goes the other way around. This isomorphism shows that your set of notations is well-ordered.

If you're concerned about using ZFC, note that this proof works in much weaker systems of set theory. If you're still concerned, you can actually work in subsystems of second-order arithmetic.

The trick to make things work in second-order arithmetic is explained in the excellent paper:

Alberto Marcone and Antonio Montalbán, The Veblen functions for computability theorists, J. Symbolic Logic 76 (2011), no. 2, 575--602; arXiv:0910.5442.

What you need is contained in Theorem 3.1:

If $\mathcal{X}$ is a $Z$-computable linear ordering, and $\omega^{\mathcal{X}}$ has a $Z$-computable descending sequence, then $Z'$ can compute a descending sequence in $\mathcal{X}$.

Since $\omega$ is well-ordered, we can use this to show even in $\mathsf{ACA}_0$ that $\omega^\omega$ is well-ordered, that $\omega^{\omega^\omega}$ is well-ordered, etc. Since $\mathsf{ACA}_0$ has limited induction, this does not prove that $\varepsilon_0$ is well-ordered in $\mathsf{ACA}_0$. (Indeed, the proof-theoretic ordinal of $\mathsf{ACA}_0$ is $\varepsilon_0$!) However, this does easily show that $\varepsilon_0$ is well-ordered in the standard model of second-order arithmetic, which appears to be enough for your purposes. (If I misunderstood your purposes, keep reading to Theorem 3.4 which shows that $\varepsilon_0$ is provably well-ordered in $\mathsf{ACA}_0^+$.)

$\endgroup$
1
  • $\begingroup$ Thanks, I think this is what I am looking for. But just for curiosity, when did you learn about ordinals? Already during your study, or afterwards? Because I am considering writing a (educational) book about logic, with different subjects than the usual ones. And writing something about ordinals is one of them. I only learned about it after my study in bits and pieces. $\endgroup$
    – Lucas K.
    Mar 21, 2016 at 20:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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