Constructive Pointfree Topology Eliminates Non-constructive Representation Theorems from Riesz Space Theory

Abstract

In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that Archimedean almost f-algebras are commutative. The proof is obtained relatively straightforward from the proof by Buskes and van Rooij by using the pointfree Stone-Yosida representation theorem by Coquand and Spitters. © 2010 The Author(s).