A topos for algebraic quantum theory

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.