The Dedekind Reals in Abstract Stone Duality

kind Reals in Abstract Stone Duality Andrej Bauer and Paul Taylor 3 June 2009 Stone Duality (ASD) is a direct axiomatisation of general topology, in contrast to the traditional and all other contemporary approaches, which rely on a prior notion of discrete set, type or object of a topos. ASD reconciles mathematical and computational viewpoints, providing an inherently computable calculus that does not sacrifice key properties of real analysis such as compactness of the closed interval. Previous theories of recursive analysis failed to do this because they were based on points; ASD succeeds because, like locale theory and formal topology, it is founded on the algebra of open subspaces. ASD is presented as a lambda-calculus, of which we provide a self-contained summary, as the foundational background has been investigated in earlier work. The core of the paper constructs the real line using two-sided Dedekind cuts. We show that the closed interval is compact and overt, where these conc...

• Type: Conference
• Year: 2005
• Where: CCA
• Authors: Andrej Bauer, Paul Taylor 0002
• Keywords: CCA 2005, Closed Interval, Dedekind Cuts, Stone Duality