[FOM] Sperner's lemma and Bishop style constructive mathematics

[Andrej Bauer]

I checked only very quickly that the proof of Sprenner's lemma at

http://en.wikipedia.org/wiki/Sperner%27s_lemma

is constructive. So the answer is yes, it holds constructively.

With kind regards,

Andrej Bauer

On Sat, Jan 9, 2010 at 9:03 AM, ochibocho2 <ochibocho2 at yahoo.co.jp> wrote:
> I am Yasuhito Tanaka at Doshisha University in Japan.
>
> Simpson's book "Subsystems of Second Order Arithmetic" states that
> Sperner's Lemma is provable in RCA_0.
>
> Then, is Sperner's lemma provable in Bishop style constructive
> mathematics or mathematics with intuitionistic logic?
> --------------------------------------
> Get the new Internet Explorer 8 optimized for Yahoo! JAPAN
> http://pr.mail.yahoo.co.jp/ie8/
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>