[FOM] Sperner's lemma and Bishop style constructive mathematics
Aatu.Koskensilta at uta.fi
Sun Jan 10 12:28:59 EST 2010
Quoting Yasuhito Tanaka:
> 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?
Sperner's lemma has direct combinatorial constructive proofs. That
said, a few observations: "Mathematics with intuitionistic logic"
doesn't mean anything in particular. Also, from the provability of a
theorem in RCA_0 it does not in general follow that the theorem is
constructively provable -- recall that various forms of excluded
middle are provable in RCA_0! Classical provability usually implies
constructive provability only for statements of a specific logical
form, viz. Pi-2 statements.
Aatu Koskensilta (aatu.koskensilta at uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
More information about the FOM