Non-separable normed spaces

[Andrej Bauer]

Dear all,

the question at

https://mathoverflow.net/questions/294746/constructive-proof-of-existence-of-non-separable-normed-space

asks for a constructive example of a non-separable normed vector
space. There isn't a definitive answer yet, so I am drawing your
attention to the question. I tihnk it's interesting, and it has likely
been considered before.

Is there a constructive example of a non-separable normed space? A
non-separable complete metric space, perhaps?

If I can get my hands on a non-countable set S with decidable equality
then I could use it to define a normed vector space with basis S, or
just a complete metric on S, but it seems like there might not be any
decidable non-countale sets.

What is known about these questions? Is any of the following known to
be a constructive taboo:

1 A non-separable complete metric space.
2. A non-separable normed vector space.
3. A non-countable set with decidable equality.

Regarding 3: in the effective topos there is a subset of N which is
neither finite nor does it contain an infinite sequence (recursion
theory calls such sets "immune"), so it is certainly possible to have
3 without having excluded middle. However, the effective topos brings
in its own bag of problems (Markov principle for instance).

With kind regards,

Andrej

[Andrew Swan]

For question 3, in function realizability every set with decidable equality is not uncountable, so there's no constructive proof of the existence of an uncountable set with decidable equality.

Best,

Andrew

[Andrew Swan]

Actually, on further thought function realizability probably works for the other two questions as well.

We know that any metric space is \neg \neg-separated because if \neg \neg (x = y), then \neg \neg d(x, y) = 0, but R is \neg \neg-separated, so d(x, y) = 0 and then x = y. Hence, working in the function realizabilty topos, the underlying object of any metric space has to be an assembly. Using the same trick again, it in fact has to be a modest object. But surely this implies that it is separable?

Best,

Andrew

[Henri Lombardi]

Dear all

Is there a known constructive proof in Bishop’s style of the Riemann existence theorem ?
On a compact Riemann surface, meromorphic functions exist and separate points.
See https://www.math.upenn.edu/~harbater/RETppr.pdf

Henri LOMBARDI
e mail : Henri.L...@univ-fcomte.fr
page web http://hlombardi.free.fr/

[Steve Vickers]

Dear Andrej,

For a non-countable set with decidable equality, is a generic set in a
classifying topos any help to you?

The classifying topos for sets with decidable equality is the topos of
covariant functors from Fin_m to Set, where Fin_m is the category of
finite cardinals and monic functions between them. The generic set with
decidable equality is the tautologous functor S: n |-> n. The nno N is
the constant functor n |-> N. If S is [sub]countable, then there should
be a surjection from N to 1+S, and clearly there isn't.

Steve.

[Kreinovich, Vladik]

There was a paper by Maurice Margenstern on constructive theory of almost periodic functions, a non-separable space introduced long ago by Harald Bohr, a brother of the famous physicist Niels Bohr. If I remember correctly, this paper contained the main results from his PhD dissertation, I am sending him a copy of this email. The paper was called "On constructive functionals on the space of almost periodic functions.", it was published in 1974 in Zapiski Nauchn. Seminarov LOMI in Russian, vol. 40, pp. 45-62, there was an English translation.

He later published a paper Maurice Margenstern:
On a Variant of Constructivisation of the Theory of Almost Periodic Functions. Math. Log. Q. 24(31-36): 495-507 (1978)

Googling on "margenstern almost periodic functions" finds some more references, including Bas Spitters's 2005 arXiv paper https://arxiv.org/pdf/cs/0512009.pdf

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Bas Spitters]

Thanks. What I do in that paper (def 2), following Bishop, is to use
quasinormed spaces.
Instead of a norm, one takes a collection || ||_i of them.
Classically, one would obtain a norm by taking their supremum.
This sup would be a generalized real number in the sense of Richman.

[Martin Escardo]

I am changing the subject of this thread, focusing on the following:

