Observational integration theory
by
Bas Spitters
University of Nijmegen, Nijmegen, The Netherlands

In this talk I will present a constructive theory of integration. The theory is constructive in the sense of Bishop or Brouwer, however we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos. To be more precise we outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem. This talk illustrates the general theme of developing mathematics observationally, connecting ideas by Kolmogorov, von Neumann and Segal on the one hand and point-free (aka formal) topology on the other. This provides a nice illustration how ideas from logic (proof theory) can be used to obtain mathematical results. By generalizing Isham ideas on quantum theory we find that this integration theory is also applicable in the non-commutative context.

Date received: May 23, 2007