A NOTE ON CHOICE PRINCIPLES IN SECOND-ORDER LOGIC

Abstract

Zermelo’s Theorem that the axiom of choice is equivalent to the principle that every set can be well-ordered goes through in third-order logic, but in second-order logic we run into expressivity issues. In this note, we show that in a natural extension of second-order logic weaker than third-order logic, choice still implies the well-ordering principle. Moreover, this extended second-order logic with choice is conservative over ordinary second-order logic with the well-ordering principle. We also discuss a variant choice principle, due to Hilbert and Ackermann, which neither implies nor is implied by the well-ordering principle.

1 Choice functions and well-orders

One of the most acclaimed classical theorems of set theory is Ernst Zermelo’s proof of the equivalence between the axiom of choice and the statement that every set can be well-ordered (see Zermelo, 1904, 1908; Kanamori, 1997, 2004; or Moore, 1982). Since Zermelo, implications and equivalences among various choice principles in set theory have been extensively mapped out (see Rubin & Rubin, 1985). Given second-order logic’s expressive resources, it is natural to ask whether second-order logic is strong enough to capture these results. If we try to capture Zermelo’s theorem, we run into expressivity issues. While the property of well-ordering can be straightforwardly expressed in second-order logic, the existence of a covering function, as postulated in the axiom of choice, cannot be expressed in pure second-order logic.

A proof of Zermelo’s equivalence theorem can be given in a third-order logic where we have the ability to quantify over what are sometimes called type $(2,1)$ -functions—functions that take elements of the power set of the domain into the domain itself. ¹ In third-order logic it is thus not difficult to prove the following:

“For every set X there is a covering function for X iff every set can be well-ordered”

If one does not have the resources of third-order logic, the situation is more complicated. The extension of second-order logic we will consider in this note stems from Shapiro’s interest in the axiom of choice in second-order logic (see Shapiro, 1991) and exploits the previous work on abstractionist neologicism by the remaining two authors. In Mancosu & Siskind (2019), one works in second-order logic extended with a (2,1)-function constant $\partial $ . The function symbol in question is defined implicitly through an abstraction principle.

Recall that in the context of (this variety of) neologicism, an abstraction principle introduces a function that assigns objects to concepts (monadic predicates) according to an equivalence relation defined on the concepts. Frege’s Basic Law V, for instance, defines an abstraction function, $\epsilon $ , according to the equivalence relation of equi-extensionality among monadic predicates:

$$\begin{align*}\mathtt{BLV}\quad\quad \epsilon(X)=\epsilon(Y) \leftrightarrow \forall x (Xx\leftrightarrow Yx)\end{align*}$$

As is well known, Russell showed the inconsistency of $\mathtt {BLV}$ (if enough comprehension on second-order formulas is available). In Mancosu & Siskind (2019), the focus was on studying abstraction principles that define a function satisfying a condition called “part-whole”. A function (or operator) $\partial $ defined by an abstraction principle satisfies part-whole iff for any $X\subsetneq Y$ , $\partial (X)\neq \partial (Y)$ . The main result is that any abstraction principle that defines a function satisfying “part-whole” is refutable in second-order logic (plus the symbol for the function). In this note, we will exploit the technique developed there for proving a result on choice functions.

Notice that, like abstraction operators, choice functions also send monadic predicates to objects. For instance Zermelo’s covering function in his celebrated proof (Zermelo, 1904) starts with a set M (whose well-ordering is sought) and assigns to every nonempty set $Z \subseteq M$ a distinguished element $z\in Z$ . In other words for each nonempty set M, and letting $P(M)^*$ stand for all the nonempty subsets of M, one postulates the existence of a $\gamma : P(M)^* \to M$ such that for any $Z\in P(M)^*$ , we have $\gamma (Z)\in Z$ .

Let $\mathtt {WOP}$ be the typical statement, in second-order logic, that every concept (or the domain itself) admits a well-ordering (see Shapiro, 1991, §5.1.3). We will show

1. 1. That by suitably introducing a symbol for a $(2,1)$ -choice function with an axiom, $\mathtt {CHOICE}$ , we have: $\mathtt {SOL}+\mathtt {CHOICE}\vdash \mathtt {WOP}$ .

2. 2. That this is the best that can be done, in the sense that $\mathtt {SOL}+\mathtt {CHOICE}$ is conservative over $\mathtt {SOL}+\mathtt {WOP}$ .

