Proving well-orderedness
Proving that an ordered set is well-ordered can be very challenging. The methods that can be used to do this vary depending on the type of ordered set. There are of course cases when none of this applies, but mainly in the context of pure apeirology, it often does apply.
Proving totality
As one of the two conditions for an order to be a well-order is that it is a total order, proving totality is a significant part of the proof of well-orderedness. In arbitrarily obscure cases, of course, the proof can be arbitrarily unusual itself. However, for common special cases, there are some shared features of the proof.
Expansion systems
In an expansion system, totality translates to "for every pair of terms \( x,y \), one is reachable from the other by expansion".
The order can usually easily be proven to respect a lexicographical order or some other order known to be total (i.e. one can prove \( x\prec y \) implies \( x<y \), where \( \prec \) is the order of the expansion system and \( < \) is a total order), and then it is simply about proving that, intuitively, repeated expansion is never forced to skip any specific term.
Then a common property that directly leads to totality is the conjunction of \( x[n]\preceq x[n+1] \), \( x[n]\prec y\preceq x[n+1]\Rightarrow x[n]\preceq y[0] \), and the statement that iterating \( [0] \) always reaches the minimum eventually, no matter what you start with. The intuitive reason why this implies totality is that if we have \( x<y\prec z \) and \( x=z[n_0][n_1]...[n_m] \), then \( x \) can be reached from \( y \) by repeating \( [0] \) until it reaches something of the form \( z[n_0][n_1]...[n_k][a] \) with \( a>n_{k+1} \), at which point \( [b] \) is used with \( b \) minimal so that this doesn't go below \( x \), and the whole process repeats. The fact that this eventually terminates follows from looking at the \( (n_0,n_1,...,n_k,a) \) that appear that way, and noticing that this decreases lexicographically as the process moves on the sequence always decreases lexicographically and its length is bounded by \( m+1 \), so this form can only be reached finitely many times, and between all that, we're only iterating \( [0] \), which is guaranteed to decrease the term as much as we need, eventually getting us to \( x \) only by expanding \( y \). Keep in mind that this is not a formal proof.
It is not always true that this property holds. This page is currently unfinished.