I've been fumbling around with order types and ordinals these past few days. I read about partial, total, and well-ordered structures, and I'm curious to see if a linearly ordered set has no subset with order type $\omega^*$, then it is in fact well ordered. Here $\omega^*$ is the order type of the negative integers.
My idea was this. Let $X$ be some totally ordered set such with subset with order type $\omega^*$. Take any nonempty subset $Y$ of $X$. If $Y$ is finite, it must have a least element, so assume $Y$ is infinite. By way of contradiction, I assume $Y$ has no least element. My strategy was to then somehow construct a subset of $Y$ which has order type $\omega^*$. I do this by first picking an element $a_0$ from $Y$. Since $Y$ has no least element, and since $Y$ is also totally ordered, there must be some other element $a_1\in Y$ such that $a_1\prec a_0$. Again, $a_1$ is not the least element of $Y$, so we can find an element $a_2\in Y$ such that $a_2\prec a_1\prec a_0$. Continuing along, I would eventually have a set $Z=\{\dots,a_3,a_2,a_1,a_0\}$, where I have written it in increasing order. But then $Z$ has order type $\omega^*$, a contradiction.
Does this argument hold up? If so, I feel it is a little handwavey, and the "continuing along" part needs to be formalized. Is there a way to do so with Choice or maybe (transfinite) recursion? I fear I may have written nonsense, as I've done many times in the past. Thanks for any criticism and insights.
Your argument is alright. There is nothing wrong with it. It's very common practice -when the axiom of choice is assumed- to say something along the lines of what you wrote. Having said that, here's a couple of ways to "formalize" your argument:
One thing you can do is use the Principle of Dependent Choices: What this says is that if we have a binary relation $E$ on a (nonempty) set $A$ and for every $a\in A$ there is a $b\in A$ such that $bEa$, then there is a sequence $a_0,\ldots,a_n,\ldots$ of elements of $A$ such that $a_{n+1}Ea_n$ for all $n\in\mathbb{N}$. Of course you can see how your argument can be formalized through this principle. Given a subset $Y\subset X$ with no least element of course for every $a\in Y$ there is a $b\in Y$ such that $b<a$. Then by the principle of dependent choice there exists a sequence that defines a set with order-type $\omega^*$.
But assume you just want to use the axiom of choice. We have that $\mathcal{P}(Y)\setminus\{\varnothing\}$ has a choice function $f$. Let $a_0=f(Y)$. Having defined $a_n$, let $Y_{n+1}=\{a\in Y : a<a_n\}$ (these are not empty since $Y$ doesn't have a least element). Then let $a_{n+1}=f(Y_{n+1})$. Every $a_n$ is well defined since $f$ is fixed. Thus the sequence is well defined, and thus the set with order type $\omega^*$ is well defined (these are all results of the recursion theorem).
As you see both "formalizations" are simple. This is why (as I said) your argument is perfectly valid and I am sure that you will encounter it in many books. I just wrote these in case you were curious as to how the axiom of choice leads to the part of your argument that you considered problematic.