Choice Principles: What are they?

What does the phrase "\(\varphi\) is a choice principle" mean? This is something that I have spent quite a lot of my time thinking about. Directly and indirectly. What are choice principles as we know them? And who gets to decide?

For a set theorist, at least a "classical" set theorist (working within the confines of \(\ZF\) and its extensions to \(\ZFC\) and so on), a choice principle can aptly be defined as "Sentence \(\varphi\) in the language of set theory which is provable from \(\ZFC\) but independent from \(\ZF\)". Indeed that is how I think of choice principles, and how I referred to them in my masters thesis (albeit I prefaced that definition by pointing out its naivety).

But one day, in a discussion over an answer of mine on math.SE regarding choice principles, Carl Mummert points out that the statement \(\lnot\AC\rightarrow\Con(\ZFC)\) is not provable from \(\ZF\) while vacuously true in \(\ZFC\). Certainly this does not look like a choice principle.

So what is a choice principle? Well, it is an assertion which tells us that we can make choices under such and such conditions. These conditions can be that all the sets concerned are finite, or if the family from which we choose is countable, and so on. So is the ultrafilter lemma a choice principle? Well, not directly. But it does tells us that we can choose a certain object from the universe. And the ultrafilter lemma implying every set can be linearly ordered certain implies that we can choose from any family of finite [non-empty] sets! So it is a choice principle after all.

Returning to Carl's Sentence, it is not clear at all what sort of choice that assertion is going to give us. Certainly assuming it holds tells us that either \(\AC\) holds or that there is a model of \(\ZF\), but how will that tell us anything about what sort of choices do we make? Furthermore, which of these things are true? They appear so unrelated that even assuming the implication holds does not give us any information about the choices we can make. So what is a choice principle exactly?

In my confusion I posted this question on MathOverflow, in which I point out that many of the so-called naive choice principles will not really tell us anything directly related to choices, and sometimes we won't be able to generate any practical choices from those either. For example the equivalence between the axiom of choice for countable families of sets of real numbers the the assumption that \(\Bbb N\) is a Lindelöf space. It turns out that assuming the latter does tell us something about choice, but this turns out to be quite an indirect choice -- almost accidental.

My question received two [somewhat contradictory] answers. The first from Andrej Bauer which suggested the meta-mathematical meaning of the pharse. That is, a choice principle is a sentence of the form "If \(P(B)\) holds, and if every \(x\in A\) has some \(y\in B\) such that \(\phi(x,y)\) holds, then there is a function \(f\colon A\to B\) such that \(\phi(a,f(a))\) holds". Certainly this sounds as a reasonable suggestion, and in fact it does not require us to have any set theory in the background, just basic logic and type theory suffice. But it also tells us that the assumption "\(\Bbb N\) is a Lindelöf space" is not a choice principle, although it is equivalent to such. Which is strange to me, because we hardly ever think of concrete things, we almost always think about things up to some equivalence, and logical equivalence (over \(\ZF\), but probably much less) seems like an excellent candidate for this equivalence in this case.

The second answer is by Joel D. Hamkins, and he suggests that my naive formulation is precise. Carl's Sentence is indeed a choice principle. Despite not even hinting about the axiom of choice itself, it tells us that some relationship between a number-theoretical statement and the axiom of choice holds. So if we want to know whether the axiom of choice holds we only need to verify that \(\Con(\ZFC)\) fails. Of course that is quite the verification, but nonetheless this means that it is perfectly legitimate to consider Carl's Sentence as a conditional choice principle (as Joel calls it).

Up until recently I was perfectly happy with those answers, and I kept my naive view of what is a choice principle. I found it interesting that the answers focused on the lines between [meta-]semantical arguments (what does the statement mean), and provability arguments (provability and independence). Both of which are syntactical in their nature, but the latter is blind to equivalence which makes it more compatible with my philosophical view of the axiom of choice.

That was until about six weeks ago, when "Rethinking set theory" appeared and generated discussions about what is set theory, what are reasonable foundations and so on. It happened that just around that time I was working on a proof that \(\WISC\) is independent from \(\ZF\), a fact that was known relative to the consistency of very large cardinals, but my proof does not require large cardinals [the paper needs a minor revision before I can upload it here, but a preliminary version can be found on arXiv]. In my efforts of understanding \(\WISC\) to begin with, I delved into the world of constructive and algebraic set theory. Wading through many diagrams and principles, I finally managed (with the great help of David Roberts) to understand something about \(\WISC\) and its relatives. But more importantly I understood that there are more people than I was willing to believe who assume \(\axiom{CZF}\), or weaker theories, as their basic framework. Now this had to seep through the cracks in my mind for a while, until recently it hit me.

Not everyone work with \(\ZF\) as their basic theory. In fact there are more than a handful of those who don't and still deal with weak versions of the axiom of choice. If your theory cannot prove the equivalence between \(\Bbb N\) being Lindel&omul;f and countable choice for sets of real numbers, there is no reason to regard the former as a choice principle. So it finally hit me, that choice principles might not belong to set theorists (again, in the classical sense) as I often feel that they do. It is true that a lot of the research about weak versions of the axiom of choice, their equivalences and consequences, took place within classical set theory and within \(\ZF\) (and often within \(\ZF\) sans foundation), but that is no longer true today.

Reading Penelope Maddy's "Does \(V\) equal \(L\)?" (J. Symbolic Logic 58 (1993), no. 1, 15–41), it hit me that much like the concept of a function had changed over the course of the centuries and developed into a relatively uniform notion (amongst mathematicians anyway), it might be fruitful to develop a relatively uniform notion of a choice principle.

What do we want from such notion? Well, we definitely want it to be able and tell us something about a possible choice. So Carl's Sentence (in some sense) should not be a choice principle, but we also want it to hold against logical equivalence, because just because something is not phrased as "You may choose this and that" doesn't mean it doesn't tell us exactly that sort of statement.

I suppose that it really depends on the background theory, and when one becomes aware of the possible differences in the common theories, this becomes hard (if not impossible). At this point I don't have an answer to this question, what is a choice principle. I feel that this definition needs to be related to provability rather than the syntactical formulation of the sentence as asserting the existence of a function in certain situation. But at the same time, I feel that conditional choice principles should be - at least to some extent - separated. How can we do both things? And how will the first requirement withstand the ages, being highly dependent on your meta-theory, I have no idea.

But I do urge you to share your ideas, and your opinions, over in the comments or in other forums and blogs (but please let me know in these cases, I'd be interested to read the discussions and conclusions).