Constructive proof of existence of non-separable normed space

AS I said, it depends way to much on your framework to give a definitive answer ! here are some exemples that works in some cases:

Take $E$ to be the free $\mathbb{Q}$-vector space on a set $S$, and define the $\ell^1$ norme on $E$. There are two cases where this is well defined:

1) if one assume that $S$ is a decidable set, in which case you define the norm of $x= \sum x_s e_s$ as $\sum |x_s|$ for a non repeating expression of $x$.

2) If one allows the norm the be an upper dedekind cut (in which case you say that $\Vert x \Vert <q$ if $x$ admit a representation as $\sum x_s e_s$ with $\sum |x_s| < q$.

Let $Y=\{y_1,\dots,y_n \dots \}$ be a countable dense subset of $E$.

I assume dense mean that for all $e \in E$ there exists an $y_i \in Y$ such that $\Vert e - s \Vert <q$.

In particular, for all $s \in S$ you define $Y_s =\{ y \in Y | \Vert y -e_s \Vert< 1/10  \}$

by assumption for each $s$ , $Y_s$ is inhabited ($=\exists x \in Y_s$).

If you are in the case $(1)$ then as norm are rational numbers, the inequality is decidable, hence each $Y_s$ is decidable, and an inhabited decidable subset of $N$ has a smallest elements. Hence you get an injective map from $S$ to $N$. So as soon as you have a decidable set which have no injection to $N$ it solves your problem.

If you allows for case $(2)$, you can take $S =\mathcal{P}(N)$ and you still get a map from $\mathcal{P}(N)$ to $\mathcal{P}(N)$ such if $ \exists x \in f(P) \wedge f(Q) $ then $P = Q$. reversing this gives you a partially defined surjection from $N$ to $\mathcal{P}(N)$ which is impossible by the usual diagonal arguments.

(I'm taking about the partial map which send $n$ to $s$ if $n$ is in one of the $Y_s$, and is not defined otherwise)

Here is a metamathematical approach, using results from Michael Beeson's 1985 Foundations of Constructive Mathematics.

Proposition: If a constructive theory $T$ proves that

• $X$ is a metric space with metric $d$
• $f:R \rightarrow X$

then $T$ proves there is a countable dense set in $f(R)$.

The proposition does not quite prove that $X$ is separable, but it shows that none of the standard examples of non-separability will work. In particular, this covers the examples in Gerald Edgar, Simon Henry, and Pietro Majer's answers.

The constructive theories covered in the proposition include $T=HA^\omega$, or any theory in the language of $IZF$ or Feferman's theories discussed in Beeson's book.

Proof: By composition, $T$ proves that $g(x,y)=d(f(x),f(y))$ is a well-defined function $g: R\times R \rightarrow R$. Then, by Beeson's theorem XVI.4.2.2, $T$ proves that $g$ is a continuous function. Furthermore, because $d$ is a metric, $g(r,r)=0$. So, by continuity, $f(Q)$ is the desired countable dense subset of $f(R)$, and this is provable in $T$. QED.

Example: What about where $X$ is the almost-periodic functions? Is $f(r) = \lambda x\, sin(rx)$ an example of an uncountable separated subset? We can verify that constructive theories prove that $f$ is well-defined. We know that there is no countable dense subset of $f(R)$ according to the $\ell^\infty$ metric. So, by the proposition, a constructive theory can never prove that the $\ell^\infty$ metric is well-defined on $X$.

Discussion (not an answer) ...

What happens if you take a standard proof that $l^\infty$ is not separable, and try to see if it is "constructive" in this weird sense? How do you show something is "not dense" constructively? I guess assuming it is dense and deriving a contradiction is not good. Similarly, how do do show something is "not denumerable"?

So the standard proof that $l^\infty$ is not separable goes like this:

Given a set $A \subseteq \mathbb N$, let $\phi_A \in l^\infty$ be the characteristic functon of $A$: that is, $\phi_A(k) = 1$ if $k \in A$ and $\phi_A(k) = 0$ otherwise.

If $A \ne B$ are two subsets of $\mathbb N$, then $\|\phi_A - \phi_B\| = 1$. There are uncountably many of these sets. Write $\cal U_A$ for the ball with center $\phi_A$ and radius $1/2$. These balls are disjoint: if $A \ne B$ then $\cal U_A \cap \cal U_B = \varnothing$

If $\cal Q \subseteq l^\infty$ is dense in $l^\infty$, then $\cal Q \cap \cal U_A \ne \varnothing$ for all $A$, and therefore $\cal Q$ is uncountable.

So for a "constuctive" proof we would need this: given uncountably many pairwise disjoint sets, and a set $\cal Q$ that meets them all, $\mathcal Q$ is not denumerable. If my guess at the top is right, then we cannot prove this by: assume $\cal Q$ is denumerable, and deduce a contradiction.

added
OK, the word from the OP is that $l^\infty$ is not a normed space, since the sup in the definition of the norm may not exist. Let me guess what this means.

Here is an element of $l^\infty$. It is a function $f : \mathbb N \to \mathbb R$. $$ f(n) = \begin{cases} 1\qquad \text{$n \ge 10$ is even but $n$ is not the sum of two primes}\\ 0\qquad\text{otherwise} \end{cases} $$ So $f$ is a constructive function. For any $n$ it is a finite computation to decide whether Goldbach's conjecture holds for $n$. And certainly $f$ is bounded: $|f(n)| \le 1$ for all $n$. But the norm $\|f\|$ does not exist constructively. The norm is $0$ if Goldbach's conjecture holds, but $1$ if not. Without the law of the excluded middle, we cannot say that $\|f\|$ exists. Right? I am not a "constructive" mathematician, so this is just a guess about what it means.