When using an axiom scheme, are we implicitly using a choice principle?

Question

I heard an interesting argument from a colleague recently that went something like this. Whenever we are using an axiom scheme, we are essentially choosing one of the instances of this scheme, and hence, whether or not we include the axiom of choice in our axioms, we are implicitly using some kind of choice principle to choose that instance. My gut feeling is that this argument seems fishy, but also interesting, and I lack the expertise to give a good answer.

My question is whether this argument holds or not, and whether it makes a difference if the axiom scheme is uncountable. I realise that the question is somewhat vague, but I hope there can be some interesting answers anyway.

Answer 1

The main problem here is that the name "Axiom of Choice" leads people to think that the axiom says something about our ability to choose things. Then, whenever we choose something, like one instance of an axiom schema, they think the axiom of choice is involved.

The axiom of choice is not about our abilities at all. It is about the existence of certain sets. Specifically, given any family $F$ of pairwise disjoint nonempty sets, the axiom of choice asserts the existence of a set $C$ that has exactly one member in common with each of the sets in the family $F$.

If we were to try to build such a $C$, then we would need to choose an element from each of the sets in $F$. But there is no need for us to build $C$, nor does the axiom claim that we could build $C$. The axiom just says that such a $C$ exists. It is entirely about the universe of sets, not about our abilities or activities.

Answer 2

The Axiom of Choice is not being invoked when choosing an instance of an axiom scheme. You are selecting one element from an infinite set. The Axiom of Choice concerns choosing an infinite set. If $\{A_\alpha\}$ is an infinite collection of distinct sets, the Axiom of Choice allows us to an element of each set.

Answer 3

No, choice is irrelevant here.

First of all, as long as your language is countable, there are only countably many formulas, so in particular the set of formulas is well-ordered and no choice is needed to select one.

More importantly, though, proofs are finite: even if we allow uncountable language, we only ever need to make finitely many choices, and this doesn't use AC, regardless of how complicated the language is.

Answer 4

No, this reflects a total misunderstanding of what the axiom of choice is. The axiom of choice is no more needed to invoke an instance of an axiom scheme than it is needed to say that $43$ is a natural number (after all, that is also "choosing" an element of an infinite set). In almost all situations where you use an instance of an axiom scheme, you specify which instance you are using. In principle, the axiom of choice could be used in some complicated argument where you are non-constructively asserting the existence of an infinite collection of different proofs in an uncountable language, and in each one of them you have to choose an unspecified instance of an axiom scheme. In practice, I have never seen such an argument and such a thing is very far removed from what is normally meant by "using an axiom scheme".

Answer 5

Your colleague is not using the term "choice principle" with the technical sense it has is set theory; probably he is not aware that those words have a specialized technical meaning, but has heard (or read) arguments that use it and tried to reconstruct their meaning from the everyday English meaning of "choice". That doesn't go well.

In set theory "choice principle" is a slightly fuzzy, but nevertheless essentially technical term for a statement that

1. Has a premise for the form "for every $y$ with such-and-such property there is at least one $x$ that is related to $y$ in such-and-such way"; and

2. Concludes that there exists an object within the set-theoretic universe that simultaneously encodes a choice of a particular $x$ for each of many (but not necessarily all, depending on which choice principle we're speaking about) of those $y$s.

In other words, to make use of a choice principle we must already know that it is possible to make individual choices for each $y$. The principles just says that we can wrap up many of those choices as a single object. Being able to do so is technically necessary in order to formalize some natural-feeling arguments into axiomatic set theory, due to how formal logic is usually set up. But it has no deep and philosophical consequences outside those technical uses.

What your colleague speaks about seems to be merely that the human who writes down a proof chooses how his proof is going to go. And that can be a perfectly good "choice" in the sense of everyday English -- it just doesn't have anything to do with the technical propositions that set theorists call choice principles.

Answer 6

In an Axiom Schema like PA (Peano Arithmetic) or ZF or ZFC (set theory) the collection of axioms is computably recursive. That is, we can write a (fairly simple) computer program that will take any finite string of symbols as input and correctly state after finitely many steps, whether or not the string represents an axiom. At no time do we say "There exists an axiom that says... " without actually exhibiting the axiom itself. This is different from the Axiom of Choice :"Every set can be well-ordered" is the axiom, but it does not state how to exhibit a specific well-order on any given set. If your axiom schema is not computably recursive you will have sentences which cannot be determined to be axioms or not axioms. (At least not from within your schema.) As has already been said, how some human brain opts to employ a given axiom is a question about how humans manage to think, not a question about axiomatics .