Non-constructive principles which involve powersets

[Andrej Bauer]

In constructive math we care about implications between (potentially)
non-constructive principles and theorems. For instance, any
self-respecting constructivist can produce the proof of

LPO ==> real numbers are linearly order

when woken up in the middle of the night.

What are some such principles and theorems that use powersets and/or
impredicative notions in an essential way? Tarski's fixed point
theorem comes to mind, but that one is just true constructively. Maybe
something involving ordinals, or Borel hierarchies?

With kind regards,

Andrej

[Paul Taylor]

> What are some such principles and theorems that use powersets and/or
> impredicative notions in an essential way? Tarski's fixed point
> theorem comes to mind, but that one is just true constructively. Maybe
> something involving ordinals, or Borel hierarchies?

You do not need ordinals or Borel hierarchies to get this.

If I understand correctly what you are asking, impredicative notions
are ubiquitous and built into the common language of many kinds of
mathematics, principally because of the equation

infimum = greatest lower bound (supremum of all lower bounds).

The categorical jargon for this is the Special Adjoint Functor Theorem.

The (original?) proof of Tarski's fixed point theorem in a complete
lattice is an example of this, but there are many more in topology
and algebra.

I would say this is the principal objection amongst ordinary
mathematicians to the religion of predicativity.

Perhaps a predicative type theorist could explain to us how to
replace the ideas in topology and universal algebra that depend
on such ideas.

Paul Taylor

[WILLIAM TAIT]

On Mar 10, 2014, at 8:52 AM, Andrej Bauer <andrej...@andrej.com> wrote:

> What are some such principles and theorems that use powersets and/or
> impredicative notions in an essential way? Tarski's fixed point
> theorem comes to mind, but that one is just true constructively. Maybe
> something involving ordinals, or Borel hierarchies?

Inductive definitions---as you say, inductive definitions such as the second number class and Borel hierarchies---involve impredicative definitions, as does the existence of the least upper bound of a bounded set of reals.

Power set is a different matter and I can't think of an example at the moment other than Zermelo's use of it in his 1908 derivation of the well-ordering principle from AC. (I think it may have been the first mention of it.)

Bill

[Fred Richman]

I know this is totally irrelevant to the point of Andrej's post, but I can't let the major premise go unchallenged.

I didn't get into constructive mathematics in order to investigate the consequences of LPO. Or even propositions that imply LPO, which is (only) slightly more respectable.

--Fred Richman

[Andrej Bauer]

Thanks Paul, I should have thought of various completeness principles.

Existence of maximal ideals is also most naturally expressed using powersets.

And then there is the Heine-Borel property, which speaks of arbitrary covers.

What else? I'd also like some interesting implications between these.

For example: if every ideal is contained in a maximal one, does that
have any consequences for the Heine-Borel property? (I am asking
without thinking carefully.)

With kind regards,

Andrej

[Andrej Bauer]

On Mon, Mar 10, 2014 at 6:04 PM, Fred Richman <fr...@math.fau.edu> wrote:
> I didn't get into constructive mathematics in order to investigate the consequences of LPO. Or even propositions that imply LPO, which is (only) slightly more respectable.

I completely understand your position and sympathize with it. I am
asking because I am working on another case of "Bauer's thesis", as it
was called once: "Any computable mathematics worth doing is done
better in in the internal language of a suitable realizability model."

After having reverse-engineered some realizers into natural
constructive definitions, I am now looking for applications that go
beyond the scope of what has been done "with brute force realizers".
Powersets are always a good candidate because nobody does
realizability toposes with bare realizers.

With kind regards,

Andrej

[Martin Escardo]

You asked about principles and theorems. But some constructions rely on
impredicativity too.

An example you of course are aware of is that of Dedekind reals. You do
need some form of impredicativity to define them. In set-theory like
foundations for constructive mathematics, you use powersets (if they are
available). In type-theory like foundations, you have various options,
e.g. in HoTT you would invoke Voevodsky's resizing axioms, or accept
that your Dedekind reals are in the next universe (which means
side-steping impredicativity).

Martin

[Nicola Gambino]

> On 10 Mar 2014, at 20:09, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
>
> An example you of course are aware of is that of Dedekind reals. You do
> need some form of impredicativity to define them. In set-theory like
> foundations for constructive mathematics, you use powersets (if they are
> available). In type-theory like foundations, you have various options,
> e.g. in HoTT you would invoke Voevodsky's resizing axioms, or accept
> that your Dedekind reals are in the next universe (which means
> side-steping impredicativity).

Peter Aczel has shown that the class of Dedekind reals is a set in Constructive Zermelo-Frankel set theory (CZF). CZF is considered a generalised predicative theory, in the sense that it admits an interpretation (also due to Peter Aczel) into a Martin-Löf type theory with one universe and W-types. In particular, CZF does not have the power set axiom.

