Topology and Analysis: Proof and Computation

Department of Mathematics and Statistics, University of Canterbury, New Zealand

Schedule of talks

• Mon 29/11: 2-2.45, Douglas Bridges: Three constructive versions of Riemann's permutation theorem for series
• Wed 01/12: 9.30-10.15, Giovanni Sambin: Foundational reasons for pointfree topology
• 10.30-11.15, Giovanni Sambin: New information brings new structures in topology
• Thur 02/12: 9.30-10.15, Erik Palmgren Constructive aspects of nonstandard analysis 1
• 10-30-11.15, Erik Palmgren Constructive aspects of nonstandard analysis 2
• 2-2.45, Viggo Stoltenberg-Hansen Domains and domain representability
• 3.00-3.45, Viggo Stoltenberg-Hansen
• Fri 03/12: 10-30-11.15, Milly Maietti: The intended semantics of the minimalist foundation for constructive mathematics
• 2-2.45, Francesco Ciraulo The `overlap' relation in intuitionistic lattice theory

Abstracts

• Bridges: Riemann's famous theorem about permutations of infinite series of real numbers splits into (at least) three constructively inequivalent statements. I shall discuss all three, paying particular attention to the third, and much the trickiest to handle, whose constructive status seems intimately linked to a simple boundedness principle (BD-N) for sets of positive integers. Some of this work is still in progress.
• Sambin 1: I will give arguments to support the claim that the point-free approach to topology is a necessity both for epistemological well-foundedness and for computer implementation. No preliminary knowledge of topology is assumed, since the same ideas can be seen in the specific example of real number. The key point is a distinction between real and ideal entitities, which in two different level of abstraction. I will hint at the fact that this approach serves on one hand as a rigourous foundation of constructive mathematics and on the other hand it admits almost automatic implementation in a proof assistant.
• Sambin 2: I will give a description, although from a bird's eye perspective, of which new structures you get by keeping on the scene some information which is usually considered irrelevant: keeping bases for a topology brings symmetry to surface, keeping the witness of existential statements (that is, using intuitionistic logic) brings to a primitive notion of closed subset which is different from complement of open, and keeping the distinction between sets and collections brings to the notion of formal space as different from a concrete space. In particular, one obtains an embedding of pointwise topology into the pointfree one, which is an improvement even on the classical situation, where one usually has an adjunction (between Top and Loc). This puts with the rigour of category theory that traditional topology with points is less general that the pointfree topology one gets constructively.
  Note: Some knowledge of topology and of category theory is assumed in this talk.
• Palmgren 1 and 2: Classical non-standard analysis was introduced by Abraham Robinson (1966). It was built on a logically sophisticated and non-constructive theory. Some years before Robinson Laugwitz and Schmieden had introduced a far more intuitive and direct approach - the so called Omega-calculus, in which one deals with sequences of real numbers introducing a natural equivalence, and extending the real operations. An infinitesimal is simply a sequence whose members go to zero. In the Omega-calculus one may give natural definitions of continuity, both pointwise and uniform, and Cauchy's theorem to the effect that the pointwise limit of continuous functions is continuous, can be turned correct, with a natural interpretation in the Omega-calculus. In fact one may formulate a weaker condition than uniform convergence to ensure continuity of the limit.
  In the second half of the talk we discuss the limitations of this model from both a constructive and a classical point of view, and its relations to issues in reverse constructive mathematics.
• Stoltenberg-Hansen 1 and 2: We present a general method to study computability and effectivity on possibly uncountable structures such as the field of real numbers or metric spaces. Effectivity on such structures is obtained via recursion theoretic computability on "concrete" approximations of the elements of the structure. For such a structure we build an effective Scott-Ershov domain that "includes" both the original structure and its approximations and then apply the general theory of effective domains to induce effectivity on the original structure. We start by giving an introduction to (effective) domain theory.
• Maietti: In constructive mathematics no foundation has become the standard reference for formalizing its theorems, as it happens for Zermelo-Fraenkel axiomatic set theory with respect to classical mathematics. In collaboration with G. Sambin, we decided to propose a two-level minimalist foundation to serve as a common core among existing constructive foundations. In this talk I will outline the intended semantics of the minimalist foundation which makes it compatible with classical predicative mathematics, contrary to what happens with other relevant foundations used by constructive mathematicians.
  I will also discuss the importance of building a constructive foundation with (at least) two levels: one serves as the set theory where to formalize theorems as usual and the other serves as the programming language where to extract their non trivial computational contents (which is a distinctive property of constructive proofs versus classical ones).
• Ciraulo: I shall show that some classical results on lattice theory can be given a constructive (hence intuitionistic) proof provided that the language of lattices is enriched with a new primitive relation (satisfying some suitable axioms): the so-called `overlap relation'. I shall describe what is called 'an overlap algebra' and compare it with the notion of a complete Heyting algebra, especially with respect to the problem of providing a satisfactory algebraic description of intuitionistic powersets. Then I shall present a few further uses of the overlap relation: new constructive analogues to Boolean algebras; a Stone-like representation theorem for overlap algebras with respect to regular open sets (in both pointwise and pointfree topology); a positive version of the least dense sublocale of an overt locale; a new positive analogous of the Dedekind-MacNeille completion (for lattices equipped with an overlap relation).