Topology and Analysis: Proof and Computation
In connection with our EU Marie Curie IRSES award we are holding a symposium on Topology and Analysis: Proof and Computation.
The talks are being held in Room 446, Erskine Building between November 29 2010 and December 3 2010. Most of the talks are aimed at nonspecialists, so anyone interested in topology, analysis, or foundations may find some of them of interest and will be most welcome to join us.
Photos, provided by Erik Palmgren
Douglas Bridges (University of Canterbury)
Three constructive versions of Riemann’s permutation theorem for series
Monday, 29 November 2.10pm – 2:55pm
Room 446, Erskine Building
Abstract. 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.
Giovanni Sambin (Universitá di Padova, Italy)
Foundational reasons for pointfree topology
Wednesday, 1 December 9.30am – 10:15am
Room 446, Erskine Building
Abstract. 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.
Giovanni Sambin (Universitá di Padova, Italy)
New information brings new structures in topology
Wednesday, 1 December 10.30am – 11:15am
Room 446, Erskine Building
Abstract. 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 statments (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.
Erik Palmgren (Uppsala University, Sweden)
Constructive aspects of nonstandard analysis
Thursday, 2 December 9.30am – 11:15am
15 minute break at 10:15am
Room 446, Erskine Building
Abstract. 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.
Viggo Stoltenberg-Hansen (Uppsala University, Sweden)
Domains and domain representability
Thursday, 2 December 2.00pm –2:45pm
15 minute break at 2:45pm
Room 446, Erskine Building
Abstract. 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.
Anton Hedin (Uppsala University, Sweden)
The domain-theoretic derivative in formal topology
Thursday, 2 December 3.00pm –3:45pm
15 minute break at 2:45pm
Room 446, Erskine Building
Abstract. The theory of formal topology can be seen as a generalization of (constructive) domain theory. I will explain this relationship and talk about the possibility to develop some of the theory of domain theoretical differential calculus constructively. In domain theory it is possible to define a total differential operator for continuous functions on the domain of real closed intervals. This is in sharp contrast to the situation in classical analysis. I will show that this is possible also constructively by considering continuous functions on the formal space of partial reals.
Milly Maietti (Universitá di Padova, Italy)
The intended semantics of the minimalist foundation for constructive mathematics
Friday, 3 December 10.30am – 11:15am
Room 446, Erskine Building
Abstract. 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).
Francesco Ciraulo (Universitá degli Studi di Palermo, Italy)
The ‘overlap’ relation in intuitionistic lattice theory
Friday, 3 December 2.00pm – 2:45pm
Room 446, Erskine Building
Abstract. 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).
