JUCS - Journal of Universal Computer Science 11(12): 1932-1944, doi: 10.3217/jucs-011-12-1932
Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems
expand article infoThierry Coquand‡, Bas Spitters§
‡ Chalmers University, Sweden§ Institute for Computing and Information Sciences, Radboud University Nijmegen, Netherlands

Corresponding author: Thierry Coquand ( coquand@cs.chalmers.se )

© Thierry Coquand, Bas Spitters.
This article is freely available under the J.UCS Open Content License.
Citation: Coquand T, Spitters B (2005) Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. JUCS - Journal of Universal Computer Science 11(12): 1932-1944. https://doi.org/10.3217/jucs-011-12-1932
Open Access
Abstract
We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.
Keywords
formal topology, constructive mathematics, Riesz space, f-algebra, axiom of choice