From owner-qed Thu Sep 1 12:15:34 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA02019 for qed-out; Thu, 1 Sep 1994 12:13:24 -0500
Received: from cats.ucsc.edu (root@cats-po-1.UCSC.EDU [128.114.129.22]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id MAA02014 for ; Thu, 1 Sep 1994 12:13:19 -0500
From: beeson@cats.UCSC.EDU
Received: from si.UCSC.EDU by cats.ucsc.edu with SMTP
id KAA02909; Thu, 1 Sep 1994 10:13:13 -0700
Received: by si.UCSC.EDU (8.6.9/4.7) id KAA26302; Thu, 1 Sep 1994 10:13:07 -0700
Date: Thu, 1 Sep 1994 10:13:07 -0700
Message-Id: <199409011713.KAA26302@si.UCSC.EDU>
To: dahn@mathematik.hu-berlin.de, qed@mcs.anl.gov
Subject: intermediate value theorem
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
Just to set a detail straight: the intermediate value theorem for
polynomials (indeed for real-analytic functions) can be proved without
recourse to set theory, and even constructively proved. See the discussion
on page 11 of my book, Foundations of Constructive Mathematics.
Of course, G\"odel's theorem shows us that it WILL happen in
general that there are theorems whose proofs require concepts not
involved in the statement of the theorem. But the intermediate
value theorem isn't one of those theorems.