I have a question about the rigorous justification of how to construct an embedding of a countable Linear Order into Q.
In brief, where/how is the Axiom of Choice applied in this construction?
More specifically, the proofs I’ve seen follow a fairly intuitive induction strategy of choosing a starting output value, then partitioning Q into intervals that preserve the linear order of the previous inputs relative to the next input, and assigning the next output from the set that preserves the ordering of inputs and outputs. (see Theorem 3.7 on p.326 of this, or Theorem 5.6.2 of this)
The individual induction steps are all finite, so I understand that they don't need any special justification.
But in the final step, it's just asserted that the outcome of the induction strategy exists. I understand that since each induction step extends a finite partial function by one more value assignment, we can use the Union Axiom to collect them all together into a single infinite function. But since each induction step involved an arbitrary assignment, the union of infinite steps implies that we have made an infinite number of arbitrary choices. So we need the Axiom of Choice(AC).
(*)Here's my problem: Don't we also have to use AC earlier in order to specify the sequence of sets generated by our induction process?
More specifically, the version of AC I'm using asserts the existence of a choice function on a sequence of non-empty sets. This choice function is the desired embedding. So, the set of non-empty sets it applies to is the specific sequence of Q-intervals from which we make an arbitrary assignment in each induction step. But aren't the boundaries of these Q-intervals dependent upon the arbitrary assignments made at each previous induction step?
If so, I can't invoke AC to choose my infinite embedding until I specify the sequence of sets I'm choosing from...but the determination of which sets make up that sequence depends upon the arbitrary choices made at each induction step, i.e., I need to make an infinite number of arbitrary choices in order to specify which infinite sequence of sets I plan to make that infinite number of arbitrary choices from.
This seems circular. Am I missing something here perhaps about Recursion or Dependent Choice?(cf. discussion of versions of AC)
In principle, yes. You need to first fix a choice function in advance. The main problem, in fact, of many hidden uses of the axiom of choice is that we don't specify in the proof where we fix that choice function.
But, of course, foundation of mathematics shouldn't interfere with the mathematics itself. So it's not necessarily a bad thing.
However, in this case, all sets of interest are countable. We can fix an enumeration of those sets and use that to define a choice function. So there is no need to use the axiom of choice at all.