[FOM] Banach spaces: A more precise question

[Timothy Y. Chow]

I wrote:

> This is a followup to my previous vague inquiry about Banach spaces.  
> Can the existence of Tsirelson's space be proved in RCA_0?

Because of interest in this question, Gowers has started a new blog entry 
for it.

http://tinyurl.com/banach2

Let me mention that one reason to suspect that the existence of 
Tsirelson's space may not be provable in RCA_0 is that according to 
Gowers, the usual definition involves an induction over a set of finite 
trees, which has a bit of the feeling of the weak Koenig lemma to it.  

This could turn into quite an interesting application of reverse 
mathematics if it pans out.

Tim