[FOM] Classical/Constructive Arithmetic

[Andrej Bauer]

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