[FOM] predicativism and functional analysis

[Bas Spitters]

Dear Nik,

Thanks for your answer.

On Thursday 23 February 2006 04:35, Nik Weaver wrote:
> The separability issue is slightly subtle.  My impression of
> constructive analysis --- correct me if I'm wrong --- is that
> Banach spaces have to be separable.  

Indeed, some authors define a Banach space to be separable.
In any case, to be able to compute the norm of all the elements the Banach 
algebra has to be separable. More precisely, if the space is inseparable (in 
some strong sense), then one can construct an element which has a 
non-computable norm.

> So spaces like l^infinity, 
> B(H), etc., exist as locally convex topological vector spaces
> but they aren't Banach spaces.  

They exist as Banach spaces, but the norm is in general not computable.
For instance, Bishop and Bridges define a "quasi-normed" space precisely for 
this purpose. Quasi-normed spaces have more structure then general locally 
convex topological vector spaces. I think the presentation by Bishop and 
Bridges can be slightly improved by working with norms which have a value in 
the `generalized real numbers' of Fred Richman.

> There are plenty of standard non-separable Banach spaces ---
> every infinite-dimensional von Neumann algebra, for example ---
> but these are usually dual spaces with separable predual, so they
> would at least appear constructively as LCTVS's, as I understand
> it.  However, there are a few standard non-separable Banach
> spaces that aren't dual spaces.  Examples: the Calkin algebra
> (C(H) = B(H)/K(H)), the almost-periodic continuous functions on
> R, the CCR algebra over a separable Hilbert space.  There are
> all predicatively legitimate and apparently constructively not
> legitimate.

Indeed, the almost periodic functions are somewhat difficult to treat 
constructively. However, it can be done. See for instance my paper on almost 
periodic functions on:
http://www.cs.ru.nl/~spitters/articles.html
and the reference cited therein for some approaches.

More generally, if I am not mistaken, Bishop once remarked that for 
applications one only needs separable subspaces of such inseparable spaces.

> Whether PRA "suffices" seems debatable.  As I indicated above,
> there are a fair number of core spaces that I don't think you can
> handle.  However, these spaces are rather exceptional and I think
> most analysts would agree they could get by without them.  Spaces
> like l^infinity and B(H) are really essential, but you could make
> a case that you could get by with only their LCTVS structure and
> not their norms.

Ye writes that the definition of quasi-normed spaces is straightforward in his 
system.

> Predicativism doesn't suffer from these defects, but there are
> still going to be occasional topics out at the margins that won't
> be allowed.  So it's a matter of degree.  I still maintain that the
> correspondence between predicativism and core functional analysis
> is stunningly exact.  The correspondence with constructivism is
> pretty good but you're missing a few things that people really care
> about.  

Arguably we "miss a few things" (although I am not sure whether B(H) is an 
example), but in return we get a computational interpretation for free.

Bas Spitters