Constructing the Reals as Dedekind Cuts of Rationals

Jacques D. Fleuriot and Lawrence C. Paulson

March 24, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The type of real numbers is constructed from the positive rationals using the method of Dedekind cuts. This development, briefly described in papers by the authors, follows the textbook presentation by Gleason. It's notable that the first formalisation of a significant piece of mathematics, by Jutting in 1977, involved a similar construction.


BSD License


Session Dedekind_Real