[FOM] Banach spaces: A more precise question

[Timothy Y. Chow]

This is a followup to my previous vague inquiry about Banach spaces.  Can 
the existence of Tsirelson's space be proved in RCA_0?  The definition of 
the space can be found on Wikipedia.

http://en.wikipedia.org/wiki/Tsirelson_space

A more informal, but easier to read, explanation was posted by Gowers on 
his blog, as I noted before.  See the February 9 post by Gowers at

http://tinyurl.com/banach

Tim