# A question about intuitionistic analysis

In Michael Dummett's book "Elements of Intuitionism" , the product of real numbers are 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 all 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