The proof that the Dedekind reals form a set uses in a crucial way the so-called Subset Collection axiom, which is a weakening of the Power Set axiom and a strengthening of the Exponentiation axiom (asserting that the class of functions from a set to another set is again a set).

Best wishes,
Nicola

[Erik Palmgren]

Some examples of use of power sets appears in formal topology. While this version of locale theory was
devised to take care of the impredicativity in the classical theory, there seems to be some places where
power sets would be natural. In type theory or CZF we have the following situation:

For example, the Sierpinski topology X has a only a class of points Pt(X). More
generally the morphisms Y -> X between two formal topologies form only a class. However if X has reasonably
strong separation properties (beyond T_1) the morphisms will form a set. See papers by Aczel 2006, Curi 2001 and myself.


Erik

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

[Thomas Streicher]

And Lubarsky has come up with a model of CZF without subset collection
where Dedekind reals are a proper class. But this model still validates
exponentiation.

On the other hand in presence of countable choice Dedekind reals
coincide with the Cauchy reals which do form a set anyway.

> The proof that the Dedekind reals form a set uses in a crucial way the so-called Subset Collection axiom, which is a weakening of the Power Set axiom and a strengthening of the Exponentiation axiom (asserting that the class of functions from a set to another set is again a set).

As already pointed out by Paul Taylor when doing abstract mathematics
(like complete lattices or locales) life gets really hard without
impredicativity. The same applies to point set topology as well.

Thus it seems disputable why one should forbid power sets unless one
is very anxious about foundations. However, proof theoretically there
is some reason to be suspicious about impredicativity because it renders
unwinding of proofs more difficult. But not as long as one considers
statements of the form \forall n \exists k A(n,k) where n and k
range over small types and existential quantification is encoded by
universally quantifying over this universe. The real problem comes up
when the existential quantifier is over non-small types.

Thomas

[Bas Spitters]

Of course, avoiding the powerset and working with presentations/sites directly has benefits for geometricity, as mostly emphasized by Steve Vickers.

http://www.cs.bham.ac.uk/~sjv/papersfull.php#LocTopSpaces

[Thierry Coquand]

>
> As already pointed out by Paul Taylor when doing abstract mathematics
> (like complete lattices or locales) life gets really hard without
> impredicativity. The same applies to point set topology as well.
>
> Thus it seems disputable why one should forbid power sets unless one
> is very anxious about foundations.

On the other hand, one can argue that locale theory and domain
theory are clearer when developed without or with limited use of
impredicativity.
For instance in domain theory, in the (predicative) form of information or neighborhood
systems, it is clearer that what matter
are the finite element of the domain, and that the general element of the domain should be thought of
as predicates on the set of finite elements. (For instance for solving a domain equations
D = A + [D -> D] one can directly describe the finite elements of this domain by an ordinary
inductive definition, which is arguably simpler than the limit/colimit description, and is also
simpler to use for proving an adequacy result, which is done by induction of finite element).


The issue is not to "forbid impredicativity", but to analyze where impredicativity
is really used and for what.
I believe that something similar happened in Bishop's mathematics. There was
no discussion of "impredicativity being forbidden", but in practice impredicativity
was almost never used.

Thierry

> However, proof theoretically there
> is some reason to be suspicious about impredicativity because it renders
> unwinding of proofs more difficult. But not as long as one considers
> statements of the form \forall n \exists k A(n,k) where n and k
> range over small types and existential quantification is encoded by
> universally quantifying over this universe. The real problem comes up
> when the existential quantifier is over non-small types.
>
> Thomas
>

[Bas Spitters]

I agree with Thierry, moreover, I once isolated two uses of impredicativity by Bishop:
 ---

I came across two instances where Bishop seems to be "impredicative". To be
precise, I mean where he uses the power set in an essential way.
* The Bishop-Cheng measure theory. He uses the space of all partial functions.
This can be "fixed" in a quite straight-forward way. See eg Feng Ye.
* The completion of a uniform space. It is in ex25 on p124 of Bishop and
Bridges. It seems that the answer Bishop has in mind is to use a construction
similar to the completion of metirc spaces, but instead of using Cauchy
*sequences* one would use all Cauchy *filters*. It is a priori not clear how
to carry out such a construction in, say, a predicative type theory or set
theory.

I am not sure what this means: Does Bishop "allow" the use of the powerset or
was he just being careless (if I may use that word).
---

http://www.cs.nyu.edu/pipermail/fom/2006-March/010301.html

Where similar issues were discussed.

[Steve Vickers]

To amplify slightly, point-free topology recognizes that a presentation
or site for a point-free space (such as that of the Dedekind reals)
already contains the information needed to say what the points and the
opens are. Briefly, it is describing a logical theory whose models are
the points and whose opens are the (geometric) propositions.

If one is willing to accept that that presentation "is" the space
(though of course there are other homeomorphic copies) then one can deal
with spaces predicatively.

