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

[Aatu Koskensilta]

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