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.