It is true that the axiom of choice is equivalent to the statement that every linear space has a Hamel basis. There are some linear spaces which definitely don't need axiom of choice to possess (rather canonical) basis: for example $c_{00}$, the space of all sequences with compact supports. Is it possible to give an example of one linear space $V$ with the property: the existence of basis in $V$ implies the axiom of choice?

3$\begingroup$ Let me offer a way to make your final question more precise: Can we give a definition $\varphi$ in the language of set theory, such that if AC fails, then $\varphi$ defines a space with no basis? $\endgroup$ – Joel David Hamkins Mar 10 '16 at 22:16
No. It is not possible.
Suppose that $V$ is a specified vector space, then it is consistent that the axiom of choice fails very far above $V$ in the hierarchy of sets (the von Neumann hierarchy). In particular it would mean that $V$ has a basis, but still the axiom of choice fails, as it fails very far above $V$.
Generally speaking, no particular set can witness the axiom of choice. It is possible, that one set can decide the axiom of choice (so it is possible that one vector space's basis decides the axiom of choice), but this requires additional assumptions. More specifically, this assumption was formulated by Andreas Blass as "Small Violations of Choice" (SVC). It means that there is a set which "more or less" decides a lot of the information regarding the axiom of choice in the universe. From this set we can create a vector space, that has a basis if and only if the original set can be wellordered and that would imply the axiom of choice in full.

$\begingroup$ Asaf, do you claim that there is no definition $\varphi$ as in my comment above on the OP? I wonder if there is such a $\varphi$, by considering $P(\kappa)$ for the least $\kappa$ for which this is not wellorderable, and then building a space on it somehow with no basis. $\endgroup$ – Joel David Hamkins Mar 10 '16 at 22:19

$\begingroup$ But this $\kappa$ is not really specified. Just like how the failure of the axiom of choice does not specify which is this $\kappa$. $\endgroup$ – Asaf Karagila Mar 10 '16 at 22:29

$\begingroup$ That $\kappa$ is definable: it is the least $\kappa$ such that $P(\kappa)$ is not wellorderable. $\endgroup$ – Joel David Hamkins Mar 10 '16 at 22:43

$\begingroup$ Definable as specified are two different things. Specified is a semantic notion, in the sense that the specific object is specified. Definable is a semisyntactic notion which means we can specify an object in the language within a single model. $\endgroup$ – Asaf Karagila Mar 10 '16 at 22:46

$\begingroup$ What I suspect is that there is a formula $\varphi(x)$ in the language of set theory, such that ZF proves $\neg\text{AC}$ implies that there is a unique object satisfying $\varphi(x)$ and it is a vector space with no basis. This would be a way of defining in ZF a particular counterexample. $\endgroup$ – Joel David Hamkins Mar 10 '16 at 22:50
Yes, it is true that AC is equivalent to the assertion that every vector space has a basis, and this is discussed in all the usual treatments of equivalents to the axiom of choice. For example, the reference is given on the wikipedia entry for the axiom of choice. The result is due to Andreas Blass, who is active here on MathOverflow.
Regarding your request for a single space witnessing AC, there is a sense in which this is trivially true. If AC fails, then let $V$ be any particular space without a basis. Then, for this particular space, it is true to say:
 If $V$ has a basis, then AC holds.
And furthermore, if AC holds, then any space $V$ makes that statement true. But I realize that is not what you meant.
Meanwhile, as Asaf points out, there is a general sense in which no particular wellorder is sufficient to ensure AC, because there could always be higher violations of AC at higher cardinals. The symmetric model methods allow you to build models of $\neg\text{AC}$ while preserving AC in any desired rankinitial segment of the universe. So that is one way of answering your final request negatively.

2$\begingroup$ (Also, enjoy tomorrow. I'll be following the videos.) $\endgroup$ – Asaf Karagila Mar 10 '16 at 22:31

2$\begingroup$ Can we eliminate that triviality? What about this question: is there a formula $\varphi$ such that ZF proves the following statements: "there exists a unique $x$ such that $\varphi(x)$", "if $\varphi(x)$ then $x$ is a vector space", and "if $\varphi(x)$ and $x$ has a basis then AC". $\endgroup$ – Nate Eldredge Mar 10 '16 at 22:35

1$\begingroup$ @Nate: No, this would be equivalent to SVC. And we know that SVC is not provable. For example in any model obtained by a class symmetric extension, SVC fails. $\endgroup$ – Asaf Karagila Mar 10 '16 at 22:44

1$\begingroup$ Asaf, I don't think what you say is correct, and I suspect that there is a formula $\varphi$ as Nate describes, since this is basically equivalent to what I am suggesting in my comments on the OP and on your answer. $\endgroup$ – Joel David Hamkins Mar 10 '16 at 22:53

3$\begingroup$ If there is a any specific field $F$ such that "every $F$vector space has a basis then AC holds" then there is such a formula: consider the direct sum of all $F$vector spaces in $V_\alpha$ where $\alpha$ is least such that some $F$vector space in $V_\alpha$ has no basis. Unfortunately, it is not yet known whether such a field $F$ exists. $\endgroup$ – François G. Dorais♦ Mar 11 '16 at 3:36