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.


1. 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$


2. 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.


3. 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\}$.



If a vector space has a basis then its dual vector space has a basis
Here are two statements you might find interesting:


1. With base field $k\subseteq\mathbb C$ your axiom implies that any free $\mathbb Z$-action has a choice of representatives.
2. 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**](http://dx.doi.org/10.2307/2045582), Proc. Am. Math. Soc. 95, 101-105 (1985). [ZBL0574.03039](https://zbmath.org/?q=an:0574.03039).


