Nuances Regarding Naturality It's frequently said, informally, that a natural isomorphism is one that doesn't depend on arbitrary choices.
But the phrase "arbitrary choices" lends itself to different interpretations.  Consider the following examples, all concerning a finite-dimensional vector space $V$ over a field $k$:
 A.  The natural isomorphism $V\rightarrow V\otimes_kk$ (by which I mean the obvious natural transformation from the identity functor to the functor  $ -\otimes_kk$) is defined by a basis-free formula $v\mapsto v \otimes  1$, and is easily proved to be an isomorphism without ever invoking the existence of a basis.
 B.  The natural isomorphism $V\rightarrow V^{**}$ is defined by a basis-free formula $v\mapsto \Big(\phi\mapsto \phi(v)\Big)$, but to prove this is an isomorphism, it seems I have to choose a basis.  Likewise for the natural isomorphism $V^*\otimes_k V\mapsto Hom_k(V,V)$.
C.  The natural isomorphism $Hom_k(V,V)\mapsto V^*\otimes_kV$ cannot, I think, even be defined by any basis-free formula.  To define the map, one first chooses a basis and then proves that the definition is independent of that choice.
Is there a more formal way to  distinguish such cases?  I'm looking for a precise definition of what it means to be "definable by a basis-free formula" or "provably an isomorphism without ever mentioning  a basis" --- precise enough so that it's possible to prove (not just suggest, as above) that a given isomorphism satisfies one, the other, both, or neither of these conditions.  
(I suppose that the business about "provably an isomorphism without ever mentioning a basis" is perhaps no more interesting than "provably an isomorphism without ever using $X$", where $X$ is some other known property of vector spaces.  But the business about being "definable by a basis-free formula" seems to me to be more interesting.)
Edited to add: I appreciate the responses, but I fear the main thing I've learned from them  is that I failed to make the question clear. This wasn't intended as a question about vector spaces; the vector spaces were meant to illustrate something more general.  I quite understand the reasons why the map $V^{**}\rightarrow V$ can't be constructed without reference to a basis (most notably, this map doesn't exist in the infinite dimensional case, so there's no hope to construct it without using the finite dimensionality, which means referring to a basis). The question is not why this is true but how to state it in a rigorous way.  How, formally, and in more general contexts than vector spaces, does one formalize the notion of "not constructible without making some choices that turn out to be irrelevant at the end"?   
 A: How, formally, and in more general contexts than vector spaces, does one formalize the notion of "not constructible without making some choices that turn out to be irrelevant at the end"?
(This is a long comment, rather than an answer.)
The first step seems to be formalizing what "making some choices" means.  To some mathematicians, this might simply mean applying the axiom of choice.  For instance, in the context of vector spaces one may want to avoid invoking the existence of a basis because the existence of a basis requires the axiom of choice (for a general space).
But even if we throw out the axiom of choice, there are still natural contexts where choice happens.  For instance, as the other answers have hinted at, we might define a finite dimensional vector space to be a vector space with a certain type of choice function.  If we ever use that choice function, then we have made a choice.
However, your definition of "making some choices" seems to be much broader than even this.  It seems to include, for instance, picking an element from a non-empty set.  Is that right?  Would you consider the fact that "a set with an element is not equal to the empty set" an example of "not constructible without making some choices that turn out to be irrelevant at the end"?
Three further questions.  Let's say you define the natural numbers using Peano arithmetic, one of the axioms being "0 is an element of $\mathbb{N}$".  Is this axiom (which is a theorem too) constructible?  Does it require making choices?  If so, is that choice irrelevant at the end?
One possible answer to formalizing "avoidance of choice making" might be working in the context of natural deduction without $\exists$ elimination.
A: Here are two examples based on sets and one more. Again a long comment.
1) For a set $S$ let $\mathcal{L}$ be the set of linear orders and $\mathcal{P}$ be the set of permutations. There is an easy proof that there is a bijection between these two things, but it depends on choosing an arbitrary but fixed distinguished linear order $\ell$ and composing the obvious bijections $\mathcal{L} \rightarrow \ell \times \mathcal{L} \rightarrow \ell \times \mathcal{P} \rightarrow \mathcal{P}$. This seems unavoidable as there is one, but only one, natural distinguished permutation (once there are three elements) but no distinguished linear order. Alternately, the orbit structure of the natural action of $\operatorname{SYM}_S$ on $\mathcal{L}$ and on $\mathcal{P}$ is not the same.
I stated it that way to highlight the natural bijection between $\mathcal{L} \times \mathcal{L}$ and $\mathcal{L} \times \mathcal{P}$ which is a projection on the first component and, for each fixed first component, a bijection between $\mathcal{L}$ and $\mathcal{P}.$ That seems like a candidate for a proof that the set of bijections is non-empty. Of course it is a little problematic if $S$ might or might not be $\emptyset.$
2) Consider the claim that there is a bijection between the even and odd cardinality finite subsets of a set  $S.$ The obvious proof depends on choosing an arbitrary but fixed element $s$ and using it to partition the finite subsets into pairs $\{{A,A \oplus \{{s\}}\}}$. Since the claim is true precisely when $S \ne \emptyset,$ this seems unavoidable.
3) This one I am less sure of. The point is that something like a Hamel basis  or an everywhere dense non-measurable set seems needed, but the result feels more discrete and concrete than Vitali Sets.
Call a real triple of the form $T_x=\{{x,x+1,x+\sqrt{2}\}}$ an ell.
I want to claim that $\mathbb{R}$ can be partitioned into disjoint ells (call this a $1$-cover). Alternately, but perhaps not equivalently, there is a subset $X \subset \mathbb{R}$ such that $X,X+1$ and $X+\sqrt{2}$ constitutes a partition of $\mathbb{R}$ into three disjoint congruent sets.
The set of all ells is a $3$-fold cover of $\mathbb{R}.$ I will give a natural partition of $\mathbb{R}$ into sets called boards such that there is an explicit and unique set of three $1$-covers for each board. Then a $1$-cover of $\mathbb{R}$ is precisely a selection of one $1$-cover (from the possible three) for each board.
It seems pretty natural that the following are equivalence relations in $\mathbb{R}$. 