On 12/03/18 10:18, Andrew Swan wrote:
> For question 3, in function realizability every set with decidable
equality is not uncountable, so there's no constructive proof of the
existence of an uncountable set with decidable equality.

I've been wondering for a while about that.

Where can I find a proof of this? And what logical systems does it
apply to?

In the following discussion, what I say makes sense in topos logic and
also in univalent type theory (and I am sure in many other systems).
(And I have implemented the arguments in Agda.)

Here are some examples where this matters.

(1) Let N' be the set of decreasing binary sequences.

We have an embedding e:N->N' that maps the natural number n to the
sequence of n ones followed by infinitely many zeros. The complement
of this embedding is a point, namely the sequence of infinitely many
ones (the point at infinity).

However, you can't say that every element of N' is either in the image
of the embedding e or else the point at infinity. This is precisely
WLPO.

Now you can prove (without assuming continuity axioms) that for every
p:N'->2, either p(x)=0 for some x:N' or else p(x)=1 for all x:N'. That
is, p either has a root or it doesn't. (Here 2 is the discrete set
with points 0 and 1.)

Using this, you can show directly that the set of all functions N'->2
is discrete.

Is this set (N'->2) countable? Well: with continuity axioms,
yes. There are "only" countably many continuous functions N'->2. With
excluded middle instead, no. There are uncountably many functions
N'->2 (using Cantor's argument). Because we are not assuming
continuity axioms or excluded middle, the countability of (N'->2) is
undecided.

The set (N'->2) is "not" countable in the meta-mathematical sense that
it can't be proved countable (because it may not be).

(2) Similarly, let Omega be the set of truth values (or the powerset
of a singleton set if you prefer).

Then again you can prove that for all p:Omega->2, either p(x)=0 for
some x:Omega or else p(x)=1 for all Omega. (Without knowing whether
excluded middle holds or not.)

And so again the function space (Omega->2) is discrete.

Is it countable? You can entertain yourself performing a similar
reasoning and getting different answers (but considering axioms for
Omega of a different nature than continuity axioms).

(3) I am not sure countability is the right notion from the
constructive point of view (except in a restricted number of
applications). Almost all sets that are classically countable are
"not" constructively countable, where "not" means that they can be
proved to be countable, rather than that they can be proved to be not
countable.

For example (as in (1)), the set N' is "not" countable. But (again as in
(1)) it does have a countable subset with empty complement.

Most cardinality questions are undecided if excluded middle is left
undecided, and have a different answer than in classical mathematics
if excluded middle is negated by assuming e.g. continuity axioms.

This applies to countability in particular.

Best,
Martin

[Martin Escardo]

Errata and addenda:

On 12/03/18 20:41, Martin Escardo wrote:
> (1) Let N' be the set of decreasing binary sequences.
>
> We have an embedding e:N->N' that maps the natural number n to the
> sequence of n ones followed by infinitely many zeros. The complement
> of this embedding is a point, namely the sequence of infinitely many
> ones (the point at infinity).
>
> However, you can't say that every element of N' is either in the image
> of the embedding e or else the point at infinity. This is precisely
> WLPO.

LPO.

> For example (as in (1)), the set N' is "not" countable. But (again as in
> (1)) it does have a countable subset with empty complement.

