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.



Reference request, proof about well-ordering of ordinals
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**](http://dx.doi.org/10.2178/jsl/1305810765), *J. Symbolic Logic* **76** (2011), no. 2, 575--602; [arXiv:0910.5442](http://arxiv.org/abs/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^+$.)


