Integrals and Valuations using Geometric Logic
Posted by Urs Schreiber
guest post by Bas Spitters
Thierry Coquand and I have
just released the paper Integrals and
Valuations.
In this paper we investigate the theory of integrals and measures(=valuations) motivated by both topos (or locale) theory and the theory of operator algebras. Not surprisingly this was precisely we needed for our work on a topos for algebraic quantum theory.
In classical (set-theoretical) treatments of integration theory one starts with a collection of integrable functions defined on a set and defines an integral on this. The integral has to be defined in such a way that if the function is changed on a null-set, then the value of the integral remains the same. So, in fact, we work on a quotient defined by these null sets. Segal and Kunze (Integrals and Operators) taught us that such a theory can be developed conveniently in an algebraic way by working with a certain commutative algebra (of abstract functions) and a positive linear functional (an abstract integral). This then defines a commutative von Neumann algebra (similar to the famous GNS construction for C*-algebras). Hence this is commutative non-commutative measure theory!
Such a treatment of integration theory is also convenient when working in a topos. Classically, one then represents such an algebra as an algebra of (continuous) functions. However, in a topos one uses locale maps. So we relate an algebras of formal functions to maps between formal opens.
In a topos there are various definitions of real numbers (as discussed by Peter Johnstone last week in London).An integral is a continuous function from the set of the continuous functions (with sup-norm) to the reals. Hence it should be presented in a topos as a function to the Dedekind reals. On the other hand, a measure (or valuation) is only lower semi-continuous. It values are thus in the lower reals.
To give a topos-valid proof of the Riesz representation theorem of the correspondence between integrals and measures we define two geometric theories: one for integrals and one for valuations. We then define maps between them in geometric logic. By the classical Riesz representation theorem we then know that the composition of those two functions is the identity on points (=models of the theories). By completeness of geometric logic we know (classically) that there must be a constructive proof of this fact, but no algorithm to find such a proof is given. In the paper we present such a proof.
This result is used in `a topos for algebraic quantum theory’ to connect states on a C*-algebra to integrals on functions internal to a topos and finally to valuations. These valuations allow us to define the state-proposition pairing for quantum theory, not dissimilar to the use of generalized truth objects by Doering and Isham (which were discovered independently).