9
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ In the question I linked you on math.se, the top answer, provided all the required ingredients for a "constructive" proof that the space of bounded continuous functions on $\mathbb R$ is not separable. $\endgroup$
    – Not Mike
    Mar 9, 2018 at 13:52
  • $\begingroup$ E. Bishop, Foundations of constructive analysis seems to have a chapter on normed linear spaces. So maybe that is a place to look for your answer. $\endgroup$ Mar 9, 2018 at 15:08
  • 3
    $\begingroup$ @ludwigmach : you really need to clarify the background you are using ! What do you call a normed space constructively, what do you call dense, what do you call countable, are you assuming countable choice etc... there are hundreds of possibilities for these choice constructively. $\endgroup$ Mar 9, 2018 at 17:03
  • 3
    $\begingroup$ Also your question $1$ and $2$ are completely equivalent: constructively $A \Rightarrow \neg B$ and $B \Rightarrow \neg A$ are equivalent and equal to $\neg (A \wedge B)$, unless "uncountable" mean something else that "not countable" $\endgroup$ Mar 9, 2018 at 17:24
  • 1
    $\begingroup$ If you assume countable choice then this reduces some of the problems. But there are lots of variation : what definition of reals number are you using for the values of the norm ? Dense can be interpreted either in the $\forall / \exists$ sense, as the existence of a sequence or as the existence of sequences with prescribed convergence rates. Countable, can mean: having a surjection from N, being in bijection with N, being in bijection with a decidable subset of N, having a monomorphisms to N, being an N indexed union of finite sets, (with all the possible meaning of finite ! ) etc... $\endgroup$ Mar 10, 2018 at 10:49

7 Answers 7

3
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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)

$\endgroup$
1
  • $\begingroup$ For the record, if you do not allow for norm with value in Dedekind cuts, it might not be possible, or at least not easy to produce an example: 1) One cannot always construct large decidable objects, as far as I know it s completely possible that the only decidable objects are subsets of $N$. 2) It is very hard to construct examples of Normed space with continuous norm (read, whose norm takes values in real numbers) which does not contains large (dense) decidable subset (I have never seen such an example). The problem is that a continuous norm "almost" allows to distinguishes elements. $\endgroup$ Mar 9, 2018 at 22:53
4
$\begingroup$

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

$\endgroup$
4
  • 1
    $\begingroup$ Interesting. Although, I don't see how it contradicts anythings I said in my answer ! In both case there is no natural functions $f:R \rightarrow X$ that you could use, especially in case $(1)$ where because of the decidability of S, any continous function from $R$ to $S$ would be constant. In case (2) you have the additional problem that you don't even have an actual metrics functions. $\endgroup$ Mar 10, 2018 at 23:19
  • $\begingroup$ @SimonHenry, it was not intended to contradict your answer! Instead, it is another way of showing that you can not take S=R as a basis set for a Q-vector space on which a reasonable $ell^\infty$ norm is defined. $\endgroup$
    – user44143
    Mar 10, 2018 at 23:34
  • $\begingroup$ @Matt: Thank you, this is very helpful. $\endgroup$
    – ludwigmach
    Mar 11, 2018 at 12:53
  • 1
    $\begingroup$ This is just to draw your attention to my answer below which constructs a model in which all metric spaces are separable. $\endgroup$ Apr 3, 2018 at 11:52
3
$\begingroup$

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.

$\endgroup$
15
  • 5
    $\begingroup$ Without the law of excluded middle, you can prove the negation of a statement by showing the original statement leads to an absurdity. What you cannot do, is prove the statement is true by showing its negation produces a contradiction. (In fact the outline you give is precisely what is shown in the top answer to the question I referred OP to on math.se) $\endgroup$
    – Not Mike
    Mar 9, 2018 at 13:35
  • $\begingroup$ This is relevant, since it implies you can show that $\cal Q$ fails to be denumerable, by standard means. $\endgroup$
    – Not Mike
    Mar 9, 2018 at 13:39
  • $\begingroup$ Thank you for your comment. However, constructively, $l^\infty$ is not a normed space because the supremum norm $||(x_n)|| = sup|x_n|$ does not exist. $\endgroup$
    – ludwigmach
    Mar 9, 2018 at 14:07
  • 1
    $\begingroup$ To echo what I think is @NotMike's point, in what sense does the supremum norm not exist constructively? $\endgroup$
    – LSpice
    Mar 9, 2018 at 14:49
  • 3
    $\begingroup$ @ludwigmach : it is very common when talking of normed space constructively to define the norm as a function taking value in upper dedekind cut, in which case $l^{\infty}$ is well defined. $\endgroup$ Mar 9, 2018 at 17:02
1
$\begingroup$

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

$\endgroup$
8
  • $\begingroup$ While I agree with you that it might not be possible to construct an example in any constructive framework. My answer shows that at least if we allows "norms" to be defined not as a real number but as a dedeking cut (or equivalently, if one only specify a collection of $B(0,r)$ for $r$ a rational numbers satisfying some natural axioms) then one can produces an example of non separable normed space. You argument does not really excluded this exemple, unless you do not accept that $N^N$ or $\mathcal{P}(N)$ are sets. But then this is not constructivism: its predicativisms. $\endgroup$ Mar 10, 2018 at 14:38
  • $\begingroup$ (And you also have to refuse to consider $\mathbb{R}$ a set in this case) $\endgroup$ Mar 10, 2018 at 14:39
  • $\begingroup$ Simon, your suggestion is certainly interesting. My answer concerns the usual definition of "norm", which is how I read the question. For clarity, I also think that the usual definition of "norm" is highly useful and I would not weaken it in order to be able to call something non-separable. Nonetheless, it seems worthwhile to study alternative broader concepts of "norm" if that helps us to incorporate more of classical math's wealth into constructive math. $\endgroup$ Mar 10, 2018 at 14:55
  • $\begingroup$ Also, imnsho, predicativism is an important part of constructive mathematics (at least in its pure form, which I differentiate from `constructivism'). $\endgroup$ Mar 10, 2018 at 14:57
  • 1
    $\begingroup$ hum I see. that is interesting, and even potentially formalisable. regarding dedekind cut, The idea is that you never need to compute or approximate a norm precesely, the only interesting things about the norm in order to do analysis is being able to say that $\Vert x - y \Vert < \epsilon $, you don't care about "downward approximation", which is what an upper dedekind cut is for. $\endgroup$ Mar 10, 2018 at 15:11
0
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ I'm affraid You are using the law of excluded middle and countable choice all over the place : $\ell_2(S)$ might not even exists constructively if you don't assume $S$ to be decidable. and, you are never going to be able to prove constructively that the support is countable. $\endgroup$ Mar 9, 2018 at 17:08
  • $\begingroup$ OK, of course that was just a hint, to try do make in a constructive context. $\endgroup$ Mar 9, 2018 at 18:46
-3
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ i downvoted this answer because it does not address the question, and also because the problem with this very answer was already discussed above... $\endgroup$ Mar 10, 2018 at 16:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.