Define dimension without referring to bases The dimension of a vector space is the common cardinality of all bases. I would like to define it in a way that does not refer to bases. I only care about finite dimensional vector spaces.
First, I need to define what it means for a vector space to be finite dimensional without referring to a basis. One definition that works is to say that $V$ is finite-dimensional if the natural map $V\rightarrow (V^*)^*$ is an isomorphism (that's the double dual). I am open to other basis-free definitions.
As for defining what $\dim V$ is, my first thought was to define it as $\text{trace}(I)$. This is true, but it is not quite basis-free:
We have an isomorphism $V^*\otimes V \cong \hom(V,V)$. On $V^*\otimes V$, I can define the trace in a basis-free way. I can also define this map $V^*\otimes V \rightarrow \hom(V,V)$ without referring to a basis. However, I don't know how to show that it is an isomorphism without referring to bases. It would be especially nice if we could pinpoint of the identity map $V\rightarrow V$ as an element of $V^*\otimes V$ without referring to bases. Maybe it's the unique fixed point of some action or something like that?
Regarding the answers: At the moment there are three answers by Andreas Blass, Thorgott and me. I accepted one because I can only accept one. All three are worth reading in my opinion.
 A: $$\dim(V)\colon=\sup\{n\in\mathbb{N}_0\vert\exists U_0\subsetneq U_1\subsetneq...\subsetneq U_n,\text{ subspaces of }V\}\in\mathbb{N}_0\cup\{\infty\}$$
A: I think the following works and is of a same flavour as the suggestion of Thorgott
Let $P: V \to V$ be a linear map. $P$ is said to be a projection map if $P^2=P$. Furthermore, we call a sequence of projection maps $P_{1}, \dots, P_{n}$ proper if $P_{i}[im P_{i-1}] \neq im P_{i-1}$ for all $i \in \{2,\dots, n\}$ and we say that a sequence of projection maps terminates at step $i$ if $P_{i} \circ \dots \circ P_{1} = 0$. 
Now we call a vector space $V$ finite dimensional of dimension $n$ if there exists some proper sequence of projection maps of length $P_{1}, \dots , P_{n}$ such that it terminates
A: I got it!
Let $V$ be a vector space over a field $F$.
Assume that the natural map $V\rightarrow V^{**}$ given by $v\mapsto(\varphi\mapsto \varphi(v))$ is an isomorphism.
Then, the natural map $f:V\otimes V^*\rightarrow (V^*\otimes V)^*$, given by $f(v\otimes\varphi)=(\alpha\otimes u\mapsto\alpha(v)\cdot \varphi(u))$, is an isomorphism.
Consider $\text{trace}\in (V^*\otimes V)^*$, and define $I=f^{-1}(\text{trace})$.
Define the dimension of $V$ to be $\text{trace}(I)$.
So the $\dim V$ is the "trace of trace"!
A: Two options that are close to using bases but don't actually mention them:
(1) The dimension of $V$ is the smallest number of vectors that span $V$.
(2) The dimension of $V$ is the largest size of any linearly independent set of vectors in $V$.
To put it another way, the notion of basis combines the two notions of spanning and linear independence. But either one of these two notions is enough to define dimension; you don't need both.
