Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 11 / Issue 12

available in:   PDF (153 kB) PS (151 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-011-12-1932


Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems

Thierry Coquand (Chalmers University, Sweden)

Bas Spitters (Radboud University Nijmegen, the Netherlands)

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: Riesz space, axiom of choice, constructive mathematics, f-algebra, formal topology

Categories: F.1.1, F.4.1, G.1