[FOM] Classical/Constructive Arithmetic
S. Spijkerman / F. Waaldijk
sufra at hetnet.nl
Tue Mar 21 13:10:29 EST 2006
well, in my thesis (see http://home.hetnet.nl/~sufra/mathematics.html) you
will find a constructive proof of the Dugundji extension theorem.
since S=Z^omega is located in R^omega, the theorem is applicable to the
situation you mention (local compactness does not enter into the picture). i
do not believe that the proof of the Dugundji theorem offered in my thesis
----- Original Message -----
From: "Andrej Bauer" <Andrej.Bauer at andrej.com>
To: <fom at cs.nyu.edu>
Cc: "Harvey Friedman" <friedman at math.ohio-state.edu>
Sent: Monday, March 20, 2006 6:13 PM
Subject: Re: [FOM] Classical/Constructive Arithmetic
> On Saturday 18 March 2006 10:18, Harvey Friedman wrote:
>> 4. Examples where the known proof is nonconstructive, and where one can
>> give a constructive proof, but it is known that all constructive proofs
>> grotesque (e.g., extremely long, or extremely unpleasant, etc.).
> A general strategy for finding such things is the following. Take a
> theorem X
> which holds classically but not constructively. Consider its constructive
> counterpart Y (which may or may not be a weakening of X), which usually
> has a
> reasonable proof. Now take a theorem Z which is a special case of X but is
> not covered by Y. If you pick Z well, a constructive proof of Z might be
> rather complicated. Example:
> Theorem X (Tietze's Extension Theorem for for metric spaces):
> Let S be a closed subset of a metric space M. Every locally uniformly
> continuous f:S-->R has a continuous extension f':M-->R.
> Theorem Y:
> Let S be a locally compact subset of a metric space M. Every locally
> uniformly continuous f:S-->R has a locally uniformly continuous extension
> (See Bishop's "Constructive Analysis", Section 4.5 for details.)
> Now to get a complicated Z, take something that follows trivially from X
> does not conform to Y. In particular, we consider the complete separable
> metric space M = R^omega (a countable product of copies of the reals) with
> subspace S = Z^omega, where Z is the set of integers.
> Theorem Z:
> Every continuous map Z^omega-->R has a continuous extension to
> I don't know of a general constructive theorem from which Z would follow.
> However, Z is valid constructively and the shortest proof I know is too
> horrible for me to try to read it again.
More information about the FOM