From owner-qed Tue Sep 6 06:42:32 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id GAA08885 for qed-out; Tue, 6 Sep 1994 06:40:01 -0500
Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id GAA08880 for ; Tue, 6 Sep 1994 06:39:33 -0500
Received: from kummmer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
(1.37.109.8/16.2/4.93/main) id AA00190; Tue, 6 Sep 1994 13:33:37 +0200
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
id AA08099; Tue, 6 Sep 94 13:39:13 +0200
Date: Tue, 6 Sep 94 13:39:12 +0200
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9409061139.AA08099@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Re: Intermediate Value Theorem
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
Proving theorems on real numbers in constructive mathematics usually requires working with sequences of codes of real numbers. The existence of a real number with specific properties (like being a zero of a function) is there frequently proved by constructing a sequence of codings (say decimal fractions) that approximate the code of this number.
In classical mathematics, sequences of real numbers (or sequences of codes) are something outside the world of real numbers - they are objects of a different type. In constructive mathematics, real numbers are sequences of codes. That's why the intermediate value theorem can be proved in constructive mathematics inside the world of real numbers.
The same effect could be obtained in "set theoretical mathematics" identifying real numbers with Dedekind cuts. This means incorporating the necessary concepts of set theory into the concept of real numbers.
The point I wanted to make is: The intermediate value theorem for polynomials (to be precise: of a given degree) is a statement that uses real numbers as primitive unstructured objects and involves only addition and multiplication. It has no reference to the internal structure of real numbers. Therefore it suggests, that no knowledge on this structure is needed for a proof. This suggestion can be easily extracted from the theorem if the theorem is stated in a well-typed language and in many cases such a suggestion will be helpful, notably if automated provers are used. But there are cases - such as this one in the context of classical mathematics - where the suggestion is wrong.
In my opinion there is no contradiction between types and sets - set theory is a simple and powerful tool to define types. "Working mathematicians" (i. e. those not involved in foundational studies) do not like to care about sets though they use them. They also do not like to care about types though they use them.
Ingo Dahn