If a vector space has a basis then its dual vector space has a basis 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\}$.
 A: Here are two statements you might find interesting:

*

*With base field $k\subseteq\mathbb C$ your axiom implies that any free $\mathbb Z$-action has a choice of representatives.

*For each prime $p,$ there is an $\omega$-categorical theory such that the associated permutation model contains a set $X$ with no basis for $\mathbb F_p^X$ - this addresses a suggestion in the comments.

I’ll use ZFA throughout, blithely ignoring the question of whether your axiom implies AC over ZF.

A free $\mathbb Z$-action on a set $X$ is (generated by) a bijection $T:X\to X$ such that $T^ix=x$ implies $i=0.$ Let $k\subseteq \mathbb C.$ Let $X$ be a set such that $k^X$ has a basis $\mathcal B.$ We will show that every free $\mathbb Z$-action on $X$ has a choice of orbit representatives.
Why might this be interesting? It seems like a non-trivial consequence because the conclusion does not directly refer to linear algebra. The conclusion for all $X$ implies the axiom $\omega\zeta\mathrm{AC}$ introduced in [1], Howard-Rubin Form 119, which is equivalent to: every free $\mathbb Z$-action with a countable number of orbits has a set of representatives. It might not seem like a huge amount of strength, but then the evidence you’ve gathered suggests your axiom is quite weak (not pejoratively!), at least over ZFA.
Restricting to a single orbit, we are given a free transitive $\mathbb Z$-action generated by $T:A\to A$ and we want to pick an element of $A,$ uniformly in $(A,T).$
Let $\delta_b\in (k^X)^*$ for $b\in\mathcal B$ be the dual vectors, so every $v\in k^X$ is a unique $k$-linear sum $\sum_{b\in\mathcal B} \delta_b(v) b$ with finitely many non-zero coefficients. Let $[A]$ be the indicator function of $A.$ For each $a\in A$ define $f_a\in k^X$ by $f_a(T^na)=n$ and $f_a(x)=0$ for $x\not\in A.$ Define
$$c(a)=\sum_{b\in \mathcal B} |\delta_b(f_a)|.$$
Then $c(T^na)\to\infty$ as $|n|\to\infty$ for fixed $a,$ because
$$|\delta_b(f_{T^na})| = |\delta_b(f_a) - n\delta_b([A])|\to\infty$$
for any $b$ such that $\delta_b([A])\neq 0.$
The set $C=\operatorname{argmin} c\subset A$ is therefore finite, and we can take the least element in the ordering generated by $a<Ta.$ $\square$