On the other hand, the set (N'->2) does "not" have a countable subset
with empty complement, even though it "may" be countable (with
continuity axioms).

M.

[Andrew Swan]

I don't know anywhere that it's written up, so I'll give a sketch proof below. I believe the proof applies to topos theory, set theory and extensional type theory. First to clarify, what I'm claiming is that it is not provable constructively that there is a set both uncountable and with decidable equality, and that the reason is that there is a model (function realizability) where every set with decidable equality is not not countable. This doesn't contradict the examples you gave, because they are countable in function realizability, and so not provably uncountable (even though in general constructive mathematics they are also not provably countable). A way to see this directly for the first example is that Brouwerian continuity principles apply in function realizabilty.

For set theoretic description of the model see Rathjen, Constructive Set Theory and Brouwerian Principles. The topos theoretic version is the realizability topos over the second Kleene algebra. It's mentioned in Van Oosten, Realizability: An Introduction to its Categorical Side (in example 1.4.3), and it appears a lot in Andrej's PhD thesis.

There are certain objects in the function realizability topos (referred to as modest), where we can view them as quotients of subspaces of Baire space, and morphisms between such objects are precisely those that are "tracked" by continuous maps between the corresponding subspaces of Baire space. One can show that every object with decidable equality is modest, and moreover, there has to be a continuous map e: X * X -> 2 where X is the subspace of Baire space (such that the object we are given is X/~ for some ~), and e(x, y) = 1 precisely if x and y are identified in the quotient.

Using the continuous map e: X * X -> 2, we partition the space X into disjoint clopen sets. However, this implies that there are only countably many set in the partition. The only proofs I know of this are nonconstructive. For each set Y in the partition choose a finite sequence s(Y) of natural numbers such that every infinite sequence in X that extends s(Y) belongs to Y (at least one such sequence exists since Y is open). There are countably many finite sequences of natural numbers, so this gives an injection from sets in the partition to N.

Hence, working externally there is a function f: N -> X that hits every equivalence class. However, this in fact also gives us a morphism N -> X, in the topos, essentially because N is discrete, and so any such map is continuous.

Furthermore, the inverse is also continuous, because given x \in X, we can use decidability again to search through N until we find an n such that f(n) = x. Hence, the object is also countable internally.

Finally, a technical point. I claimed not not countable rather than countable, because in order to get the universal quantifier and the implication to work in "*every* set with decidable equality is countable" it's necessary to show that f and its inverse can be constructed in a "uniformly computably" way, which I didn't do. But we can still show the double negated version without doing that.

Best,

Andrew

[robertl...@att.net]

Depending on what you mean by non-countable, this may or may not be relevant. Under number realizability, K_1, every set with decidable equality is sub-countable (bijectible with a subset of the naturals).

Bob

-----Original Message-----
From: construc...@googlegroups.com <construc...@googlegroups.com> On Behalf Of Andrej Bauer
Sent: Monday, March 12, 2018 5:21 AM
To: constructivenews <construc...@googlegroups.com>
Subject: Non-separable normed spaces

[Martin Escardo]

Thanks for the nice answer, Andrew.

Now I know I should stop looking for an uncountable discrete set.

(I wasn't doubting what you said or trying to imply a contradiction. I
was just saying that, with excluded middle left undecided, many
cardinalities are left undecided.)

Best,
Martin

On 13/03/18 11:34, Andrew Swan wrote:
> I don't know anywhere that it's written up, so I'll give a sketch proof
> below. I believe the proof applies to topos theory, set theory and
> extensional type theory. First to clarify, what I'm claiming is that it
> is not provable constructively that there is a set both uncountable and
> with decidable equality, and that the reason is that there is a model
> (function realizability) where every set with decidable equality is not
> not countable. This doesn't contradict the examples you gave, because
> they are countable in function realizability, and so not provably
> uncountable (even though in general constructive mathematics they are
> also not provably countable). A way to see this directly for the first
> example is that Brouwerian continuity principles apply in function
> realizabilty.
>
> For set theoretic description of the model see Rathjen, Constructive Set
> Theory and Brouwerian Principles

> <http://www1.maths.leeds.ac.uk/~rathjen/jucs_douglasO.pdf>. The topos

> --
> You received this message because you are subscribed to the Google
> Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to constructivene...@googlegroups.com

> <mailto:constructivene...@googlegroups.com>.

[Bas Spitters]

I haven't read Andrew's argument in detail, but perhaps it is related
to the intuitionistic proof of the continuum hypothesis.
The principles used there hold in Kleene-Vesley realizability.
There has been some further development along these lines. However, I
don't have access to these notes.
Perhaps Frank Waaldijk knows more.
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/continuum-hypothesis-in-intuitionism/96D8EC6DD445B790ACD12C4711DDA9B8

> email to constructivene...@googlegroups.com.

[Bas Spitters]

A small correction: quasinormed spaces were introduced not by Bishop,
but by David Johns, in his Liverpool PhD thesis around 1970; see
Bishop&Bridges.

[Frank Waaldijk]

Thanks Bas for your confidence [unfortunately misplaced here as i know very little about further developments :-)]. The person to ask this to is Wim Veldman...

