It's easy to look at point-free topology and think it's too difficult. Frank has said this to me.
Thanks Steve, I will have a read.My own view on pointwise vs pointfree in constructive topology is not so clear-cut as yours :-). I think I understand why many people prefer pointfree approaches, but...I'm a slow thinker, and very sensitive to details. So, philosophically I would not hesitate to say:`in the end everything is pointfree'to indicate my belief that we cannot understand (let alone manage) infinity. But mathematically, I find I have a much more intuitive understanding of an approach which combines pointfree with pointwise thinking. And I so far have had too hard a time when checking whether purely pointfree approaches are a) really predicatively constructive b) adequate wrt analysis and topology, and other math areas. [`adequate' covers a vague combination of `cross-platform stable, clear, foundationally sound, not too complicated,...)You may have seen some critical remarks I posted about formal topology in this regard. I'm becoming more and more convinced that formal topology is way too complicated for the 'basic' constructive spaces, and moreover that there are serious issues with cross-platform compatibility and foundational soundness (especially regarding predicativity and transfinite induction).So, until I come across a purely pointfree approach that adequately meets these criteria, I find myself more attracted to Brouwer's approach which is in fact a very clever combination of pointfree and pointwise thinking. Its cleverness (or elegance if you prefer) partly becomes apparent when considering a smooth transition from theory to computation. This can in fact be done seamlessly, even directly yielding computational efficiency. The reason for this is that morphisms can be elegantly coded as elements of Baire space themselves.However, to be fair, I cannot to mathematics even devote a fraction of the time that you and many others spend on these questions, so it seems highly likely that I'm somewhat of a dilettante, missing important parts of the bigger picture. For this I try to apologize from time to time...but I'm also obstinate enough to think that a `good' approach should have enough simplicity to make it explainable to someone like me.We'll see :-)To be continued...best wishes,Frank
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.
--
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.
One thing I should mention about point-free approaches is that is quite hard to describe spaces as quotients of other spaces. We cannot say, for instance, that real numbers "are" Cauchy sequences modulo an equivalence, which I am guessing would be similar to how your sequences of shrinking quasi-neighbourhoods work. We define the real line R as the space of Dedekind sections and then it has a good point-free topology.
Cross-platform stable? Yes.
Clear? Yes.
Foundationally sound? Yes.
Not too complicated? Yes.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.
This may be true, but this is how computable real numbers come from real life: we have a value x of a physical quantity, we can measure it with higher and higher accuracy – or we have a number like pi and we can compute it with higher and higher accuracy if needed to compute f(x) for some algorithm x. In all these cases, Cauchy sequence is what we get – or, equivalently, a sequence of embedded intervals converging to the desired number.
Why is there a big difference? In one case, you have the rational numbers r_n for which |r_n – x| <= 2^{-n}, in another case we have an interval [r_n -2^{-n}, r_n + 2^{-n]], they can easily transferred between these two representations.
I think what you mean is not Cauchy sequences Bishop-style, where we just have r_n as above, but Cauchy sequences in the style of some older pre-Bishop definitions, Markov-Shanin-style 1960s, when you have r_n and a modulus of convergence so that for every k, this gives n_k for which |r_{n_k} –x |<= 2^{-n}. In this case, I agree, this definitely much more cumbersoms
--
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.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
Agreed, this is (almost) exactly how Bishop’s version differs from what was done before.
--
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.
The good reason is that the underlying physical theory predicts that we can. It predicts that a variety of observations will be tantamount to getting approximations of a single, fixed real number q.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.