How is the axiom of choice used (or not used) in the proof of the Lesbegue covering theorem in Andrej Bauer's paper in constructive mathematics?

Question

In this paper Five stages of accepting constructive mathematics on page 484 (shown in the image below) it contrastingly shows the use of the axiom of choice ($\sf AC$) in the first proof and avoidance of its usage in the second proof. However I fail to see how the two proofs are distinct because it seems that the second proof appears exactly like the first except with the absence of the subscript $x$ in $\epsilon_x$. In the image below it says,

"Such hidden choice happens whenever we introduce a new symbol and subscript it with another one to indicate a dependence, in our case $\epsilon_x$."

but in the second proof the $\epsilon$ still depends on the $x$, so based on this dependence are we not still implicitly applying $\sf AC$ in the second proof? It seems to me that the two proofs are "isomorphic", the only difference is in the labelling of $\epsilon$.

This leads me to my question:

1. If such a hidden choice happens based on dependence with subscripts appended to a symbol, how is this essentially different to the second proof where $\epsilon$ still depends on $x$ (except one didn't write down the subscripts)? How is it then that we are not implicitly applying $\sf AC$ in the second proof?

Addendum (November 14, 2021):

I'd like to add what I understand regarding how $\sf AC$ is used in the first proof. I'm not sure if this is what is really going on so I very much welcome corrections!

Given $\sf AC$

$\forall S \left[ \varnothing \notin S \Rightarrow \exists f:S\to\bigcup S \enspace (\forall A \in S)(f(A)\in A)\right]$ $\qquad (*)$

I'm under the impression that to show "For every $x\in X$, take $\epsilon_x>0$" requires more work using $\sf AC$ as we would have to construct the the following set¹

$\displaystyle \mathcal{F}:=\{ Z \in \mathcal{P}\mathcal{P}(X) : (\exists x\in X)(\forall Y\in \mathcal{P}(X)) \left[ Y\in Z \leftrightarrow (\exists \epsilon>0) (Y=B(x,\epsilon) \wedge (\exists A\in\mathcal{A})(B(x,2\epsilon)\subseteq A)\right] \}$

and then we apply $\sf AC$ to the set $\mathcal{F}$ by substituting $\mathcal{F}$ into $S$ in $(*)$ to deduce the consequent of $(*)$, then apply existential instantiation to the consequent so that we have $f:\mathcal{F}\to \bigcup\mathcal{F}$ such that $(\forall Z\in\mathcal{F})(f(Z)\in Z)$. Then define² $g:X\to\mathcal{F}$ where

$$g(x):=\{B(x,\epsilon): \epsilon>0 \wedge (\exists A\in\mathcal{A})(B(x,2\epsilon)\subseteq A)\} $$

It is then evident that $f\circ g :X\to \bigcup X$ such that $f\circ g:x\mapsto \epsilon_x$ is the function in the paper that includes a choice function $f$ (via $\sf AC$). Now we can obtain the open cover $\{B(x,\epsilon_x)\}_{x\in X}$ via $f\circ g$. Therefore by existential instantiation we have our open cover $\{B(x,\epsilon_x)\}_{x\in X}$.

Thus I'm led to further additional questions:

2. So based on this it seems like invoking $\sf AC$ required more work to actually spell it out? Is this what is really going on in the phrase "For every $x\in X$, take $\epsilon_x>0$"?

3. Admittedly the way I initially (before this addendum) interpreted the first proof was really in accordance with what the second proof was saying. So when we do "introduce a new symbol and subscript it with another one to indicate dependence", does this really mean that I implicitly used $\sf AC$?

4. Constructing the function $g$ and the set $\mathcal{F}$ did not require $\sf AC$ (at least as far as I'm aware), but asserting the existence of $f$ necessarily requires (based on my intuitive understanding of heuristic arguments for usage of $\sf AC$) $\sf AC$. So how do we know a priori (if this is even possible to "know"?) that there is a plausible argument without $AC$ before we find one? Conversely, what types of formulations indicate to us that a priori (again, is this even possible to "know"?) we know $\sf{AC}$ will be necessary so that trying to find an argument without $AC$ is futile? Can you provide examples?

---

Footnotes.

1. Apologies for the readability as I eschewed using $\sf AC$ by ensuring that the set formed did not use it. The set $\{\{B(x,\epsilon) : (\exists A\in\mathcal{A})(B(x,2\epsilon)\subseteq A)\}_{x} \in \mathcal{P}\mathcal{P}(X) : x\in X \}$ is exactly the set $\mathcal{F}$ above, but I'm not sure if I needed $\sf AC$ to form this (In a sense it doesn't really matter if this implicitly uses $\sf AC$ or not since we will end up using $\sf AC$ to obtain the function $f:\mathcal{F}\to \bigcup\mathcal{F}$ anyway, but I just wanted to push and see how far I could go without using $\sf AC$).

2. I'm aware that this is subscripting $x$ to the family of balls so it looks like I may have used $\sf AC$ but it seems to me that I haven't because I'm not making an arbitrary choice. In fact we can show that $(\forall x\in X)(\exists ! Z\in \mathcal{F})(\forall Y\in Z)\left[x\in Y\right]$ so in fact I did not make an arbitrary choice and $g(x)$ is that unique $Z$ that satisfies the given formula. I'm not so sure whether it is necessary to show that this formula holds in order to completely assert that choice is not used, but sufficiently so implies we did not. So we really only used choice to obtain the function $f$ and not $g$.

Answer 1

Here is a clear way (imo) to see that the first proof uses choice:

Let $\mathcal{A}$ be an open cover of $X$. Then each $x$ lies in some $A \in \mathcal{A}$, and so each $x$ has an open ball $B(x, 2 \epsilon) \subseteq A$. Of course, there are many choices of $\epsilon$ which work for a given $x$. Now choose an $\epsilon_x$ for every $x \in X$. Then $\{ B(x, 2 \epsilon_x) \mid x \in X\}$ is an open cover, thus has a finite subcover, and taking the minimum of the resulting $\epsilon_x$s finishes the job.

Notice what we've done here: We first argue that every $x$ has an associated family $E_x \triangleq \{ \epsilon \mid B(x,2 \epsilon) \subseteq A \text{ for some } A \in \mathcal{A} \}$. Since $\mathcal{A}$ is an open cover, we know that each $E_x$ is nonempty, so by $\mathsf{AC}$ we can choose an $\epsilon_x$ from each $E_x$. This is what the author means by "hidden choice": We have a family of objects (in this case the $E_x$s) associated to each $x$, and then we want to choose one $\epsilon_x$ from each family. Anytime we have to make an arbitrary choice for (infinitely many) points, we need $\mathsf{AC}$ to actually do it. Again, in this example we know that for every $x$ there exists some $\epsilon$ which does the trick, but if you actually want to choose a specific $\epsilon_x$ for each $x$, we need $\mathsf{AC}$ to do so.

Now let's take a look at the second proof.

Let $\mathcal{A}$ be an open cover of $X$. Note $\{ B(x, 2 \epsilon) \mid x \in X, \epsilon \in (0,\infty), B(x,2 \epsilon) \subseteq A \text{ for some } A \in \mathcal{A} \}$ is an open cover too. By compactness, it admits a finite subcover, and taking the minimum of the resulting $\epsilon$s does what we want.

So, what's different here? The idea is that we don't make any choices! Instead of choosing an $\epsilon$ for each $x$, we just (inefficiently!) take every possible $\epsilon$ at once. This is a very common strategy for avoiding arbitrary choices: Instead of choosing one thing, find a way to use everything, even if it contains irrelevant information. This is the same reason that the fundamental group is not canonical (it depends on a choice of base point) while the fundamental groupoid is canonical (we can choose every point to be a base point).

---

As for your follow-up questions:

2. It's not infrequent that proofs requiring $\mathsf{AC}$ are formally less efficient than their $\mathsf{AC}$-free counterparts (in exactly the way you've noticed). Philosophically one could say that this is because a proof without $\mathsf{AC}$ has computational content (which makes it easier to formalize), but I don't know of a way to make this precise. That said, oftentimes the $\mathsf{AC}$-free proofs feel inefficient at a higher level. After all, why would we consider the whole huge family $\{ B(x, \epsilon) \mid x \in X, \epsilon \in (0,\infty) \}$ when the (much smaller looking) family $\{ B(x, \epsilon_x) \mid x \in X \}$ suffices? We as humans really like efficiency, and so it can be hard to see the option of taking everything all at once when the option of taking only what's required (even if it requires making choices) is available.

3. Introducing a symbol with a subscript implicitly assumes $\mathsf{AC}$ exactly when you have to arbitrarily choose what that symbol should mean from a set of possible options. For instance, in the above example any element of $E_x$ will do, but if you want to fix a specific $\epsilon_x$ then we have to choose an $\epsilon_x \in E_x$ for every $x$! However, there are two situations where this is ok. First, if you're only making finitely many choices. There's nothing wrong with choosing a finite number of things -- we only need $\mathsf{AC}$ to simultaneously make an infinite number of choices! Second, if your "choices" are actually canonical in some sense. In the above example, no $\epsilon_x$ was better than any other. But suppose instead we let $\epsilon_x = \max \{ \frac{1}{k} \mid k \in \mathbb{N}, B(x, \frac{2}{k}) \subseteq A \text{ for some } A \in \mathcal{A} \}$. Provided $\mathcal{A}$ is definable in some sense, then our function $x \mapsto \epsilon_x$ is definable too! Here instead of needing to choose an $\epsilon_x$ arbitrarily, we come up with a rule for determining $\epsilon_x$ for us! The study of cleverly coming up with these rules to sidestep $\mathsf{AC}$ is part of descriptive set theory, and there is a wealth of machinery for solving problems like this.

4. Knowing whether $\mathsf{AC}$ is necessary is a fairly subtle matter. There are a ton of statements that are equivalent to $\mathsf{AC}$ (in fact, there's an entire book dedicated to them!) and some are quite surprising. Moreover, I don't have a ton of intuition for knowing which results necessarily depend on choice, so I can't provide any words of wisdom here. Hopefully someone more knowledgeable is able to chime in!

---

I hope this helps ^_^

Answer 2

Let me try to illustrate the difference by giving yet another example.

Let $M \neq \emptyset$ be some set. Using the definition of equality on sets and the fact that $y \in \emptyset$ is wrong for any $y$, we get that the statement $M \neq \emptyset$ is equivalent to $$ \neg (\forall x : x \in M \iff x \in \emptyset ) \\ \iff \neg (\forall x : x \in M \implies x \in \emptyset ) \\ \iff \exists x: x \in M \land x \notin \emptyset \\ \iff \exists x: x \in M $$ By existential instantiation then, we get an element $x$ with the porperty $x \in M$.

Now here is the path we can take using $\mathsf{AC}$. Take the collection $S = \{ M \}$, then by $\mathsf{AC}$ there is a function $f : S \to \bigcup S$ such that $\forall A : f(A) \in A$. Given this particular $S$ this means: $$ f : \{ M \} \to M \hspace{3em} f(M) \in M $$ This time, the choice function $f$ gives us the desired element with property $f(M) \in M$.

---

The above illustrates a case where $\mathsf{AC}$ is clearly not needed, since $M \neq \emptyset$ is already equivalent to a statement giving us the existence of some element in $M$ (the argument was not constructively valid though!). I a setting without $\mathsf{AC}$ it therefore matters greatly to be aware of these possibilities.