The theorem and proof argument given in §2 of the Gielen-Veldman paper that you mentioned does seem to bear close resemblance to Andrew's account. So that might be of interest to study closer. For the proof, use is made of the continuous choice axiom AC_11. 

By the way, I had already answered the question on mathoverflow when Andrej reposted it here... and a similar metamathematical consideration led me to the conclusion that an uncountable decidable set cannot be proved to exist constructively. But as, at least in my fragile ego's eyes, my metamathematical arguments seem seldom appreciated ;-) I decided not to bother to repeat them here...

best wishes to all! frank

---

frank waaldijk
visual artist
www.fwaaldijk.nl
fwaaldijk.blogspot.com

 

>> email to constructivenews+unsubscribe@googlegroups.com
>> <mailto:constructivenews+unsub...@googlegroups.com>.

>> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to constructivenews+unsubscribe@googlegroups.com.

[frank waaldijk]

I haven't looked at it closely, but I would immediately suspect that for the spaces that I deem constructible, the quasinorm topology is the same as the apartness topology (either in INT or in NToP). If so, perhaps it could be interesting to investigate whether using the apartness topology is easier/harder/comparable?

I'm also expecting that the inductive-limit topology used in a classical construction of a linear space which is not an absolute retract (see Un espace métrique linéaire qui n’est pas un rétracte absolu, Robert Cauty,
Fundamenta Mathematicae 146, 1994) is in fact also the same as the apartness topology. In NToP there is an example of a non-metrizable inductive-limit topology which can be described very naturally as an apartness space.

Since this NToP apartness topology is defined constructively, it could be of classical interest as well to see if apartness gives an easier approach to non-metrizable (infinite-dimensional) spaces.

cheers, frank

[Andrej Bauer]

Dear all,

Andrew Swan and I wrote up a short note explaining that in function
realizability all metric spaces are separable and all objects with
decidable equality are countable. The note is now available on arXiv
at https://arxiv.org/abs/1804.00427.

With kind regards,

Andrew and Andrej

[frank waaldijk]

Nice work, always good to have metamathematical considerations backed up by formal methods.

Still, the metamathematical essence of the question goes further than metric spaces. The relevant property for the topology to have is effectivity (O4 in my PhD thesis modern intuitionistic topology, chpt. 1, page 50). 

A space  (X,T) is effective if for any x in an open U in T, for all y we have: y in U or there is V containing x such that y is not in V.

Metric spaces are but one category of effective spaces. A mostly broader effective category is that of apartness spaces.

To offer more insight into the crux of the matter, let me recap my earlier remarks as follows:

 

Meta-theorem:

It is not possible to construct a non-separable effective topological space. 

Meta-proof:

