[FOM] predicativism and functional analysis

[Nik Weaver]

A reply to Bas Spitters:

> In this context you might be interested in the work by Feng
> Ye[1] and more generally in constructive mathematics where
> such separability assumptions are standard practice. In his
> PhD-thesis he shows that (almost) all of Bishop's work on
> constructive analysis can be formalized in PRA(!).

Thanks for the reference.  I did look at Ye's thesis but it
was a while ago.

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.  So spaces like l^infinity,
B(H), etc., exist as locally convex topological vector spaces
but they aren't Banach spaces.  The could be taken to be a
disadvantage as compared to predicativism, where these are
legitimate Banach spaces and one is merely unable to form
their duals.

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.

> Also, Ulrich Kohlenbach has shown that PRA is usually sufficient
> for (classical) functional analysis. He uses this for his
> impressive work on proof mining. Kohlenbach manages to `mine'
> classical proofs for computational information (effective bounds)
> that the experts in the field usually can not find themselves.
> See his forthcoming book:
> Proof Interpretations and the Computational Content of Proofs
> http://www.mathematik.tu-darmstadt.de/~kohlenbach/newcourse.ps.gz
>
> for more information.
>
> Thus it seems that in fact a much weaker system then the one you
> have in mind would suffice.(?)

I wan't aware of this reference --- I'll take a look.

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.

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.  The correspondence with set theory is terrible because the
interesting objects are buried in an ocean of uninteresting,
pathological objects.

Nik