# Multiplication of Cauchy and Dedekind real numbers

In Michael Dummett's book "Elements of Intuitionism", the product of real numbers is defined as follow:

$x\cdot y= \{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$, where $\langle r_n\rangle ,\langle s_n\rangle$ are Cauchy sequences of rational numbers, and $\langle r_n\rangle \cdot \langle s_n\rangle=\langle r_n\cdot s_n\rangle$.

This definition is valid iff we can prove intuitionistically $\{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$ is indeed a real number, i.e. $\{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$ is closed under "equivalent" (we say that $\langle r_n\rangle$ is equivalent to $\langle s_n\rangle$ if for any natural number $k$, we can find a natural number $n$ such that $|r_m-s_m|<2^{-k}$ for all $m>n$ ). This is to say, we must prove the following proposition intuitionistically:

Let $\langle r_n\rangle , \langle s_n\rangle , \langle t_n\rangle$ be Cauchy sequences of rational numbers, and $\langle t_n\rangle$ is equivalent to $\langle r_n\rangle \cdot \langle s_n\rangle$. Then we can construct two Cauchy sequences $\langle r_n'\rangle , \langle s_n'\rangle$ of rational numbers such that
(1)  $\langle r_n'\rangle$ is equivalent to $\langle r_n\rangle$;
(2)  $\langle s_n'\rangle$ is equivalent to $\langle s_n\rangle$;
(3)  $\langle t_n\rangle =\langle r_n'\rangle \cdot \langle s_n'\rangle$.

But Michael Dummett doesn't justify his definition, and I find it's very difficult to prove the above proposition intuitionistically. Could you help me?

-
The classical proof of the above proposition uses the fact " $\langle r_n\rangle$ is equivalent to 0 or not", but this fact isn't valid intuitionistically. –  Set Dec 3 '12 at 8:55
I don’t have Dummett’s book, but are you sure you are reading the definition correctly? Isn’t it simply defined as the equivalence class of $\langle r_n\cdot s_n\rangle$, which would make it closed under equivalence by definition? What is really needed to ensure the function is well-defined is that $\langle r_n\cdot s_n\rangle$ is equivalent to $\langle r'_n\cdot s'_n\rangle$ whenever $\langle r_n\rangle$ is equivalent to $\langle r'_n\rangle$ and $\langle s_n\rangle$ is equivalent to $\langle s'_n\rangle$, but this should be straightforward to prove. –  Emil Jeřábek Dec 3 '12 at 15:40
@Jeřábek Yes, I'm sure that it's defined as above in Dummett’s book (first edition in 1977). But I don't know whether he justify his definition in the second edition (in 2000) of the book. I'm also Surprised that he uses this definition. I consult other books about constructive analysis, such as Bishop's "Foundations of constructive analysis" and Troelstra's "Principles of Intuitionism" , the definition in these books are unlike the definition of Dummett’s, but it is the same as you say, defined as the equivalence class of <$r_n S_n$> . –  Set Dec 3 '12 at 17:02

Whilst the definition of addition of Cauchy or Dedekind real numbers is "obvious", multiplication is rather more tricky. Unfortunately, most accounts, including [RD], leave it as an "exercise for the reader", without even giving a hint about what the problem is, so the questioner is right to ask about this. The difficulty is intrinsic to multiplication: the only difference in the intuitionistic setting is that we must do the job properly, instead of bodging it by treating positive, zero and negative numbers separately.

The point is that, if you want to achieve precision $\epsilon$ in the product of two numbers, one of which is bounded by $B$, then the other must be given within $\epsilon/B$.

[MD] is not quoted verbatim in the Question, but it is close enough, whilst the accounts in [AH] and [AT] are essentially the same.

[TD] gives a more general account of uniform continuity, taking explicit account of the modulus of convergence of Cauchy sequences (the function that says how far down the sequence you have to go to get a desired accuracy). This is needed elsewhere in constructive analysis.

[BB] has by far the clearest treatment that I have seen of the arithmetic of Cauchy reals, building the modulus into the definition. (I admire this book for its "can do" attitude, not dwelling on the counterexamples.) It gives the explicit (but snappy) proof of correctness for multiplication.

[BT] defines multiplication for Dedekind reals and proves correctness. It shows how Dedekind reals are the limiting case of intervals and also considers "back-to-front" (Kaucher) intervals, which are related to existential quantification just as ordinary intervals are related to universal quantification.

[JC] defines multiplication in a completely novel fashion for Conway (surreal) numbers. This is adapted to multiplication of real numbers in a topos in [PJ].

Since [MD,AH,AT] do not give the explicit answer to the Question, here it is.

As above, $\langle r_n\rangle$ is a Cauchy sequence if $\forall k.\exists n.\forall m.|r_{n+m}-r_n|\lt 2^{-k}$.

We write $\alpha(k)$ for such an $n$ for each given $k$; this is the modulus of convergence.

In particular, with $k=0$, for any Cauchy sequence $\langle r_n\rangle$ there are integers $N=\alpha(0)$ and $K=\log_2(r_N)$ such that $\forall m.-2^{K}\lt r_N-1\lt r_{N+m}\lt r_N+1\lt 2^{K}$.

Let $M$, $L$ and $\beta$ be the corresponding integers and modulus for the Cauchy sequence $\langle s_n\rangle$.

Now, given $h$, let $k\geq h+L+1$, $l\geq h+K+1$, $n\geq\alpha(k)$ and $n\geq\beta(l)$. Then, for all $m$, $$\begin{eqnarray} |r_{n+m} s_{n+m} - r_n s_n| &\leq& |r_{n+m}| |s_{n+m} - s_n| + |r_{n+m} - r_n| |s_n| \\ &\lt& 2^K 2^{-l} + 2^{-k} 2^L \leq 2^{-h}. \end{eqnarray}$$ Hence $\langle r_n s_n\rangle$ is a Cauchy sequence with modulus $\gamma(h)=\max(\alpha(h+L+1),\beta(h+K+1))$.

We can avoid considering equivalence of sequences explicitly, by observing that two Cauchy sequences are equivalent iff they are both subsequences of the same Cauchy sequence. Rationals are represented by constant Cauchy sequences and the new operation for them agrees with multiplication of rationals.

This argument amounts to saying that the new operation is continuous with respect to the Euclidean topology. Also, the rationals are dense amongst Cauchy reals. Hence the new operation is the unique continuous extension and it follows that it obeys the usual algebraic laws for multiplication.

[BT] Andrej Bauer and Paul Taylor, The Dedekind Reals in Abstract Stone Duality, in Mathematical Structures in Computer Science, 19 (2009) 757-838.

[BB] Errett Bishop and Douglas Bridges, Foundations of Constructive Analysis, Grundlehren der mathematischen Wissenschaften, Springer-Verlag, 1985.

[JC] John Horton Conway, On Numbers and Games, Number 6 in London Mathematical Society Monographs. Academic Press, 1976. Revised edition, 2001, published by A K Peters, Ltd.

[RD] Richard Dedekind, Stetigkeit und irrationale Zahlen, Braunschweig, 1872. Reprinted in [DW], pages 315–334; English translation, Continuity and Irrational Numbers, in [DE].

[DE] Richard Dedekind, Essays on the theory of numbers, Open Court, 1901; English translations by Wooster Woodruff Beman; republished by Dover, 1963.

[DW] Richard Dedekind. Gesammelte mathematische Werke, volume 3. Vieweg, Braunschweig, 1932; edited by Robert Fricke, Emmy Noether and Oystein Ore; republished by Chelsea, New York, 1969.

[MD] Michael Dummett, Elements of Intuitionism, Oxford University Press, 2000.

[AH] Arend Heyting, Intuitionism, an Introduction, Studies in Logic and the Foundations of Mathematics, North-Holland, 1956. Third edition, 1971.

[PJ] Peter Johnstone, Topos Theory, London Mathematical Society Monographs 10, Academic Press, 1977.

[AT] Anne Troelstra, Principles of Intuitionism, Lectures presented at the Summer Conference on Intuitionism and Proof Theory (1968) at SUNY at Buffalo, NY, Lecture Notes in Mathematics 95, Springer-Verlag, 1969.

[TD] Anne Sjerp Troelstra and Dirk van Dalen, Constructivism in Mathematics, an Introduction, Number 121 and 123 in Studies in Logic and the Foundations of Mathematics, North-Holland, 1988.

If you know of other explicit accounts of multiplication for Cauchy or Dedekind reals then please give the references in comments below.

-