This is a 🧵 about the Dedekind cut construction of real numbers in #constructiveMathematics , particularly two technical details. The first has to do with defining additive inverse and multiplication, when we can't use excluded middle for things like "is a real number positive or not?". The second is about one sided versus two sided cuts.
1/8
We start with the familiar two sided Dedekind cut where a cut is a pair of sets of rationals which are inhabited, rounded, disjoint, and located (see section 11.2 of the HoTT book for this definition, which is also used by a lot of other papers on constructive Dedekind cuts). Addition of two cuts is readily defined (again, see HoTT, section 11.2.1), but what about multiplication (when numbers may be negative)?
2/8
The solution in the HoTT book is one solution (see definition of multiplication also in section 11.2.1) but may be a bit intimidating especially in the sense that you'll need to prove a bunch of lemmas about arithmetic with rational numbers (multiplication, minimum/maximum of two rationals, comparison, etc). As these are rationals rather than reals this presents little trouble constructively, just legwork.
3/8
There is another solution, which is to form Dedekind cuts of positive rationals to construct positive reals and then later define signed reals. I learned it from Metamath's classical set theory Dedekind cuts, and then adapted it to constructive set theory. Metamath cites Gleason, Andrew M., Fundamentals of Abstract Analysis (1991).
4/8
When just dealing with positive reals defined as Dedekind cuts of positive rationals, the definition of multiplication becomes as simple as the one for addition and you don't need to worry about additive inverse yet.
5/8
To go from positive reals to signed reals, take pairs of positive reals. I'll give the intuition: the real number -2 can be defined as 3 - 5, two positive reals. The details involve an equivalence relation, recasting in terms of addition (because we haven't defined subtraction yet), and a quotient. These might seem tough if you aren't used to those concepts, but it is no worse than the quotient and equivalence relation which we likely used to go from positive integers to positive rational numbers.
6/8
I said I'd also talk about one sided versus two sided Dedekind cuts. My own work has been with two sided Dedekind cuts and indeed orthodoxy in #constructiveMathematics is that these are the ones which are well defined. But I did find there is a one sided definition, that I learned from James E Hanson, which apparently works. I'll just refer to https://mathoverflow.net/a/495508/489586 for further details (which are not as simple as the classical one sided cut).
7/8
8/8 sources for this thread:
* https://mathoverflow.net/questions/495504/arithmetic-of-constructive-dedekind-reals
* constructive formalization of the positive real Dedekind cuts in Metamath is at https://us.metamath.org/ileuni/mmtheorems.html (scroll down to "Dedekind-cut construction of real and complex numbers")
@soaproot At the very least I've heard Peter Aczel give a definition of one-sided cuts that works constructively, predating the MO post by around 13 years or so. And I would be surprised if Peter's was first. What does Johstone's Elephant say about it?
@andrejbauer Fair. I have edited that post to say "that I learned from" rather than "due to".
@soaproot This is a special case of the adjunction between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1). You could formalize the fact that any rig R gives a ring R* such that R embeds into R* universally. I believe this is how Unimath library formalizes reals.
@andrejbauer In Metamath we develop reals way before we do anything with rings (or rigs, or groups, or any other algebraic structures). Which I guess is to my taste, but I try not to be too dogmatic about whether one or the other is better. (In this case the order of topics was decided WAY before I was working on the project).
@andrejbauer @soaproot "*adjunction* between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1)"???
@Paul_Taylor @andrejbauer It is called "completion" at https://ncatlab.org/nlab/show/rig , if I am reading that page correctly.
@Paul_Taylor @soaproot A reflection would be a better word to use (especially if we restrict to cancelative rigs so that the unit is monic).
Oct 29, 2026, 8:33 PM@andrejbauer Does the adjunction (nicely) factor through "cancellative rigs", i.e., rigs where the addition is a cancellative monoid?
Oct 29, 2026, 10:42 PM@andrejbauer Nor do I! The forgetful functor obviously so factors. Working with AFTs is not really my area of expertise.
@soaproot Dedekind cuts should *absolutely* be two-sided, because the two sides may sometimes come adrift.
First of all, mathematics is about *symmetry* and there is no reason for favouring one side of the real line over the other. (Classical logic often gratuitously throws symmetry away.)
In *any* real number computation (for example Archimedes' calculation of pi by inscribing and escribing polygons in a circle) what we calculate is *always* an interval, or a sequence of nested intervals.
An "interval" is a Dedekind cut in which they two halves don't quite meet.
Then in analysis there are lots of apparent pathologies that are easily explained by saying that the "number" is a one-sided real number, not a two-sided one. Of course it could be either upper or lower.
As for multiplication, in fact Richard Dedekind chickened out of doing it in his famous paper.
John Conway has a fascinatingly original answer in "On Numbers and Games".
Multiplication can be defined for intervals fairly easily, but there is also a version including "backwards" intervals, such as [1,0] instead of [0,1], originally due to Edgar Kaucher.
See the two papers by @andrejbauer and me: https://www.paultaylor.eu/ASD/analysis
@Paul_Taylor I spent a LOT of time poring over that "The Dedekind Reals in Abstract Stone Duality" paper as I was formalizing the IZF real number construction in Metamath. Thanks for writing it! The details of this construction are often assumed but much more rarely explained in detail. @andrejbauer