The combined effect of these two results is that we go beyond second-order logic in a limited way—the same way in which abstractionist neo-logicist theories such as $\mathtt {SOL}+\mathtt {HP}$ (second-order logic plus Hume’s Principle) ² go beyond second-order logic, and we obtain an implication from $\mathtt {CHOICE}$ to $\mathtt {WOP}$ which is unavailable in pure second-order logic. One way to put the result is: a single choice function on (the powerset of) the universe gives us a well-ordering for all the possible concepts. Thus, our result is comparable to the statement of global choice.

As noted above, the full Zermelian equivalence cannot be regained unless we go to third-order logic, but we have the best next thing: $\mathtt {CHOICE}$ does not allow us to prove anything in the old language that $\mathtt {WOP}$ could not already prove. This result will be better appreciated considering the strength of $\mathtt {WOP}$ in comparison to other choice principles. In the next section, we discuss what is known about implications and equivalences between some choice principles which are expressible in second-order logic. Section 3 discusses the role extensionality (i.e., the assumption that our second-order objects are extensional) plays in our results. In §4, we prove the results on the relationship between $\mathtt {CHOICE}$ and $\mathtt {WOP}$ mentioned above. In §§5 and 6, we establish the mutual independence of $\mathtt {WOP}$ and another choice principle $\mathtt {HAC}$ , defined below. We end the paper with some reflections on these independence results.

2 Choice principles in second-order logic

Choice principles in second-order logic have been studied by, among others, Asser (1981), Shapiro (1991), and Gassner (1994). ³ In pure second-order logic one can formulate a variety of choice principles that, in the classical set-theoretic setting, are equivalent to the axiom of choice (i.e., the existence of covering functions for every set). In second-order logic, these principles turn out to be, with an important exception to be mentioned below, all weaker than the statement formalizing the well-ordering principle ( $\mathtt {WOP}$ ). That is, the well-ordering principle implies the relevant statement over pure second-order logic but the reverse does not hold. Examples of such principles are the formalized versions of the axiom of choice for relations (requiring quantification over type (1,1)-functions, which is expressible in pure second-order logic), cardinal comparability, and Zorn’s lemma. ⁴ We discuss in detail only the first one, which is designated as $\mathtt {AC}$ . The techniques for showing that these principles do not entail $\mathtt {WOP}$ use permutation models (see Gassner, 1985, 1994). In a sense, and with an important exception to be mentioned below, $\mathtt {WOP}$ is the strongest choice principle available in pure second-order logic. This in itself explains the interest of our first result described above. The other result proved in this note explains the exception we have alluded to. There is a choice principle which is due to Hilbert and Ackermann that can be presented as a schema in second-order logic. ⁵ The schema appears for the first time in a 1935 article by Ackermann (1935) and became widely known through its inclusion in the second edition of the famous textbook by Hilbert and Ackermann Grundzüge der mathematischen Logik (1938). The schema, which we will call $\mathtt {HAC}$ , was presented in Shapiro (1991, p. 77) for monadic predicates as follows:

$$\begin{align*}\mathtt{HAC}\quad\quad\forall x \exists X \varphi(x,X)\to \exists R^2\forall x \big(\forall Z (Zz\leftrightarrow R^2xz)\to \varphi(x,Z)\big),\end{align*}$$

where⁶ $\varphi $ is a formula in second-order logic.

If R is a binary relation and x a variable, let $R_x$ be the concept (or property, or set) $\lambda yRxy$ . Then, under extensionality, ⁷ the following is a definitional abbreviation of $\mathtt {HAC}$ (Shapiro, 1991, pp. 130–131):

$$\begin{align*}\forall x\exists X\varphi(x,X)\to \exists R\forall x\varphi(x,R_x).\end{align*}$$

A generalization of $\mathtt {HAC}$ to n-ary predicates is simple and is sometimes presented, as in Asser (1981, p. 120) with $\lambda $ -terms (which can however be eliminated):

