[FOM] Classical/Constructive Arithmetic

[S. Spijkerman / F. Waaldijk]

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 
is complicated.


----- 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 
>> are
>> 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
>  f':M-->R.
>  (See Bishop's "Constructive Analysis", Section 4.5 for details.)
>
> Now to get a complicated Z, take something that follows trivially from X 
> but
> 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 
> R^omega-->R.
>
> 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.
>
> Andrej
>
>