In this paper (pp 2-3) Friedman proves a version of Higman's Lemma for infinite sequences of finite words on a finite alphabet. Such a sequence $S$ is called "bad" if no element of $S$ occurs as a subsequence in a later element of $S$. (E.g., a sequence that contains $\dots,oar,\dots,foobar,\dots$ is not bad, because $oar$ occurs as a subsequence in the later word $foobar$.)
The proof begins by supposing (for the sake of contradiction) that there exists at least one bad sequence, then it constructs a so-called "minimal bad sequence" $y_1,y_2,y_3,\dots$ as follows:
- Choose $y_1$ to be a shortest word that starts some bad sequence, then
- choose $y_2$ to be a shortest word such that $y_1,y_2$ starts some bad sequence, then
- choose $y_3$ to be a shortest word such that $y_1,y_2,y_3$ starts some bad sequence, then
- etc.
This would seem to be an evident use of the AoC, and the proof continues after merely remarking parenthetically that "The axiom of choice can be eliminated in an obvious way."
Question: In what "obvious way" can the AoC be eliminated from this proof? How can a (hypothetical) minimal bad sequence be constructed without the AoC?
You don't need AC to prove that the set of all finite words on a finite alphabet is a countable set. Fix an enumeration of the set of all finite words. Whenever you have to choose an element from a nonempty set of words, choose the one that comes first in the enumeration.