Definable Banach Spaces

This is an attempt to summarize in the form of a wiki the proposals for formalizing the notion of a "definable" Banach space that has been brought in the comments to this post at Gower's Weblog.

Fundamental Tension Resulting in This Problem

As with much of mathematics, Banach spaces developed from explicit examples, leading to an axiomatization and consequent theory. The explicit examples of Banach spaces have historically been function spaces.

Let [math]\displaystyle{ (A,{\mathcal{M}},\mu) }[/math] be a measure space. The [math]\displaystyle{ L_p }[/math], Lorentz, Olicz, Schreier, Sobolev, Besov spaces are in general defined as the class of functions [math]\displaystyle{ f:X\to {\mathbb{R}} }[/math] with a finite norm [math]\displaystyle{ \| f\| \lt +\infty }[/math]. These spaces contain either [math]\displaystyle{ c_0 }[/math] or [math]\displaystyle{ l_p }[/math] as a subspace for some [math]\displaystyle{ p\in [1,+\infty) }[/math].

In the above paragraph, we make the choice to use function spaces of functions over an abstract measure space rather than over the natural numbers with counting measure. Choosing to focus on Banach spaces of sequences of real numbers obscures the dual role that the natural numbers [math]\displaystyle{ {\mathbb{N}} }[/math] plays in the notion of definablility:

1. The natural numbers serve as the domain of these functions;
2. The real numbers can be coded as subsets of the natural numbers, via a bijection between [math]\displaystyle{ {\mathcal{P}}({\mathbb{N}}) }[/math] and [math]\displaystyle{ {\mathbb{R}} }[/math].

Admittedly, using an abstract measure space entails that the notion of definability of a Banach space will be relative to this abstract measure space. By focusing on an abstract measure, the first role that the natural numbers play will be removed, and the recursion theory used when employing the second role will be stark and clear.

Let us now look at a space, Tsirelson space, which when contrasted with the spaces above lead to the fundamental tension resulting in this problem.

Proposals To Formalize The Notion of Definability

These proposals are listed in approximate choronological order as they appear on this post at Gower's Weblog.

• The asymptotic complexity of functions which the norm gives rise to.

Although the Tsirelson space gives rise to fast-growing functions, Gowers defined a variant known as Schlumprecht’s space in an attempt to give an example of a norm that does not give rise to fast-growing functions.

• The recursive complexity of functions which the norm gives rise to.
• The extent to which the space is combinatorial.
• Placing the definition of norm in a hierarchy of recursive notions weaker than primitive recursion.

The definition of the norm of the Tsirelson space is primitive recursive. In order to distinguish the Tsirelson space from other spaces explicitly defined, it is necessary to have notions of recursion that are weaker than recursive notions.

• Impredicativity of the definition of norm.