Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 19, 2008

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).

Posted at May 19, 2008 7:51 AM UTC

TrackBack URL for this Entry:

0 Comments & 0 Trackbacks

Post a New Comment