Add example from Bridges-Vita that a non-Decomposable proximity space need not be induced by a uniform space in the usual way.
]]>I also added the missing nonemptiness condition to the definition of clusters in the Smirnov compactification, and some remarks on how a cluster is kind of like a prime filter.
]]>Now I decided to rename Complete Regularity to Decomposability, and replace Regularity with a similar axiom (the “perfect” analogue of Decomposability) that doesn’t imply any symmetry, called Local Decomposability. The latter corresponds quite exactly to local decomposability for point-set structures. And Decomposability only implies complete regularity if we also have Symmetry, while classically Symmetry is the crucial ingredient ensuring complete regularity, so it seems not quite right to call Decomposability “complete regularity” (plus there is the countable choice issue).
]]>I added Complete Regularity to the list of axioms at proximity space, along with the above remarks, and a proof that assuming Complete Regularity and are inter-definable. I am not sure how to state Complete Regularity for , and seems unreasonable anyway constructively, so I left it blank.
]]>Unrelatedly, it occurs to me that in addition to there is a fourth classically-equivalent way to express proximities (and, hence, I guess, also syntopogenies). Actually there are at least three more, but only one of them seems likely to be interesting. In proximity-space theory it’s sometimes written “” (where is the proximity space), defined classically to mean . Its Complete Regularity axiom is probably “if , there exist and such that and and ”; but I don’t immediately see how to formulate any weaker notion of Transitivity for it.
]]>Oh! There is a way to define a proximity from a uniform space that satisfies (1) or (1): instead of the obvious definition ( if there is an entourage such that ), say that if there is a uniformly continuous function such that and , and similarly. And conversely, conditions (1) and (1) are likewise sufficient to prove complete regularity, modulo countable choice. So it does make sense to call them (or maybe their modulated versions) a sort of proximal complete regularity.
Of course if the uniform space we started from is not completely regular, then this proximity doesn’t really underlie it itself, but some kind of “completely regular reflection” of it. (In particular, it might not have the same underlying topology.) I’m not sure exactly what it should mean to say that a uniform space is “uniformly completely regular”, but maybe something like “for any entourage and point , there is a uniformly continuous function such that and and (not sure about whether to include that last condition). That’s at least sufficient that the above proximity has the same underlying topology.
I think a (completely regular) uniform space can also be interpreted as a syntopogenous space satisfying (1) or (1), if we define say to mean there is a uniformly continuous function such that and and also . If the uniform space is completely regular as above, then this syntopogeny is sufficient to determine the uniformity, and its simple coreflection is the above completely regular proximity. But this syntopogeny is no longer biperfect or even perfect, and I don’t see any easy way to characterize the syntopogenies arising from uniformities in this way.
]]>I added some further remarks on the relationship between the three definitions constructively. It seems to me that contains strictly more information that , since the latter is determined by its restriction to complements, whereas the axioms of are just too strong to be reasonable. I haven’t been able to think of a way to define a in terms of that works for proximities (or more general syntopogenies), although there are point-based ways that work for point-set apartnesses and uniform apartnesses.
]]>Back on #13-14, proximities as profunctors, I would think that if we are talking about -enriched profunctors then there is no extra structure to be gotten rid of, since composites of -enriched profunctors are just relational composites. Am I missing something?
]]>Thanks!
]]>In topological spaces, dropping transitivity gives us pretopological spaces, and since some people do drop that from proximity spaces, we should name their objects of study, and I propose to call them ‘preproximity spaces’. That doesn't seem to be used in the literature except in some literature on fuzzy logic; the only problem is that this literature's abstracts suggests that ‘preproximity’ is used outside of their field (and in a way analogous to ‘preuniformity’, which is not what I want here); but if so, Google can't find it.
Anyway, I introduced that term to the article.
]]>Okay, I have:
Go ahead and edit, and I'll bring it up if I don't like how it looks.
]]>As for the “Transitivity (constructive)” row, its current entry for is boringly equivalent to the “simplified” version, while its entry for is too strong. My lengthy discussion above suggests removing this row entirely and changing the “simplified” version for (which is currently equivalent to my (2)) to my (3) by switching and .
For , I would also switch and in the “simplified” version (which in this case is stronger than the “constructive” one) to get “if for every either or , then ”. I think this is also true in any quasi-uniform space, where means : given an entourage , let be such that and ; then clearly , so , so we have (so that ) and also such that , hence .
Does that sound ok?
]]>I don’t like the notation for the complement of ; it’s too light and easy to miss for such a drastic operation. Can we switch to something like or at proximity space?
]]>I renamed “Normality” to “Transitivity” at proximity space, and added a remark about it to the Warnings about terminology.
]]>Also, I don’t think I like the axiom for labeled “Symmetry (constructive)” at proximity space. It’s actually weaker constructively than the one labeled “Symmetry (simplified)” — its hypotheses ensure that and , so implies by isotony — and I can’t see any problem constructively with asserting the “simplified” version — it’s true in any uniform space, for instance. If anything, the “simplified” symmetry axiom for seems likely to be too weak, but I can’t think of any way to strengthen it that doesn’t amount to regularity.
]]>Well, I can’t see how to prove that even a metric space satisfies (1) or (1) constructively, so probably those are two strong. Here’s another possibility for “proximal regularity” that I think is implied by uniform regularity and implies ordinary regularity:
To get regularity, take to be open and consider the interiors of and . To get this from uniform regularity, if implies , take such that and such that , and let and and .
We could simplify the axiom by taking or .
]]>Well, maybe, although the last time we tried that, we had some additional gaps. Besides which, if I'm looking for the deep inner meaning of complete regularity, I'm not sure that I want something so fiddly as a modulated property.
]]>We should be able to get rid of the countable choice gap by asking for a “modulated” version, no?
]]>As you say, it looks more like complete regularity, but it’s not exactly complete regularity of the underlying topological space; we still need countable choice to produce a real-valued function
Well, I am looking for a deep underlying meaning of complete regularity that doesn't refer to . One would not expect this to match the usual definition without a bit of countable choice.
]]>A rule of thumb in constructive mathematics is to treat negation with suspicion; thus, (1) and (2) are the most natural. But one should also be suspicious of disjunctions in conclusions, since these may be too strong, and this is what you are claiming about (1). Letting every subset be located, even subsets such as for an arbitrary constant proposition , is way too strong.
Indeed, if the obvious simple structure on an inhabited metric space satisfies (1) , then the forbidden de Morgan law follows (hence LLPO, etc).
]]>I think this analysis sheds some light on the uniform regularity / local decomposability conditions: the reason it’s unclear whether to include them as part of the definition or as extra properties is that they result from classically-equivalent ways to contrapose a statement. But if we want to keep the standard definition of “topological space” (rather than requiring all spaces to be locally decomposable), it seems that for consistency we should not include such conditions in the definition of point-set apartness space or uniform space.
Finally, this suggests that for set-set apartness spaces and proximal neighborhood spaces, we should not use (1) or (1) as the definition constructively, but rather (3) or (2). The observations above show that any uniform space has an underlying proximal neighborhood space satisfying (2), and if it is uniformly regular then it has an underlying set-set apartness space satisfying (3). (A non-uniformly-regular uniform space doesn’t even give rise to a point-point apartness space, so that requirement here isn’t so bad.)
As for a name for (3) and (2) in the definition, I would lean towards “transitivity”, because it would seem reasonable to call conditions (1) and (1) proximal regularity. Just like uniform regularity, they are classically automatic, but constructively ensure a stronger regularity property. As you say, it looks more like complete regularity, but it’s not exactly complete regularity of the underlying topological space; we still need countable choice to produce a real-valued function, in which case I think we get not just topological complete regularity but “proximal complete regularity”, i.e. a separating function that’s proximally continuous. So I would rather call it just “proximal regularity”; the corresponding “modulated” version that doesn’t require countable choice could then be “proximal complete regularity”.
One somewhat unfortunate fact is that the underlying proximity space of a uniformly regular uniform space apparently need not be proximally regular. I’m not sure exactly what to conclude from that.
]]>Now how are all these conditions related to known definitions? Consider first the case of a simple perfect syntopogeny (so or ), giving notions of topological space:
Condition (2P) is exactly the condition on a collection of neighborhood filters (a perfect topogenous order ) for it to define a topology. Moreover, in the perfect case, (2P) is equivalent to (2).
Condition (1P) implies (2P), so it defines an extra condition on a topological space. In fact it is precisely local decomposability.
Condition (1) implies (1P), so it also induces an extra condition on a topological space. But this condition seems too strong to be constructively reasonable: since every open set satisfies , it requires that every open set is complemented.
Condition (3P) is precisely Bridges-Schuster-Vita’s last axiom for a point-set apartness space. (Their phrasing is more complicated since they want to incorporate the possibility of a previously-given point-point apartness, but if the latter is the denial inequality then their condition reduces to (3P).) Moreover, in the perfect case, (3P) is equivalent to (3).
Condition (1P) is again precisely local decomposability for a point-set apartness space.
Condition (2P) also appears in Bridges-Schuster-Vita (Proposition 2.10), but they don’t give it a name. It’s a weaker version of local decomposability.
Condition (1) is unreasonably strong constructively: it implies that the basic opens are all complemented. Condition (2) is also too strong: it asserts that the basic opens are complements.
Now consider instead a biperfect symmetric syntopogeny, giving notions of uniform space.
Condition (1P) is the one that I used to define a uniform apartness space: Given a co-entourage , there is a co-entourage such that whenever , for any we have either or . In particular, it is true for the notion of apartness defined by a uniformly regular uniform space.
Conditions (2P) and (3P) (equivalent under symmetry) give a weaker axiom for uniform apartness spaces, equivalent to the stronger version under uniform regularity, and always satisfied by the complements of entourages of a uniform space (though the union axiom is, I believe, still not satisfied by those).
Conditions (2) and (3) seem stronger than (2P) and (3P), but are still always satisfied by the complements of entourages of a uniform space. For if is an entourage such that for all and , let be an entourage such that . With and we have and . And if is such that and for some , then for any we have since , a contradiction; thus .
I can’t make much sence of the right perfection condition stated for at proximity space, but it seems to me that in the biperfect case, a relation is essentially equivalent to a relation: to say that should be the same as saying for all . Under this translation, condition (2P) is just the usual condition in the definition of a uniformity, and is equivalent to (2).
Condition (1P), I believe, translates exactly to uniform regularity (combined with ).
Conditions (1) and (1) seem unreasonably strong: in addition to , they imply that all subsets of are almost located.
(continued…)
]]>Let’s see, here’s the syntopogeny condition:
() For any , there exists a such that if have the property that whenever , either or , then .
I can think of three natural (classically-equivalent) ways to contrapose this to a condition on relations:
(1) For any , there exists a such that whenever , there exist and such that , , and .
(2) For any , there exists a such that whenever , there exist and such that , , and .
(3) For any , there exists a such that whenever , there exist and such that , , and .
The version of (1) in the “simple” case () is that currently appearing under “Normality (constructive)” at proximity space. Of course, (2) and (3) are equivalent if we have symmetry. On the other hand, under (left) perfection, in all three conditions we may as well take . Moreover, under perfection it is natural to also consider the weakened versions where is a singleton:
(1P) For any , there exists a such that whenever , there exists such that and .
(2P) For any , there exists a such that whenever , there exists such that and .
(3P) For any , there exists a such that whenever , there exists such that and .
In (3P) we also may as well take , giving the equivalent:
(3P) For any , there exists a such that whenever we have .
Similarly, I can think of two (classically-equivalent) ways to translate () into a condition on relations:
(1) For any , there exists a such that whenever , there exist and such that , , and .
(2) For any , there exists a such that whenever , there exist and such that .
Of course, in (2) it is equivalent to take :
(2) For any , there exists a such that whenever , there exists such that .
These two (constructively) equivalent versions of (2) are the ones currently appearing under “Normality (constructive)” and “Normality (simplified)” at proximity space. Under (left) perfection, we can take in both conditions, and then it is natural to also consider the restricted versions where is a singleton:
(1P) For any , there exists a such that whenever , there exists such that and .
(2P) For any , there exists a such that whenever , we have .
(continued…)
]]>