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

Andrej Bauer andrej.bauer at andrej.com
Sun Jan 10 06:03:54 EST 2010

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


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

More information about the FOM mailing list