|
In two related presentations, I will show how modern techniques from computer mathematics (type theory, geometric logic, formal topology, duality theory, etc.) lead to simpler proofs of old results which directly generalize in some unexpected directions.
- A simple constructive proof of Gelfand duality for C*-algebras (with Thierry Coquand)
- A topos presentation of algebraic quantum theory (with Chris Heunen)
We show how a C*-algebra naturally induces a topos in which the family of its commutative subalgebras becomes a commutative C*-algebra. Its internal spectrum is a compact regular locale, and the Kochen-Specker theorem is equivalent to this spectrum having no points. (Quasi-)states become integrals, and self-adjoint elements become functions to the pertinent generalised real numbers (the interval domain). This provides a probabilistic interpretation of propositions in quantum theory. The topos-theoretic truth value of such a proposition is the collection of pure states of commutative subalgebras that make it true; in a physical interpretation these are the pure states for a classical observer making the proposition true. These results were motivated by a topos-theoretic approach of the Kochen-Specker theorem by Isham and co-workers. Our main tool is the use of the internal mathematics of a topos, such as the constructive Gelfand duality of Banaschewski and Mulvey, which simplifies the computations and provides very natural connections between internal and external reasoning.
|