The problem comes when one wishes to incorporate this point-free notion
of space into some other notion of collection, such as a set theory or a
type theory, that is meant to be all-embracing. Then it seems one
generally does need impredicativity to construct a set or type whose
elements are the points of a given point-free space (such as the
Dedekind reals). You might conclude that impredicativity seems
necessary; or you might conclude that the given theory of sets or types
was not as all-embracing as you thought - maybe the theory just needs to
be more comprehensive, or maybe the point-free spaces need to form a new
layer on top of the original sets or types.

I thought all this was well known (as formal topology) to predicative
type theorists, so maybe I'm missing a subtlety in the discussion.

Steve.

[Fred Richman]

Is Bishop's treatment of Borel sets predicative?

When you "fix Bishop in a quite straightforward way" is that like fixing a classical proof to make it constructive?

--Fred

[Thomas Streicher]

Dear Steve,

> The problem comes when one wishes to incorporate this point-free notion
> of space into some other notion of collection, such as a set theory or a
> type theory, that is meant to be all-embracing.

Thanks, that's precisely the point. I don't disagree with the fact
that geometric logic (like equational or Horn logic though pleasantly
stronger) provides an excellent DEFINITIONAL MECHANISM for a lot of
structures.
But though most algebraic structures (besides fields) are equational
one certainly cannot do algebra in equational logic. This applies even
more to topology.

I do agree that locales or Grothendieck toposes are a kind of natural
alternative to spaces but the category Loc or BTop_Set is not a universe
with sufficiently nice properties to work in it (it is not even a
regular category!).

It is also certainly true that Thierry and collaborators have made
excellent use of inductive presentations of bases for formal spaces
for constructivizing some topological arguments which as such are not
constructive.

But that doesn't mean that when developing constructive functional
analysis one should work with the formal reals or formal Banach spaces
etc. It is evident that this would be much more cumbersome.

But I think we had all this before already. Sorry for stirring it up again!

Thomas

PS I never understood why people were so fond of classifying
toposes. Sure, if we know that EE is the classifying topos B[T] of a
geometric theory T then we know that geometric morphisms of from FF to
EE correspond to models of T in FF. But it doesn't help one to reason
inside EE. Or has it been of any impact on simplicial homotopy that
the topos of simplicial sets is the classifying topos for linear
orders with endpoints. Not that I know of.
Another point in this vein is that categorists are fond of the fact
that many gadgets of their main interest appear as models of
essentially algebraic theories. This certainly gives one that free
such gadgets do exist. But it doesn't mean that topos theory can be
done in left exact logic.
My impression is that there is some "fetischism" going on which has
its origin in the dream of early topos theory that geometry is superior
to logic.

[Bas Spitters]

Feng Ye wrote a PhD thesis in the Princeton philosophy department reducing much of the Bishop/Bridges book to a conservative extension of PRA.

I believe it was this one:
https://sites.google.com/site/fengye63/strictlyfinitisticsystemforappliedmath

[Fred Richman]

Bas,

Thanks for the reference. Looks interesting. I guess that answers my second question in the affirmative.

I'm trying to analyze exactly what I meant by that second question. It is something like: if we try to "fix up" theorems of classical mathematics by rewriting them so that they admit constructive proofs, are we showing that classical mathematics was constructive all along? It is that analogy that makes me wonder about the sense in which Bishop was operating predicatively.

There is a story about Heraclitus who said that you couldn't step into the same river twice. His students went him one better and claimed that you couldn't even step into it once. That somewhat reflects my feeling about operating in weaker and weaker systems, although I must admit that I'm an advocate of rejecting countable choice.

When I first understood Bishop-style constructive mathematics, I thought it quite exciting and was convinced that mathematics should be done that way. It struck me, for example, as much more natural to reject the law of excluded middle than to reject the axiom of choice, which seemed like an unmotivated, boring, and technical thing to do. I don't sense the same excitement in those people who investigate predicative (and other) systems. They seem interested in the systems, not in the mathematics. I realize that the study of systems is also mathematics, but it's not like functional analysis, or even homotopy theory.

I've been accused many times of being a logician, and, once in a while, I start believing those accusations, at least to a certain extent. But when I read most of the things on constructivenews, I realize how far that is from being the case.

[Bas Spitters]

Dear Fred,

Different people have different reasons for developing mathematics predicatively.

As Steve, Thierry and I have mentioned there are good technical reasons for predicativity.
If you allow me some self-promotion, here is a recent paper where we crucially use predicative (geometric) methods in mathematical physics.
In this case, it just seems to be the best way to get to the results. I am not sure whether that makes me a logician, or whether that is a bad thing to be.
http://www.cs.ru.nl/~spitters/geoBS.pdf

Bas

[Giovanni Sambin]

Dear All,

I have been reading the discussion but couldn't write properly, since I am too busy (a talk tomorrow here in Christchurch, then flight back).

But I feel that I must answer to at least one claim by Fred. Being predicative (strictly, with no exceptions) for me it is not at all a matter of formal system, but absolutely the converse. Only with predicative mathematics I feel at ease and can follow what is going on. Impredicative arguments are always difficult to follow for me.

