Consider the following statement:

**If a vector space has a basis then its dual vector space also has a basis.**

It is not an axiom of ZF. It clearly follows from the Axiom of Choice. But it is also strictly weaker than the Axiom of Choice.

I have convinced myself that this statement holds in a variety of models of set theory with atoms (e.g. it holds in the first Fraenkel-Mostowski model, in the second Fraenkel-Mostowski model, in the ordered Fraenkel-Mostowski model, etc.).

I am wondering:

**What is the strength of the above statement?**

I am also interested in any reasonable variant of the question --- e.g. what if we restrict to a particular field $\mathbf{K}$? In case $\mathbf{K} = 2$, the statement can be rephrased as:

*For any set $A$ the vector space $\mathcal{P}(A)$ has a basis.*

Can the general statement be reduced to this special one over two-element field $2$?

Let us work out some examples in ZFA. For simplicity, I shall assume that our vector spaces are over the field of real numbers.

- Let $A$ be the set of all atoms in the first Fraenkel-Mostowski model. Then the vector space $\mathbb{R}^A$ consists of all symmetric functions $f \colon A \rightarrow \mathbb{R}$. Let us assume that the support of $f$ is $A_0$. Then $f$ has to be constant on $A \setminus A_0$ and arbitrary on $A_0$. Therefore, the set of vectors: $$\{1, a_1^*, a_2^*, \cdots \} \approx A \sqcup 1$$ where:

- 1 is the constant function, i.e. $1(a)=1$
- $a^*$ is the characteristic function, i.e. $a^*(b) = [a = b]$

is a basis for $\mathbb{R}^A$

- Let $Z_*$ be the set of all atoms in the second Fraenkel-Mostowski model (thought of as non-zero integer numbers with symmetry given as multiplication by $-1$). A symmetric function $f \colon Z_* \rightarrow \mathbb{R}$ must satisfy $f(-n) = f(n)$ for all but finitely many $n$. Let us consider
*classical*(i.e.~in the real world) vector space $\mathbb{R}^{\mathcal{N}_*}$, where $\mathcal{N}_*$ is the set of*positive*natural numbers. Let us consider standard vectors $e_1, e_2, \cdots$ and extend them (in any way) to a basis of $\mathbb{R}^{\mathcal{N}_*}$. Let us denote the set of these additional vectors by $\Lambda$, i.e. $\{e_1, e_2, \cdots\} \cup \Lambda$ is a basis for $\mathbb{R}^{\mathcal{N}_*}$. For every vector $\lambda \in \Lambda$ define a symmetric function $\overline{\lambda} \colon Z_* \rightarrow \mathbb{R}$ as follows: $$\overline{\lambda}(z) = \lambda(|z|)$$ I claim that the set of vectors: $$\{\overline{\lambda} \colon \lambda \in \Lambda\} \cup \{z^* \colon z \in Z_*\} \approx \Lambda \sqcup Z_*$$ forms a basis for $\mathbb{R}^{Z_*}$ Indeed, it is clear that this set generates $\mathbb{R}^{Z_*}$. To see that the vectors are linearly independent consider the following two cases:

$\overline{\lambda} = \sum_{i=1}^k a_i\overline{\lambda_i} + \sum_{i=1}^l b_i z^*_i$ where all vectors are distinct. In particular, this implies that: $$\overline{\lambda}(n) = \sum_{i=1}^k a_i\overline{\lambda_i}(n) + \sum_{i=1}^l b_i z^*_i(n)$$ for every positive natural number $n$. But this reduces to: $$\lambda(n) = \sum_{i=1}^k a_i \lambda_i(n) + \sum_{i=1}^l b_i e_{z_i}(n)$$ where $e_{z_i} \equiv 0$ if $z_i < 0$. But this leads to the contradiction with the assumption that $\{e_1, e_2, \cdots\} \cup \Lambda$ are linearly independent.

$z^* = \sum_{i=1}^k a_i\overline{\lambda_i} + \sum_{i=1}^l b_i z^*_i$ where all vectors are distinct and $z < 0$ (the case $z> 0$ is symmetric). In particular, this implies that: $$z^*(-n) = \sum_{i=1}^k a_i\overline{\lambda_i}(-n) + \sum_{i=1}^l b_i z^*_i(-n)$$ for every positive natural number $n$. This reduces to: $$e_{-z}(n) = \sum_{i=1}^k a_i \lambda_i(n) + \sum_{i=1}^l b_i e_{-z_i}(n)$$ This leads to the contradiction with the assumption that $\{e_1, e_2, \cdots\} \cup \Lambda$ are linearly independent.

- Let $Q$ be the set of all atoms in the ordered Fraenkel-Mostowski model. Consider a symmetric function $f \colon Q \rightarrow \mathbb{R}$. Then there is a finite decomposition $Q = I_1 \sqcup I_2 \sqcup \cdots I_n$ on intervals $I_k$, such that $f$ is constant on each $I_k$. Therefore, the set of vectors: $$\{1, p_1^*, p_2^*, \cdots, p_1^{<}, p_2^{<}, \cdots \} \approx Q \sqcup Q \sqcup 1$$ where:

- 1 is the constant function, i.e. $1(a)=1$
- $p^*$ is the characteristic function, i.e. $p^*(q) = [p = q]$
- $p^{<}$ is the open down set of $p$, i.e. $p^{<}(q) = [p > q]$

generates $\mathbb{R}^Q$. Moreover, these vectors are linearly independent: if $S$ is any non-empty finite set of the above vectors, then there exists vector $m \in S$ and an atom $p$ with $m(p) = 1$ such that for every $s \in S \setminus \{m\}$ we have that $s(p) = 0$, so $m$ cannot be a linear combination of $S \setminus \{m\}$.

6more comments