Take the $\omega$-categorical theory to be the Fraïssé limit of the class of bilinear forms $B:X\times \Phi\to \mathbb F_p,$ where $X$ and $\Phi$ are finite-dimensional vectors spaces over $\mathbb F_p.$ These are structures in the language with unary symbols $X,\Phi,\mathbb F_p,$ field operations, two sets of vector space operations, and a binary operation for $B.$ The finite support permutation model $N$ of this structure will therefore contain a bilinear form which I’ll also call $B:X\times\Phi\to\mathbb F_p.$
I’ll need a “unique minimal support” property. Unique support arguments often require a lot of care. To make life as easy as possible I’ve tried to prove only the exact statement that the argument needs. Define an “acl support” to be a pair $(X_0,\Phi_0)$ where $X_0$ is a finite subspace of $X$ and $\Phi_0$ is a finite subspace of $\Phi.$ (“acl” stands for algebraically closed, the same as definably closed here). A set $x\in N$ is “supported by” $(X_0,\Phi_0)$ if every automorphism that fixes $(X_0,\Phi_0)$ elementwise also fixes $x.$
Lemma. Every $f\in \mathbb F_p^X$ in $N$ is supported by
a unique minimal acl support $\operatorname{supp}(f).$
Proof: $f$ is supported by $(X_0,\Phi_0)$ if and only if: $f(x)=f(x’)$ whenever $x$ and $x’$ have the same $1$-type over $(X_0,\Phi_0).$ These $1$-types (extending the partial type of elements of $X$) have an explicit description: there are exactly $|X_0|+|\Phi_0|.$ corresponding to the points of $X_0$ and the $1$-types defined by the formula $$(\bigwedge_{x_0\in X_0}x\neq x_0)\wedge (\bigwedge_{\phi\in\Phi_0}B(x,\phi)=\hat x(\phi))$$ for each $\hat x\in \Phi_0^*.$
Suppose $f$ is supported by both $(X_0,\Phi_0)$ and $(X_1,\Phi_1).$ We will show that $f$ is supported by the intersection of these supports, which clearly implies the Lemma. Consider $x,x’\in X$ with the same $1$-type over $(X_0\cap X_1,\Phi_0\cap \Phi_1)$; we want to show $f(x)=f(x’).$ The case $x\in X_0\cap X_1$ is immediate. If $x\in X_0\setminus X_1$ then we can replace $x$ by $x’’$ where $x’’$ has the same $1$-type over $(X_1,\Phi_1)$ but $x’’\not\in X_0.$ Since $f$ is supported by $(X_1,\Phi_1),$ we know $f(x)=f(x’’).$ So we can reduce to the case $x\not\in X_0\cup X_1,$ and by a similar argument we can reduce to the case $x’\not\in X_0\cup X_1.$
Now pick $x’’\in X\setminus (X_0\cup X_1)$ such that $B(x’’,\phi)=B(x,\phi)$ for all $\phi\in\Phi_0,$ and $B(x’’,\phi)=B(x’,\phi)$ for all $\phi\in\Phi_1.$ Then $f(x)=f(x’’)$ because $f$ is supported by $(X_0,\Phi_0).$ And $f(x’’)=f(x’)$ because $f$ is supported by $(X_1,\Phi_1).$ Therefore $f(x)=f(x’’)$ as required. $\square$
Corollary. If a finite set $\mathcal S\subset\mathbb F_p^X$ is supported by $(X_0,\Phi_0),$ then every element of $\mathcal S$ is supported by $(X_0,\Phi_0).$
Proof. Let $Z=\bigcup_{f\in\mathcal S} \operatorname{supp}(f).$ Then $Z$ is a finite subset of $X\cup \Phi$ supported by $(X_0,\Phi_0).$ Suppose for contradiction that there exists $z\in Z\setminus (X_0\cup \Phi_0).$ There are infinitely many $z’$ with the same $1$-type as $z$ over $(X_0,\Phi_0).$ So we can find an automorphism fixing $(X_0,\Phi_0)$ elementwise but sending $z$ to some $z’\not\in Z,$ a contradiction. $\square$
Suppose for contradiction that $N$ has a basis $\mathcal B$ of $\mathbb F_p^X.$ Work in the full universe of ZFCA. $\mathcal B$ is supported by some $(X_0,\Phi_0),$ which can be taken to be vector subspaces but are not assumed minimal or unique in any sense.
Pick two elements of $\Phi$ that map to linearly independent vectors in $\Phi/\Phi_0.$ Their span $\Phi_1$ has dimension $2.$ Let $L$ be the set of $p+1$ one-dimensional subspaces of $\Phi_1.$ Each $\ell\in L$ determines a function $f_{\ell}\in \mathbb F_p^X$:

*

*$f_{\ell}(x)=0$ if $B(x,\phi)=0$ for all $\phi\in \ell$

*$f_{\ell}(x)=1$ otherwise

For any $x\in X$ the kernel $\{\phi\in\Phi_1: B(x,\phi)=0\}$ either has dimension $1,$ in which case $f_\ell(x)=0$ for exactly one $\ell,$ or has dimension $2,$ in which case $f_\ell(x)=0$ for all $\ell.$ Thus
$$\sum f_\ell = 0.$$
Let $F_0\subset \mathbb F_p^X$ denote the space of functions that are supported by $(X_0,\Phi_0).$ Let $F_\ell$ denote the space of functions that are supported by $(X_0,\operatorname{span}(\Phi_0\cup \ell)).$ Then $F_\ell\cap F_{\ell’}=F_0$ for distinct $\ell,\ell’$ - consider the unique minimal acl support of functions in $F_\ell\cap F_{\ell’}.$
Let $\delta_b(f_\ell)$ denote the coefficient of the basis function $b\in\mathcal B$ when expanding $f_\ell$ in the basis $\mathcal B.$ $f_\ell$ is not in the span of $F_0,$ because it is possible to find $x,x’$ satisfying $f_\ell(x)=0$ and $f_\ell(x’)=1$ with the same $1$-type over $(X_0,\Phi_0),$ specifically $x,x’\not\in X_0$ and $B(x,\phi)=B(x’,\phi)=0$ for all $\phi\in\Phi_0.$ By the Corollary applied to the set $\{b:\delta_b(f_\ell)\neq 0\},$ every $b$ with $\delta_b(f_\ell)\neq 0$ lies in $F_\ell.$ Pick any $\ell$ and $b\in F_\ell\setminus F_0$ with $\delta_b(F_\ell)\neq 0.$ For $\ell’\neq\ell,$ we have $b\not\in F_{\ell’}$ and hence $\delta_b(f_{\ell’})=0.$ We can finally state the contradiction to the assumption of a basis of $\mathbb F_p^X$:
$$0\neq \delta_b(f_\ell)=\delta_b(\sum_{\ell’} f_{\ell’}) = 0.$$

[1] van Douwen, Eric K., Horrors of topology without AC: A nonnormal orderable space, Proc. Am. Math. Soc. 95, 101-105 (1985). ZBL0574.03039.