Such a construction would carry over to intuitionistic mathematics. In INT however, the finest possible effective topology is the natural Baire space topology (see the above phd-thesis, although there is some inaccuracy in the definitions there which needs to be sorted...never got around to that sorry). This topology is separable. 

  
Corollary: it is not possible to construct an uncountable discrete set (this already follows from Andrej & Andrew's work)

Proof: on such a set, the discrete topology would be a counterexample to the meta-theorem. (In Andrej & Andrew's setting we can define a metric topology which would form a counterexample)

Best wishes, Frank

[Andrej Bauer]

> Nice work, always good to have metamathematical considerations backed up by
> formal methods.

I think we use words differently. To me "formal methods" something
like "formal proof verified by a computer", and "metamathematical
consideration" is what Andrew and I did. What do you mean? To my mind
arguments that use phrases such as "it is not acceptable" and "true
intuitionism" is not mathematics. It's a heuristic.

> Still, the metamathematical essence of the question goes further than metric
> spaces. The relevant property for the topology to have is effectivity (O4 in
> my PhD thesis modern intuitionistic topology, chpt. 1, page 50).
>
> A space (X,T) is effective if for any x in an open U in T, for all y we
> have: y in U or there is V containing x such that y is not in V.
>
> Metric spaces are but one category of effective spaces. A mostly broader
> effective category is that of apartness spaces.

Our theorem hinges on the fact that metric spaces are (good enough)
quotients of not-not-stable subspaces of the Baire space. I would
expect that the theorem can be generalized to spaces that still have
this sort of property.

> To offer more insight into the crux of the matter, let me recap my earlier
> remarks as follows:
>
> Meta-theorem:
>
> It is not possible to construct a non-separable effective topological space.
>
> Meta-proof:
>
> Such a construction would carry over to intuitionistic mathematics. In INT
> however, the finest possible effective topology is the natural Baire space
> topology (see the above phd-thesis, although there is some inaccuracy in the
> definitions there which needs to be sorted...never got around to that
> sorry). This topology is separable.

Here I lost you, when you said "In INT however, the finest possible
effective topology is the natural Baire space topology". The finest
effective topology on what? Can you point to a particular place in
your thesis where this is explained?

Also note that we proved something a bit stronger. We proved that in
function realizability (which is a model of INT -- INT is a *theory*)
all metric spaces are separable. This is stronger than "in function
realizability there is no non-separable space".

With kind regards,

Andrej

[Thierry Coquand]

Two other remarks on this question:

-Bishop commented on a related issue in a text “The constructivization of abstract mathematical
analysis” (reprinted in his Selected Papers)

“It is interesting to speculate whether we can relax the separability and metrizability assumptions
that occur throughout most of the above development. Surprisingly, the way to do this does not seem
to be to introduce larger spaces, but rather to examine functorial properties of mapping between the
spaces already introduced. An example will suffice. Let A be a commutative uniformly-closed algebra
of normal Hermitian operators on a Hilbert space H. In case A is separable the spectrum S of A is
compact, and the spectral theorem asserts that A is isomorphic to C(S). In case A is non-separable, on the
other hand, there seems to be no way of constructing even one element of S, so that the spectral theorem
is apparently not constructively valid unless A is separable. Nevertheless, the following theorem shows the
situation in its true light: if A1 and A2 are separable commutative uniformly-closed algebras of normal
Hermitian operation, with A1 subset A2 and i the inclusion map, then the adjoint map i* from the spectrum
S2 of A2 to the spectrum S1 fo A1 has dense range (classically the range therefore equals S1). Thus the
partially ordered family F of a given (non necessarily separable) A, together with the inclusion maps i, gives
rise to a dual family F* of compact sets, with corresponding maps i*. Classically it would be a simple
matter to use F* and the maps i* to extend the spectral theorem to the algebra A, but constructively we can
go no further.”

-we can force the existence of a large discrete set with a variation of Steve’s example: over sheaves
on the opposite category of discrete sets and monic functions in a given universe
where any map is a covering, we should have a discrete set which is not countable

Thierry

[Bas Spitters]

Bishop's example of the spectral theorem can be understood using
locales/formal spaces:

The norm of the algebra takes values in the upper reals, and the
spectrum is no longer a set, but a locale.
This insight comes from topos theory and is due to Banaschewski and Mulvey.

A fully constructive treatment and the link to Bishop's mathematics
can be found here:
Thierry Coquand, Bas Spitters, Constructive Gelfand duality for C*-algebras
Mathematical Proceedings of the Cambridge Philosophical society Volume
147, Issue 02, September 2009, pp 323-337.
https://arxiv.org/abs/0808.1518

[Andrej Bauer]

Thanks to Frank, Thierry and Bas for all the interesting remarks.

Let me just say one thing. Paul Taylor taught me that separability is
"poor man's overtness". If one were to pursue this direction further,
a natural generalization would be:

Theorem: All (good enough) spaces are overt in function realizability.

I wish I hadn't said that. Now I will want to check that this is the
case in function realizability. Perhaps Peter Lietz already did it in
his thesis?

With kind regards,

Andrej

[Andrej Bauer]

Here is an outline of a generalization of "every metric space is
separable in function realizability". We work internally, mostly, and
since this is an outline, we let the reader guess which bits are
external. We rely on countable choice in serveral places.

We first recall some standard definitions.

**Definition:** The *Sierpinski space* Σ is the quotient of 2ᴺ by the
relation u ~ v iff (∃ n . u n = 1) ⇔ (∃ m . v m = 1).

Remark: Σ is just Rosolini's dominance, i.e., Σ is isomorphic to

{ p : Ω | ∃ f : N → 2 . p ⇔ (∃ n . f n = 1) }.

We call the truth values in Σ *semidecidable* or *open*.

**Definition:** An object X is said to be a *T₀-space* if the
transpose εX : X → Σ^(Σ^X) of the evaluation map is injective (mono).

**Definition:** An object X is *overt* when Σ is closed under
X-indexed joins, i.e., for every u : X → Σ we have (∃ x ∈ X . u x) ∈
Σ.

**Lemma:** In function realizability every ¬¬-stable subobject S of Nᴺ is overt.

*Proof.* A realizer for a morphism u : Nᴺ → Σ can be thought of as an
enumeration of basic open balls in Nᴺ whose union is u. The same holds
for a ¬¬-stable subobject S. There is an enumeration α ∈ Nᴺ of all
open balls B for which B ∩ S ≠ ∅ (this is where we use a bit of
classical reasoning). To semidecide inhabitation of u realized by some
β ∈ Nᴺ, we use α and β to look for a ball which is non-empty in S and
is contained in u. □

**Theorem:** In function realizability every T₀-space is overt.

*Proof.* Suppose X is T₀. Then it is a subobject of the modest object
Σ^(Σ^X), therefore X is modest. There exists a ¬¬-stable subobject S
of Nᴺ and a quotient map q : S → X. Because S is overt, its image X is
overt, too. □

To connect this with the previous theorem, we observe that:

**Theorem:** A metric space is a T₀-space. It is overt iff it is separable.

*Proof.* A metric space is T₀ because open balls are Σ-open. If (X, d)
is separable then it is overt because N is overt. For the converse, we
already showed that every metric space is separable in function
realizability. □

Remark: We shot down the converse with our meta-theorem. Is there a
more economic and generally applicable proof that an overt metric
space is separable (under some circumstances)?

With kind regards,

Andrej

[Andrej Bauer]

P.S. Does the generalization surely covers the kinds of spaces that
Frank was talking about?

[Bas Spitters]

Thanks Andrej. That's a nice result!

It seems to generalize a relation between overtness, having a
computable norm and Bishop's compactness that we developed with
Thierry here:
Formal topology and constructive mathematics: the Gelfand and
Stone-Yosida representation theorems
https://arxiv.org/abs/0808.2705

We show that: all elements of a function algebra C(X) have a
computable norm iff X is compact over.

This is based on Thierry's fundamental paper:
Thierry Coquand. About Stone’s notion of spectrum. J. Pure Appl.
Algebra, 197(1-3):141–158, 2005.
https://www.sciencedirect.com/science/article/pii/S0022404904001847

On Fri, Apr 6, 2018 at 5:31 PM, Andrej Bauer <andrej...@andrej.com> wrote:
> P.S. Does the generalization surely covers the kinds of spaces that
> Frank was talking about?
>