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

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?

• /Checks watch. Begins counting down until Asaf's arrival./ – Cameron Buie Jun 1 '13 at 22:12
• @Cameron: I was interrupted by a phone call that ended up being the wrong number... :-) – Asaf Karagila Jun 1 '13 at 22:13

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.

• Don't you mean "If ZF is consistent"? ZFC is consistent if ZF is, so those are really the same, but it seems more natural to drop that C. – dfeuer Jun 1 '13 at 22:14
• @dfeuer: No, I mean $\sf ZFC$. Yes, those are the same thing, but almost all the constructions begin with a model of $\sf ZFC$. It's easier to skip the step of consistency of $\sf ZFC$ from the consistency of $\sf ZF$. – Asaf Karagila Jun 1 '13 at 22:16
• @Feanor: You're welcome. – Asaf Karagila Jun 1 '13 at 22:24
• I could be wrong, but I don't think it quite answers the question. I don't know what a Hammel basis is, but my understanding is that the asker wanted to know if there was an object $x$ that can be constructed in ZF which ZFC, but not ZF, can prove to have property $P$. The answer is yes, in a very trivial way: let $P(x)$ hold iff for every set $S$ of non-empty sets, $S \setminus x$ has a choice function. Then in ZFC, $P(x)$ holds for every ZF-constructable set, but this property cannot be proven in ZF for even one set. – dfeuer Jun 1 '13 at 22:37
• @dfeuer: I think Asaf Karagila answered my problem, but thank you for the concern. What I understand now is that given a set $A \subset \mathbb{R}$ (possible to construct without AC), if it was a Hamel basis, then $ZF +$ "no Hamel basis exists" would not have a model, hence would not be consistent (but we already know it is). I think the difference is that such set $A$ is (or isn't) a Hamel basis as soon as it is constructed, and this can't be changed by adding additional assumptions about general sets. – Jakub Konieczny Jun 1 '13 at 23:59

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.

• I assume it's the fact I only managed to sleep for one hour "this morning", but the first part of your answer, about $V=L$, is completely incomprehensible to me. As for the second part, to drive the point home, we can have $M\subseteq N\subseteq M'$ such that $M,M'\models\sf ZFC$ and $N\models\sf ZF+\lnot AC$. – Asaf Karagila Jun 2 '13 at 7:19
• @Asaf Yes, it's not very clearly written. However, I too am getting sleepy, so maybe I will write more tomorrow. In the meantime it's probably easier to think about wellorderings of the reals rather than Hamel bases. One can always define a well-ordering of the set $\mathbb{R} \cap L$, and this set may be all of $\mathbb{R}$ or it may be merely countable. – Trevor Wilson Jun 2 '13 at 7:26
• Well, to drive that point further, one can use the same definition outside of $L$, it's just not provable that this set is a Hamel basis/well-ordering/etc. (because of often it won't be.) I think Miller proved that there is a $\Pi^1_1$ Hamel basis in $L$, but I'm far from being in the right cognitive state of mind to be certain. – Asaf Karagila Jun 2 '13 at 7:29
• I was thinking of a definition that is absolute to $L$, in which case whether it is a Hamel basis for $\mathbb{R} \cap L$ (resp. well-ordering of $\mathbb{R} \cap L$) is absolute to $L$. What is not absolute to $L$ is the statement $\mathbb{R} \cap L = \mathbb{R}$, of course. – Trevor Wilson Jun 2 '13 at 7:34
• Yes, I'm glad that we both understand each other, and that we both agree that we're both tired... :-) – Asaf Karagila Jun 2 '13 at 7:35