Constructive proof of existence of non-separable normed space

Question

I am looking for a constructive proof of one of the following two statements. If they are not constructively provable, I would be very thankful for an explanation as to why that is so (i.e., at which point in a proof must non-constructive means be employed?).

1. There exists a normed space X such that for all Y $\subset$ X, if Y is denumerable, then Y is not dense in X.

2. There exists a normed space X such that for all Y $\subset$ X, if Y is dense in X, then Y is not denumerable.

I'd consider a proof constructive if it includes no applications of the:

• Law of Excluded Middle: $\phi$ $\lor$ $\neg$$\phi$
• Law of Double Negation Elimination: $\neg$$\neg$$\phi$ $\rightarrow$ $\phi$
• Axiom of Choice or any of its equivalents (Zorn's Lemma, etc.).

Suggestions would be much appreciated.

Answer 1

Andrew Swan and I proved that in the function realizability topos every metric space is separable (and that every object with decidable equality is countable). Therefore, it is not possible to prove constructively that a non-separable metric space exists. This result strengthens the answer by Matt Frank.

The note is available as arxiv 1804.00427.

Answer 2

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)

Answer 3

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

Answer 4

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.

Answer 5

Neither 1. nor 2. is provable constructively, in my not so humble opinion. To answer your question completely, let me explain the reason for this which goes back to the fundamental research of Brouwer, around 1910 (say) when he started constructive mathematics.

In constructive mathematics [at least in its pure original form] we stipulate that we only work with objects, concepts,... that we can construct in our mind, given potentially infinite time.

At any given time however, we can only have finished a finite number of finite constructions.

So anything that we work with, starts with the natural numbers 0, 1, 2,... and $\mathbb{N}$ is what we call the never-ending and ever-unfinished construction of these natural numbers.

Since $\mathbb{N}^*$, the collection of finite sequences of natural numbers, is countable, we can also start constructing elements of Baire space $\mathbb{N}^{\mathbb{N}}$. But each element of $\mathbb{N}^{\mathbb{N}}$ is as much work as $\mathbb{N}$ itself, and never finished.

From this, thinking it through, we see that we can never really construct any entities that are not based in some way on Baire space (as elements of a subset of Baire space). That means that if we have a constructive effectively calculable norm, it is based in some way on Baire space topology, and that implies that the space is separable.

To construct the space of all bounded real sequences $'l^{\infty}$, we can use a different norm than the sup-norm. But with this norm $'l^{\infty}$ becomes separable. We can still define the sup-norm, but we cannot always calculate it, and this implies that we cannot really work with it constructively to arrive at a meaningful non-separable space.

It is worth mentioning that Brouwer's analysis of how far we can reach constructively is impopular in contemporary constructive math. This is perhaps due to the necessity of competing with the classical math community, where not even the sky is the limit. One might then get the (not always accurate) impression that we think Baire space is too easy, too limited, for our light-speed brains...

Answer 6

I will not check any detail, but in general for these matters I would go for $X:=\ell_2(S)$ (because all constructions are the most constructible, due to the existence of orthogonal projectors etc), with an uncountable set $S$. (So $u\in\ell_2(S)$ means $u:S\to\mathbb{R}$ is a function with $\sum_{s\in S} |u(s)|^2<\infty$). Since any $u\in \ell_2(S)$ has a countable support $\operatorname{supp}(u):=\{s\in S: u(s)\neq0\}$, any countable subset $Q\subset \ell_2(S)$ in fact belongs to the closed subspace $ \ell_2(D)\subsetneq\ell_2(S)$ for the countable subset $D:=\cup_{u\in Q}\operatorname{supp}(u)\subsetneq S$.

Answer 7

An answer to Q1. The Cantor's tune.

Let $\ \mathbb N:=\{1\ 2\ \ldots\}\ $ be the set of natural numbers. Let $\ C\ $ be the space of all bounded sequences:

$$ C\ :=\ \{a\in \mathbb R^\mathbb N : \exists_{\beta\in\mathbb R} \forall_{n\in\mathbb N}\,\ |a_n|<\beta \} $$

Let the norm in $\ C\ $ be the uniform norm $\ sup.$

Consider an arbitrary sequence $\ f:\mathbb N\rightarrow C.\ $ We will see that (the image $\ Y\ $ of) this sequence is not dense in $\ C.\ $ Indeed:

Let $\ \gamma_n := -1\ $ if $\ (f(n))_n \ge 0\;\ $ and let $\ \gamma_n := 1\ $ if $\ (f(n))_n < 0. $ The the distance from $\ \gamma\ $ to any term $\ f(n)\ $ is equal at least $\ 1;\ $ indeed, $\ |(f(n))_n - \gamma_n |\ge 1\ $ for every $\ n\in\mathbb N$.

REMARK: $\ $ I am not (sufficiently) logically trained or competent but I feel that this proof, in my opinion, is about as constructive as it gets.

---

---

A general comment: The usage of the axiom of choice (and it's equivalent versions) in algebra is ubiquitous. But this applies mainly to the general theorems. Indeed, the concrete algebraic examples utilize specific (concrete, constructive) choices of the needed objects most of the time. This tells us that we need a relative notion of constructive PROOFS more than an absolute version -- so that the constructive proofs applied to their constructive foundations define the constructive total results. In general, a full mathematical theory is a path of the form:

$\qquad\ \qquad\ $ finite data $\ \Rightarrow\ $ infinity $\ \Rightarrow\ $ finite data

In this sense, a full mathematical theory is constructive. It follows that several mathematical theories are only a useful stage of a full theory while on their own they are not full. Such a theory, by definition, is the functional analysis. A full theory could be the whole path:

$\qquad\ \qquad\ $ hard analysis $\ \Rightarrow\ $ functional analysis $\ \Rightarrow\ $ hard analysis

The intermediate stage of a full theory is not constructive but it may take advantage of the relatively constructive proofs.

PS. There is, of course, a difference between OP's Q1 and Q2; and an under 2h difference between the timing of thread's answers is not crucial at all (for all kind of reasons).