A Tour with Constructive Real Numbers

Abstract. The aim of this work is to characterize constructive real numbers through a minimal axiomatization. We introduce, discuss and justify 16 constructive axioms. Then we address their expressivity considering the alternative axiomatizations. 1 Overview of the work This work tries to understand (again) constructive real numbers. Our main contribution is a new system of axioms, synthesized with the aim of being minimal, i.e. of assuming the least number of primitive notions and properties. Such a system is consistent with respect to reference models we have in mind -(equivalence classes of) Cauchy sequences [TvD88] and co-inductive streams of digits [CDG00] -- and will be compared to other proposals of the literature [Bri99, GN01]. In particular we will prove that our axiomatization has a sufficient deductive power. We have formalized and used our axioms inside the Logical Framework Coq [BB+ 01]. However, the axioms can be stated and worked with in a general constructive logical se...

• Type: Conference
• Year: 2000
• Where: TYPES
• Authors: Alberto Ciaffaglione, Pietro Di Gianantonio
• Keywords: Cauchy Sequences, Constructive Axioms, Constructive Real Numbers, Formal Methods, TYPES 2000