I'm reading "All the mathematics you missed but need to know for graduate school", and in page 208, the author is talking about axiom of choice and says:
This leads to the observation that if the axiom of choice is needed to prove the existence of some object, then you will never be able to actually construct that object.
My question is, is this a theorem? In case it is, where can I find the formal statement of that theorem? and what formally it says.
On
In the 1930's Kurt Godel showed that if the set-theoretic axiom system $ZF$ (Zermelo-Fraenkel) is consistent then neither the negation of $AC$ (the axiom of choice) nor the negation of $GCH$ ( the generalized continuum hypothesis) can be provable from $ZF.$ Godel used what is now called "Godel's Constructible Class" , usually denoted by $L.$
The axiom system $ZF+AC$ is usually denoted as $ZFC.$ Godel proved that $Con(ZF)\implies Con(ZFC+GCH).$ In particular Godel proved that $$Con(ZF)\implies Con (ZF+AC).$$ BTW . Godel's Incompleteness Theorems showed the impossibility of proving $Con (ZF)$ from $ZF$ itself (unless $ZF$ is actually inconsistent, in which case it proves every sentence in the language of set theory).
In the late 1960's Paul Cohen developed a method he called Forcing (It's still called Forcing) to show that if $ZF$ is consistent then $AC$ is not provable from ZF (and also that if $ZFC$ is consistent then $CH$ (the Contnuum Hypothesis) is not a theorem of $ZFC$ ). So Cohen proved that $$Con(ZF)\implies Con (ZF+(\neg AC)).$$
So if you $need$ $AC$ to show something, then you can't do it from the rest of the axioms (i.e. from $ZF).$ (Unless you have a set-theoretic proof from $ZF$ that $1=0.$)
I learned Forcing mainly from "Set Theory: An Introduction To Independence Proofs" (1st edition) by K. Kunen, and from some excellent teachers. But I find Kunen's treatment of Godel's $L$ (in the section "Defining Definability") almost unreadable. For a brief, clear introduction to $L$ there is an article in the book "Lectures In Set Theory" (various authors; edited by Morley).
This is an intuitive explanation of modern mathematical use of the axiom of choice.
Hamel basis for $\Bbb R$ over $\Bbb Q$ exist because the axiom of choice can prove them, but you can't quite do it without the axiom of choice, since indeed it is consistent without choice that no such basis exist.
But that's just an example. Modern mathematics is not concerned that much about using the axiom of choice. And many things which you might think that you "construct" are actually using implicitly some weak version of the axiom of choice in one way or another. Other things, where the general proof is using choice, can actually be proved without choice in some way or another.
For example, one might think that the Baire Category Theorem is constructive, since given a countable sequence of dense open sets, and a point $x$, we can "construct" a sequence which lies in the intersection of these sets and converges to $x$. But, BCT is in fact equivalent to a weak choice principle known as Dependent Choice. Nonetheless, BCT is actually provable for separable spaces without using choice, so suddenly all that use of choice can be avoided by being clever.
And all of this is not even starting to take into account the fact that the word "construct" is not entirely mathematical, but rather a natural language term we use to describe mathematics. So the meaning is not well-defined like the term "vector space". Some people would say that a construction with transfinite recursion is a perfectly valid construction, and indeed you don't need choice for that. But using choice, you can construct things with transfinite recursion, e.g. a Hamel basis for $\Bbb R$ over $\Bbb Q$. So which one is it?
But as far as intuition goes, that is generally a good rule of thumb. If you can construct something explicitly, you probably didn't use the axiom of choice in that definition. And if you can't quite do that, well, then you probably needed to use the axiom of choice somewhere in a substantial way.
There are essentially two ways to move forward from your position: either become an expert on the axiom of choice, which will make you a bona fide set theorist, and then you can judge whether or not choice was used on this or that construction; or accept that the axiom of choice is a perfectly reasonable and accepted mathematical principle in our day and age, and use this rule of thumb while remember that that what it is, a rule of thumb and nothing more.