Let $V$ denote the vector space of sequences of real numbers that are eventually 0, and let $W$ denote the vector space of sequences of real numbers. Given $w \in W$ and $v \in V$, we can take their "dot product" $w \cdot v$, and for any give $w \in W$, this defines a linear functional $V \to \mathbb{R}$. In fact, under this association, we see that $W \cong V^{\ast}$. Assuming choice, $W$ has a basis and has uncountable dimension, whereas $V$ has countable dimension. So $\mathrm{dim} (V) < \mathrm{dim} (V^{\ast}) \leq \dim(V^{\ast \ast})$ so $V$ is not isomorphic to its double-dual. In particular, the canonical map $\widehat{\cdot} : V \to V^{\ast \ast}$ defined by $\widehat{x} (f) = f(x)$ is not an isomorphism.

**Question 1**: Can you explicitly write down an element of $V^{\ast \ast}$ that isn't of the form $\widehat{x}$?

**Question 2**: What's the situation if we don't assume choice? (i.e. might the canonical map be an isomorphism, might $W$ not even have a basis, might $V$ be isomorphic to its double-dual but not via the canonical map, etc?)

In light of Daniel's and Yemon's comments, and Konrad's related question here, I'd like to reorganize my question(s). So consider the following statements:

- The canonical map $\widehat{\cdot} : V \to V^{\ast \ast}$ is injective but not surjective.
- The canonical map is not an isomorphism.
- There is no isomorphism from $V$ to its double-dual.
- The double-dual is non-trivial.
- $V^{\ast}$ has a basis.

This is the question I'm really interested in, and which clarifies and makes more precise my original Question 1:

**Revised Question 1**: Are there models without choice where (1) holds? If so, can we find some $x \in V^{\ast \ast}$ witnessing non-surjectivity to describe a witness to non-surjectivity in choice models? Are there models of choice where (1) fails?

The following question is a more precise version of Question 2.

**Revised Question 2**: Under AC, all 5 statements above are true. There are $2^5 = 32$ ways to assign true-false values to the 5 sentences above that might hold in some model of ZF where choice fails. Not all 32 are legitimate possibilites, some of them are incompatible with ZF since, for instance, (1) implies (2), (5) implies (4), and the negation of (4) implies (1) through (3), etc. Which of the legitimate possibilites actually obtains in some model of ZF where choice fails?

This second question is rather broad, and breaks down into something on the order of 32 cases, so seeing an answer to any one of the legitimate cases would be cool.