[FOM] Classical/Constructive Arithmetic

[S. Spijkerman / F. Waaldijk]

for the proof of the dugundji theorem the fan theorem is not used, nor is
ac_10 used. the theorem is proved using only bishop-math. however, the
bishop definition of continuous function is not used, the condition
`uniformly continuous on compact subspaces' is dropped.

this means that in general, the conclusion that the extension (of the
original continuous function) is uniformly continuous on compact subspaces
cannot be drawn from this theorem.

this has sparked my follow-up paper which has only just been published. the
dugundji theorem made me discover that the definition of `continuous
function' in bish is somewhat problematic. i would like very much for people
to appreciate these problems, so i repeat the link to my math page:
http://home.hetnet.nl/~sufra/mathematics.html and hope that you will find
time to ponder on these issues.

i have not considered replacing normal continuity with sequential continuity
in the dugundji theorem. but you may find some interesting results on
sequential continuity in my recent paper, towards the end.

----- Original Message ----- 
From: "Andrej Bauer" <Andrej.Bauer at andrej.com>
To: <fom at cs.nyu.edu>
Cc: "S. Spijkerman / F. Waaldijk" <sufra at hetnet.nl>
Sent: Wednesday, March 22, 2006 7:50 AM
Subject: Re: [FOM] Classical/Constructive Arithmetic


> On Tuesday 21 March 2006 19:10, S. Spijkerman / F. Waaldijk wrote:
>> 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.
>
> Ah thank you, this is very interesting. Do you use Fan Theorem or AC_1,0 
> to
> prove your theorem (I know you use them in your thesis, but what about the
> particular proof, I have not had the time yet to look at it)? Also, what
> happens if you replace pointwise continuity with sequential continuity?
>
> Andrej
>
>