Munich, Monday 28 March 2011
Monday 28 March 2011, 09:00-13:00 and 15:00-19:00
Universität München, Hauptgebäude (Geschwister-Scholl-Platz 1), Room A 017
| 09:00-09:45 | Douglas Bridges | "Two or Three Disparate Problems in Constructive Analysis" |
| 10:00-10:45 | Masahiko Sato | "Formalization of Mathematics of Metamathematics" |
| Break | ||
| 11:30-12:15 | Alex Simpson | "Towards a Constructive Theory of Randomness" |
| 12:30-13:00 | Matthew Hendtlass | "On the Construction of General Equilibria" |
| Lunch | ||
| 15:00-15:45 | Thomas Streicher | "Brouwer Meets von Neumann" |
| 16:00-16:30 | Iosif Petrakis | "A Constructive Proof of Dickson's Lemma" |
| Break | ||
| 17:15-18.00 | Josef Berger | "The Fan Theorem for Pi-0-1-Bars" |
| 18:15-19.00 | Dieter Spreen | "On an Idea of Martin-Löf" |
| Dinner |
Coffee/tea cannot be provided but may be taken in cafes around
Places for lunch/dinner will be announced during the workshop
There will not be any free food/drinks nor will there be a fee
Douglas Bridges, "Two or Three Disparate Problems in Constructive Analysis"
I shall outline two or, if time permits, three problems that have occupied me lately. The first is the extension of weak-operator continuous linear functionals; the second, the search for decent notions of precompactness and compactness for an apartness space; and the third, the construction of a product of two frames with an appropriate apartness structure. It being the earliest talk of the day, perhaps the first two of these problems will be more than enough.
Alex Simpson, "Towards a constructive theory of randomness"
Recently, I have been working on an approach to randomness based on point-free topology. Given a probability measure on a topological space, there is a canonical "subspace" of random elements. The quotes are there because this "subspace" is not itself an ordinary topological space, but rather the point-free analogue of a subspace, a sublocale. My preliminary results in this programme have been obtained in a classical metatheory. In this talk, I will discuss prospects for the constructivisation of these results, and mention some envisaged applications of such a constructivisation.
Thomas Streicher, "Brouwer meets von Neumann"
One could imagine to develop basic quantum theory (as in von Neumann's classical book) in an intuitionistic framework `a la Brouwer, i.e. in the function realizability topos RT[K_2]. We prefer to proceed externally, i.e. work in the full subcategory QCB_0 (introduced independently by M. Schroeder and A. Simpson) which hosts both separable Hilbert space H and the Hilbert lattice L of closed subspaces of H. Since QCB_0 hosts also the unit interval we can speak about states of L and also about L-valued valuations on objects X corresponding to observables with values in X.