I have been developing topology  according to this attitude since '84. I have discovered that one can do (I mean, in practice, not just by a metamathematical argument) topology in a totally predicative framework. Not only that. To the contrary, I have discovered (beginning in  '95) that by being strictly predicative a lot of nice structures emerge, which were obscured before. I soon decided to write a book on that. But, contrary to Fred's feeling, there are so many new things coming out that the book is still on its way. I apologize for that. But wanted to inform Fred that his claim has (or will have) at least a counterexample.

Thank you for the attention

Giovanni

[Bas Spitters]

Dear Fred,

Maybe I was unclear before. My observation was that I only spotted two places where Bishop used impredicative methods (perhaps "by accident"?).

Feng Ye did a careful analysis of how to express all of Bishop's work in PRA. It deserves to be known that this is possible.

On the other hand, it is not how I would prefer to develop integration theory.

Here is a nice short motivation from Gian-Carlo Rota for algebraic probability, and in fact this is the way we have been developing it constructively, and a forteriori predicatively.

http://books.google.nl/books?id=eaJyGXguokIC&pg=PA58&lpg=PA58#v=onepage&q&f=false

Best,

Bas

[Steve Vickers]

Dear Thomas,

What you say about working in a category of point-free spaces does not accord with my own experience. Loc and BTop_S (even with S a generic base topos rather than assuming the classical S = Set) are nice enough to work in, and people do. Lack of regularity is just a fact of mathematics.

Neither is it so evident that doing constructive functional analysis is more cumbersome with formal reals and formal Banach spaces. For the reals at least there are good techniques for dealing with the formal reals, though formal Banach spaces are less well developed. The payoff is automatic continuity and good fibrewise behaviour of bundles, also that important results of topology are true.

It is misleading to characterize works such as Thierry's as using formal spaces "for constructivizing some topological arguments which as such are not constructive". Often the constructive point-free arguments are substantially different from the usual classical ones, without (in my opinion) being more cumbersome. In my own work I have been struck by the fresh arguments using powerlocales as hyperspaces.

As for classifying toposes, I would say this. Grothendieck understood toposes as generalized topological spaces essentially, as I understand it, because you can do algebraic topology with them. If you can identify a given topos as a classifying topos then you know what what its points are - what it is the generalized space of. This gives a rather clear intuition for what geometric morphisms are doing in terms of how they transform points. For example, let E be the object classifier. It classifies "sets", understood as objects of whatever topos you happen to be working in. Now by definition a geometric morphism f: F -> E is an object of F, but as a point transformer it transforms points of F to sets. If F is the topos Sh(X) then from one point of view f is a sheaf over X, while from the other it transforms points of X to sets: it is a "continuous set-valued map on X", albeit that that characterization doesn't make sense in ordinary topology. It still makes intuitive sense, though. The sheaf is equivalent to a local homeomorphism to X, a fibrewise discrete bundle over X, and then f(x) is the stalk, the fibre, at x.

I agree it's not clear how our understanding of simplicial sets is helped by knowing what the topos classifies.

All the best,

Steve.

[Fred Richman]

Giovanni,

It would seem that you have the excitement for predicative mathematics that I have missed. Personally, I have somewhat of a blind spot for impredicativity, although I recall once, when I was studying certain ordinal valued functions on abelian groups, which were closed under the taking of pointwise minima, that I was uncomfortable enough with the argument that there was a smallest one that I came up with an alternate description of the smallest one. I think I would agree with Peter that "in mathematical practice, impredicative definitions can be avoided to a large extent, often with little effort, by just being more sensitive."

I guess what bothers me about what tends to go by the name of constructive mathematics in this group is less the formality (which does bother me) than simply the emphasis on what might be called metamathematics, or foundations, rather than on mathematics.

[Erik Palmgren]

I think it is fair to say that it is mostly logicians or at least logically well schooled mathematicians
that take an interest in constructive mathematics in the sense of a globally worked out theory based on
intuitionistic logic. Locally constructive mathematics is of course done in almost every area when particular
calculations are required.

Maybe a few more beautiful books on constructive mathematics covering a standard undergraduate
curriculum of could widen the interest.

Erik

[Fred Richman]

Erik,

I noticed many years ago that the people most sympathetic to constructive mathematics tended to be logicians and computer scientists.

Recently I've experimented with a different explanation of what constructive mathematics is all about. Rather than emphasizing computation, which, after all, we only care about in principle (if at all), or intuitionistic logic, which is usually an immediate turnoff, I say that it is a systematic preference for direct proof over indirect proof. Presumably most mathematicians have some appreciation for that distinction, and it is easy to come up with examples to illustrate it. Of course the "systematic" part (your "globally worked out theory") eventually leads you to reject the law of excluded middle, but that is a consequence, not a motivation.

--Fred


