From a programmatic viewpoint that would be describing the axiom of countable choice, since such recursion can only occur countably infinite number of times. E

From a programmatic viewpoint that would be describing the axiom of countable choice, since such recursion can only occur countably infinite number of times. Even if we ignore that by allowing for syntax where we fanout uncountably many times with each recursion, the construction as shown requires the collection of sets to be orderable, to be able to do have a "first", unless we are implementing first in terms of choose itself. (Alternatively one could also argue in terms of Axiom of Choice implying the well-ordering theorem, allowing up to pick a minimum via some such ordering (although you may need to use the choice function to pick one such ordering), but this won't fully help here anyway). But even if you do that (implement iterator's first in terms of choose) it is not immediately obvious that you really have covered everything some full statements of the axiom of choice does. The axiom of choice is generally phased in terms of collections or families of sets, not sets of sets, but obviously the choose function takes in a set, not a more general family or collection. It is easy enough to dismiss away certainly non-set collections of sets, like multisets of sets, since "choose" being a function will return the same value every time from a repeated input, and in the above formulation we are returning a set of results, so such duplicates won't matter. We could even handwave away a version where we return a multiset without too much trouble. But the more expansive versions of the axiom of choice allow us to do something like "choose one element from each set in the class of non-empty sets." This is a real problem, as the "class of non-empty sets" is pretty well known to not be a set, and thus trying to implement iterator first in terms of it would not even be possible for that scenario.