finitary axiom of choice

In mathematics, being able to select an element from a single non-empty set S is not judged to be problematic, because the condition that S is non-empty is supposed to supply automatically an element x∈S.

Is there something fishy going on here?

What is the negation of the statement "S is empty"? Is it "S contains at least one element" or "There exists an x∈S"? The latter seems to be providing you information beyond the fact that S is non-empty, but this impression is wrong. The second sentence does not really present an element from S, it presents a label for an arbitrary element of A. In formal logic, one can not construct sentences such as "S contains at least one element". An assertion of existence needs to contain a label for referring to the existent:

You manipulate the label as if you are manipulating an arbitrary element of S. The word "arbitrary" here is very important. Since you do not know which element you are manipulating, you can not use the specific properties of individual elements. But you can still utilize their shared properties! And this is what you often desire anyway. You want to operate at a symbolic level. The ambiguity works in your favour because you are interested only in the shared properties.

Note that x itself is not literally in S. It is a new symbol satisfying all the properties associated with belonging to S. Hence, in some sense, we are voluntarily setting up a curtain of epistemological ignorance here. This is the essence of any abstraction process. Many stumbling blocks in the history of mathematics was of this nature. People could not get their heads around a certain new construction because they insisted on knowing "what" they were manipulating. For instance, zero seemed to be some sort of a mystical embodiment of nothingness, while in reality it was just a symbol satisfying certain algebraic properties.

Anyway let us go back to our discussion. So, in the finite case, Axiom of Choice is indistinguishable from the statement that there exists an x∈S. In order to see this in detail, let us recall the exact statement of the axiom:

A choice function is a function f, defined on a collection X of nonempty sets, such that for every set S in X, f(S) is an element of S. With this concept, the axiom can be stated: For any set X of nonempty sets, there exists a choice function f defined on X. (Source)

Say X consists of a single non-empty set S. Then Axiom of Choice guarantees that the set of choice functions defined on X is non-empty. This allows you to pick an arbitrary choice function f. You know that f(S) is an element of S, but you can not tell which element because you can not tell which choice function f is. In order words, you are provided with an arbitrary element of S.

Note that the distinction between an actual element and an arbitrary one becomes more blurred as the set itself becomes more arbitrary. If S is equal to {1,2,3}, then the distinction is clear. What if S is an arbitrary set with three elements? Then there is almost no difference between an actual element and an arbitrary one. Hence, in that case, the label presented by the formal statement of the fact that S is non-empty can be literally treated as an element of S.

Hence, in the finite case, axiom of choice is a by-product of the notion of a "finite" arbitrary set and "finitistic" logic. Therefore we do not need it as an additional axiom in finitistic set theory. In the infinite case, it needs to be taken as an additional axiom since we continue to work in finitistic logic. If we could form infinitely long logical statements, then again axiom of choice would be a mere by-product.

This observation really clarifies the matter. Axiom of Choice comes implicitly embedded inside the notion of an arbitrary set. The basic, fundamental problem is arbitrariness... In the case of finitary Axiom of Choice, we do not recognize its presence because the logic itself takes care of it. Of course, all that the logic does is to sweep the problem under the rug.

Abel and Galois unraveled the ambiguity inherent into every algebraic equation of degree greater than one - the ambiguity in choosing one out of several solutions (roots) of such equation. Thus, they founded a mathematical framework for the study of symmetry, arbitrariness and ambiguity which has eventually grown into the modern group theory. It may seem to a non-mathematician that only Buridan's ass would have any difficulty in choosing one of the two * from **. But try to program a robot doing this, where the two * are not conveniently positioned on a line, you can not just command: "take the left one".
Gromov - Structures, Learning and Ergo Systems (Page 56)

Choosing an actual element from a non-empty structureless set is not as simple as it sounds.You need a human being to ignite the mathematical engine! In fact, constructivists claim that even a human being is incapable of this feat unless he is provided with an actual instruction for locating an element.

Don't let the simplicity of the content of this discussion fool you. These are issues of deep philosophical importance. The difficulty of making a choice in a structureless set is precisely the first problem that a believer in an observer-independent theory of reality needs to overcome.