Constructive Stone representations for separated swap and Boolean algebras

Abstract

Swap algebras generalise Bishop's complemented powerset as Boolean algebras generalise the powerset. Actually, all Boolean algebras are swap algebras. We prove constructively a Stone representation theorem for separated swap algebras of type (II), where the notion of a separated swap algebra generalises the corresponding notion of a separated Boolean algebra. Moreover, we prove a Stone-Cech theorem for swap algebras of type (II), showing that the restriction to separated swap algebras is not a loss of generality from the point of view of the theory of swap characters. A constructive Stone representation theorem and a Stone-Cech theorem for Boolean algebras follow as special cases. We introduce sets with a Boolean inequality, that is sets with an internal falsum. These sets allow a book-keeping of the use of the Ex falso principle in constructive mathematics. If we restrict to swap algebras with a Boolean inequality, then the proof of the Stone representation theorem for swap algebras of type (II) is within minimal logic.