Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The entry closed subspace was a bit weird. I have touched it to try to improve a little. But if anyone has ten minutes to spare, it might still be good to bring this into more decent shape.
I agree with the re-sectioning; thanks. I slightly rearranged the section on definitions.
I added to closed subspace some further discussion of how the localic case relates to the spatial one, and how the various definitions of closed subspace diverge constructively.
I have never doubted that the correct definition in constructive point-set topology is (3).
That’s not unreasonable, but are there theorems to back it up? The inarguably correct localic definition (4) does declare a closed subspace to be the complement of an open one, even constructively.
You only think that that's an argument because you're looking at the open subspaces as the fundamental concept and the closed subspaces are the derived one. But in locale theory, the things that we traditionally call ‘opens’ can just as easily be thought of as ‘closeds’, although in that case we'd be inclined to reverse all of the symbols. It's true that open subsets are more fundamental in constructive point-set topology, since the closed subspaces may be defined from them but not conversely; but in locale theory, the classical duality is restored.
I guess that this means that I object to the claim that (1) is the closest of the point-set definitions to the localic definition. For one thing, instead of defining a closed sublocale as the complement of an open sublocale, you could just as easily define it as a sublocale whose complement is open, fitting definition (2); this is because we're talking honest-to-Boole complementation here. But besides that, you could just as easily define closed sublocales first and then define open sublocales as either their complements or the sublocales whose complements are them. At sublocale, we (or I, since nobody else has edited that) define them both directly and then note that they are complements.
As for theorems, the first thing that a definition of closed subspace must do is have the closed intervals in the real line as examples, which (without the analytic Markov principle) rules out (2). I need a more philosophical argument to rule out (1): every subset of a discrete space should be closed.
You’re right that (1) and (2) are actually equally close to the localic definition, but that doesn’t yield an argument for the correctness of (3). I don’t see any reason to believe that every subset of a discrete space should be closed, especially since not every sublocale of a discrete locale is closed.
By the way, it seems that (2) is the only definition for which binary unions of closed subspaces are closed. Although not including closed intervals in does seem a pretty good reason to rule it out.
open subsets are more fundamental in constructive point-set topology, since the closed subspaces may be defined from them but not conversely
It doesn’t work to say that is open if for all , whenever lies in the closure of a set then is inhabited?
One might argue that viewing the elements of the frame of a locale as “opens” makes more sense than as “closeds” because they induce open subsets, not closed subsets, of its set of points. I suppose another might reply that that’s not about pointless topology as such but its relationship to point-ful topology. But the first one might counter-reply that such a relationship is already implied by using words like “open” and “closed”.
I just discovered that the usual localic definition is not “inarguably correct” – in fact there is also a notion of “weakly closed sublocale” analogous to Definition (3)! I added some discussion of this to closed subspace, which depends on a corresponding notion of “strong density” that I added to dense subspace.
Just a thought: in the presence of an apartness , definition (2) would make more constructive sense to me if formulated thus:
(2’) A subspace is closed if its strong complement is open.
This is too weak to include (3), so one could then combine this with (3), to arrive at:
(4)=(2’)+(3) A subspace is closed if is open, and contains all its limit points, i.e. if for any such that is inhabited for all neighborhoods of , we have .
which has a simpler, yet probably stronger variant:
(4’) A subspace is closed if is open, and for all : if is open then .
I think that (2’) and (4) have probably already been investigated closely, but I wouldn’t know where, off the top of my head. It seems to me of interest to look for strong variants which ’work’ for metric spaces (or better even apartness spaces). I’ve not really thought all this through, so I’m not sure if it helps, but it won’t hurt either I suppose :-)
It occurs to me that in the apartness topology (which coincides with the metric topology in most metric Baire space quotients) (2’) has another elegant variant (2”) which actually does imply (3).
(2”) A subspace is closed if its strong complement is open, and
For if is open, and is such that for all open containing we know is inhabited, then we can look at and and decide: or there is a containing (the latter which is clearly impossible). Since is arbitrary, it follows that .
Some more reflection yields that (2”) above has an unexpected consequence, which might imply that (2”) is too strong. However, if one is interested in eliminating ’static’, this consequence might not be undesirable.
If is an apartness space containing an isolated point , and is any proposition, then the set is closed as defined by (2”) iff . I’ve always been wary of sets like ’’, it might be nice to characterize them as ’closed iff ’.
With ’static’ I mean situations such as ’’ when we are mostly interested in ’’. By introducing the apartness, one turns a negative statement into a positive. With above we have , which we turn into a positive statement when claiming that is closed according to (2”).
Still, this example illustrates that (4’) might be preferable to (2”), since is closed according to definition (4’) because is open.
A much stronger variant of ’closed’ can be obtained using the topological notion ’strongly sublocated’ (see my PhD thesis modern intuitionistic topology, pages 65 and 113) which for general metric spaces becomes very useful when strengthened to ’strongly halflocated’ (much more useful than ’strongly located’).
see my PhD thesis
To check how famous you are, you might try signing with just your initials, and then referring people to “my PhD thesis”. However to ease the communication, it would be polite to offer a link with that. In this case even a link with a page number might seem in order.
(Just a friendly remark from the sidelines, I am not actually participating in this discussion. But I just tried, and in the minute of procrastination of the task that I am really working on at the moment I didn’t find your thesis.)
Thanks Urs. The link omission arose because in the minute that I could spare between more important tasks, I did not have time to also look up the markdown code for links… I added link and page numbers as per your suggestion.
[still, when I google ‘fwaaldijk PhD thesis’, there it is pronto… no author’s fame required]
Anyway, I forgot an important criterion (imho) for a definition of ’closed subspace’:
Transitivity of closedness: For subspaces with ’the subspace topology’ (also to be defined…!): if is closed in , and is closed in , then is closed in .
I have to check this for the variants above. ’Strongly sublocated’ and ’strongly halflocated’ have this transitive property. (’Strongly located’ does not).
(2’) is interesting. For general topology I don’t really like the idea of equipping a topological space with a separate apartness relation, but fortunately (as noted in your thesis) any locally decomposable space (or I guess any “effective” space in the sense of your thesis, which is weaker) comes with a canonical (non-symmetric) apartness relation defined by iff there is an open with and , or equivalently if is in the interior of the ordinary complement of , . If we use this apartness relation, then the strong complement is , so (2’) is asserting that this -indexed intersection of opens is still open. In particular, every finite subset is (2’)-closed, so this wouldn’t be an extension of the classical notion of “closed”.
I think strong sublocatedness also has this problem: in particular, with the above topological apartness, every singleton is strongly sublocated, whereas classically not every singleton is closed.
Glancing quickly through your thesis, the only positive result I found about strong sublocatedness was 3.2.4 that the closure of a sublocated subspace of a complete metric space is strongly sublocated, which moreover uses countable choice. Can you prove constructively (without countable choice) that there are any infinite strongly sublocated subsets of a metric space (especially a non-complete one)? Is strongly sublocated?
You didn’t say what you mean by “apartness topology”, but I guess probably it is that defined in i.2.0 of your thesis: is open if for every and either or . However, I don’t see how this can ever be proven to coincide with a nontrivial metric topology, since LEM implies that it is discrete.
(or I guess any “effective” space in the sense of your thesis, which is weaker) comes with a canonical (non-symmetric) apartness relation defined by iff there is an open with and , or equivalently if is in the interior of the ordinary complement of , .
That is not the correct definition. An apartness is symmetric, so the definition should read (as in 1.0.3 of my thesis): iff .
…so this wouldn’t be an extension of the classical notion of “closed”.
I think strong sublocatedness also has this problem: in particular, with the above topological apartness, every >singleton is strongly sublocated, whereas classically not every singleton is closed.
This is not a real problem, if you ask me. It makes no constructive sense (to me at least) to study non-effective topologies. Yet, as I show in my thesis, any effective topological space is , because the correct apartness to consider is . So right from the start we have the situation where we do not consider certain classical topologies, simply because they are essentially non-constructive. If you want to keep on including these topologies in your definitions, you will certainly raise the level of ’static’ in the sense described above in one of my previous posts.
Bishop called the wish to keep up with classical math ’pseudo-generality’ (and he hit the nail on the head, in my opinion). This pseudo-generality is extremely pervasive in contemporary constructivism…but it doesn’t help one bit when doing ’basic’ math in Baire space quotients. In fact I even think it hurts. We cannot build (really build, that is: predicatively, from the ground up, step by step, constructively) any space that is not a (subset of a) Baire space -quotient (possibly with a coarsened topology). I pose the refutation of that statement as a general challenge.
Therefore the apartness topology as defined in my thesis for INT, and in the book Natural Topology for BISH, is actually the finest effective topology that any constructive topological space can have, from a meta-level perspective. Bishop even thought that there were no interesting constructive non-metric topological spaces, but he was wrong. In Natural Topology (NToP) it is shown for instance that Silva spaces carry the apartness topology.
However, in the theory of the apartness spaces as developed by Bridges et al. (after they read my thesis, and borrowing from it, without proper mention by the way) the question of whether they can actually give a concrete non-metric example of their definitions is not even considered as far as I know. More pseudo-generality then, if the only interesting constructive spaces satisfying their axioms are metric spaces.
But it would not surprise me if the completely elementarily defined natural spaces in NToP (which are apartness spaces in BISH corresponding precisely to the INT-defined apartness spaces in my thesis) might satisfy many of these axioms. With NToP, one achieves much more than this complicated approach of Bridges et al., in my not so humble opinion. Which is why I am not happy to see their work extensively described under apartness space in nLab, and no mention of NToP or my thesis (which is the source of the idea of ’apartness topology’ and ’apartness space’ as well as of those words themselves, as far as I know. Douglas Bridges was a member of the thesis committee, and as such read my thesis already in 1996).
Can you prove constructively (without countable choice) that there are any infinite strongly sublocated subsets of a metric space (especially a non-complete one)? Is strongly sublocated?
is strongly sublocated without countable choice. For , we can decide: or . In the first case, take , in the second case, take . Then and implies . Since is arbitrary, this shows that is strongly sublocated in . Since the apartness topology coincides with the metric topology, is also strongly sublocated in .
Glancing quickly through your thesis, the only positive result I found about strong sublocatedness was 3.2.4 that >the closure of a sublocated subspace of a complete metric space is strongly sublocated, which moreover uses >countable choice.
In general we have two other non-trivial intuitionistic theorems, of which the first (thm. 3.2.9) already strikes me as a quite positive result:
Theorem: Strongly sublocated subspaces of a locally compact metric space are strongly located in
[: theorem 3.2.9. uses the definition 2.2.7 of ’boundedly strongly compact’, which equals ’locally compact Baire quotient and metrically complete wrt ’ which equals ’locally compact in BISH’ (which is a non-topological metric-dependent definition) of which is an example.].
But the second intuitionistic theorem (thm. 4.5.3) is the real kicker, and requires most of my thesis to prove:
Theorem If is (strongly) sublocated in a complete separable metric space , then there is a strongly -equivalent metric such that is (strongly) halflocated in .
[: two metrics on are strongly equivalent iff any -Cauchy sequence is a -Cauchy sequence and vice versa.].
One can almost hear the sigh of many readers on reading ’intuitionistic theorem’. However, I am confident that these results can be translated meaningfully into BISH, and perhaps more importantly: this doesn’t really matter, because it shows (yes, once again on that blasted meta-level) that both ’strongly sublocated’ and ’strongly halflocated’ are far more promising notions than the ones currently known from BISH.
In my thesis, I prove in BISH the Dugundji extension theorem for strongly halflocated subspaces. I know of no proof for strongly located subspaces (other than as special cases of strongly halflocated subspaces). Moreover, like I already said, ’(strongly) sublocated’ and ’(strongly) halflocated’ behave transitively (another very positive result I would say), where ’(strongly) located’ does not.
(Constructive) definition (3) of ’closed subspace’ (in closed subspace) does not seem to behave transitively either, which is a real issue if you ask me. Much more important than whether it faithfully extends the classical notion or not…
An apartness is symmetrical
That’s why I said “non-symmetric apartness”. I don’t know a good name for a relation that satisfies the other two axioms of an apartness but is not symmetric, but it’s what you get naturally from a non-symmetric effective apartness space, just like a non-symmetric (i.e. non-) topological space gives you a specialization preorder that isn’t necessarily symmetric. I don’t see any reason to arbitrarily symmetrize it.
I do think it is important that constructive notions be conservative extensions of classical ones, because the main point of constructivism for me is that it is more general than classical mathematics (e.g. having models in all toposes). If we start doing things that don’t reduce to their classical analogues, then that is no longer true. And I see no reason to discard the powerful and conceptually organizing tools of abstraction and generalization that all mathematicians have come to value over generations; they are just as useful constructively, if not more so. Arguably the whole point of general topology is to include non-metrizable examples like the Alexandrov topology of a poset or the uncountable product of metric spaces. Probably you claim those are not “build predicatively” “from the ground up”, but why should I care about that?
I would be very happy to include more references at apartness space; I wrote it simply based on the references I knew about, which I think I got from Toby. Can you point to exactly where in your thesis or book one can find a definition of “apartness space” analogous to the one on the page now? I wasn’t able to find it.
… is open if for every and either or . However, I don’t see how this can ever be proven to coincide with a nontrivial metric topology, since LEM implies that it is discrete.
I didn’t quite understand your answer to this question. Are you saying that it “being” the metric topology in some cases is only a meta-theorem?
definition (3) of ’closed subspace’ (in closed subspace) does not seem to behave transitively either
If is closed in and is closed in , suppose every open neighborhood of intersects . Then in particular every such open neighborhood intersects , so since is closed in we have . Now every open neighborhood of in is (by definition of the subspace topology) the intersection with of some open neighborhood of in , and therefore intersects by assumption; thus since is closed in we have . Therefore is closed in .
Ah nice, I did not see that last argument quickly! Too busy with my own propaganda I suppose…
OK let me: a) postpone going to bed, b) apologize a little for the purist-constructive propaganda above, c) try to quickly answer before my mind becomes too drowsy.
First: I agree with you that classical math is quite worthwhile. I disagree probably mainly on what kind of math should be called constructive. There is imnsho a tangible added value in differentiating between constructive-as-per-my-rant-above and constructive-as-including-impredicative-or-more. If that distinction is blurred, then to me too much clarity is lost, resulting in miscommunication but also in a muddier transition from theory to application and vice versa. Classically, one just calls the latter transition ’applied math’, but I personally am interested both philosophically and practically in an elegant and smooth framework enabling a completely transparant transition from theory to application [without having to formulate mathematics in type theory, I add as clarification, that for me is not an elegant way to do math theory (it is probably very elegant for applications, but I’m still primarily interested in math, not in computer science)].
I would not presume to speak for any majority, I know, but that’s maybe a big reason to speak at all. You need not care about my concerns, in that you are quite correct, but -just like constructive math enriches classical math- you might find that pursuing things from the purist constructive standpoint enriches your approach as well. Just a thought.
In NToP you will find a definition of ’apartness topology’ for BISH. But basically, classically, it is simply the quotient topology on Baire space corresponding to the equivalence derived from the apartness. The challenge is in turning this classical definition into something completely workable from the purist-constructive view. The benefit for classical math is some really nice structures emerging which went unnoticed before.
For a complete separable metric space , we can prove that it is isometric to a natural space (Baire space quotient) equipped with a metric , and in this natural space the apartness topology coincides with the metric topology. More generally, to define an apartness topology on a Baire-derived metric space is possible if we can pinpoint a metric homeomorphism between and a metric space where is a natural space equipped with a metric , since in that case we can pull back the apartness topology on to . But in general, the metric topology and the apartness topology need not coincide on (the apartness topology refines the metric topology always though).
Can you point to exactly where in your thesis or book one can find a definition of “apartness space” analogous to the one on the page now? I wasn’t able to find it.
I will get back to you on this, but it is actually the definition of ’natural space’ in NToP (I thought it would be useful to distinguish it from the definition/terminology used by Bridges et al., even though they borrowed it from my thesis). For constructive workability, the definition in my thesis presupposes the continuity principle CP, which amounts to the same thing as saying that Baire topology is the underlying motherspace. NToP is what you get when you translate my thesis’ use of CP into BISH, well almost because NToP has some pretty cool extras for exact computation (see Exact computation over topological spaces, preprint 2013). That last reference is probably easier to read than NToP, and contains the definition as well.
Hi Frank! The reason that the nLab refers more to Bridges than to you is probably that I find (or rather found, about a decade ago now) Bridges easier to read than you. This may have to do with Bridges's following classical mathematics more closely. I'm sorry about that, and I do admire your work; I just don't understand it yet (and haven't tried to in about a decade). Of course, I also didn't realize (or I forgot) that Bridges's work is based on yours.
That said, I do agree with Mike that constructive math should be backwards-compatible with classical math, even if just for the pragmatic reason that classical math dominates the literature now, and we need to be understood. That shouldn't be an insurmountable problem, however; even Bishop wasn't entirely backwards-compatible, and it should just be a matter of stating assumptions and perhaps using some less attractive terminology. I wouldn't want to exclude anything on the grounds that it's incompatible with classical math; it just can't be the full story.
For a complete separable metric space , we can prove that it is isometric to a natural space (Baire space quotient) equipped with a metric , and in this natural space the apartness topology coincides with the metric topology.
How do you reconcile that with the fact that classically, the apartness topology is always discrete? Are you using some nonclassical axioms? Or am I wrong about that “fact”?
Glancing at your definition of “natural space”, it seems like a sort of presentation of a “proximal apartness locale” with some countability conditions imposed. (What does mean in the definition of “point” of a pre-natural space? I don’t see it defined earlier, only .) In general I always find it simpler to give definitions first without axioms like countability, and to define objects first rather than their presentations. Can you imagine how much harder it would be to understand group theory if instead of “a set with an associative and unital operation with inverses”, a group were defined to be a countable set of generators together with a countable set of relations between formal words in the generators? Certainly it is sometimes helpful to talk about presentations for objects, and some theorems and applications require assumptions such as countability, but the conceptual development is greatly obscured by imposing such requirements from the outset.
I have at various times tried to read predicative-constructive mathematics, and so far it has always felt to me like trying to run a marathon hopping on one foot. (This is in contrast to impredicative topos-valid constructive mathematics, which — once you get used to it and learn how to do it in the right way — is often more elegant than classical mathematics.) But maybe one day I’ll find some value in it. (-: It is a shame that “constructive” means so many different things to so many different people.
Thanks Toby and Mike, I feel we’re getting somewhere, notwithstanding some differences in outlook. At the same time, to explain my view on the more philosophical issues that Mike raises requires more discussion, which I would like to postpone just a little.
Because I first would like to help formulate NToP in a more familiar impredicative way (even though its current definition is quite OK classically), to accommodate Mike’s remark.
The idea is to do pointfree topology, yet we do not start with opens or closeds, but with a very nifty idea of Wim Couwenberg’s (the germ of which was already Brouwer’s, and which Freudenthal already applied very beautifully in 1937), which we dub ’basic dot’. We all speak ZF, so let’s go from there.
A pre-apartness space is a triple where is an infinite set (with elements called ’basic dots’), and are subsets of satisfying:
For the motivating example of the real numbers, the basic dots can be thought of as the (closed) rational intervals, where for closed rational intervals we define: iff , and iff (as subsets of ), and where the maximal dot is (an extra added interval representing itself).
Now we turn to defining points wrt . A point is an infinite subset of such that:
The set of points in is denoted , it is a subset of the powerset of . However, clearly many points in are ’equivalent’ in the intended topological sense. Therefore we extend and to points in the following way:
For and , we write
From here on, the classical mathematician switches to the set of the -equivalence classes of . To save myself work, I refrain from doing that here, but it is straightforward to replace the following with the traditional classical approach.
(or more colloquially ) is called an apartness space iff in addition every basic dot contains a point.
There is a natural topology on , which we call the apartness topology, denoted by , and defined thus:
A subset of is -open iff a) for all there is an such that is a subset of , and b) is closed under .
One easily checks that this does define a topology (for of opens , we have with and , now use that is a total order wrt ).
On writing this all down, I realize that this must correspond to something already well-known in classical math, probably to the quotient topology of an ’order-induced topology’ or some similar term. So that would be useful to add to my description of NToP, where I only mention Baire space quotients. I also would like to emphasize that the basic ideas of Wim Couwenberg played a paramount role in the genesis of NToP, especially concerning ’basic dot’, ’filtering’, ’morphism’. Therefore, I mostly feel to be the translator/technician of other people with the real ideas…
Without having checked thoroughly, I believe the above to be a faithful classical translation of the apartness topology described in my thesis. But I understand that this may not be immediately apparent to the non-initiated (in intuitionistic math). My thesis research and its written completion was done in 2,5 years under rather trying family circumstances. I still tried to be as explanatory as possible, but I never really had the opportunity to explain all its contents in a more expository style. Also it contains some (very irritating but not fundamental) errors, which I would like to correct in a clear manner when I find time and energy.
Then again, I would also like to try and better explain my view that INT is the perfect meta-language for purist BISH, and that Brouwer’s intuitionism actually is more easily understood from that viewpoint. That viewpoint can be stated thus: ’In a (purist-)constructive theory of Baire space (quotients) having also non-recursive elements, Brouwer’s axioms AC and BT (transfinite induction, say BI_D) hold in every concrete situation’.
Mike, in a way I still start with a presentation and generators…but in this case, I do not see how to prevent it. You are probably better informed how to rephrase the above more to your liking. Still, you should now see that the apartness topology is generally not the discrete topology, and that the apartness topology on coincides with the metric topology.
Oh, before I forget: you write
That’s why I said “non-symmetric apartness”. I don’t know a good name for a relation that satisfies the other two axioms of an apartness but is not symmetric, but it’s what you get naturally from a non-symmetric effective apartness space, just like a non-symmetric (i.e. non-) topological space gives you a specialization preorder that isn’t necessarily symmetric. I don’t see any reason to arbitrarily symmetrize it.
Still, any such non-symmetric apartness can be trivially turned into a symmetric apartness by putting iff . So for me there has to be a good reason to not symmetrize it, for one because the condition of ’being apart’ is a very symmetric idea from the start, and for the other because I prefer to introduce new terms only when I really need them.
Still, you should now see that the apartness topology is generally not the discrete topology
Okay – where I went wrong was way back in #20 when I said
You didn’t say what you mean by “apartness topology”, but I guess probably it is that defined in i.2.0 of your thesis: is open if for every and either or .
since evidently that isn’t what you meant. I’m glad we finally got that sorted out.
So for me there has to be a good reason to not symmetrize it
For me, the good reason is that there are lots of interesting spaces that are not .
How do you view the real numbers as “points” of your apartness space defined by rational closed intervals? I can’t think of any canonical way to represent a real number as a set of rational closed intervals that is totally ordered.
Oh, are you saying that we can use any such representation and then identify them all with later? That seems really weird to me. Why would you expect, in the absence of choice, that any point of a space can be represented by a totally ordered collection of neighborhoods?
Actually, there seems to be a choice issue even in your example of real numbers. If I give you a Dedekind real, how can you produce a totally ordered set of rational closed intervals shrinking around it? I don’t see any way to do that without some sort of bisection procedure and countable choice. Maybe you want to consider Cauchy real numbers instead, but in the converse direction I don’t see how to get a Cauchy sequence out of one of your “points” without countable choice either.
Frank accepts some choice axioms, listed in §0.0.7ff. (§0.0.8) is enough to identify Dedekind and Cauchy reals, allowing one to go in both directions.
Hmm. Okay, well, that means the definition may need more substantial modification before it becomes something suitable to be compared with the abstract one we have at apartness space. In general on the nLab, “constructive” means not assuming any choice axioms (among other reasons, because no choice axioms are valid in all toposes).
I can think of several possibilities for how to get a more familiar abstract structure out of the construction you described, Frank, but which one is best depends on what you are trying to achieve with your construction. In particular, how do you define a morphism between your apartness spaces?
I wouldn't say that ‘constructive’ on the nLab means not assuming any choice axioms1, because I've written a lot about constructive math on the nLab (possibly the most), and I've never tried to use the word that way. However, it's true that we're particularly interested in what can be done in all toposes, and that I have always preferred not to use any choice axioms if I can help it, even without that motivation.
Other than Unique Choice, since we work almost entirely in a context where that is trivial. ↩
I can think of several possibilities for how to get a more familiar abstract structure out of the construction you described, Frank, but which one is best depends on what you are trying to achieve with your construction. In particular, how do you define a morphism between your apartness spaces?
Yes, I was going to come to that. [Please believe that it isn’t easy for me either to understand your and Toby’s viewpoints and questions, which I’m trying to answer as best as I can. I hoped that the classical ZF definition above would suit you, because I removed the countability requirements (to accommodate your remark in #27). But for separable spaces like it then does get a little over the top, I agree. I’m inclined to think that in ZF one doesn’t need countable choice to prove this ZF-apartness- homeomorphic with metric-Cauchy-, but that is in the presence of excluded middle… Also I haven’t checked this, the above posts being the first time I tried a general ZF-definition.]
For clarity, let me first point you to the BISH-valid definitions in NToP of ’apartness topology’ and ’morphism’. Like I said, the easiest place to read them is in the preprint Exact computation over topological spaces, where ’natural space’ is a synonym for ’apartness space’.
Section 2 (pages 4-8) defines pre-natural space (2.1), apartness topology (2.4), natural space (2.5) and natural real numbers (2.6).
Section 3 (pages 8-11) describes morphisms. The most important morphisms are refinement morphisms defined in (3.2). To be complete, in (3.4) the reader is referred to the more involved trail morphisms defined in NToP (1.1.4, page 19). Most often, the distinction is unimportant, and we simply say natural morphisms (3.5). Finally isomorphisms are defined in (3.7)
With or without countability requirements, the definition of ’refinement morphism’ remains the same I believe. Continuing from #28-#29:
Idea: When going from one natural space to another, a refinement morphism sends basic dots to basic dots, respecting the apartness and refinement relations inasfar that ’points go to points’. This means that any refinement morphism is an order morphism with respect to the partial order . (Not all order morphisms are refinement morphisms though).
Definition: Let and be two apartness spaces, with corresponding pre-apartness spaces and . Let be a function from to . Then is called a refinement morphism (notation: -morphism) from to iff for all and all :
As indicated in (1) above we write also for the induced function from to . By (2), a -morphism from to respects the apartness/equivalence relations on points, but not necessarily on dots since does not necessarily imply for . This stronger condition however in practice obtains very frequently.
Every natural morphism is continuous wrt the apartness topology. For Baire space the apartness topology ’is’ the product topology (which coincides with the usual metric topology on Baire space). Also for Baire space, if we add the countability requirements like in NToP, the refinement morphisms are in 1-1 correspondence with Brouwer’s spread-functions. Every refinement morphism then is unambiguously coded by an element of Baire space itself, and every continuous function from Baire space (product topology) can be represented by a morphism (well, you need some axioms for this, notably the Lindelöf-type axiom BDD, but these axioms hold in CLASS, INT and RUSS).
This idea of Brouwer’s is highly underappreciated in my view, because it avoids impredicativity of the most important function spaces. Continuous funtions can be treated as elements of Baire space, and not as subsets of the squared powerset of Baire space. This is not ’just’ a predicativist advantage…because this is directly connected to actual computation. Yes, it is hard work to (show that it is possible to) reduce everything to the very bare bones essence, but the gain is not inconsiderable if you ask me.
The very nice extra of NToP is that it shows how to replace Brouwer’s trail morphisms (which are necessary in his beautiful but still not optimally efficient construction of the reals and other quotients) with the computationally very efficient refinement morphisms. Using lean representations, such as for : the lean dyadic intervals (), one gets a comprehensive theory of Baire quotients (including all complete separable metric spaces) that at the same time corresponds quite precisely to the recommendations for exact computation in Bauer&Kavkler2008 and Bauer&Kavkler2009.
I’ve been trying to get Andrej Bauer to really read this preprint, his interest looks to be growing but he is pressed for time.
As we are all, I guess. Which is why I repeat that I appreciate your and Toby’s interest, and I remain willing to try and clear up any unclear definitions or ideas to the best of my ability.
OK now I’m more confused than ever. Why would you require a morphism to send basic dots to basic dots?
You ask the right questions, that is the hard ones. Don’t forget it took a long time to develop this stuff and get it right (hopefully), even though I was already quite familiar with intuitionistic topology and had help from Wim Couwenberg.
Why do we require a refinement morphism to send basic dots to basic dots: to simplify, and to better use the pointfree advantages. I’ll try to explain, it is both a simplification and generalization of ideas in Formal Topology.
The sets of basic dots act almost like a neighborhood basis of the apartness topology. In fact, we can specialize and require all these basic dots to represent opens in the apartness topology. If for all , the set is open, then we call a basic-open apartness space. [This corresponds I believe to the idea of formal opens in Formal Topology].
Let be apartness spaces, where is basic-open. Then we can describe a pointwise continuous function from to , already one powerset-level lower, by a pointfree function from to (at least for NToP, in CLASS, INT, and RUSS).
How so? For a continuous function from to and (open) basic dot , the inverse is open in . If is actually inhabited, say containing , then there is a basic dot such that . That means that , in other words if we are looking for a pointfree function from to representing , we can safely specify: … but we must ensure overall that points go to points, so we have to be vigilant that for ’converging’ basic dots, the -images converge as well.
That this can be done starting with a continuous function is NOT trivial at all. In NTop there is a nice theorem about this, see below, but for the ZF-definition I haven’t got a clue. But the other way round is much easier: every refinement morphism is continuous.
For NToP-spaces we can prove (in CLASS, INT and RUSS) that every continuous function from an apartness space to a basic-open space can be represented by a natural morphism (which sometimes has to be given as a refinement morphism on an alternative NToP-representation of , but that is a technical detail here).
Pff, even I find this tiring, because it is just not easy. Sorry for that. And I have to stop for today again…
But will in general be contained in the inverse images of many different ’s. Why is it enough to choose one?
[Oh sorry Mike, I was writing this already]
I forgot an important other reason to define refinement morphisms in this way. If you want to forget about the points as much as possible, and primarily consider the pointfree relations, then a morphism should be a structure-preserving function from to . So basic dots get sent to basic dots, by the meaning of ’morphism’.
In the #38-definition of refinement morphism I would therefore prefer to exchange
(2.) implies (for points )
for the stronger
2’. implies (for basic dots )
but precisely this change blocks the most general proof that continuous functions can be represented by morphisms. The cause for this is that the ’convergence rate’ for points is not specified, for an arbitrary continuous function , and so for our intended morphism representing we can prove 2. but not 2’.
(Not easy at all.)
@ Frank # 27:
I’m inclined to think that in ZF one doesn’t need countable choice to prove this ZF-apartness- homeomorphic with metric-Cauchy-, but that is in the presence of excluded middle…
I didn't entirely grasp that you were working in ZF just then. Certainly with excluded middle, Mike's objection that Dedekind ≠ Cauchy disappears.
But will in general be contained in the inverse images of many different ’s. Why is it enough to choose one?
You are quite correct, it is not obvious at all that this would suffice, but it can be arranged so that it does. At least in NToP, using a nice method which took me quite some time to find.
In NToP the basic dots can be ’graded’ through the partial order combined with the pre-apartness . That means we have a sense of ’large’ and ’small’ basic dots. This enables us to send ’small’ basic dots in to ’small enough’ basic dots in to ensure convergence of the images of points.
How to define this grading is specified in the proof of theorem 2.2.0 (page 40 of NToP), the proof is given in the appendix A.3.4. (page 126).
This grading is then used in the quite difficult proof of the relevant theorem 1.2.2 (page 25), that proof is given in appendix A.3.1 (page 122).
Ok. Unfortunately I’m running up against the limit of the amount of time I have available to spend on this. Overall the impression I’m getting is that you have a very complicated setup (compared to the simplicity of a topological space, a locale, or a point-set apartness space as currently defined on the lab), which it takes a lot of work to prove has anything to do with topology, and I don’t see any benefit that I will get from figuring out the relationship. I do want to acknowledge your contributions to the field, but right now the best way I can think of to do that (unless Toby is willing to spend longer working out the details than I am) is to add a brief note to apartness space (which I have now done).
I am sympathetic to the desire to compute things efficiently; computers are a very important tool for the modern mathematician. However, in my opinion, to define mathematical objects in terms of a computational representation for them is to “become the tool of one’s tool”, in Thoreau’s words. Mathematics is a study of ideas, and to me conceptual understanding is its primary goal. Once we understand an idea, then we can seek to represent it in a computationally effective way; but the idea remains the same whatever computational representation we use (and we might use different ones for different purposes). If we limit ourselves to work directly with computational representations at all times, then we are likely to miss the forest for the trees, not seeing the unity of disparate concepts, and failing to formulate new ideas that don’t yet have a direct computational significance.
OK Mike, your time-limit is quite understandable. Thanks for your interest, and for the mention/reference in apartness space.
Still: the intuitionistic definition in my thesis is very conceptual and captures the constructive heart of the apartness topology much more conceptually than any other definition so far mentioned. But no-one seems to understand intuitionistic mathematics (or want to understand it, because it is very sharply defined in a very simple and stable setting which has been around since 1965).
This constructive heart is characterized by:
is -open iff for all (the defining property of -open in my thesis)
In other words: a set is a -neighborhood of iff for all we can constructively decide: ’ is -close to ’ () or ’ is apart from ’.
To prove that for a apartness on Baire space this definition actually describes the quotient topology of the corresponding -quotient, one uses the continuity principle CP.
But you may rest assured that also outside Baire space, the above definition faithfully describes the finest topology that any effective constructive topological space can have. How much more conceptual can you get?
NToP was written to translate Brouwer’s topological ideas (which really are conceptually very beautiful, for more than a couple of reasons) to BISH and CLASS mathematicians. The NToP definitions are in my opinion still quite conceptual, but in the absence of CP one has to introduce some technical machinery. Yes, one can do so in the Bridges et al. style…which like I said borrows substantially from my thesis. BUT did you know that compactness and uniform continuity is still not resolved in that style? So it doesn’t really work so well, if you ask me. [And even then, every predicative topology that they describe can be described by NToP as well (I saw that they do give a non-metric example, so that is good and I retract my statement on this in an earlier post).].
This is because in that style, transfinite induction cannot be done(!). In the much more complicated Formal Topology, transfinite induction is used, but in NToP this is shown for Baire space to be reducible to the simpler genetic induction which is in essence the translation of Brouwer’s Bar Induction (from axiom to induction scheme).
So, other than both the Bridges style and Formal Topology, NToP has simple definitions which work elegantly simultaneously in a pointwise (analysis-oriented) setting and a pointfree (topology-oriented) setting. The only complicated thing is to prove that these definitions do the right things.
[Actually, this is only complicated in the absence of Brouwer’s axioms, which like I said are a tremendous conceptual simplification, allowing one to go straight to the heart of many constructive definitions. But who wants to consider this, in the constructive community? So let me rephrase my earlier challenge thus: give me any predicative effective topology defined in BISH, and I will describe the very same topology much simpler and much more conceptual in INT (!)]
Once the fundamental ’correctness’ work is done, to use NToP is quite simple and elegant. Yet, in order to create tangible added value as compared to Brouwer’s spreads, I spent a lot of time to also flesh out a more efficient way of representing spaces and computing with them. That is not the main thrust of NToP, as witnessed also by both book and article mentioned above.
This is not meant as a continuation of the discussion, I know and respect that we will probably keep our differences of outlook and style. And I repeat: I really appreciate you putting in quite some time and effort to understand NToP. For me, I spent more time on math lately than I can really spare, but I’m glad to see such interest from a number of people. Nonetheless, it also suits me better to leave this topic for now.
Just for the record, the ‘constructive heart’ above is at apartness relation#topology (and has been for a while). To my mind, it expresses a compatibility condition between an apartness relation and a topology.
Your “constructive heart” is a great definition. But it is not an abstract definition of “apartness space” or “topological space”, rather it is a construction of a particular topology induced by a point-point apartness relation.
1 to 49 of 49