----- Original Message -----
From: Erik Palmgren <palm...@math.su.se>
To: construc...@googlegroups.com
Sent: Wed, 12 Mar 2014 09:59:15 -0400 (EDT)
Subject: Re: Non-constructive principles which involve powersets

[Thomas Streicher]

Dear Steve,

I think we agree mathematically but disagree w.r.t.

1) what is simple and what isn't
2) the role of the ambient logic.

Thanks for pointing out that Thierry's work not only constructivized
existing topological arguments but that he also invented new such
arguments. It hasn't been my intention to deny this.

What really is the background of my complaints is that I don't see
what is the intended application of formal topology and related
approaches like yours. Do you suggest to redo constructive analysis in
a pointfree and prediactive way or do you reserves those methods for
topology beyong Polish spaces. I can see the point of the latter but
not of the former.
Quite concretely, I think it is a nightmare to rewrite the first
chapters of Bishop (and Bridges) in terms of formal topology. Just
think of introducing sine a cosine or logarithm in such formal terms.
I wonder whether anyone seriously want's to do this.

Thomas

[Martin Escardo]

On 12/03/14 21:34, Thomas Streicher wrote:
> Dear Steve,
>
> I think we agree mathematically but disagree w.r.t.
>
> 1) what is simple and what isn't
> 2) the role of the ambient logic.
>
> Thanks for pointing out that Thierry's work not only constructivized
> existing topological arguments but that he also invented new such
> arguments. It hasn't been my intention to deny this.

I have (temporarily?) suspended my thoughts about locale theory/formal
topology, to focus on recent interests. (And also because very few
people in the world were/are interested in this (less than I have
fingers to count).)

But I would like to make a few comments.

From my *personal* point of view (and (published) experiences with the
subject), in this particular case, impredicative arguments are more
natural (for what I did do and tried to do).

Formal topology = locale theory developed predicatively.

Formal topology is too "syntactic" to my personal taste. This is fine
when the applications are to algebra, like in Thierry's work. But when
the applications are to analysis and to (point-free) topology regarded
as a generalization of analysis, more generally, the predicative
calculations are possible but do seem to become cumbersome (although
some people enjoy them).

> What really is the background of my complaints is that I don't see
> what is the intended application of formal topology and related
> approaches like yours.

Well, if you are looking for "applications", you already are aware of
some.

In programming language semantics, logics and verification, developed
*non constructively* (as is the tradition in theoretical computer
science), the locales are the "logic of observable properties", their
formal presentations are their algebraic treatment, and their
corresponding topological spaces give the official "intended"
semantics of programs (perhaps in the form of domain theory).

(BTW, it is a *myth*, as you know, that theoretical computer
scientists are constructively minded (alluded to by Fred
Richman). Most of them are not. Most of them don't understand what
constructive mathematics is (not). And don't care. And even dismiss
it. The idea is that if you already have written a computer program,
there is no point in working hard to prove constructively that it
works. A classical proof is regarded as perfectly sufficient.)

> Do you suggest to redo constructive analysis in a pointfree and
> prediactive way or do you reserves those methods for topology beyong
> Polish spaces. I can see the point of the latter but not of the
> former. Quite concretely, I think it is a nightmare to rewrite the
> first chapters of Bishop (and Bridges) in terms of formal topology.

I will wait to see what Steve has to say about this.

But here is my take: I would suggest that (constructive and
non-constructive) analysis can and should be done in a point-free way.

Regarding the nightmare: This is what Hilbert told Brouwer, and then
came Bishop, who transformed the nightmare into a dream (for some).

What is needed, again, is somebody to rewrite analysis in a compelling
pointfree way. Arguments in this mailing list won't be enough.

> Just think of introducing sine a cosine or logarithm in such formal
> terms. I wonder whether anyone seriously want's to do this.

Ah! I think this is not a problem at all, once the right
infrastructure is introduced.

