Constructivity in Analysis and Topology

Programme (Abstracts: see below)

10:15-10:40 Douglas Bridges (Universität München and University of Canterbury, Christchurch, New Zealand),
Finite-dimensional locally convex spaces have a unique topology

10:45-11:10 Thomas Streicher (Technische Universität Darmstadt), Relating toposes and set theory via categories of classes

-break -

11:30-11:50 Vasco Brattka (Universität Hagen), Selection theorems for effectively Borel measurable functions
11:55-12:15 Peter Lietz (Technische Universität Darmstadt), Continuity principles in constructive mathematics

- lunch -

14:00-14:25 Helmut Schwichtenberg (Universität München), Witnesses in constructive analysis
14:30-14:50 Josef Berger (Universität München), From finite sets to continuous functions

- break -

15:30-15:50 Frank Rosemeier (Universität Hagen), Formalizing Bishop-style constructive mathematics withMartin-Löf's type theory
15:55-16:15 Peter Schuster (Universität München), On the scarcity of primes

Abstracts

Josef Berger (Universität München), From finite sets to continuous functions

A continuous function on a compact interval can be considered as a sequence of functions with finite domains, equipped with a modulus of continuity. We do constructive analysis in this setup, including differential equations.
Vasco Brattka (Universität Hagen), Selection theorems for effectively Borel measurable functions

We prove an effective version of the Bhattacharya-Srivastava Selection Theorem for effectively Borel measurable functions. This Theorem allows to generalize the Kreitz-Weihrauch Representation Theorem to all finite levels of the hierarchy of effectively Borel measurable functions. Moreover, we disucss an effective version of the Kuratowski-Ryll-Nardzewski Selection Theorem which indicates that multi-valuedness is less important in case of effectively Borel measurable functions of all higher levels.
Douglas Bridges (Universität München and University of Canterbury, Christchurch, New Zealand),
Finite-dimensional locally convex spaces have a unique topology

It is proved constructively that every n-dimensional real locally convex space is homeomorphic to the n-dimensional euclidean space. The key lemma embodies a recursive algorithm bounding points away from simplices in n-space.

Peter Lietz (Technische Universität Darmstadt ), Continuity principles in constructive mathematics

Continuity principles are statements of the form "Every function from X to Y is continuous, where X and Y range over certain classes of metric spaces". We examine a series of three increasingly strong continuity principles and give relatively easily described separating models. In the presence of the boundedness principle BD-N, the weakest continuity principle under examination implies the strongest, which is why the described models are also countermodels for BD-N.
Frank Rosemeier (Universität Hagen), Formalizing Bishop-style constructive mathematics withMartin-Löf's type theory

It is considered how Bishop-style contructive mathematics can be formalized with Martin-Löf's type theory and how they can be implemented in systems like Alf, Agda/Alfa, Coq, Isabelle/Isar, Lego or Yarrow.
Peter Schuster (Universität München ), On the scarcity of primes

The canonical covering relation for the point-free Zariski spectrum of a commutative ring can indeed be defined without any talk of points. We show that if for every ring there still were enough points to recover the covering, then the limited principle of omniscience would hold. This is a fragment of the law of the excluded middle which allows us to solve the halting problem for Turing machings, if only in principle. Our argument works both for concrete and formal points: that is, for prime ideals and prime filters, respectively.
Helmut Schwichtenberg (Universität München), Witnesses in constructive analysis

Constructive analysis is developed in such a way that witnesses have as low a type level as possible. This clearly is important for the complexity of extracted programs. For example, the Cauchy-Euler construction of approximate solutions to ordinary differential equations can be seen as a type-level one process.
Thomas Streicher (Technische Universität Darmstadt), Relating toposes and set theory via categories of classes

From work by Cole, Mitchell and Osius in the early 1970ies one knows that well-pointed toposes with natural numbers object (nno) are equiconsistent with bounded Zermelo set theory (bZ). The aim of our work is to go beyond a mere equiconsistency result by exhibiting a first-order set theory, bIZFA, such that every elementary topos with nno (whether well-pointed or not) appears (up to equivalence) as the category of sets associated with a model of bIZFA.

To obtain a set theory with such properties we are forced to modify ZF in three ways: (i) restrict separation to bounded formulas; (ii) use intuitionistic logic; and (iii) allow urelements/atoms.

It turns out that these are the only essential modifications we need to make to ZF, hence bIZFA: bounded Intuitionistic Zermelo-Fraenkel with Atoms. It is noteworthy that bIZFA retains the full (unbounded) collection axiom of ZF (in a strong form appropriate in the presence of bounded separation). This is made possible by the use of intuitionistic logic. (As is well known, under classical logic, collection implies full separation.)

As our main result we show that every elementary topos with nno provides a model of bIZFA.

The motivation for our work is to justify, in a mathematically precise way, the admissibility of set-theoretic figures of speech in situations where a universe of sets is not a priori available, i.e. we demonstrate ``how to fake a universe''. Such a programme has been suggested and advertised by S.MacLane in various talks over the recent years, with the aim of bringing together topos logic and the practice of the working mathematician.