[FOM] predicativism and functional analysis

[Bas Spitters]

Dear Nik,

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(!). 
Like Bishop, he treats: metric spaces, complex analysis, integration and 
normed linear spaces (including dual spaces).

[1]Ye, Feng,  Strict Constructivism and the Philosophy of Mathematics, January 
2000, Princeton University

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.(?)

Bas Spitters
-------------------------------------------------------
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/

On Tuesday 21 February 2006 08:18, Nik Weaver wrote:
> This is a follow-up to a previous post of mine,
> http://www.cs.nyu.edu/pipermail/fom/2006-February/009778.html
> in which I argued that Cantorian set theory fits normal
> mathematical practice rather poorly, because core mathematics
> takes place only at the very bottom of the cumulative hierarchy.
>
> Here I want to illustrate the point that there is a remarkably
> exact fit between predicativism and core mathematics.  I would
> even say a *stunningly* exact fit!
>
> (I hasten to add that this is only weak evidence for the actual
> correctness of predicativism, although I do think it is some
> evidence in favor of correctness.)
>
> I'll use functional analysis as my illustration.  Here the objects
> of study have no a priori cardinality restrictions, so the field
> is not as it were "automatically" predicative.
>
> At least in my interpretation of predicativism, which I call
> "conceptualism", it is possible to treat things like the real
> line and the power set of N essentially as proper classes.
> Let me simply use the term "proper class" to refer to such
> things.  (Everything I'm writing here is made precise in my
> paper "Analysis in J_2".)
>
> What constructions are possible with proper classes?  Well,
> we can form the cartesian product of two classes.  So we can
> get spaces like R^n as proper classes.  Moreover, we can form
> the cartesian product of any set of proper classes.  More
> precisely, if S is a class contained in the cartesian product
> A x B where A is a class and B is a set, then we can form the
> cartesian product of the classes S_b = {a in A: (a,b) in S}
> over b in B.  So we can even get R^omega as a proper class,
> and sitting inside it l^p sequence spaces.
>
> It's not hard to see that one can recover all of the standard
> Banach spaces as proper classes.  What about standard Banach
> space constructions?  The dual space construction particularly
> concerned me because this is such an important construction in
> functional analysis.  On its face the construction is problematic
> because the elements of the dual of E are the continuous linear
> maps from E to R.  (Let's assume the scalar field is real.)
> However, any function from one proper class to another proper
> class must itself be a proper class of ordered pairs.  So we
> can't talk about the class of all continuous linear functionals
> because a proper class can't be an element of another class.
> We can talk about individual continuous linear functionals but
> not the Banach space they constitute.
>
> This problem is easily resolved if E is separable.  In that case
> there is a countable dense subset and every continuous linear
> functional is determined by its values on that subset, so we
> can effectively restrict these functionals to the subset; this
> renders them sets of ordered pairs and we can then form the class
> of all such functions.
>
> Second duals are trickier.  This bothered me for a while.  It
> seemed that second duals are a critical test of predicativism
> because second dual techniques really are fundamental in
> functional analysis, but according to the above reasoning one
> can't generally form the second dual even of a separable Banach
> space because its first dual need not be separable.
>
> What I finally realized is that standard second dual techniques
> don't actually make use of the second dual as a Banach space.
> They only use individual elements of the second dual, which is
> predicatively okay!  For example, the most basic theorem about
> the second dual says that the unit ball of E is weak* dense in
> the unit ball of E''.  That could be rephrased as saying that
> every norm one vector in E'' can be approximated by norm one
> vectors in E, which is a statement about individual elements
> of E''.
>
> In ZFC, starting with any Banach space E you can successively
> form E', E'', E''', etc.  However, in practice functional
> analysts almost never use any dual beyond the second, and
> they generally use the second dual only to the extent that
> predicativity allows.  That is an *exact fit*.
>
> We have a name for the separable sequence space c_0.  We
> have a name for its (separable) dual l^1.  We have a name for
> l^infinity, the (nonseparable) dual of l^1.  We have no name
> for the dual of l^infinity.
>
> We have a name for the spaces of compact operators on a separable
> Hilbert space: K(H).  We have a name for its dual, the space of
> trace-class operators: TC(H).  We have a name for the dual of
> TC(H), the space of bounded operators on a Hilbert space: B(H).
> We have no name for the dual of B(H).  K(H) and TC(H) are
> separable; B(H) is not.
>
> We have a name for C[0,1] (separable).  We have a name for its
> dual, M[0,1] (non-separable).  We have no name for the dual of
> M[0,1].
>
> It goes on and on.  If you pick a standard Banach space and
> start taking duals, invariably the first one that doesn't have
> a standard name is the first one that's impredicative.  This
> is a *stunningly exact fit* between predicativism and core
> mathematics.
>
> Nik Weaver
> Math Dept.
> Washington University
> St. Louis, MO 63130 USA
> nweaver at math.wustl.edu
> http://www.math.wustl.edu/~nweaver
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

--