FOM: Immaterial choice rule?

[Todd Wilson]

Some uses of the Axiom of Choice (AC) in set theory can be eliminated,
for example when the choice can be made in a uniform (definable) way.
Thus, if X = {X_i : i in I} is an infinite set of non-empty subsets of
the natural numbers, then we can define a choice function

    f : I -> Union_{i in I} X_i  (f(i) in X_i for all i in I)

by setting f(i) equal to the least element of X_i, using the fact that
the natural numbers are well-ordered.  On the other hand, in the
general case, when we don't have any specific information about the
elements of the X_i, the full power of AC is needed to get f.

I want to inquire about a possibly intermediate case.  Suppose that,
in order to construct a certain object A, we proceed by using AC to
get an f as above, then use f to construct A, and finally end by
showing that, for any other choice function f', the same A would
result.

A typical case is the following.  We have a set X, an equivalence
relation R on X, and an infinitary operation p : X^I -> X that
respects R in the sense that, for all I-tuples h,k : I -> X (i.e.,
elements of X^I), we have

    forall i in I  R(h(i),k(i))    implies    R(p(h), p(k)).

Then we can use AC to construct an operation p/R on the set X/R of
equivalence classes of R as follows.  Given an I-tuple of equivalence
classes h : I -> X/R, let f be a choice function for {h(i) : i in I}
and then define p(h) to be the equivalence class containing p(f).
That p respects R is exactly what is needed to show that this
definition succeeds, i.e., that any other choice function f' would
have resulted in the same equivalence class.

Questions:  What is the strength of the choice principle being used
here?  Is it equivalent to the full AC?  Is it strictly weaker than
AC?

To make this question more concrete, consider adding to ZF a new rule,
IC, along the following lines:  having proved that X = {X_i : i in I}
is a non-empty set of non-empty sets, one is allowed to introduce a
parameter f_X and an axiom stating that f_X is a choice function for
X.  All formulas in the proof are tagged with the parameters on which
they depend, and the rule of existential generalization is amended so
that one or more tags may be eliminated from the resulting existential
formula if it can be proven that the set claimed to exist does not
depend on the particular values of any of these parameters.  A formula
is a theorem of ZF+UC if it has a proof that doesn't depend on any
parameters.

Has anyone investigated this "immaterial choice" rule?

-- 
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh