Formally continuous functions on Baire space and the principle of point-free continuity

[frank waaldijk]

Dear all,

having read Tatsuji Kawai's preprint Formally continuous functions on Baire space and Tasuji Kawai & Giovanni Sambin's preprint The principle of point-free continuity , I feel obliged to point out the following:

a) I'm glad that this way of looking at things is finally gaining a wider circle than just me...(!)

b) I'm sad that it seems that noone reads Natural Topology (NToP), especially since in my eyes the main results of the above mentioned two preprints, and much more, is covered in NToP. At least a reference would have been nice.

c) what adds to b) is that I myself over the years have read countless publications by authors on this list, often struggling very hard to make sense of scattered definitions, scattered or lacking foundational references, unclear terminology, unresolved foundational issues etc etc etc. This effort I gladly continue to make, unpaid, mostly unrecognized, with the only intention to understand what others are thinking.

So my question is:

Would it really be such a waste of anyones time to sit down and read a clear, self-contained book that has as its only objective to simplify and unify constructive mathematical practice?

Thank you for kindly considering this question,
best wishes,

Frank

[Henri Lombardi]

> Le 13 mai 2018 à 12:41, frank waaldijk <fwaa...@gmail.com> a écrit :
>
> b) I'm sad that it seems that noone reads Natural Topology (NToP), especially since

I have read your https://arxiv.org/pdf/1210.6288.pdf (NToP)
and found it is a very nice and very natural approach

but for the moment I’m not able to see what should be a simple and clear book
as an introductive textbook to constructive analysis

my reference is always Bishop

even if we might hope something
more uniform, more simple, without dependent choice,
perhaps without « points » ?
perhaps with ideal nonstandard elements ?

the mystery of the constructive real line is always here !

Note:
If we want to understand à la Bishop what is a continuous function
from N^N to N
we have to give a modulus of uniform continuity m near to each compact subspace of N^N

since a compact subspace is included in a basic compact (sequences bounded by an
element of N^N)
we see that in order to give a Bishop-continuous function f: N^N \to N
we have to give a well defined operation m: N^N \to N
is there any hope that m would be Bishop-continuous ?
and that an inductive definition
would be adequate for Bishop-continuous functions f: N^N \to N ?

could this help to « solve » the mystery of the real line ?

Henri

[frank waaldijk]

Dear Henri,

thanks for your kind response.

Perhaps the biggest aim of NToP is to retain and salvage as much as possible from Bishop's (& Bridges' !) formidable book on constructive analysis. I will refer to this book as FCA, although I always read the later version (Constructive Analysis) brought out by Douglas. (Also, perhaps too unmodestly, I consider myself one of Bishop's biggest admirers.)

You are right that there is a lot of work to be done in order to show that one can indeed combine the pointwise approach of FCA with the pointfree inductive approach (essentially Brouwer's), even if one does not want to accept bar induction as an axiomatic principle.

But this is discussed quite thoroughly in NToP, and I am confident that NToP gives a very solid approach to analysis, using morphisms (essentially Brouwer's spread-functions) and genetic-inductive definitions/machinery (essentially Brouwer's bar induction but simpified and incorporated into the definitions, rather than imposed as an axiom). I show for instance that any continuous_BIS real function can be represented by an inductive real morphism,  and vice versa that any inductive real morphism represents a continuous_BIS real function. A much sharper theorem is presented in my (rejected after a 3.5 years review process, for very unclear reasons...) article Exact computation over topological spaces .

I also show that with respect to FCA, NToP does at least as good a job as what formal topology has to offer. In my opinion even a much better job, since NToP allows a pointwise approach, which for analysis seems far better suited.

Still, I have some reserves in what is possible without accepting bar induction as an axiom. But I did come up with another possible way of reuniting FCA with Brouwer, through work of Kleene (whom I admire if possible even more than Brouwer). SO I asked the question, both on Mathoverflow and on FoM, if it is possible that Kleene proved Brouwer's axioms on the meta-level for the formal system FIM, when one combines this with realizability results. I have not had one single answer, only Bas Spitters asked for some elucidation.

------

Now for your question on modulus-of-continuity:

In chapter 4 of my PhD thesis modern intuitionistic topology , actually thm. 4.4.2, it is proved for INT that every continuous function from a spreadlike metric space to another metric space has a modulus of continuity. The proof uses the Michael Selection Theorem (intuitionistic version, the proof of which is almost completely valid in BISH as well, except for the use of a Lindelöf property. In NToP this property is incorporated in the definitions, so one would expect to be able to prove some version of thm. 4.4.2 for BISH  as well.).

Throughout my thesis, the paragraphs that are directly valid in BISH have been marked with an asterisk, and they are I believe in the  majority.

There is no longer a good reason, in my not so humble opinion (well...as a mathematician I can be obnoxious but as a person I'm not so self-assured I assure you), to reject Brouwer's work to the extent as what has been common in BISH. Thanks largely to Kleene (and to Wim Veldman, at least for me!)  there is no longer anything mystic about Brouwer's axioms. His topological-analytical machinery (spread-functions, bar induction) is very very adequate, even if there are some improvements to be found. 

But in the end my own heart lies in Bishop's direction: constructivize as much as possible of classical mathematics, in such a way that any mathematician (classical, applied, or whatever) can see its appeal (to which I personally add: `and use it in a coherent and foundationally sound way'.).

Thanks again for your interest and positive attitude,

best wishes Frank

[Steve Vickers]

Dear Henri,

It's true that there is still (as far as I know) no single choice-free point-free text on constructive analysis, but there is accumulating evidence that much analysis goes through in a natural way. The central idea is that "point-free" does not have to mean working with impenetrable structures that abandon all geometric insight of points. Rather, it is that the set of points as in point-set topology is replaced by a (geometric) theory of which the points are the models. Then the points can be validly used as long as one's constructions respect the logical constraints of geometric logic (essentially: use colimits and finite limits).

Topos theory gives us strong reasons for working point-free. One is that toposes as generalized spaces don't really make much sense point-set. Another comes in when you work with bundles instead of individual spaces. Bundles have the pleasant property of just being internal spaces in the topos of sheaves of the base, *provided you work point-free*. It's point-free topology with sets replaced by sheaves.

It's easy to look at point-free topology and think it's too difficult. Frank has said this to me. However, the good reasons for using it don't go away and most of my own work this century has aimed at giving natural point-free reasoning.

For those whose reference is always Bishop, Palmgren has made a connection between Bishop's metric spaces and my own point-free account of "localic completion". Bishop has an apparently ad hoc technique of turning theorems into definitions in order to ensure that spaces have the properties that we really need. Palmgren's translation enabled him to compare those with the definitions that naturally arise point free, and show that Bishop's definitions could be recovered as theorems about the localic completions.

In "The connected Vietoris powerlocale" I gave a choice-free point-free account of the Intermediate Value Theorem and Rolle's Theorem, using R as localic completion of Q, and showed how one single narrative using points (including points of hyperspaces) could be interpreted in two inequivalent ways to give a point-free result and a classical point-set result.

To conclude, then, how far does this go in solving "the mystery of the constructive real line"? What are the mysteries that still need to be solved if this point-free approach is to prove itself?

I haven't said anything about Baire space. Clearly there is a point-free notion of continuous map from N^N to N, as N is locally compact so N^N exists as a point-free space. (Doesn't go to higher order, of course, as N^N is not locally compact.) There are point-free spaces of Cauchy sequences, with point-free surjections to the localic completions, so I speculate that there's scope there for getting more concretely computational accounts of Dedekind real analysis.

Best wishes,

Steve Vickers.

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

[Frank Waaldijk]

dear Steve,

thanks again for your continued interest! Allow me to improve something you wrote:

It's easy to look at point-free topology and think it's too difficult. Frank has said this to me.

I do not recall saying this at all...but this is best explained by replicating my email to which you refer below:

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 

I'm reneging a bit on the dilettante part, by the way, since it seems there are few people who take the time to really study INT and Brouwer's topological methods in order to understand to see that Brouwer and Freudenthal were already quite advanced in their pointfree approach. In my thesis the pointfree approach to apartness is also very explicitly studied.

Best wishes,

Frank

---

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

 

> To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.

[frank waaldijk]

For clarity let me therefore summarize:

NToP is completely point-free, but it allows the familiar pointwise thinking in analysis, since points arise as an enumerable sequence of shrinking quasi-neighborhoods (which I prefer to call 'dots', to honor the original and wonderful idea of Wim Couwenberg, that forms the basis for NToP). NToP spaces can be thought of as quotients of Baire space for a Pi^1_0 equivalence relation (or better a Sigma^0_1 apartness).

It is proved in NToP (using only a Lindelöf property which is valid in CLASS, INT and RUSS) that at least for all Polish spaces: 

(*) Every continuous function from a Polish space to a natural-topological space can be represented by a natural (pointfree) morphism

So in answer to Steve's remark on Baire space: yes, every continuous function from Baire space to itself can be represented by a natural morphism. Brouwer already knew this and his spreadfunctions are the embodiment of this knowledge.

Friendly greetings,

Frank

[Steve Vickers]

Dear Frank,

It's true I didn't have your message in front of me when I wrote, but let me pick out your view that "formal topology is way too complicated for the 'basic' constructive spaces".

As an observation of how manipulations get done at a low level, I think this is self-evidently true. Likewise the frame manipulations of locale theory and the categorical manipulations of topos theory, which in addition have the foundational fragility of being impredicative, or at least expressed impredicatively.

Twenty years ago, inspired by a technique Johnstone used in a proof, I started exploring the use of geometric logic to "combine pointfree with pointwise thinking", as you put it. The idea is that you can validly use points to prove point-free results, as long as the reasoning is geometric. The points are described as models of a geometric theory, and maps are described by geometric constructions (colimits and finite limits) on points. There are metatheorems available to show that that high-level pointwise reasoning can then be compiled down to valid low-level point-free results using locales and toposes, and I hope with my arithmetic universe approach we are not far off doing the same for predicative formal topology.

That's not the same as an approach using Baire space, but I agree Baire space looks likely to come in useful when discussing actual algorithms and computations, and we have a point-free treatment of it.

Foundationally, the geometric approach is very robust. It is predicative and choice-free (except for unique choice). How adequate it is for capturing analysis still remains to be fully tested out, but so far there is a lot of positive evidence.

I mentioned one case study, in "The connected Vietoris powerlocale", where a single pointwise discussion yields valid proofs of inequivalent point-set and point-free results (for the Intermediate Value Theorem and Rolle's Theorem). An interesting practical technique was that hyperspace methods turned out to be very effective.

So:

Cross-platform stable? Yes.

Clear? Yes.

Foundationally sound? Yes.

Not too complicated? Yes.

Oops! Sorry, I meant to let you fill those in. Anyway, see what you think.

All the best,

Steve.

[Steve Vickers]

Dear Frank,

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.

On the other hand, it is possible to get point-free spaces of Cauchy sequences and define evaluation maps ev: Cauchy sequences -> Dedekind sections.

Moreover, ev is surjective in a point-free sense. That's not to say that every Dedekind section can be got as ev of a Cauchy sequence; we would need some choice to be able to choose one. Nonetheless, the Cauchy sequences are dense enough that maps on them can be used to give maps on all Dedekind sections. Specifically, ev is a triquotient surjection, and hence the coequalizer of its kernel pair. This is in my old Imperial report "Localic completion of quasimetric spaces" http://www.cs.bham.ac.uk/~sjv/papersfull.php#LocCQS, a forerunner of my localic completion papers.

I used similar trick recently in my interval object paper http://www.cs.bham.ac.uk/~sjv/papersfull.php#IntervalNote, by showing that an evaluation map ev from Cantor space 2^ω to [0,1] is a proper surjection, and the equalizer of two maps from finite sequences 2^* to 2^ω. ev treats a point of 2^ω as an infinite sum of signed powers of 1/2.

I conjecture that results like these give a better point-free computational handle on Dedekind sections.

Regards,

Steve.

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

[sasa...@cage.ugent.be]

Dear Frank,

I would like to point out one small but nasty detail regarding your latest
email. You wrote the following:

> It is proved in NToP (using only a Lindelöf property which is valid in
> CLASS, INT and RUSS) that at least for all Polish spaces:

> ...


The statement "only a Lindeloef property" is a poor choice of words, at least
from the classical point of view: Dag Normann and I show in the below
arxiv paper
that to prove even just the original version of the Lindeloef lemma,
one classically
needs *full second-order arithmetic*.

https://arxiv.org/abs/1711.08939

Similarly, the open-cover (aka Heine-Borel) compactness of the unit interval
(involving uncountable covers) classically requires full second-order
arithmetic.
Before people roll their eyes at CLASS, this observation is directly
relevant to constructive math as follows:

We all have an intuitive understanding of "easy versus hard" to
compute/prove. There are
whole disciplines devoted to answering the question "how hard is X to
compute compared to Y",
resulting in various "scales". What Dag Normann and I have shown is
that the "scale" originating from Bishop's mathematics is
fundamentally different from the "scale" originating
from classical mathematics:

In the constructive math community, open-cover compactness (say of
[0,1) is called "semi-constructive" or even "more constructive" than
the sequential compactness of [0,1] (which is equivalent to LPO). See
Beeson's book, Diener's PhD thesis, etc for such claims.

Now, the functional 2E embodies the BHK-interpretation of LPO, but 2E
is *nothing* compared to
the Heine-Borel compactness of [0,1] in classical math: indeed, the
latter requires full second-order arithmetic for a proof, while 2E
lives *way* below that (namely at the level of ACA_0/PA).

Although I generally do not endorse this kind of language, let me put
it this way: if 2E/LPO is a taboo, then Heine-Borel is -classically at
least- tantamount to mass murder.

Best,

Sam




----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

[frank waaldijk]

dear Sam,

the Lindelöf property that I referred to adheres to the axiom BDD (Bar Decidable Descent, introduced and explained in my paper On the foundations of constructive mathematics).

BDD says: every bar on Baire space descends from a decidable bar

To prove this classically, one certainly does not need more than LEM. In INT the axiom BDD follows from AC_10 (Continuous choice). In RUSS it can also be proved not too difficultly.

So BDD would not appear to be all that nasty as you fear. Still, one cannot prove it in BISH (I say this without proof but ...).

On the other hand the main relevance of BDD for this discussion lies in showing that the notion of `natural morphism' adequately captures the notion of `continuous function'.

Best wishes,

Frank

[Frank Waaldijk]

dear Steve, you write:

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.

but I don't understand, since NToP is as I said completely point-free. And yet, one easily describes quotients in NToP. And also, please let's not focus so often on Cauchy sequences since that is one of the most inefficient and inelegant ways of building real numbers. Brouwer's way is already quite efficient, but in NToP there is an even more efficient way.

So perhaps you mean that for the point-free approaches that you are familiar with, it is hard to describe quotients. I'm taking a liberty here by surmising that in those approaches one does not have a point-free apartness relation.

In my thesis I studied point-free apartness relations in the context of INT. Since noone apparently wants to be seen wasting her/his time on INT (after all, who still takes Brouwer seriously, in this day and age?), Wim Couwenberg and I set out to build up a completely point-free approach in BISH which turned out to be both a (slight) generalization of Brouwer's spreads and a specialization. The specialization concerns extremely efficient morphisms, generally quite more efficient than Brouwer's spread-functions, especially in the presence of a non-trivial apartness relation like on the reals.

So the ingredient which I miss in the few point-free developments that I have had time to study (just a bit I admit), is a point-free notion of apartness. Actually, as I mentioned in the book NToP, I came across a nice unpublished paper by Thierry Coquand (1996 if I recall correctly, also the year in which my thesis came out) in which Thierry suggests (I have to look this up again but I'm pretty sure it's close) that it would be worthwhile to study the advantages of adding a point-free notion of apartness to the point-free topology he was discussing (I forget if it was formal topology or something else).

*******

Anyway, I do not presume to know enough about geometric logic to see whether it should or could be preferred to NToP. You write that it is:

Cross-platform stable? Yes.

Clear? Yes.

Foundationally sound? Yes.

Not too complicated? Yes.

So perhaps I should be bold enough to relinquish my personal pride in NToP and say:

I don't care which point-free development we pick... as long as it is elegant and it really works on all levels.

(and my marketing department tells me that I should run an ad campaign: Forget about NToP!! :-) )

So thanks again Steve. If it works, I'm all for your approach, I have to admit that what you write sounds very attractive.

Best wishes,

Frank

---

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

 

To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.

[Steve Vickers]

Dear Frank,

Why should apartness be an issue, point free? Apartness on R - as the Dedekind reals - is an open subspace of RxR, and equality is its closed complement. I can't see any problems there.

Steve.

[Kreinovich, Vladik]

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.

[Frank Waaldijk]

Sure, but the sequence of embedded intervals is much to be preferred, since this can be done quite bloody efficiently :-) That is what I was trying to say,

all the best, Frank

---

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

 

[Kreinovich, Vladik]

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.

[frank waaldijk]

I don't see any problems either :-) , that is why NToP works.

But seriously, I meant that introducing an abstract apartness relation between basic 'opens', 'neighborhoods' or 'quasi-neighborhoods' is a very useful tool. This tool allows for efficiency and elegance I believe. For instance in the filtering property, when defining points, a lot is gained by having the apartness relation already given on the basic 'opens' etc.

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.

[frank waaldijk]

Oh, I see... but what I mean is that we can work with a sequence of standard diadic (binary) intervals with at least a standardly decreasing diameter instead of working with all rational intervals and any convergence speed. And then it still is or represents a Cauchy sequence, but at least one has thrown out all the very very inefficient representations.

[Kreinovich, Vladik]

Agreed, this is (almost) exactly how Bishop’s version differs from what was done before.

[Ingo Blechschmidt]

Dear Vladik,

On Thu, May 17, 2018 at 08:55:17PM +0000, Kreinovich, Vladik wrote:
> 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.

in the case that the real number is determined by a physical experiment
which we envision to carry out with higher and higher accuracy, one
might actually argue that the number is *not* given by a Cauchy
sequence: A Cauchy sequence always has to return the same
epsilon-approximation for any positive rational error bound epsilon, but
performing the same experiment twice might yield different outcomes in
each case.

Thus one could argue that a physical real number is not given by a
Cauchy sequence, but by a Cauchy *process*, which could for instance be
modeled by a function alpha : Q^+ --> P(Q) from the positive rationals
to the powerset of the rationals. Intuitively, alpha(eps) is the set of
all possible outcomes of the experiment when carried out to precision
eps. [*]

One should then require the usual consistency condition (for any
positive rationals eps and eps', and any values x in alpha(eps) and x'
in alpha(eps'), we should have |x - x'| <= eps + eps') and define an
equivalence relation on the set of Cauchy processes.

Any Cauchy sequence gives rise to a Cauchy process, by postcomposing
with {} : Q --> P(Q), but in the absence of the axiom of countable
choice, a Cauchy process might not be induced from a Cauchy sequence.

Does the construction using Cauchy processes give rise to a new kind of
reals? No. It turns out that the resulting set of reals is isomorphic
(as a metric ordered ring with apartness relation) to the set of
Dedekind reals.

This construction doesn't seem to be as well-known as the constructions
involving sequences, cuts, or higher inductive types; I'm writing to
draw some attention to it, even though it's obviously impredicative and
not point-free. I think Cauchy processes are quite nice because they are
just as easy to handle as Cauchy sequences, but don't come with their
deficiencies. In particular, defining multiplication is a bit simpler
than with the Dedekind reals. They have been studied under the name
"Cauchy approximation", probably first by Banaschewski and Mulvey in
their work on Banach spaces internal to toposes.

Cheers,
Ingo

[*] Haskell programmers could substitute the powerset monad by the IO
monad, for true nondeterminism like in physical experiments.

[Steve Vickers]

Actually, in the point-free result I cited, I assumed a canonical rate of convergence with d(x_m, x_{m+k)) < 2^{-m}. Those were the Cauchy sequences I referred to.

Steve.

[Steve Vickers]

Dear Ingo,

On the face of it, the way physicists deal with their experimental
results is more subtle, as they use Gaussians to describe the error.

Conceivably that requires a different theoretical notion of what a real
is, though I don't know of any work along these lines. Have you seen
anything like that?

All the best,

Steve.

[Bhup Anand]

Dear Steve/Ingo,

I argue along seemingly parallel lines (albeit from a different, evidence-based, perspective) that if mathematics is to be treated as, and given the respect due to, a lingua franca for the applied sciences, then we may need to perforce define reals formally as `Cauchy processes'.

See:

(a) Part 5, Chapter 23 (Section 23.5, p.198 and Section 23.7, p.200); and

(b) Part 7, Chapter 27 (Section 27.6, p.232 and Section 27.7, p.233);

of the thesis:

Three Dogmas of First-Order Logic

https://www.dropbox.com/s/58lv1tc0w307uli/39_Anand_Dogmas.pdf?dl=0

Regards,

Bhup

======================

-----Original Message-----
From: construc...@googlegroups.com [mailto:construc...@googlegroups.com] On Behalf Of Steve Vickers
Sent: Friday, May 18, 2018 3:31 PM
To: ibl...@web.de
Cc: constructivenews
Subject: Re: Formally continuous functions on Baire space and the principle of point-free continuity

[Kreinovich, Vladik]

In some cases, yes, we know that the measurement errors are normally distributed, and this is what is taught to engineering students in Engineering 101, but an experimental analysis shows that only about half of measuring instruments are normally distributed. A very frequent situation is when we do not know the probability distribution, the only information that we have about the measurement errors is the upper bound on the absolute value.

This happens in two cases: state-of-the-art measurements and measurements on the shop floor. In the first case, the impossibility to find a probability distribution is caused by the fact that to find this distribution, we need to compare measurement results with results of more accurate ("standard") measuring instrument, and for state-of-the-art measurements, the instruments that we use are the best. In such situations, the best we can do is come up with upper bounds.

In shop floor measurements, we could potentially calibrate every sensor by finding its probability distributions, but this costs much more money than buying the sensors -- so people do not do it.

Dealing with the resulting interval data is common in practice, it is also the subject of the whole area of interval computations, see, e.g., http://www.cs.utep.edu/interval-comp, a research area that Yuri Matiyasevich called applied constructive mathematics -- because of the similarity between intervals and representation of reals in constructivism.

Yes, true, if we know the probability distribution -- or if we have partial information about probabilities -- the problem becomes more complicated, see, e.g., Vladik Kreinovich, Andrzej Pownuk, and Olga Kosheleva, "Combining
Interval and Probabilistic Uncertainty: What Is Computable?", in:
Panos Pardalos, Anatoly Zhigljavsky, and Julius Zilinskas (eds.),
Advances in Stochastic and Deterministic Global Optimization,
Springer Verlag, Cham, Switzerland, 2016, p. 13-32.
http://www.cs.utep.edu/vladik/2015/tr15-66a.pdf

-----Original Message-----
From: construc...@googlegroups.com [mailto:construc...@googlegroups.com] On Behalf Of Steve Vickers
Sent: Friday, May 18, 2018 4:01 AM
To: ibl...@web.de
Cc: constructivenews <construc...@googlegroups.com>
Subject: Re: Formally continuous functions on Baire space and the principle of point-free continuity

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

[frank waaldijk]

dear Ingo,

it seems to me that there is absolutely no good reason to assume that one can measure the same physical quantity twice.

The old saying is: one cannot cross the same river twice. And it reflects a very true scientific phenomenon: everything is constantly changing. So if you ask me, I would describe your situation as follows:

There is an somewhat unknown physical quantity q for which we have no guarantee that it does not fluctuate/decay/increase ever so slightly over time. We attempt to measure q using measuring instruments which probably are both inherently inaccurate and subject to auto-oscillating. The first measurement yields a finite sequence of interval approximations to what for convenience we model as a real number. The second measurement yields a similar finite sequence, but it would in my eyes be already most optimistic to assume that the first and second approximation intervals keep on overlapping...

The introduction to NToP starts out with exactly such a situation, in which an engineer is measuring a physical quantity. The NToP-approach is a generalization of interval computation, I believe, making it is directly suited for applied mathematics. This is explained further and really specified in the paper 'Exact computation over topological spaces' mentioned above with link.

Best wishes,

Frank

[frank waaldijk]

(dear Ingo,) to be precise, as I forgot to mention:

in your situation we are not dealing with one real number coming from a fixed physical quantity, but we are dealing with two real numbers coming from our two measurements of this (probably changing) physical quantity. And then your objection disappears.

[Steve Vickers]

Dear Frank,

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.

That's not an a priori reason, of course. Alternative theories might allow the number to vary with time or according to the observation made.

What this means is that the impossibilities in the definition of - let's say Dedekind - real number (essentially: for any rational r it is impossible to observe both r < q and q < r) provide Popperian falsifiabilities for the theory.

Steve.

--

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.

[Frank Waaldijk]

dear Steve, you write:

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.

but I respectfully disagree, for two reasons:

a) Predicting that we can model something as a fixed quantity is absolutely not the same as experimentally `establishing' that we are dealing with a fixed quantity. There is a vicious circle here: how to falsify this theoretical prediction? which is related to b) below:

b) Notwithstanding a), we still obtain our measure approximations through our instruments which as I said are fallible, and definitely not fixed (auto-oscillating). Therefore it is really quite possible that our approximations yield two different real numbers... which in my eyes contradicts what you write above.

For practical purposes it will probably not matter all that much since we cannot go beyond the finite level, but for myself I like to have a sharp framework expressing what I believe to be our fundamental incapacity to *prove* that science is right. It all remains a human assumption, if you ask me, which yields amazing results as well as spectacular failings.

best wishes, Frank 

---

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

 

To unsubscribe from this group and stop receiving emails from it, send an email to constructivenews+unsubscribe@googlegroups.com.

[Steve Vickers]

Dear Frank,

Here's the line of argument.

1. Theory (that includes theory of the instruments as well as theory of the science) predicts that a variety of observations are measuring a single real number.

2. The definition of real number says that certain combinations of observed properties are inconsistent.

3. If you ever do get such inconsistent properties for what your theory says is a single real number, then there's something wrong with the theory. That's the Popperian falsification.

4. Otherwise, and provisionally, you continue to accept the theory, and that is your good reason to assume you are measuring the same quantity twice.

I wrote more on that in "Issues of logic, algebra and topology in ontology", which examines the ontological commitment of geometric logic. It expands on what I said in the first couple of chapters of "Topology via Logic". Geometric logic is a positive logic, and its formulae do not include connectives for negation or implication. Nonetheless, they are needed at some level, and appear as sequents used to provide the axioms in a geometric theory. The formulae are understood as observations, while the sequents are background assumptions. Any sequent of the form "formula |- false" provides a possible falsification of the theory, if the formula is observed.

Regards,

Steve.

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.

[Andrej Bauer]

To bolster Steve's points, le me just notice that nowhere does he, or
anyone else, claim to have "experimentally `establishied' that we are
dealing with a fixed quantity", or that we are that we even think
that's possible. I am not sure what Frank is trying to say or why he
is bringing up something that appears to be a strawman.

With kind regards,

Andrej

[Frank Waaldijk]

dear Andrej,

actually I think we are all knowledgeable and careful enough to understand the issues surrounding physical experiments. So what remains in my eyes is just that we tend to phrase things differently, and look at them from (sometimes just slightly) different perspectives.

Without (I hope!) giving the impression that I think to know everything better, let me explain what I meant to say as follows:

Let q be a physical quantity. I think that both of the following statements  `q is a fixed quantity' and  `q is not a fixed quantity' cannot a priori be assumed to have a scientifically valid basis.

For this I repeat my earlier remark: there are many situations in which neither of these statements can be falsified in a Popperian way. Let me explain what I mean by this: suppose we can only measure q with a precision up to \epsilon. Then we cannot falsify the statement `q fluctuates over time within a margin of 1/4 /epsilon' but for the same reason we cannot falsify `q does not fluctuate' either.

In my eyes, for the argument that Ingo was giving, already `q fluctuates over time within a margin of 1/4 /epsilon' is enough to reject the idea that we are measuring the same real number twice.

However, as I understand what Steve said, it is of course quite valid to see different measurements as approximations to the same real number (assuming that q is fixed `enough', because it doesn't really matter so much for most of our theories if q is fixed or oscillates with unmeasurable small amplitude). And I understand that this is a much easier intuitive way of handling most physical theories. BUT: specifically for Ingo's argument, I disagree that these measurements should behave the same each time in the way that a fixed Cauchy-modulus works.

When looking at it purely mathematically, I think it is simpler, more direct and also more reflective of what we really do when measuring, to consider each measurement as a `separate' real-number-in-progress (rnip). Of course, something does not add up if these rnips are seen to lie apart, but that is for later consideration (usually we blame our instruments, sometimes we reject the theory).

If we do so, Ingo's objection disappears, I believe. That was my main point.

Anyway, as interesting as these things are, they also distract a little from the point-free topic that we were discussing.

Unfortunately I am rather overwhelmed at this time by non-mathematical responsibilities, so for the next week at least I will only be able to reply summarily and not in a very timely fashion to follow-ups in this topic.

Best wishes,

Frank

---

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

 

[frank waaldijk]

Before I forget: the unpublished paper by Thierry Coquand that I referred to earlier is called Formal Topology with Posets

[frank waaldijk]

And Thierry's suggestion that I referred to, to start with a pointfree apartness, is the QUESTION on page 2.

[Andrej Bauer]

Dear Frank,

thank you for your explanation.

There indeed seems to be a difference of how we use words, mostly. A
statement such as

"The mass of an electron is constant and all electrons have the same mass."

has a scientific basis, namely the theory which describes our
understanding of the world. This is different from an experimentally
verified fact, I think we can all see this. As I said, nobody has
suggested that constancy or non-constancy of the mass of an electron
can be experimentally verified. However, this does not render the
working assumption that this is indeed the case useless or
non-scientific. It is a valid scientific method to act upon the
consequences of the best available theory that has so far not been
discredited (experiments are only one way of discrediting a theory,
and the whole process of paradigm shift is a bit more complicated than
"Frank observed two different masses of electrons, therefore we throw
particle physics out of the window").

But we're moving very far away from constructive mathematics here. I'd
still prefer to know how to prove uncountability of reals without
using countable choice.

With kind regards,

Andrej

[Steve Vickers]

Dear Andrej,

I know this is not the question you asked, but of course you know
already that the answer is easy if you only consider continuous maps.
There's no homeomorphism between the reals and any space with discrete
topology, countable or otherwise - just show that the interior of {0} is
empty.

If (as I do) you work point-free, then that's job done. Countability,
equivalence with N (or a finite set), is not simply a matter of "size",
but also of topology.

It's only if you have mechanisms for working with the set of reals, and
allowing discontinuous isomorphisms, that the question becomes non-trivial.

So the metaquestion I would like to ask you is, What would you say is
the interesting maths that appears to depend on analysing the set of
reals and discontinuous maps? That's not a rhetorical question, because
actually there's lots. Cohomology, for instance, also schemes. The
affine real line as a scheme does not have the Euclidean topology on its
closed points. In my dreams I imagine there might be ways round, but I'd
like to understand better what I'm up against. We already know, for
instance, that Palmgren has found a firm link between Bishop's metric
spaces and my localic completion. That suggests that some of Bishop does
can be transferred to a point-free style.

All the best,

Steve.

On 20/05/2018 15:31, andrej...@andrej.com wrote:
> ...

> But we're moving very far away from constructive mathematics here. I'd
> still prefer to know how to prove uncountability of reals without
> using countable choice.

> ...