Sizes of bases of vector spaces without the axiom of choice Assuming the axiom of choice does not hold we have that there is a vector space without a basis. The situation can be, in some sense, worse. It is consistent that there are vector spaces that have two bases with completely different cardinalities. 
Is anything known on when a vector space is spanned by sets of different cardinalities, and on the relation between those cardinalities? 
Is there a known relation between common choice principles (BPIT, DC, etc.) and possible cardinalities of a vector space? (For example, does BPIT implies that every two bases have the same size?)
 A: Yes, ZF+BPIT implies that vector space dimension is well-defined.
[Edit: some Googling shows that James Halpern gave the same answer back in the 1960s.]
Working in ZF+BPIT, fix a field $F$ and an $F$-vector space $V$ and bases $A$ and $B$ of V. That is, each element of $V$ is a unique $F$-linear combination of elements of $A$; likewise for $B$. For each $a\in A$, let $S_a$ be the minimal subset of $B$ such that $a$ is spanned by $S_a$. Each $S_a$ is finite; give it the discrete topology.  Let $X=\prod_{a\in A}S_a$, which is nonempty by BPIT (and is compact Hausdorff). By Schroeder-Bernstein, it suffices to show that some $f\in X$ is injective. By compactness, it suffices to show that for every finite subset $K$ of $A$, there is an $f\in X$ that is injective on $K$. Since each $\prod_{a\in A\setminus K}S_a$ is nonempty by BPIT, it suffices to show that there is an injection in every $\prod_{a\in K}S_a$. That is a nice little linear algebra exercise you can solve in ZF using the finite case of Hall's marriage theorem.
A: If I'm  not mistaken there is another proof that BPI implies that any two bases of a vector space have the same cardinality. As has been noted earlier, if $(u_i)_{i \in I}$ and $(v_j)_{j\in j}$ are two bases of $V$ vector space over $K$ it suffices to show that there's an injection $I\to J$. 
We're going to use the equivalence "BPI$\iff$ Compactness for propositional logic". For each $i\in I$ there exists a unique minimal finite set $J_i \subset J$ such that $u_i$ is spanned by $J_i$. For $i \in I, j\in J$ we create a propositional variable $P_{i,j}$ supposed to mean $f(i)=j$. Then we create a theory $T$ that contains all the $\neg (P_{i,j} \land P_{i, j'})$ when $j\neq j' \in J$, and $\neg (P_{i,j}\land P_{i',j})$ when $i\neq i' \in I$. This is supposed to mean "$f$ is injective". But obviously this isn't enough (otherwise one could prove that any set injects into another), as we need to express something like "$f(i)$ is defined for any $i\in I$". This is where we use the $J_i$ : we add to the theory the formulas $\displaystyle\bigvee_{j\in J_i} P_{i,j}$ for $i\in I$, which is a well defined formula (up to logical equivalence), as each $J_i$ is finite. Now if $T$ is satisfiable, then we have found our injection : assume $v$ is a model for $T$, then $f:=\{(i,j) \in I\times J\mid v(P_{i,j}) =1\}$ is an injection, whose domain is $I$. Compactness shows it's enough to have $T$ finitely satisfiable, and if $T_0$ is a finite subtheory of $T$, ot is contained in a finite subtheory $T_1$ which expresses (modulo our identification) that a certain finite subset $I_0\subset I$ is injected into $J$ with every $i\in I_0$ being sent into $J_i$. Now unless I'm making a mistake, this is possible, as it only uses the cardinality of bases for finite dimensional spaces, which is true without any sort of choice.
So $T$ is satisfiable, we have our injection, and symmetry + Cantor-Bernstein allow us to conclude
EDIT : I might actually be making a mistake, it's possible that a "Hall's mariage theorem" argument can't be avoided
