Suppose we have a single set whose members are not specified in advance. We know the set contains at least one member.
We have a single input we want to associate with one of the numbers in the set.
Suppose we want a map from b to a set X, and we know X contains at least one value. So we want the function with a single ordered pair (b,c) for some c in X.
Do we need the axiom of choice to form this function?
This topic is discussed at several threads.
The answer that emerges in these threads is that you do not need the axiom of choice or a new finite axiom of choice.
You can make a finite number of picks from sets that are finite or infinite without the axiom of choice.
Although not discussed specifically, making a finite number of choices, even with the number of choices indefinite, from indefinite sets, even infinite ones, is all allowed without the axiom of choice.
It is only when you make an infinite number of choices that you need the Axiom of Choice is the answer implied by these thread discussions.
For teaching grade K-6, we can see how this is a fundamental concept. We deal with rules that apply to situations not yet specified where the number of choices or the number of elements in a set or which set is not specified in advance.
This is what variables are all about. Variable are indefinite choices not yet made or not yet disclosed. But we can reason about what will happen when we make a definite choice for the variables we reason with.
This thread says we can iteratively choose in the finite case. So this argument would apply to when:
- We iteratively choose from the same set without replacement.
- We don’t specify how many choices are made in advance, as long as it is finite.
- We specify the number of choices to be made in advance is determined in terms of some other indefinite information not specified in advance, but which we know will be finite.
Do we need to have developed the machinery of Peano Arithmetic to do this?
Can we choose iteratively before we have developed initial segments of natural numbers?
Can we specify a do while construction for a set not specified in advance where we know in advance we will have a finite number of choices? Can we do this before we construct initial segments of natural numbers? What we call head segments at this blog? so 1 to n or 0 to n.
Paper by Blair and Tomber “Axiom of Choice for finite sets”.