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 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.

References in corpus (3)

• A topos for algebraic quantum theory
• Intuitionistic quantum logic of an n-level system
• Constructive Gelfand duality for C*-algebras