Any version of real analysis will need to begin with some
infrastructure (even the HoTT people have proposed what this
infrastructure ought to be in HoTT, although the HoTT infrastructure
hasn't been "tested" yet).

The infrastructure will always (even in the classical case) be a bit
artificial and "logically looking". But once this is settled, I expect
point-free real analysis (when it is done properly) to look very much
like point-set analysis.

Martin

[Erik Palmgren]

12 mar 2014 kl. 22:34 skrev Thomas Streicher:

Quite concretely, I think it is a nightmare to rewrite the first
chapters of Bishop (and Bridges) in terms of formal topology. Just
think of introducing sine a cosine or logarithm in such formal terms.
I wonder whether anyone seriously want's to do this.

Indeed, a direct development would probably be quite cumbersome. But there

are indirect methods.

As for the first chapters of these books one can employ the method of localic completion of metric

spaces introduced by  Steve Vickers 2005  which allows a translation of results 

between formal topology and metric spaces. Quite general results of this 

form are in some papers of mine if I may promote them here (see below). 

Open sublocales of localic completions. Journal of Logic and Analysis. 2(2010), 1 - 22.

Resolution of the uniform lower bound problem in constructive analysis. Mathematical Logic Quarterly, 54 (2008), 65 - 69.

A constructive and functorial embedding of locally compact metric spaces into locales. Topology and its Applications,154 (2007), 1854 - 1880.

Continuity on the real line and in formal spaces. In: L. Crosilla, P. Schuster, editors, From Sets and Types to Topology and Analysis: Towards Practicable Foundations of Constructive Mathematics , Oxford Logic Guides, Oxford University Press 2005. 

Erik

[Toby Bartels]

Martin Escardo wrote parenthetically:

>BTW, it is a *myth*, as you know, that theoretical computer
>scientists are constructively minded (alluded to by Fred
>Richman). Most of them are not. Most of them don't understand what
>constructive mathematics is (not). And don't care. And even dismiss
>it. The idea is that if you already have written a computer program,
>there is no point in working hard to prove constructively that it
>works. A classical proof is regarded as perfectly sufficient.

This suggests that computer scientists accept a sort of Markov's Principle.
In fact, if by "computer program" you mean a Turing machine
and by "it works" you mean that it has the specified output on all inputs
(although in reality computer programs are more than that),
then the idea that a computer program works if it doesn't fail
is precisely Markov's Principle.


--Toby

[Martin Escardo]

I think this goes beyond MP, when you consider computation with infinite
objects, e.g. higher type computation or "TTE". For termination, you can
e.g. use compactness or well-ordering principles in a non-constructive
way (essentially or non-essentially).

Martin

[Toby Bartels]

Martin Escardo wrote in part:

>I think this goes beyond MP, when you consider computation with infinite
>objects, e.g. higher type computation or "TTE".

Sure, this is one reason that I wrote

>>in reality computer programs are more than that

But it still strikes me as a SORT of Markov's Principle.
(Arguably, Excluded Middle is also a sort of Markov's Principle,
but my hope is that this sort is not be quite as strong as that.)


--Toby

[Steve Vickers]

Dear Thomas,

Yes, the dream is indeed to redo everything point-free and predicative. That includes analysis, domain theory, and even toposes as generalized spaces. You can see it set out in "Topical categories of domains", and the major part of my work since the 90's has been case studies to test out its scope.

You say it would be a nightmare to rewrite Bishop. Obviously it's a huge task, but it's the analogue of the task that Bishop himself faced: How do you make practical mathematics out of such stringent rules? In Bishop's time I think people were saying roughly what you are saying now, that intuitionistic mathematics was just too cumbersome. Bishop had some better ideas than that.

As Martin pointed out, a lot of the trick is to build a good infrastructure of top of which the mathematics can be somewhat as it always was, but with the addition of novel techniques (e.g. hyperspaces). The work so far on predicative point-free spaces gives us plenty of clues as to what is needed.

Here are a couple of examples of how to proceed.

1. You ask about sin, cos, log. I can sketch how I would attack log, at least. First define exponentials x^y (x > 0). This is roughly what one learns in school. Start by dealing with the case where y is a natural number, by using iterated multiplication. Multiplication is already known geometrically for Dedekind sections, but we do need to account for the iteration. Next extend to y a non-negative rational using roots, got by inverting powers. Next extend to y a rational, using division. Now by the nature of Dedekind sections we hope to extend to arbitrary real y by continuity. Once x^- is defined, I think you can get log to base x without too much pain.

Note that frames are not mentioned (it's meant to be predicative). Moreover, the closest one gets to presentations of frames is that the reals are specifically characterized as Dedekind sections - because that's what the presentation of formal reals tells us that a real is. Throughout the reasoning needs to be geometric, because that allows us to reason in terms of points. I've been working with the geometric mathematics so long that it has become second nature to me, but it is definitely hard for newcomers to see what the ground rules are. Bas will probably confirm this! Hence a big part of the necessary infrastructure would be a formalization of the geometric mathematics and rules. (But ... see my discussions on arithmetic universes. The full geometric logic with its "arbitrary set-indexed" disjunctions may be the wrong target. This will give you even worse nightmares, of course.)

2. When Bishop defines compactness (for example), he does not directly translate the usual notion but instead adopts a non-trivial theorem that gives an equivalent condition of total boundedness in the restricted case of metric spaces. I would say that is a weakness: it is restricted and ad hoc. By contrast, impredicative point-free topology has a general definition that straightforwardly translates the traditional one. This can be made predicative, in terms of generators and relations, but, and more usefully, can be expressed in hyperspace terms using existence of a particular point in the upper powerlocale. The intuition is clear: as point of the hyperspace it is a compact subspace Y of the original space X; and the particular conditions on Y ensure that it contains all (geometrically) the points of X and so is the whole of X. When applied to my localic completion of metric spaces, this compactness is equivalent to a total boundedness condition. Erik showed how to make a mathematical equivalence between Bishop's account and mine.

All the best,

Steve.

[Thomas Streicher]

Dear Martin and Steve,

thanks for your mails. I guess the infra structure is provided by a
result of Fourman where he showed that the gros topos over the
category of separable locales is a model of INT. In INT you have bar
induction which gives you the missing points. By Kripke-Joyaling you
can translate everything to the language formal topology if you really like.

So INT is a kind of high level language which can be translated into the
machine/assembly language of formal topology. I was asking whether
there is some benefit in doing so. Must say I haven't received an
answer that would convince me.
It's true that constructive analysis is often more cumbersome than
classical analysis but one is rewarded for this effort by getting
witnesses. A similar benefit I don't see when doing things in a point
free way.

One should keep in mind that Grothendieck introduced his toposes as
generalisation of spaces because there were things he couldn't do with
sober spaces. That's a good reason I would say. I was hoping for
something similar in case of formal topology.

Best, Thomas

[Bas Spitters]

For reference, here is a recent paper by Mike Fourman on the topic, which of course is connected to the work by Martin.

http://homepages.inf.ed.ac.uk/mfourman/research/publications/pdf/fourman2013-continuous-truth-II.pdf
http://www.cs.bham.ac.uk/~mhe/papers/xu-escardo.pdf

One place where one needs a more general approach is for (spectra of) non-separable spaces, like von Neumann algebras.

More generally, one wants to avoid sequential reasoning. Fred has also been arguing for this. Steve mentions Bishop's compactness.

[Erik Palmgren]

Dear Thomas

13 mar 2014 kl. 12:19 skrev Thomas Streicher:

So INT is a kind of high level language which can be translated into the
machine/assembly language of formal topology. I was asking whether
there is some benefit in doing so. Must say I haven't received an
answer that would convince me.
It's true that constructive analysis is often more cumbersome than
classical analysis but one is rewarded for this effort by getting
witnesses. A similar benefit I don't see when doing things in a point
free way.

I think there are examples where extra witnesses are produced in the formal setting.

Consider uniformly continuous map f:[0,1] -> (0,+oo). If regarded as point-function between

metric spaces we can in BISH not find a uniform lower bound, as we can in

INT or CLASS.  However if we consider f as continuous morphism between 

formal topologies (suitable subspaces of the formal reals), this lower bound can be 

found  (in BISH)  from its inverse using a covering compactness argument.

Best regards

Erik

[Thomas Streicher]

Dear Erik,

that's a nice example. But it is a reformulation of the problem, isn't t?
I moreover wonder whether there is a systematic translation between
"normal" and point-free. As I understand it it is a creative reformulation
already in case of locales.
There is the adjunction between Locales and Spaces but that doesn't really
preserve too much of structure. At least it is not used when reformulating
a topological question in point free terms as e.g. Tychonoff.

I am not at all against locales or even point free topology. But one
should make it clear that one builds up a sort of parallel world which
undeniably has its own beauty. But as longs as one considers csm's I don't
see the advantage. For those problems type 2 computability in particular in
the form of function realizability seems to be much more convenient.
Moreover, representing a point of an abstract space as an approximating
sequence with a modulus of convergence is much more useful than a filter
of open neighbourhoods. Well, if this filter is enumerated with a modulus
of convergence then it amounts to the same but then why go via formal
topology?

Thomas

[Martin Escardo]

On 13/03/14 11:19, Thomas Streicher wrote:
> It's true that constructive analysis is often more cumbersome than
> classical analysis but one is rewarded for this effort by getting
> witnesses. A similar benefit I don't see when doing things in a point
> free way.

Bishop said that general topology cannot be done constructively (and
then called it pseudo generality), in his preface to his book. This may
well be the case for point-set topology.

The benefit of the point-free setting is that you can do topology
constructively, including the Tychonoff theorem and many other things
that are not possible in the point-free approach.

And Erik gave you examples of desirable facts, including witnesses, that
do take place when you work point-free, but fail in a point-set approach.

And Thierry and collaborators replaced point-set topological arguments
in algebra by point-free ones to get constructive theorems in algebra.

This is particularly interesting, because the formulations of the
theorems don't use topology; only their proofs do. When you replace a
point-set proof by a point-free proof, you keep the formulation of the
theorem in algebra unchanged. Then you get witnesses in algebra by
working point-free in your topological arguments. So we revert to your
(p)referred benefit above.

But you were asking specifically in the case of analysis, for which
Erik's is the best answer/example so far.

M.

[Bas Spitters]

But in this case, you would obtain a similar (the same?) witness via Fourman (/Troelstra/Kreisel/Moerdijk/...)'s "compilation".

The "fan rule". Thomas, is this what you are asking about? Or do you want an example from analysis where this does not work?

[Thomas Streicher]

> But in this case, you would obtain a similar (the same?) witness via
> Fourman (/Troelstra/Kreisel/Moerdijk/...)'s "compilation".
> The "fan rule". Thomas, is this what you are asking about? Or do you want
> an example from analysis where this does not work?

Right, the fan rule or even bar induction do the same job and hold in
function realizability. And there I can use the internal language and
reason about points even if they aren't such. That's the very point of
the internal language, isn't it?

Thomas

[Bas Spitters]

Thomas, are you in fact asking about examples *in analysis* where the csm approach (function realizability) does not work so well?

If so, I would suggest comparing Bishop/Bridges' measure theory (Ch6) and their approach to spectral theory (Ch7.8) with the pointfree approach.

Also, the work on commutative Banach algebras (Ch9) has a pleasant pointfree presentation, it is implicit here:
http://www.logicandanalysis.org/index.php/jla/article/view/84/33

Interestingly, this uses some of Bishop's ideas.

Perhaps, one way of understanding some of the work in formal topology is to try and build a better/more general compiler.

[Giovanni Curi]

Dear Andrej,


> What are some such principles and theorems that use powersets and/or
> impredicative notions in an essential way? Tarski's fixed point
> theorem comes to mind, but that one is just true constructively.


you may find results of this kind in:


- G. Curi, "On Tarski's fixed point theorem". Submitted

- G. Curi, M. Rathjen, "Formal Baire space in constructive set theory." In:
Logic, Construction, Computation.
Ontos Verlag, Frankfurt (2012), pp. 123-135

- G. Curi, "Topological inductive definitions". APAL, 163 (2012), pp.
1471-1483

- G. Curi, "On the existence of Stone-Cech compactification". JSL, 75, 4
(2010), pp. 1137-1146.

- G. Curi, "On some peculiar aspects of the constructive theory of
point-free spaces". MLQ, 56, 4 (2010) pp. 375-387

(available through http://www.giovannicuri.com/).


The paper "On Tarski's fixed point theorem" moreover contains a constructive
and predicative version of Tarski fixed point theorem (a revised version,
that ought to be more accessible to the non-specialist reader, will soon be
available).
Theorem 2.5 of this paper and its corollaries give simple examples of
results of the kind you are looking for.

The slides of the talks:

- "Intuitionistic theorems that fail constructively" (Kanazawa 2010)

- "Independence results in constructive set theory and constructive type
theory" (Vienna 2011)

(also available at www.giovannicuri.com/) summarize some of those results,
and present the general program of identifying theorems from standard areas
of mathematics that can be proven in fully impredicative (classical or
intuitionitic) systems, but cannot be derived in the main systems for
constructive predicative mathematics.

With best regards,

Giovanni Curi

[Thomas Streicher]

I think a lot of the jobs done by formal topology are done bar
theorem/recursion in a way that avoids the point-free view.
I think one of the reason for developing formal topology was that bar
recursion/induction doesn't fit into the framewoek of MLTT type theory
since it can't be formulated as structural recursion over an
inductively defined data type.
But it does make sense as a program and thus can be used for
extracting programs (or bounds) from proofs in INT.

I think this answers the question I brought up. Of course, there are
also - as always - aesthetical preferences which may be the actual
motivations.

Thomas

[frank waaldijk]

Sorry for arriving late at this thread. It contains some interesting viewpoints, which I cannot not comment on :-) .

@pointfree vs pointwise constructive topology

Allow me to repeat that I believe NToP (Natural Topology) to be a fertile mix of pointfree and pointwise constructive topology. It allows for the same inductive compactness results as formal topology, but it seems to me simpler in some important ways. Since we work with a countable set of basic dots, one obtains points simply as sequences of sufficiently-shrinking dots. This is entirely in the Bishop-style of pointwise mathematics. Bar induction is very natural, since all spaces are seen to arise as (sub)quotient spaces of Baire space under a Sigma_01 apartness relation.

(I have always wondered why in formal topology the set of basic opens is not assumed to be countable to begin with; and subsequently why points are so complicated. Since if we work with sequences of sufficiently-shrinking neighborhoods then we can obtain both the pointwise and the pointfree setting. I do not believe that doing analysis in a way which is completely rewritten for formal topology will be attractive, or even feasible. It might be possible to do some translation, but this is not how I would want to practice analysis myself.) 

I also think that NToP is very suitable for exact-computational purposes, it seems to correspond rather well to recommendations in [BauerKavkler2009]. 

Therefore I disagree with Martín's comments that certain results cannot be obtained in Bishop-style pointwise topology. They already have been obtained.

It would be nice to (finally) get some in-depth comments on NToP...criticism is also highly appreciated.

@Fred: I also sometimes wonder if this group is about constructive mathematics or about constructive-math-related metamathematics. My own interests are primarily with the first. Perhaps I can add to this interest with the following question:

Does anyone know of constructive results for polyhedral approximation of n-dimensional manifolds in R^{n+1}? Say for example we have a uniformly continuous embedding of D_n or S_n in R^{n+1}, can we construct a non-self-intersecting polyhedral approximation of the image?

Best wishes,

Frank