$$ \begin{align*} &\forall x_1,\ldots, x_m \exists X^n \varphi (x_1,\ldots, x_m, X^n)\to \\&\exists R^{m+n}\forall x_1,\ldots, x_m \varphi(x_1,\ldots, x_m, \lambda_{m+1}x_{m+1}\ldots\lambda_{m+n}x_{m+n}R^{m+n}(x_1,\ldots,x_{m+n}), \end{align*} $$

where $\varphi $ is a formula in second-order logic.

When we look at the secondary literature we find a number of conflicting claims concerning the status of this schema. Consider the following remark appearing in Shapiro (1991):

I have been informed that Günter Asser and Christine Gassner have established the independence of $\mathtt {WOP}$ from $\mathtt {AC}$ without the assumption of the consistency of real-determinacy. In Chapter 3, it was mentioned that Hilbert and Ackermann (1928) ⁸ include a stronger version of the axiom of choice in their presentation of second-order logic [i.e., $\mathtt {HAC}$ ] …Asser and Gassner have established the independence of $\mathtt {WOP}$ from this as well. (Shapiro, 1991, note 15, pp. 130–131)

The proof of independence of $\mathtt {WOP}$ from $\mathtt {AC}$ refers to a result showing that, over pure second-order logic, $\mathtt {WOP}$ proves $\mathtt {AC}$ (see Asser, 1981) but $\mathtt {WOP}$ cannot be proved from $\mathtt {AC}$ (see Gassner, 1985, 1994). As noted, the independence of the former from the latter is proved with permutation models.

The basic choice principle $\mathtt {AC}$ is formalized by Shapiro (1991, p. 67) as

$$ \begin{align*}\mathtt{AC}\quad\quad &\forall X^{n+1} (\forall x_1,\ldots, x_n\exists y\,X^{n+1}(x_1,\ldots,x_n, y) \\&\to \exists f^n\forall x_1,\ldots,x_n\,X^{n+1}(x_1,\ldots, x_n , f^n(x_1,\ldots,x_n)).\end{align*} $$

The formalization given by Asser (1981) is equivalent but uses a functional relation instead of a function. It is called $(m, n)$ - $\mathtt {AC}$ : ⁹

$$ \begin{align*}&\forall X\exists Y\forall x_1,\ldots, x_m (\exists y_1,\ldots, y_n\,X (x_1,\ldots, x_m , y_1,\ldots, y_n)) \\&\to \exists ! y_1,\ldots,y_n \,X(x_1,\ldots, x_m , y_1,\ldots,y_n) \wedge Y(x_1,\ldots, x_m , y_1,\ldots, y_n)).\end{align*} $$

Note that both X and Y have $m+n$ arguments. Thus, Shapiro’s formalization of $\mathtt {AC}$ is $(n, 1)$ - $\mathtt {AC}$ in Asser’s presentation. ¹⁰

As is clear from the above quote, Shapiro was under the impression that Asser and Gassner also proved $\mathtt {HAC}$ does not imply $\mathtt {WOP}$ . However, a search in the publications of Asser and Gassner did not bring up any proof of the alleged result. Gassner (1985, 1994) does not consider $\mathtt {HAC}$ . As for Asser (1981), he states that the relation between $\mathtt {HAC}$ and $\mathtt {WOP}$ seems to be unknown:

Whether in an Henkin structure in which $WO^{(2)}_1$ [ $\mathtt {WOP}$ ] is true, all the sentences from $choice^{(2)}$ [ $\mathtt {HAC}$ ] are valid does not seem to be known. The author also ignores whether, for instance, from ${}^h ax^{(2)}\cup choice^{(2)}$ [ $\mathtt {SOL}+\mathtt {HAC}$ ] the sentence $WO^{(2)}_1$ [ $\mathtt {WOP}$ ] is derivable; the known set-theoretic proofs of the well-ordering principle from the axiom of choice are in any case not yet representable on the basis of $choice^{(2)}$ . (Asser, 1981, p. 125)

In §5 and §6, we clarify the situation and show that neither $\mathtt {WOP}$ nor $\mathtt {HAC}$ implies the other.

We work in the language of second-order logic expanded by a (2,1)-type function symbol $\partial $ . A term in this language is either an object variable x or $\partial (X)$ for a unary predicate variable X. The formulas of the language are generated from the terms in the usual way.

For $\varphi $ a formula with free variables including the n-tuple $\bar {v}$ , we put

$$\begin{align*}\mathtt{CA}(\varphi, \bar{v}) =_{def}\text{(the universal closure of) } \exists R\,\forall \bar{v}\, \big(R(\bar{v})\leftrightarrow \varphi(\bar{v})\big),\end{align*}$$

where R is an n-ary predicate variable.

We let $\mathtt {SOL}(\partial )$ denote the system of full second-order logic in this language with extensionality, that is, we have all the usual natural deduction rules, extensionality, and the comprehension schema $\mathtt {CA}(\varphi , \bar {v})$ for every formula $\varphi $ . We can also look at subsystems where we restrict comprehension to natural syntactic classes, for example, $\Pi ^1_1$ or $\Delta ^1_1$ . See Mancosu & Siskind (2019) for a detailed discussion of these subsystems.

In this context, we introduce the following axiom which expresses that $\partial $ is a choice function on nonempty sets.

$$\begin{align*}\mathtt{CHOICE} \quad\quad \forall X\,(\exists x\, Xx\to X\partial x).\end{align*}$$

We also need the following notation. For X a unary relation, we let $X^c$ be the complement of X. For R a binary relation, $\mathsf {Field}(R)$ denotes the field of R, that is, $\{x\, |\, \exists y(R(x,y)\vee R(y,x))\}$ and $\mathsf {WO}(R)$ is the formula expressing that R is a nonstrict well-order of its field, that is, that R is transitive, reflexive on its field, and for every nonempty subset X of $\mathsf {Field}(R)$ , there is an $x\in X$ such that $\forall y (y\neq x\to \neg R(y,x))$ . This is straightforwardly formalizable as a second-order formula in the binary second-order term R (see Mancosu & Siskind, 2019 for details).

3 Extensionality

Before presenting our main results, we have a brief discussion on how our results depend on extensionality. For this section, let us call the items in the range of the monadic second-order variables “properties”, being neutral for now on whether they are construed extensionally or intensionally.

The system in Shapiro (1991) has no identity relation on properties in the object language, so the matter of extensionality can not even be stated in that language. There are three model-theoretic semantics. In standard and Henkin semantics, the properties are indeed extensional, since they are interpreted as sets. The third kind of semantics construed the language as a two-sorted first-order language, and, in that context, there are both extensional and intensional interpretations.

Notice that the principles $\mathtt {AC}$ and $\mathtt {WOP}$ both make sense in the neutral framework. All that is needed for these is an identity relation on the first-order variables (so one can speak of a function in the case of $\mathtt {AC}$ and a well-ordering in $\mathtt {WOP}$ ). The original formulation of $\mathtt {HAC}$ also makes sense, as that schema does not presuppose an identity relation on the properties.

Recall, however, the “definitional abbreviation” of $\mathtt {HAC}$ (Shapiro, 1991, pp. 130–131):

$$\begin{align*}\forall x\exists X\varphi(x,X)\to \exists R\forall x\varphi(x,R_x).\end{align*}$$

If we do not construe the properties extensionally, this is not quite right. Recall that $R_x$ is the property $\lambda yRxy$ . If we want to remain neutral on extensionality, the consequent of this version of $\mathtt {HAC}$ should be that there is a relation R such that for every x, $R_x$ is coextensive with an X such that $\varphi (x, X)$ . And that would not have been much of an abbreviation.

Introduce an identity relation on the properties. Let $X\equiv Y$ be an abbreviation for the statement that X and Y are coextensive. Then, of course, extensionality would be $\forall X\forall Y (X\equiv Y\to X=Y)$ (and similarly for n-ary relations). ¹¹

In Mancosu & Siskind (2019) and in what follows, we need to either assume that properties are extensional or assume that coextensive properties always get the same $\partial $ . In particular, in the main lemmas below, we need that there is a unique well-ordering with various features. One of those features is that for each x, if we apply $\partial $ to the property of not being less-than x, the result is x. For example, suppose that there are two distinct universal properties with different $\partial $ -values, but that everything else is extensional. Then there will be two well-orderings that satisfy the features in question.

Worse, it is too easy to satisfy CHOICE, and there will be models of this principle in which the universe is not well-ordered (so that our main theorem fails). Start with a model of set theory, M, in which, say, the real numbers have no well-ordering. Look at the model $(\mathbb {R}, P(\mathbb {R}),...)^M$ . Since there is no identity relation on the property variables, we can add as many coextensive copies of each property as we want. So, for each nonempty property S of natural numbers, we replace S with “continuum-many” properties $S^x$ , one for each real number $x\in S$ . It will still be the case that this model has no well-ordering of its objects, that is, satisfies $\neg \mathtt {WOP}$ . But now we can interpret $\partial $ by letting $\partial (S^x)=x$ . Clearly this satisfies CHOICE.

In short, if we don’t assume extensionality (or at least that $\partial $ acts the same on coextensive properties), then CHOICE does not give us a genuine choice function.

4 The main results

We need the following variation of the main lemma from Mancosu & Siskind (2019). The only difference in the statement is that we’ve replaced taking $\partial \mathsf {Field}(R_x)$ with $\partial [\mathsf {Field}(R_x)^c]$ . ¹² The proof is simple modification of the proof given in that paper, making this replacement in appropriate places.

Lemma 4.1. The following is provable in $\mathtt {SOL}(\partial )$ . There is a unique binary predicate R such that

1. (i) $\mathsf {WO}(R)$ ;

2. (ii) for all $x\in \mathsf {Field}(R)$ , $\partial [\mathsf {Field} (R_x)^c]= x$ ; and

3. (iii) $\partial [\mathsf {Field}(R)^c]\in \mathsf {Field}(R).$

Lemma 4.2. $\mathtt {SOL}(\partial )+\mathtt {CHOICE}\vdash \mathtt {WOP}$

Proof. Let R as in 4.1 We claim that $\mathsf {Field}(R)$ is just the universal predicate. If not, $\mathsf {Field}(R)^c$ is nonempty and so $\partial [\mathsf {Field}(R)^c]\in \mathsf {Field}(R)^c$ , by $\mathtt {CHOICE}$ . But property $(iii)$ tells us that $\partial [\mathsf {Field}(R)^c]\not \in \mathsf {Field}(R)^c$ , a contradiction.□

The preceeding argument is really the same as the Zermelo–Kanamori argument for obtaining a well-order of X from the set-theoretic version of Lemma 4.1 for X with $f:P(X)\to X$ .

We can now establish the main result.

Theorem 4.3. $\mathtt {SOL}(\partial )+\mathtt {CHOICE}$ is a conservative extension of $\mathtt {SOL}+\mathtt {WOP}$ .

Proof. By Lemma 4.2, we just need to see that $\mathtt {SOL}(\partial )+\mathtt {CHOICE}$ is conservative over $\mathtt {SOL}+\mathtt {WOP}$ . Let $\mathcal {M}=\langle M, S_1, S_2,\ldots \rangle $ be a Henkin model of $\mathtt {SOL}+\mathtt {WOP}$ . We show that there is an extension of $\mathcal {M}'$ of $\mathcal {M}$ such that $\mathcal {M}'\models \mathtt {SOL}(\partial )+\mathtt {CHOICE}$ . Fix $a\in M$ . Fix $R\in S_2$ such that $\mathcal {M}\models \mathsf {WO}(R)$ . Define $f:S_1\to M$ by

$$ \begin{align*} f(X)= \begin{cases} a & \text{if } X=\emptyset\\ x & \text{if } X\neq \emptyset \text{ and } x \text{ is the } R\text{-least element of } X. \end{cases} \end{align*} $$

Let $\mathcal {M}'=\langle M,S_1,S_2,\ldots , f\rangle $ . By choice of f, we have that $\mathcal {M}'\models \mathtt {CHOICE}$ . Moreover, since f is definable over $\mathcal {M}$ with parameters R and a, any subset of $M^n$ definable using f as a parameter is definable using R and a as parameters, instead. So $\mathcal {M}'\models \mathtt {SOL}(\partial )$ .□

A natural variation of this result is to start not with a choice function picking elements of nonempty sets, but elements of the complements of sets with nonempty complements. For this, we use the original version of Lemma 4.1 from Mancosu & Siskind (2019).

Lemma 4.4. The following is provable in $\mathtt {SOL}(\partial )$ . There is a unique binary predicate R such that

1. (i) $\mathsf {WO}(R)$ ;

2. (ii) for all $x\in \mathsf {Field}(R)$ , $\partial \mathsf {Field} (R_x)= x$ ; and

3. (iii) $\partial \mathsf {Field}(R)\in \mathsf {Field}(R).$

Now let

$$\begin{align*}\mathtt{CHOICE'} \quad\quad \forall X\,(\exists x \,\neg Xx\to \neg X\partial X).\end{align*}$$

By a simple modification of the above proofs we get

Theorem 4.5. $\mathtt {SOL}(\partial )+\mathtt {CHOICE'}$ is a conservative extension of $\mathtt {SOL}+\mathtt {WOP}$ .

Consider the predicate $\mathsf {Big}$ , which asserts that some set X is in one-to-one correspondence with the domain of all objects. Notice that in second-order logic, if there is an X such that $\mathsf {Big}(X)$ and X can be well-ordered, then $\mathtt {WOP}$ . So if for R as in Lemma 4.1 or 4.4, we have $\mathsf {Big}(\mathsf {Field}(R))$ , then $\mathtt {WOP}$ . Of course, $\mathtt {CHOICE}$ and $\mathtt {CHOICE'}$ both imply that $\mathsf {Big}(\mathsf {Field}(R))$ for the appropriate R.

There is another familiar instance of this phenomenon. Consider the abstraction principle $\mathtt {NewV}$ (discussed extensively in Shapiro & Weir, 1999):

$$\begin{align*}\mathtt{NewV}\quad\epsilon X=\epsilon Y\kern1.5pt{\leftrightarrow}\kern1.5pt \big( \big(\mathsf{Big}(X)\wedge \mathsf{Big}(Y)\big) \vee \big(\neg \mathsf{Big}(X)\wedge \neg \mathsf{Big}(Y)\wedge\forall x(Xx\leftrightarrow Yx)\big)\big).\end{align*}$$

Suppose¹³ $\mathtt {NewV}$ . Now let R be as in Lemma 4.4 We must have $\mathsf {Big}(\mathsf {Field}(R))$ , since for $x=\epsilon \mathsf {Field}(R)$ , $x\not \in \mathsf {Field}(R_x)$ and $\epsilon \mathsf {Field}(R)=\epsilon \mathsf {Field}(R_x)$ implies $\mathsf {Big}(\mathsf {Field}(R))$ (and $\mathsf {Big}(\mathsf {Field}(R_x))$ ). So this gives a proof of $\mathtt {SOL}(\partial )+\mathtt {NewV}\vdash \mathtt {WOP}$ , a result of Shapiro & Weir (1999). ¹⁴

5 $\mathtt {WOP}$ does not imply $\mathtt {HAC}$

In this section we show that $\mathtt {WOP}$ does not imply $\mathtt {HAC}$ by producing a Henkin model of $\mathtt {SOL}+\mathtt {WOP}+\neg \mathtt {HAC}$ . Our model will be $(\omega ,P(\omega )^N)$ , where N is a transitive model of set theory. We’ll obtain N via the following folklore result, which uses a construction due to Feferman and Lévy (see Jech, 2003, p. 259, Example 15.57).

Proposition 5.6. There is a relation $R(n,x)$ which is $\Sigma ^1_3$ , provably over $\mathtt {ZF}$ , such¹⁵ that

$$\begin{align*}\mathtt{ZF}\not\vdash \forall n\exists x \,R(n,x)\to \exists y \forall n R(n,(y)_n).\end{align*}$$

Proof. We first define R, then check that it is $\Sigma ^1_3$ .

$$ \begin{align*} R(n,x)\leftrightarrow x \text{ is a real coding a well-order of length } \aleph_n^L. \end{align*} $$

The right-hand side is equivalent to

$$ \begin{align*}\exists y\, \big( &y \text{ is a real coding a well-founded model of } V=L + "\text{there are exactly } n\\ &\text{infinite cardinals"} \wedge x=Ord^y \wedge \forall z\, \big(z\text{ is a real coding a well-founded model of } \\ & V=L + "\text{there are exactly } n \text{ infinite cardinals"} \to \exists f: z\trianglelefteq y\big)\big). \end{align*} $$

This is easily seen to be provably $\Sigma ^1_3$ over $\mathtt {ZF}$ . Of course, if $V=L$ , then $\forall n \exists x R(n,x)$ fails, since $\aleph _1=\aleph ^L_1$ , and only countable well-orders can be coded by reals.

Now let N be the usual symmetric extension of L where $\aleph ^N_1=\aleph ^L_\omega $ (see Jech, 2003). Work in N. Since for all n, $\aleph _n^L<\aleph _1$ , we have that there is a real coding $\aleph _n^L$ , that is, $\forall n\exists x R(n,x)$ . On the other hand, if there were a real y such that $\forall n R(n,(y)_n)$ , then the lexicographic ordering on y is a well-ordering of length $\aleph _\omega ^L=\aleph _1$ , which is a contradiction (since it is a countable well-order).

So we’ve shown $N\not \models \forall n\exists x \,R(n,x)\to \exists y \forall n R(n,(y)_n)$ .□

By replacing L with a sufficiently large countable $L_\alpha $ in the above proof, we get a countable transitive N such that

It follows that $(\omega ,P(\omega )^N)\models \mathtt {WOP}+\neg \mathtt {HAC}$ . ¹⁶

6 HAC does not imply WOP

Assuming the consistency of some large cardinal axioms, $\mathtt {HAC} \not \vdash \mathtt {WOP}$ . This is accomplished as follows. Steel & Van Wesep (1982) showed that under a strong determinacy hypothesis, (among other things). This strong determinacy hypothesis was proved consistent from a moderate large cardinal hypothesis by Sargsyan (2014) so that, assuming the consistency of the large cardinals used, we get that .

The large cardinals involved in Sargsyan’s result are measurable cardinals and Woodin cardinals; we refer the reader to Jech (2003), §10 and §20 for the definitions. We turn to the strong determinacy hypothesis. ${\bf AD}$ is that statement that all two player games of perfect information of length $\omega $ where the players alternate playing integers are determined, that is, one player has a winning strategy. $\mathsf {AD}$ implies that there is no well-order of the reals, so the Axiom of Choice fails in this setting. $\mathsf {AD}_{\mathbb {R}}$ is the strengthening of $\mathsf {AD}$ which states that all two player games of perfect information of length $\omega $ where the players alternate playing real numbers are determined. $\mathsf {DC}_{\mathbb {R}}$ is the statement of dependent choice, restricted to the real numbers.

Under just $\mathsf {ZF}$ , for every set X, there is an ordinal $\alpha $ such that there is no surjection $f:X\to \alpha $ . $\Theta $ is the least ordinal which is not the surjective image of $\mathbb {R}$ . The hypothesis that $\Theta $ is regular says that for no $\alpha <\Theta $ is there a cofinal function $f:\alpha \to \Theta $ .

(Sargsyan, 2014) showed the following

Theorem 6.7 (Sargsyan).

Suppose the theory $\mathsf {ZFC+}$ “there is a Woodin limit of Woodin cardinals with a measurable above” is consistent. Then the theory is consistent.

Steel & Van Wesep (1982) showed

Theorem 6.8 (Steel-Van Wesep).

Assume . Then

$$\begin{align*}(\mathbb{R}, P(\mathbb{R}))\models \neg\mathtt{WOP} +\mathtt{HAC}.\end{align*}$$

Since this isn’t literally stated in Steel & Van Wesep (1982) and the proof is elementary, we give the proof here. We’ll need the following easy consequence of $\mathsf {AD}_{\mathbb {R}}$ .

Proposition 6.9. Assume $\mathsf {ZF}+\mathsf {AD}_{\mathbb {R}}$ . Then $\mathsf {DC}_{\mathbb {R}}$ .

Proposition 6.10. Assume $\mathsf {ZF}+\mathsf {AD}_{\mathbb {R}}$ . Let $R\subseteq \mathbb {R}\times \mathbb {R}$ . Then there is $R^*\subseteq R$ such that

$$\begin{align*}\forall x(\exists y R(x,y)\to \exists ! y\, R^*(x,y)).\end{align*}$$

In the situation of the previous proposition we say that $R^*$ uniformizes R.

We’ll need just one substantial consequence of determinacy, due to Martin. We will use some nonstandard definitions for expository reasons. Let $X,Y$ be sets of reals. We put $X\leq _W Y$ iff there is a continuous function $f:\mathbb {R}\to \mathbb {R}$ such that $X=f^{-1}[Y]$ . Continuous functions are coded by reals, so we will also let for any real y, $y^{-1}[Y]= f^{-1}[Y]$ if y codes a continuous function and, $y^{-1}[Y] = \emptyset $ , say, otherwise. The Wadge degree of a set X is $[X]_W=\{Y\, |\, Y\leq _W X \vee Y\leq _W (\mathbb {R}\setminus X)\}$ . We put $[X]_W\leq _W [Y]_W$ iff $X\in [Y]_W$ .

Theorem 6.11 (Martin).

Assume $\mathsf {ZF}+\mathsf {AD}+\mathsf {DC}_{\mathbb {R}}$ . Then the Wadge degrees are well-ordered by $\leq _W$ in order-type $\Theta $ .

Under $\mathsf {ZF}+\mathsf {AD}+\mathsf {DC}_{\mathbb {R}}$ , we define the Wadge rank of a set of reals X, $|X|_W$ to be the rank of the Wadge degree of X. So $|X|_W$ is always some ordinal $<\Theta $ .

We need an easy consequence of the hypothesis that $\Theta $ is regular.

Proposition 6.12. Assume $\mathsf {ZF}$ . Suppose $\Theta $ is regular. Then any $f:\mathbb {R}\to \Theta $ has bounded range, that is, there is $\alpha <\Theta $ such that for all $x\in \mathbb {R}$ , $f(x)<\alpha $ .

Proof. Let $f:\mathbb {R}\to \Theta $ . Towards a contradiction, suppose that f is cofinal (i.e., the conclusion of the proposition fails). Let h be the increasing enumeration of the range of f, that is, $h(\xi )$ is the $\xi ^{th}$ ordinal in the range of f. Then h is a cofinal, strictly increasing function from some $\alpha \leq \Theta $ into $\Theta $ . Since $\Theta $ is regular, we must have $\alpha =\Theta $ . But then we have a surjection from $\mathbb {R}$ to $\Theta $ given by $h^{-1}\circ f$ , contradicting the definition of $\Theta $ .□

We can now prove Theorem 6.8.

Proof. As remarked above, $\mathsf {AD}_{\mathbb {R}}$ implies that there is no well-order of the reals, that is, $(\mathbb {R},\mathcal {P}(\mathbb {R}))\models \neg \mathtt {WOP}$ . So we just need to verify that $(\mathbb {R},\mathcal {P}(\mathbb {R}))\models \mathtt {HAC}$ . Let $\varphi $ be a formula in second-order logic. Suppose that $(\mathbb {R},\mathcal {P}(\mathbb {R}))\models \forall x \exists X \varphi (x, X)$ .

We define a function f from $\mathbb {R}$ into $\Theta $ as follows.

$$\begin{align*}f(x)=\text{ the least } \xi \text{ such that there is } X \text{ with } |X|_W=\xi \text{ and } \varphi(x,X).\end{align*}$$

By Proposition 6.12, we have that the range of f is bounded in $\Theta $ . Let $\alpha $ be an upper bound. So for every x there is an X with Wadge degree $<\alpha $ such that $\varphi (x,X)$ . Let A be a set of reals of Wadge degree $\alpha $ . Then for every x there is an $X\leq _W A$ with $\varphi (x,X)$ .

Finally, consider the relation

$$\begin{align*}R(x,y)\Leftrightarrow \varphi(x, y^{-1}[A]).\end{align*}$$

By Proposition 6.10. Let $R^*$ uniformize R. Finally, let

$$\begin{align*}S(x,z)\Leftrightarrow \exists y R(x,y) \wedge z\in y^{-1}[A].\end{align*}$$

Then we have $\forall x \varphi (x, S_x)$ , as desired.□

7 Concluding reflection

As noted $\mathtt {WOP}$ implies all of the indicated choice principles, with the exception of $\mathtt {HAC}$ , which is actually independent of $\mathtt {WOP}$ . We conclude by speculating as to why that is.

Let S be a set (or class) and let T be a set (or class) of sets (or classes). We won’t keep repeating the “or classes”.

Say that $S/T$ -choice holds just in case

If f is a function from S to T such that for each $x \in S, f(x)$ is not empty, then there is a function g such that for all $x \in S, g(x) \in f(c)$ .

The idea is that $S/T$ choice holds just in case the subsets of T that are indexed by S have choice functions.

If S is a set, then let $\mathcal {P}(S)$ be its powerset. Consider, first, the simplest version of the principle $\mathtt {AC}$ :

$$\begin{align*}\forall R(\forall x \exists y Rxy \rightarrow \exists f \forall x Rxfx).\end{align*}$$

This holds on a domain S just in case $S/\mathcal {P}(S)$ -choice holds.

As above, this is not sufficient to guarantee that the domain S is well-ordered. Zermelo’s proof that a given set S has a well-ordering uses a choice function on the powerset of $\mathcal {P}(S)$ of S. This, in turn, is equivalent to $\mathcal {P}(S)/\mathcal {P}(S)$ -choice. Indeed, Zermelo’s proof is that the well-ordering principle and $\mathcal {P}(S)/\mathcal {P}(S)$ -choice are equivalent (in contexts in which both can be stated). Our principle CHOICE is, in effect, $\mathcal {P}(S)/\mathcal {P}(S)$ -choice.

It is a little curious, perhaps, that $\mathtt {AC}$ , or $S/\mathcal {P}(S)$ -choice, is not enough for $\mathtt {WOP}$ since, in the course of the Zermelo-proof, we only apply choice $|S|$ -many times (so to speak)—but we do so in a dependent way.

Turning, finally, to $\mathtt {HAC}$ . Suppose that that holds on a domain S. Then we are in the neighborhood of $S/\mathcal {P}\mathcal {P}(S)$ -choice. In effect, the antecedent of an instance of $\mathtt {HAC}$ amounts to the existence of a function from the domain (S) to a set of sets on S, that is, to $\mathcal {P}\mathcal {P}(S)$ . The difference is that this function has to be definable by a formula in the second-order language. In a third-order language, we could define a principle equivalent to $S/\mathcal {P}\mathcal {P}(S)$ -choice.

So we can, perhaps, see why $\mathtt {HAC}$ is not enough to get $\mathtt {WOP}$ : HAC gives us a choice function on a rich enough set, the powerset of the powerset of the domain, but the sets with choice functions must be indexed by the domain.

And perhaps we can also see why WOP is not enough to get HAC. WOP involves choice functions on the powerset of the domain, and HAC involves choice functions on the powerset of the powerset of the domain.