*

*$x \sim y$ when $x-y \in \{{a+b\sqrt{2} \mid a,b \in \mathbb{Z}\}}$ 

*$x \approx y$ when $x-y \in \{{a+b\sqrt{2} \mid a,b \in \mathbb{Z} \text{ and }a\equiv b \bmod 3\}}.$


This does not require extending $\{{1,\sqrt{2}\}}$ to an explicit basis of $\mathbb{R}$ over $\mathbb{Z}.$ Note that an equivalence class is everywhere dense. Call an $\sim$-equivalence class a board. Also, consider the equivalence relations on the set of ells defined by $T_x \sim T_y$ and $T_x \approx T_y$ when $x \sim y$ and $x \approx y.$
Each ell lies entirely in one board and its $\approx$-equivalence class is the unique $1$-cover of that board including that ell. A $\sim$-equivalence class constitutes a $3$-cover of its board and it resolves into three $\approx$-equivalence classes which are the only $1$-covers of that board.
A: The issue here is that the inverses to $V\rightarrow V^{**}$ and $V^*\otimes V\rightarrow \mathrm{Hom}(V,V)$ don't exist in the infinite dimensional case. So in order to show that they exist one has to assume that $V$ is finite dimensional. Now, if your definition of "finite dimensional" is "has a finite basis", then of course you have to use a basis at some point.
One option is to instead take your definition of "finite dimensional" to be "the natural map $V^*\otimes V\rightarrow \mathrm{Hom}(V,V)$ has an inverse". Then you can prove many facts about finite dimensional vector spaces without using a basis at all, and in particular you can construct an inverse to the map $V\rightarrow V^{**}$.
A: An object $V$ in a symmetric monoidal category is said to be dualizable with dual $V^{\ast}$ if you can find maps
$$\text{ev} : V^{\ast} \otimes V \to 1$$
and
$$\text{coev} : 1 \to V \otimes V^{\ast}$$
such that the zigzag identities hold (the same zigzag identities in the unit-counit definition of an adjunction). It's a formal exercise to show that if $V$ is dualizable with dual $V^{\ast}$ then $V^{\ast}$ is dualizable with dual $V$; moreover, if the ambient symmetric monoidal category is closed, then you can always take $V^{\ast} = [V, 1]$ to be the internal hom of $V$ and the unit, and $\text{ev}$ to be the evaluation map. From here it's not hard to show that
$$V \to [[V, 1], 1] \cong (V^{\ast})^{\ast}$$
is an isomorphism for any dualizable $V$; in other words, dualizable objects are reflexive. It's also true that if $V$ is dualizable then
$$[V, W] \cong V^{\ast} \otimes W$$
for any $W$. None of this requires making any choices and is completely canonical once you show that if duals (together with their evaluation and coevaluation maps) exist then they are unique up to unique isomorphism. 
Now, in the case of vector spaces, the dualizable objects are precisely the finite-dimensional ones. Whether you need to exhibit a basis to prove this depends on whether your definition of finite-dimensional is "has a basis." Here it is the coevaluation map which it is troublesome to define without a choice of basis; with a choice of basis $e_i$ it's given by
$$\text{coev} : 1 \ni 1 \mapsto \sum e_i \otimes e_i^{\ast} \in V \otimes V^{\ast}$$
where $e_i^{\ast}$ is the dual basis. But this does not weaken the naturality of anything that's been said here, again because of the important fact that duals (together with their evaluation and coevaluation maps) are unique if they exist.
As in Oscar Cunningham's answer, if your definition of "finite-dimensional" happens to be "the natural map $V \otimes V^{\ast} \to [V, V]$ is an isomorphism" (this map always exists and requires nothing to define) then you can define the coevaluation map to be the inclusion of the identity element into $[V, V]$. At some point you will want to show that something is finite-dimensional, though, and then you might need to pick a basis. But that's okay. 
