| I agree that "some x such that .." will be problematic, because that sounds
| like a choice operator rather than definite description. I don't see how the
| axiom of choice is implied by the use of "the x such that ..." provided that
| the axiom which is associated with the construct is the usual one:
|
| (there exists a unique x such that P x) => P (the x such that Px)
|
| Can John (or anyone else) explain more fully how this can ever entail the
| axiom of choice and/or give an example of such a use?
I think you are right: the above axiom won't yield choice. However it might
prove too weak in a number of situations. In particular, if P does not
contain any variables other than x, then the addition of the stronger axiom
(there exists an x such that P x) => P (some x such that Px)
does not, I believe, extend the logic nonconservatively, in that any use of
the above axiom could be eliminated using exists-elimination in a rather
tedious but completely straightforward way. Thus the stronger axiom might be
the most natural way of embodying the fact that one can make finitely many
arbitrary choices without AC.
It is this stronger axiom which is liable to yield AC if additional
free variables are allowed, since then one is effectively sanctioning a
uniform choice scheme. Since this is the form of the actual HOL axiom
(SELECT_AX), I was thinking in terms of that.
There is an interesting discussion of this near the start of Potter's book
"Sets: An Introduction" (such discussions seem to be few and far between in
the logical literature).
John.