Sciweavers

Share
TYPES
2000
Springer

Constructive Reals in Coq: Axioms and Categoricity

9 years 3 months ago
Constructive Reals in Coq: Axioms and Categoricity
We describe a construction of the real numbers carried out in the Coq proof assistant. The basis is a set of axioms for the constructive real numbers as used in the FTA (Fundamental Theorem of Algebra) project, carried out at Nijmegen University. The aim of this work is to show that these axioms can be satisfied, by constructing a model for them. Apart from that, we show the robustness of the set of axioms for constructive real numbers, by proving (in Coq) that any two models of it are isomorphic. Finally, we show that our axioms are equivalent to the set of axioms for constructive reals introduced by Bridges in [2]. The construction of the reals is done in the `classical way': first the rational numbers are built and they are shown to be a (constructive) ordered field and then the constructive real numbers are introduced as the usual Cauchy completion of the rational numbers.
Herman Geuvers, Milad Niqui
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TYPES
Authors Herman Geuvers, Milad Niqui
Comments (0)
books