Signed-Bit Representations of Real Numbers and
the Constructive Stone-Yosida Theorem

Robert S. Lubarsky and Fred Richman

Dept. of Mathematical Sciences

Florida Atlantic University

777 Glades Rd.

Boca Raton, FL 33431

Robert.Lubarsky@alum.mit.edu

fred@math.fau.edu

The signed-bit representation of reals, as developed classically,
is like binary, only in addition to 0 and 1 you can also use -1.
This representation lends itself especially well to the
constructive (intuitionistic) theory of the reals. (For background on
constructive analysis, see [Bi] or [BV].) We develop
the signed-bit equivalents of three common
notions of real numbers: Dedekind cuts, Cauchy sequences, and
Cauchy sequences with moduli of convergence.

This theory is then applied to representations of Riesz spaces. A
Riesz space is a lattice ordered vector space (here taken to be
over the rationals), and a representation of such is a
homomorphism into the reals. The canonical example of a Riesz
space is a space of real-valued functions, and a representation is
evaluation at a point in the domain. Constructively, in order to
find a point in the domain, one must often make an additional
assumption, such as Dependent Choice. This is proven for example in [CS],
where the authors ask whether DC is necessary for this result. In this talk,
the existence of (appropriate) Riesz space representations is recast in terms
of signed-bit representations, and a possible way to show that to
be independent from the regular axioms of set theory sans DC,
using a topological model (as in [FH], [G], and [L]), is then sketched.

[Bi] Errett Bishop, Foundations of Constructive Analysis, McGraw-Hill, 1967

[BV] Douglas Bridges and Luminita Vita, Techniques of Constructive Analysis,
Springer, 2006

[CS] Thierry Coquand and Bas Spitters, Formal Topology and
Constructive Mathematics: the Gelfand and Stone-Yosida
Representation Theorems, Journal of Universal Computer
Science, 11 (2005), p. 1932-1944

[FH] M.P. Fourman and J.M.E. Hyland, Sheaf models for
analysis, in M.P. Fourman, C.J. Mulvey, and D.S. Scott (eds.),
Applications of Sheaves, Lecture Notes in Mathematics Vol.
753 (Springer-Verlag, 1979), p. 280-301

[G] R.J. Grayson, Heyting-valued models for intuitionistic
set theory, in M.P. Fourman, C.J. Mulvey, and D.S. Scott (eds.),
Applications of Sheaves, Lecture Notes in Mathematics Vol.
753 (Springer-Verlag, 1979), p. 402-414

[L] Robert Lubarsky, On the Cauchy Completeness of the
Constructive Cauchy Reals, accepted for publication, available at
www.math.fau.edu/Lubarsky