A metamathematical question in Banach space theory.

In the 1970s, Boris Tsirelson constructed a Banach space which was the first one known that did not contain a copy of one of the classical spaces c₀ or l_p. He used a clever inductive technique which has subsequently been at the heart of many further constructions of Banach spaces with strange properties.

Interestingly, nobody has found a way of obtaining Banach spaces with these properties without using Tsirelson's inductive approach, which leads to rather indirect definitions. In particular, all the usual Banach spaces that come up in nature, and have more straightforward descriptions, have either c₀ or l_p as a subspace. This raises the following metamathematical challenge: define a notion of `explicit definition' which encompasses all the usual definitions of down-to-earth Banach spaces - c₀, l_p, L_p, C[0,1], Orlicz spaces, Lorentz spaces, Sobolev spaces and so on - and prove that every explicitly defined Banach space contains c₀ or l_p. Neither part of this programme has been done.