Delivery-Date:
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