[FOM] Classical/Constructive Arithmetic
Andrej.Bauer at andrej.com
Wed Mar 22 01:50:34 EST 2006
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?
More information about the FOM