How far is it true that statements dependent on Axiom of Choice are not constructive.

Question

Axiom of Choice is often used in mathematics to construct various objects, such as basis of $\mathbb{R}$ as a vector space over $\mathbb{Q}$, unmeasurable subset of $\mathbb{R}$, or a non-principal ultrafilter on $\mathbb{N}$.

It is a popular "meta-theorem" that if such construction essentially relies on the Axiom of Choice, then the object cannot be constructed explicitly. Here, by "essentially relying" I mean that it is consistent with ZF that what we are constructing (Hamel basis, ultrafilter, etc.) does not exist; by "explicit construction" I mean one that can be carried out within ZF.

My question is: Is this meta-theorem really true? Certainly, it is not possible to carry out a construction within ZF, and then prove it correct in ZF. However, it struck me that it might be possible that the construction itself fits in ZF, and it is only verification that requires the Axiom of Choice. Of course, it would be very bizarre, but bizarre things do happen. Do we have some strong evidence that they won't occur in this situation? How certain is it that, say, a Hamel basis can't be constructed in ZF?

Answer 1

We know it is impossible to define a Hamel basis for $\Bbb R$ over $\Bbb Q$ (or construct a non-principal ultrafilter, and so on) because it is a theorem:

If $\sf ZFC$ is consistent, then the theory $\sf ZF+\text{There is no Hamel basis for }\Bbb R\text{ over }\Bbb Q$ is consistent.

Since it is consistent with $\sf ZF$ that there is no such basis, it means that we cannot prove from $\sf ZF$ that such basis exists. We have to assume more, in terms of choice.

Remember the completeness theorem tells us that $\sf ZF\vdash\varphi$ if and only if $\varphi$ is true in every model of $\sf ZF$. Similarly for $\sf ZFC$. So given a statement $\varphi$ which is provable from $\sf ZFC$, if we can find a model of $\sf ZF$ where $\varphi$ fails, we can be certain that $\sf ZF$ cannot prove it, and some axiom of choice is needed for the proof.

For example, we know that if $\sf ZFC$ is consistent then we can create a model in which there is no Hamel basis of $\Bbb R$ over $\Bbb Q$. Of course, in that model the axiom of choice fails, but the process itself is consistent. Of course it might be the case that there are no models of $\sf ZFC$ at all, but we still know how to make it work then. We can translate these arguments into syntactic arguments which state the quote text above.

Answer 2

Depending on one's interpretation of the "meta-theorem" you stated, the following might be seen as a counterexample.

There is a sentence $\varphi$ such that it is a theorem of $\mathsf{ZF}$ that $\varphi$ defines a Hamel basis $B$ of $\mathbb{R} \cap L$ over $\mathbb{Q}$. Here $L$ denotes Goedel's constructible universe. It is a theorem of $\mathsf{ZF}$ that $L \models \mathsf{ZFC} + V=L$, that the relativization $\varphi^L$ of $\varphi$ to $L$ defines the same set $B$ within $L$, and that $L \models B \text{ is a Hamel basis of $\mathbb{R}$ over $\mathbb{Q}$.}$

So here we have a "construction" (definition) $\varphi$ such that $\mathsf{ZF}$ proves that it defines a unique object, and that this object is a $\mathbb{Q}$-linearly independent set of reals, but does not prove that the $\mathbb{Q}$-linear span of the set of reals so defined is all of $\mathbb{R}$. On the other hand, the theory $\mathsf{ZFC} + V = L$ "verifies" (proves) that the set $B$ defined by $\varphi$ does in fact span $\mathbb{R}$, and therefore is a Hamel basis for $\mathbb{R}$ over $\mathbb{Q}$.

The only problem with this counterexample is that the "verification" requires the theory $\mathsf{ZFC} + V = L$, which is properly stronger than $\mathsf{ZFC}$. I'm not sure if this addresses your question (which is a bit fuzzy) but I thought it was worth mentioning.

EDIT: One main point of this "counterexample" is that, although many people think of models of AC as containing more sets (e.g. more $\mathbb{Q}$-linearly independent subsets of $\mathbb{R}$, including some that span) it makes just as much sense to think of them as containing fewer sets (e.g. fewer reals, so that spanning becomes easier.) Given models $M$ and $N$ of $\mathsf{ZF}$ with $M \subset N$, one can have $M \models \mathsf{AC}$ and $N \models \neg \mathsf{AC}$ or vice versa. So it is not always right to think of $\mathsf{AC}$ as providing "extra" sets.