A Model of the Real Numbers

Description: This library consists of a formalisation of a concrete model of a real numbers structure and a proof of categoricity of the axioms for a real number structure. Real numbers are defined as the set of Cauchy sequences of rational numbers. A detailed discussion of the axioms and the formalisation is given in [2]. The formalisation includes:

• Formalisation of rational numbers as a set of pairs of natural numbers and integers and the proof that this model is an Archimedean constructive ordered field.
• Proof of the fact that the set of Cauchy sequences of any Archimedean constructive ordered field is a real numbers structure.
• Definition of a notion of isomorphism between two real number structures and proof of the fact that any two real number structures are isomorphic.
• Proof of the fact that the axioms for a real numbers structure are equivalent to those introduced in [1].

References:

• [1] Douglas S. Bridges; Constructive mathematics: a foundation for computable analysis , Theoretical Computer Science 219 (1999) 95-109
• [2] Herman Geuvers, Milad Niqui; Constructive Reals in Coq: Axioms and Categoricity, In P. Callaghan, Z. Luo, J. McKinna, R. Pollack (Eds.), Proceedings of TYPES 2000 Workshop, Durham, UK, LNCS 2277, 79-95, 2002

Maintainer: Milad Niqui

Developers: Milad Niqui

Documentation

Download